Modeling and Analysis of Information Systems / Моделирование и анализ информационных систем (МАИС)
Not a member yet
    782 research outputs found

    Автоматизированная обучающая система «Множества» (исследования организации 1-й части проекта)

    Get PDF
    The issues of building an automated learning system “Sets” which will allow students to master one of the important topics of the discipline “Discrete Mathematics” and to develop logical and mathematical thinking in this direction are studied. The corresponding topic of the 1st part of the project includes materials related to the concept of a set, operations on sets, algebra of sets, proofs of statements for sets, and the derivation of formulas for the number of set elements. The system is based on a construction of the statements proof editor for a set and of the formulas derivation editor for the number of set elements, both editors are to be used for teaching. The first of these allows students to split the original statement into a number of simpler statements, taken together equivalent to the original statement, to choose a method of proving each simple statement and to conduct their step-by-step proof. The second editor allows (using the inclusion-exclusion principle and the formula of the number of complement elements) to derive a step-by-step formula for the number of set elements through the specified numbers of elements for sets from which the resulting set is constructed. An important part of the system is to monitor the correctness of all actions of students, and on this basis the entire learning system is developed. The logical supervision over the correctness of the selected action in the first editor is performed by a Boolean function created by the system and corresponding to this action and by checking it for identical truth. In the second editor, invariants such as characteristic strings of the set and of its number of elements are used for verification. The rest of the system is related to learning of set algebra and to preparation to editors usage. The main focus here is on the learning strategy in which testing the understanding of the learned material is rather rigorous and eliminating the random choice of answers. The division of the material into sections with verification of the success of teaching not only by tests, but also by exercises and tasks, allows students to master the complex logical and mathematical techniques of proving statements for sets and derivation of formulas for the number of set elements.Исследуются вопросы построения автоматизированной обучающей системы «Множества», которая позволит учащемуся освоить одну из важных тем дисциплины «Дискретная математика» и развить логико-математическое мышление в этом направлении. Соответствующая тема 1-й части проекта включает материал, связанный с понятием множества, операциями над множествами, алгеброй множеств, доказательствами утверждений для множеств, выводом формул для количества элементов множества. В основе системы лежит построение с целью использования для обучения редактора доказательства утверждений для множества и редактора вывода формул для количества элементов множества. Первый из них позволяет студенту разбить исходное утверждение на ряд более простых утверждений, в совокупности эквивалентных исходному утверждению, выбрать метод доказательства каждого простого утверждения и провести их пошаговое доказательство. Второй редактор позволяет, используя формулу включения и исключения и формулу количества элементов дополнения, вывести пошагово формулу для количества элементов множества через заданные количества элементов, связанных с ним множеств. Важной частью системы является контроль правильности всех действий студента, и на этой основе разработана вся система обучения. Логический контроль правильности выбранного действия в первом редакторе осуществляется созданием системой булевой функции, соответствующей этому действию, и проверкой ее на тождественную истинность. Во втором редакторе для контроля используются такие инварианты, как характеристическая строка множества и характеристическая строка количества элементов множества. Остальная часть системы связана с обучением алгебре множеств и подготовке к использованию редакторов. При этом основное внимание уделяется стратегии обучения, при которой проверка понимания усвоенного материала является довольно строгой, исключающей случайный выбор ответов. Разбиение материала на секции с контролем успешности обучения не только тестами, но и упражнениями и задачами, позволяет студенту овладеть сложным логико-математическим аппаратом доказательства утверждений для множеств и вывода формулы для количества элементов множества

    Решение задач линейного программирования приведением к виду с очевидным ответом

    Get PDF
    The article considers a method for solving a linear programming problem (LPP), which requires finding the minimum or maximum of a linear functional on a set of non-negative solutions of a system of linear algebraic equations with the same unknowns. The method is obtained by improving the classical simplex method, which when involving geometric considerations, in fact, generalizes the Gauss complete exclusion method for solving systems of equations. The proposed method, as well as the method of complete exceptions, proceeds from purely algebraic considerations. It consists of converting the entire LPP, including the objective function, into an equivalent problem with an obvious answer. For the convenience of converting the target functional, the equations are written as linear functionals on the left side and zeros on the right one. From the coefficients of the mentioned functionals, a matrix is formed, which is called the LPP matrix. The zero row of the matrix is the coefficients of the target functional, a00a_{00} is its free member. The algorithms are described and justified in terms of the transformation of this matrix. In calculations the matrix is a calculation table. The method under consideration by analogy with the simplex method consists of three stages. At the first stage the LPP matrix is reduced to a special 1-canonical form. With such matrices one of the basic solutions of the system is obvious, and the target functional on it is a00 a_{00}, which is very convenient. At the second stage the resulting matrix is transformed into a similar matrix with non-positive elements of the zero column (except a00a_{00}), which entails the non-negativity of the basic solution. At the third stage the matrix is transformed into a matrix that provides non-negativity and optimality of the basic solution. For the second stage the analog of which in the simplex method uses an artificial basis and is the most time-consuming, two variants without artificial variables are given. When describing the first of them, along the way, a very easy-to-understand and remember analogue of the famous Farkas lemma is obtained. The other option is quite simple to use, but its full justification is difficult and will be separately published.В статье рассматривается способ решения задачи линейного программирования (ЗЛП), которая требует найти минимум или максимум линейного функционала на множестве неотрицательных решений системы линейных алгебраических уравнений с теми же неизвестными. Способ получен при усовершенствовании классического симплекс-метода, который, привлекая геометрические соображения фактически обобщает метод полных исключений Гаусса решения систем уравнений. Предлагаемый способ, как и метод полных исключений, исходит из чисто алгебраических соображений. Он заключается в преобразовании всей ЗЛП, включая целевую функцию, в эквивалентную задачу с очевидным ответом. Ради удобства преобразования целевого функционала, уравнения записываются как линейные функционалы в левой части и нули в правой. Из коэффициентов упомянутых функционалов составляется матрица, которая называется матрицей ЗЛП. Нулевая строка матрицы -- коэффициенты целевого функционала, a00a_{00} -- его свободный член. Описание и обоснование алгоритмов ведется в терминах преобразования этой матрицы. При вычислениях матрица является расчетной таблицей. Рассматриваемый метод, по аналогии с симплекс-методом, состоит из трех этапов. На первом этапе матрица ЗЛП приводится к специальному 1-каноническому виду. При таких матрицах одно из базисных решений системы очевидно, и на нем целевой функционал равен a00a_{00}, что очень удобно. На втором этапе полученная матрица преобразуется в аналогичную матрицу с неположительными элементами нулевого столбца (кроме a00a_{00}), что влечет неотрицательность базисного решения. На третьем этапе матрица преобразуется в матрицу, обеспечивающую неотрицательность и оптимальность базисного решения. Для второго этапа, аналог которого в симплекс-методе использует искусственный базис и является наиболее трудоемким, приводятся два варианта без искусственных переменных. При описании первого из них, попутно, получен очень простой для понимания и запоминания аналог знаменитой леммы Фаркаша. Другой вариант совсем прост в применении, но его полное обоснование сложно и будет опубликовано отдельно

    Оценка степени опасности дефектов при расшифровке вихретоковых дефектограмм

    Get PDF
    To ensure traffic safety of railway transport, non-destructive tests of rails are regularly carried out by using various approaches and methods, including eddy-current flaw detection methods. An automatic analysis of large data sets (defectograms) that come from the corresponding equipment is an actual problem. The analysis means a process of determining the presence of defective sections along with identifying structural elements of railway tracks in defectograms. At the same time, severity estimation of defined defects is also of great interest. This article continues the cycle of works devoted to the problem of automatic recognition of images of defects and rail structural elements in eddy-current defectograms. In the process of forming these images, only useful signals are taken into account, the threshold levels of amplitudes of which are determined automatically from eddy-current data. The article is devoted to the issue of constructing severity estimation of found defects with various lengths. The construction of the severity estimation is based on a concept of the generalized relative amplitude of useful signals. A relative amplitude is a ratio of an actual signal amplitude to a corresponding threshold level of useful signals. The generalized relative amplitude is calculated by using the entropy of the half-normal distribution, which is assumed to be a model for a probability distribution of an appearance of certain relative amplitudes in an evaluated defect. Tuning up the formula for calculating severity estimation of a defect is carried out on the basis of eddy-current records of structural elements. As a reference of the most dangerous defect, the bolted rail joint is considered. It models a fracture of a rail. A reference weak defect is a flash butt weld, a defectogram of which contains signals with low amplitude values. The proposed approach to severity estimation of defects is shown by examples.Для обеспечения безопасности движения на железнодорожном транспорте регулярно проводится неразрушающий контроль рельсов с применением различных подходов и методов, включая методы вихретоковой дефектоскопии. Актуальной задачей является автоматический анализ больших массивов данных (дефектограмм), которые поступают от соответствующего оборудования. Под анализом понимается процесс определения по дефектограммам наличия дефектных участков наряду с выявлением конструктивных элементов рельсового пути. При этом также большой интерес представляет и оценка степени опасности выявленных дефектов. Данная статья продолжает цикл работ, посвященных задаче автоматического распознавания образов дефектов и конструктивных элементов железнодорожных рельсов по вихретоковым дефектограммам. При формировании этих образов принимаются в расчет только полезные сигналы, пороговые уровни амплитуд которых определяются автоматически по вихретоковым данным. Статья посвящена задаче построения оценки степени опасности для выявленных поверхностных дефектов различной протяжённости. Построение оценки опирается на понятие обобщённой относительной амплитуды полезных сигналов. Относительная амплитуда представляет собой отношение реальной амплитуды сигнала к соответствующему пороговому уровню полезных сигналов. Обобщённая относительная амплитуда вычисляется с использованием энтропии полунормального распределения, которое предполагается модельным для распределения вероятностей появления тех или иных относительных амплитуд в оцениваемом дефекте. Настройка формулы расчёта степени опасности дефекта осуществляется на основе записей конструктивных элементов. В качестве эталонного наиболее опасного дефекта рассматривается болтовой рельсовый стык, который моделирует излом рельса. Эталонным слабым дефектом выступает электроконтактная сварка, дефектограмма которой, как правило, содержит сигналы с невысоким значением амплитуд. Предложенный подход к оценке степени опасности дефектов демонстрируется на примерах

    Вычислительный анализ количественных характеристик некоторых аппроксимационных свойств разрешимых групп Баумслага-Солитэра

    Get PDF
    Let GkG_{k} be defined as Gk=a,b; a1ba=bkG_{k} = \langle a, b;\ a^{-1}ba = b^{k} \rangle, where k0k \ne 0. It is known that, if pp is some prime number, then GkG_{k} is residually a finite pp-group if and only if pk1p \mid k - 1. It is also known that, if pp and qq are primes not dividing k1k - 1, p < q, and π={p,q}\pi = \{p,\,q\}, then GkG_{k} is residually a finite π\pi-group if and only if (k,q)=1(k, q) = 1, pq1p \mid q - 1, and the order of kk in the multiplicative group of the field Zq\mathbb{Z}_{q} is a pp-number. This paper examines the question of the number of two-element sets of prime numbers that satisfy the conditions of the last criterion. More precisely, let fk(x)f_{k}(x) be the number of sets {p,q}\{p,\,q\} such that p < q, pk1p \nmid k - 1, qk1q \nmid k - 1, (k,q)=1(k, q) = 1, pq1p \mid q - 1, the order of kk modulo qq is a pp\-number, and pp, qq are chosen among the first xx primes. We state that, if 2k100002 \leq |k| \leq 10000 and 1x500001 \leq x \leq 50000, then, for almost all considered kk, the function fk(x)f_{k}(x) can be approximated quite accurately by the function αkx0.85\alpha_{k}x^{0.85}, where the coefficient αk\alpha_{k} is different for each kk and {αk2k10000}(0.28;0.31]\{\alpha_{k} \mid 2 \leq |k| \leq 10000\} \subseteq (0.28;\,0.31]. We also investigate the dependence of the value fk(50000)f_{k}(50000) on kk and propose an effective algorithm for checking a two-element set of prime numbers for compliance with the conditions of the last criterion. The results obtained may have applications in the theory of computational complexity and algebraic cryptography.Пусть Gk=a,b; a1ba=bkG_{k} = \langle a, b;\ a^{-1}ba = b^{k} \rangle, где k0k \ne 0. Известно, что если pp - некоторое простое число, то группа GkG_{k} аппроксимируется конечными pp-группами тогда и только тогда, когда pk1p \mid k - 1. Известно также, что если pp и qq - простые числа, не делящие k1k - 1, p < q и π={p,q}\pi = \{p,\,q\}, то группа GkG_{k} аппроксимируется конечными π\pi-группами тогда и только тогда, когда (k,q)=1(k,q) = 1, pq1p \mid q - 1 и порядок числа kk в мультипликативной группе поля Zq\mathbb{Z}_{q} является pp-числом. В настоящей статье исследуется вопрос о количестве двухэлементных множеств простых чисел, удовлетворяющих условиям последнего критерия. Более точно, пусть fk(x)f_{k}(x) - количество множеств {p,q}\{p,\,q\} таких, что p < q, pk1p \nmid k - 1, qk1q \nmid k - 1, (k,q)=1(k, q) = 1, pq1p \mid q - 1, порядок kk по модулю qq является pp-числом и pp, qq выбираются среди первых xx простых чисел. Установлено, что если 2k100002 \leq |k| \leq 10000 и 1x500001 \leq x \leq 50000, то почти для всех рассматриваемых kk функция fk(x)f_{k}(x) может быть достаточно точно приближена функцией αkx0,85\alpha_{k}x^{0,85}, где коэффициент αk\alpha_{k} - свой для каждого kk и {αk2k10000}(0,28;0,31]\{\alpha_{k} \mid 2 \leq |k| \leq 10000\} \subseteq (0,28;\,0,31]. Также исследована зависимость величины fk(50000)f_{k}(50000) от kk и предложен эффективный алгоритм проверки двухэлементного множества простых чисел на соответствие условиям последнего критерия. Полученные результаты могут иметь приложения в теории сложности вычислений и алгебраической криптографии

    Объектно-ориентированная проверка соответствия модели на основе воспроизведения журнала событий: выявление желаемого поведения и локальных отклонений

    Get PDF
    Conformance checking methods diagnose to which extent a real system, whose behavior is recorded in an event log, complies with its specification model, e.g., a Petri net. Nonetheless, the majority of these methods focus on checking isolated process instances, neglecting interaction between instances in a system. Addressing this limitation, a series of object-centric approaches have been proposed in the field of process mining. These approaches are based on the holistic analysis of the multiple process instances interacting in a system, where each instance is centered on the handling of an object. Inspired by the object-centric paradigm, this paper presents a replay-based conformance checking method which uses a class of colored Petri nets (CPNs) -- a Petri net extension where tokens in the model carry values of some types (colors). Particularly, we consider conservative workflow CPNs which allow to describe the expected behavior of a system whose components are centered on the end-to-end processing of distinguishable objects. For describing a system’s real behavior, we consider event logs whose events have sets of objects involved in the execution of activities. For replay, we consider a jump strategy where tokens absent from input places of a transition to fire move from their current place of the model to the requested places. Token jumps allow to identify desire lines, i.e., object paths unforeseen in the specification. Also, we introduce local diagnostics based on the proportion of jumps in specific model components. The metrics allow to inform the severity of deviations in precise system parts. Finally, we report experiments supported by a prototype of our method. To show the practical value of our method, we employ a case study on trading systems, where orders from users are matched to trade.Методы проверки соответствия позволяют установить, в какой степени реальная система, поведение которой регистрируется в журнале событий, соответствует ее модели, например, в виде сети Петри. Большинство таких методов направлены на проверку изолированных экземпляров процесса и игнорируют взаимодействие между экземплярами в системе. Для преодоления этого ограничения в области интеллектуального анализа данных был предложен ряд объектно-ориентированных подходов. Эти подходы основаны на целостном анализе нескольких экземпляров процесса, взаимодействующих в системе, где каждый экземпляр соответствует некоторому объекту. В этой статье объектно-ориентированный подход применяется к методу проверки соответствия между журналами событий и цветными сетями Петри (CPN) -- расширением сетей Петри, в котором фишки в модели представляют собой значения некоторых типов (цветов). В частности, мы рассматриваем консервативные CPN потоков работ, которые позволяют описывать ожидаемое поведение системы, в которой компоненты соответствуют обработке различных объектов. Реальное поведение системы описано в журнале событий, в котором события атрибутированы участвующими в них объектами. Для воспроизведения журнала событий мы используем стратегию прыжков, когда фишки, необходимые для срабатывания перехода, перемещаются из своих текущих позиций во входные позиции этого перехода. Прыжки фишек позволяют идентифицировать линии желаний, то есть поведения объектов, не предусмотренные в спецификации. Также мы представляем локальную диагностику, основанную на доле прыжков в поведении конкретных компонент модели. Эти метрики позволяют судить о серьезности отклонений в тех или иных частях системы. Наконец, мы приводим эксперименты, выполненные с помощью программного прототипа. Практическая ценность нашего метода показана на примере моделирования торговых систем, при котором устанавливаются соответствия между заявками пользователей и сделками

    Рекурсивная проверка включения для рекурсивно определенных подтипов

    Get PDF
    We present a tableaux procedure that checks logical relations between recursively defined subtypes of recursively defined types and apply this procedure to the problem of resolving ambiguous names in a programming language. This work is part of a project to design a new programming language suitable for efficient implementation of logic. Logical formulas are tree-like structures with many constructors having different arities and argument types. Algorithms that use these structures must perform case analysis on the constructors, and access subtrees whose type and existence depend on the constructor used. In many programming languages, case analysis is handled by matching, but we want to take a different approach, based on recursively defined subtypes. Instead of matching a tree against different constructors, we will classify it by using a set of disjoint subtypes. Subtypes are more general than structural forms based on constructors, we expect that they can be implemented more efficiently, and in addition can be used in static type checking. This makes it possible to use recursively defined subtypes as preconditions or postconditions of functions. We define the types and the subtypes (which we will call adjectives), define their semantics, and give a tableaux-based inclusion checker for adjectives. We show how to use this inclusion checker for resolving ambiguous field references in declarations of adjectives. The same procedure can be used for resolving ambiguous function calls.Мы представляем табличную процедуру, которая проверяет логические отношения между рекурсивно определенными подтипами рекурсивно определенных типов, и применяем эту процедуру к проблеме разрешения неоднозначных имен в языке программирования. Эта работа является частью проекта по разработке нового языка программирования, подходящего для эффективной реализации логики. Логические формулы представляют собой древовидные структуры со множеством конструкторов, имеющих различные свойства и типы аргументов. Алгоритмы, использующие эти структуры, должны выполнять анализ вариантов для конструкторов и получать доступ к поддеревьям, тип и существование которых зависят от используемого конструктора. Во многих языках программирования анализ прецедентов обрабатывается путем сопоставления, но мы хотим использовать другой подход, основанный на рекурсивно определенных подтипах. Вместо сопоставления дерева с различными конструкторами мы будем классифицировать его с помощью набора непересекающихся подтипов. Подтипы являются более общими, чем структурные формы, основанные на конструкторах, мы ожидаем, что они могут быть реализованы более эффективно и, кроме того, могут использоваться при статической проверке типов. Это позволяет использовать рекурсивно определенные подтипы в качестве предварительных условий или постусловий функций. Мы определяем типы и подтипы (которые мы будем называть прилагательными), определяем их семантику и даем проверку включения прилагательных на основе таблиц. Мы показываем, как использовать эту проверку включения для разрешения неоднозначных ссылок на поля в объявлениях прилагательных. Та же процедура может быть использована для разрешения неоднозначных вызовов функций

    О свойствах правильного симплекса, вписанного в шар

    Get PDF
    Let  BB be a Euclidean ball in Rn{\mathbb R}^n and let C(B)C(B) be a space of continuos functions f:BRf:B\to{\mathbb R} with the uniform norm fC(B):=maxxBf(x).\|f\|_{C(B)}:=\max_{x\in B}|f(x)|. By Π1(Rn)\Pi_1\left({\mathbb R}^n\right) we mean a set of polynomials of degree 1\leq 1, i.e., a set of linear functions upon Rn{\mathbb R}^n. The interpolation projector  P:C(B)Π1(Rn)P:C(B)\to \Pi_1({\mathbb R}^n) with the nodes x(j)Bx^{(j)}\in B is defined by the equalities Pf(x(j))=f(x(j))Pf\left(x^{(j)}\right)=f\left(x^{(j)}\right),  j=1,,n+1j=1,\ldots, n+1.The norm of PP as an operator from C(B)C(B) to C(B)C(B) can be calculated by the formula PB=maxxBλj(x).\|P\|_B=\max_{x\in B}\sum |\lambda_j(x)|. Here λj\lambda_j are the basic Lagrange polynomials corresponding to the nn-dimensional nondegenerate simplex SS with the vertices x(j)x^{(j)}. Let PP^\prime be a projector having the nodes in the vertices of a regular simplex inscribed into the ball. We describe the points yBy\in B with the property PB=λj(y)\|P^\prime\|_B=\sum |\lambda_j(y)|. Also we formulate some geometric conjecture which implies that PB\|P^\prime\|_B is equal to the minimal norm of an interpolation projector with nodes in BB.  We prove that this conjecture holds true at least for n=1,2,3,4n=1,2,3,4. Пусть  BB - евклидов шар в Rn{\mathbb R}^n, C(B)C(B) - пространство непрерывных функций f:BRf:B\to{\mathbb R} с равномерной нормой fC(B):=maxxBf(x).\|f\|_{C(B)}:=\max_{x\in B}|f(x)|. Под Π1(Rn)\Pi_1\left({\mathbb R}^n\right) понимается совокупность многочленов от nn переменных степени 1\leq 1, то есть линейных функций на  Rn{\mathbb R}^n. Интерполяционный проектор P:C(B)Π1(Rn)P:C(B)\to \Pi_1({\mathbb R}^n) c узлами x(j)Bx^{(j)}\in B определяется равенствами Pf(x(j))=f(x(j))Pf\left(x^{(j)}\right)=f\left(x^{(j)}\right),  j=1,,n+1j=1,\ldots, n+1. Норма PP как оператора из C(B)C(B) в~C(B)C(B) вычисляется по формуле PB=maxxBλj(x),\|P\|_B=\max_{x\in B}\sum |\lambda_j(x)|, где λj\lambda_j - базисные многочлены Лагранжа невырожденного nn-мерного симплекса с вершинами x(j)x^{(j)}. Пусть PP^\prime - проектор, узлы которого совпадают с вершинами правильного симплекса, вписанного в шар. В статье найдены точки yBy\in B, для которых PB=λj(y)\|P^\prime\|_B=\sum |\lambda_j(y)|. Формулируется геометрическая гипотеза, из справедливости которой следует, что PB\|P^\prime\|_B есть минимальное значение нормы интерполяционного проектора, узлы которого принадлежат BB.  Доказывается, что эта гипотеза справедлива по крайней мере для n=1,2,3,4n=1,2,3,4.

    LTL-спецификация счётчиковых машин

    Get PDF
    The article is written in support of the educational discipline “Non-classical logics”. Within the framework of this discipline, the objects of study are the basic principles and constructive elements, with the help of which the formal construction of various non-classical propositional logics takes place. Despite the abstractness of the theory of non-classical logics, in which the main attention is paid to the strict mathematical formalization of logical reasoning, there are real practical areas of application of theoretical results. In particular, languages of temporal modal logics are widely used for modeling, specification, and verification (correctness analysis) of logic control program systems. This article demonstrates, using the linear temporal logic LTL as an example, how abstract concepts of non-classical logics can be reƒected in practice in the field of information technology and programming. We show the possibility of representing the behavior of a software system in the form of a set of LTL-formulas and using this representation to verify the satisfiability of program system properties through the procedure of proving the validity of logical inferences, expressed in terms of the linear temporal logic LTL. As program systems, for the specification of the behavior of which the LTL logic will be applied, Minsky counter machines are considered. Minsky counter machines are one of the ways to formalize the intuitive concept of an algorithm. They have the same computing power as Turing machines. A counter machine has the form of a computer program written in a high-level language, since it contains variables called counters, and conditional and unconditional jump operators that allow to build loop constructions. It is known that any algorithm (hypothetically) can be implemented in the form of a Minsky three-counter machine.Статья написана в поддержку учебной дисциплины “Неклассические логики”. В рамках этой дисциплины объектами изучения являются базовые принципы и конструктивные элементы, с помощью которых происходит формальное построение различных неклассических логик высказываний. Несмотря на абстрактность теории неклассических логик, в которой основное внимание уделяется строгой математической формализации логических рассуждений, существуют реальные прикладные области применения теоретических результатов. В частности, языки темпоральных модальных логик широко используются для моделирования, спецификации и верификации (анализа корректности) программных систем логического управления. В этой статье на примере линейной темпоральной логики LTL демонстрируется, как абстрактные понятия неклассических логик могут находить отражение на практике в области информационных технологий и программирования. Показывается возможность представления поведения программной системы в виде набора LTL-формул и использования этого представления для проверки выполнимости программных свойств системы через процедуру доказательства справедливости логических выводов, выраженных в терминах линейной темпоральной логики LTL. В качестве программных систем, для спецификации поведения которых будет применяться логика LTL, рассматриваются счётчиковые машины Минского. Счётчиковые машины Минского — один из способов формализации интуитивного понятия алгоритма. Они обладают той же вычислительной мощностью, что и машины Тьюринга. Счётчиковая машина имеет вид компьютерной программы, написанной на языке высокого уровня, поскольку содержит переменные, называемые счётчиками, и операторы условного и безусловного перехода, позволяющие строить конструкции циклов. Известно, что любой алгоритм (гипотетически) может быть реализован в виде трёхсчётчиковой машины Минского

    Исправление к статье: Ю. В. Косолапов, «Об обнаружении эксплуатации уязвимостей, приводящей к запуску вредоносного кода», Моделирование и анализ информационных систем, Том 27, №2, с. 138–151, 2020. DOI: https://doi.org/10.18255/1818-1015-2020-2-138-151

    Get PDF
    In the article by Y. V. Kosolapov “On the Detection of Exploitation of Vulnerabilities Leading to the Execution of a Malicious Code” (Modeling and analysis of information systems, vol. 27, no. 2, pp. 138–151, 2020; https://doi.org/10.18255/1818-1015-2020-2-138-151) an inaccurate description of the algorithm CheckTrace is committed. The correct description of the algorithm CheckTrace is given below. The author apologises for the inconvenience.В статье Ю. В. Косолапова «Об обнаружении эксплуатации уязвимостей, приводящей к запуску вредоносного кода» (Моделирование и анализ информационных систем, том 27, №2, с. 138–151, 2020; https://doi.org/10.18255/1818-1015-2020-2-138-151) допущена неточность в описании алгоритма CheckTrace. Корректное описание алгоритма CheckTrace приведено ниже. Автор приносит извинения за причинённые неудобства

    Векторизация текстов на основе word-embedding моделей с использованием кластеризации

    Get PDF
    It is known that in the tasks of natural language processing, the representation of texts by vectors of fixed length using word-embedding models makes sense in cases where the vectorized texts are short.The longer the texts being compared, the worse the approach works. This situation is due to the fact that when using word-embedding models, information is lost when converting the vector representations of the words that make up the text into a vector representation of the entire text, which usually has the same dimension as the vector of a single word.This paper proposes an alternative way for using pre-trained word-embedding models for text vectorization. The essence of the proposed method consists in combining semantically similar elements of the dictionary of the existing text corpus by clustering their (dictionary elements) embeddings, as a result of which a new dictionary is formed with a size smaller than the original one, each element of which corresponds to one cluster. The original corpus of texts is reformulated in terms of this new dictionary, after which vectorization is performed on the reformulated texts using one of the dictionary approaches (TF-IDF was used in the work). The resulting vector representation of the text can be additionally enriched using the vectors of words of the original dictionary obtained by decreasing the dimension of their embeddings for each cluster.A series of experiments to determine the optimal parameters of the method is described in the paper, the proposed approach is compared with other methods of text vectorization for the text ranking problem – averaging word embeddings with TF-IDF weighting and without weighting, as well as vectorization based on TF-IDF coefficients.Известно, что в задачах обработки естественного языка представление текстов векторами фиксированной длины с использованием word-embedding моделей оправдано в тех случаях, когда векторизуемые тексты являются короткими. Чем сравниваемые тексты длиннее, тем подход работает хуже. Такая ситуация обусловлена тем, что при использовании word-embedding моделей происходит потеря информации при преобразовании векторных представлений слов, составляющих текст, в векторное представление всего текста, имеющее обычно ту же размерность, что и вектор отдельного слова.В настоящей работе предлагается альтернативный способ использования предобученных word-embedding моделей для векторизации текстов. Суть предлагаемого способа заключается в объединении семантически близких элементов словаря имеющегося корпуса текстов путем кластеризации их (элементов словаря) эмбеддингов, в результате чего формируется новый словарь размером меньше исходного, каждый элемент которого соответствует одному кластеру. Исходный корпус текстов переформулируется в терминах этого нового словаря, после чего на переформулированных текстах выполняется векторизация одним из словарных подходов (в работе применялся TF-IDF). Полученное векторное представление текста дополнительно может обогащаться с использованием векторов слов исходного словаря, полученных путем уменьшения размерности их эмбеддингов по каждому кластеру.В работе описана серия экспериментов по определению оптимальных параметров предлагаемого подхода; для задачи ранжирования текстов приведено сравнение подхода с другими способами векторизации – усреднением эмбеддингов слов со взвешиванием по TF-IDF и без взвешивания, а также с векторизацией на основе TF-IDF коэффициентов

    707

    full texts

    782

    metadata records
    Updated in last 30 days.
    Modeling and Analysis of Information Systems / Моделирование и анализ информационных систем (МАИС)
    Access Repository Dashboard
    Do you manage Open Research Online? Become a CORE Member to access insider analytics, issue reports and manage access to outputs from your repository in the CORE Repository Dashboard! 👇