Modeling and Analysis of Information Systems / Моделирование и анализ информационных систем (МАИС)
Not a member yet
782 research outputs found
Sort by
Верификация алгоритмов мультиагентного анализа данных с помощью системы проверки моделей SPIN
Get PDFThe paper presents an approach to formal verification of multi-agent data analysis algorithms for ontology population. The system agents correspond to information items of the input data and the rule of ontology population and data processing. They determine values of information objects obtained at the preliminary phase of the analysis. The agents working in parallel check the syntactic and semantic consistency of tuples of information items. Since the agents operate in parallel, it is necessary to verify some important properties of the system related to it, such as the property that the controller agent correctly determines the system termination. In our approach, the model checking tool SPIN is used. The protocols of agents are written in Promela language (the input language of the tool) and the properties of the multi-agent data analysis system are expressed in the liner time logic LTL. We carried out several experiments to check this model in various modes of the tool and various numbers of agents.В статье представлен подход к формальной верификации алгоритмов мультиагентного анализа данных для пополнения онтологий. Агенты системы на основе входных данных устанавливают значения элементов объектов, полученных на предварительной стадии анализа. Агенты параллельно осуществляют проверку семантической и синтаксической согласованности, используя правила пополнения онтологий и обработки данных. Поскольку агенты действуют параллельно, необходимо верифицировать некоторые важные свойства системы, связанные с этим, например, свойство корректности определения завершения работы системы. В нашем подходе используется инструмент проверки моделей SPIN. Протоколы агентов записаны на языке Promela, а свойства мультиагентной системы анализа данных выражены в логике LTL. Мы провели ряд экспериментов по проверке данной модели
Счётная аддитивность распространения оператора дифференцирования
Get PDFIn this article, we continue the study of the properties acquired by the differentiation operator Λ with spreading beyond the space W1¹. The study is conducted by introducing the family of spaces Yp¹ , 0 < p < 1, having analogy with the family Wp¹, 1 ≤ p < ∞. Spaces Yp¹ are equiped with quasinorms constructed on quasinorms spaces Lp as the basis; Λ : Yp¹ → Lp. We have given a sufficient condition for a function, piecewise belonging to the space Yp¹ to be in this space (if f ∈ Yp¹ [xi-1; xi ], i ∈ N, 0 = x0 < x1 < · · · < xi < · · · < 1, then f ∈ Yp¹ [0; 1]). In other words, it is the sign when the equality: Λ(S fi) = S Λ(fi) is true. The bounded variation in the Jordan sense is closest to the sufficient condition among the classic characteristics of functions. As a corollary, it comes out that, if a function f piecewise belongs to the space of W1¹ and has a bounded variation, f belongs to each space Yp¹ , 0 < p < 1
О поддержке рекурсивно-параллельного программирования в .NET Framework
Get PDFThe paper describes software components to support recursive-parallel programming for the .NET Framework. They are dynamic link libraries providing the necessary functionality for developing and debugging applications for parallel execution on a local network. Communication module library classes provide user-friendly software tools to establish ”each with each” network connection and reliable asynchronous transmission for serializable objects. Classes of the recursive-parallel programming library provide representation of parallel computation branches as migratory processes, their initial distribution over the network, the transmission parameters and return results with the necessary synchronization, dynamic reallocation of work for load balancing and also sharing data processing. By this example it also describes some variants of the recursive-parallel algorithm to solve the problem of finding a maximum clique in a non-oriented graph and the results of testing the considered components
Классические и неклассические симметрии нелинейного дифференциального уравнения для описания волн в жидкости с пузырьками газа
Get PDFA nonlinear differential equation is considered for describing nonlinear waves in a liquid with gas bubbles. Classical and nonclassical symmetries of this equation are investigated. It is shown that the considered equation admits transformations in space and time. At a certain condition on parameters, this equation also admits a group of Galilean transformations. The method by Bluman and Cole is used for finding nonclassical symmetries admitted by the studied equation. Both regular and singular cases of nonclassical symmetries are considered. Five families of nonclassical symmetries admitted by this equation are constructed. Symmetry reductions corresponding to these families of generators are obtained. Exact solutions of these symmetry reductions are constructed. These solutions are expressed via rational, exponential, trigonometric and special functions.Рассматривается нелинейное дифференциальное уравнение для описания нелинейных волн в жидкости с пузырьками газа при учете вязкости жидкости и процесса межфазного теплообмена. Исследованы классические и неклассические симметрии данного уравнения в частных производных. Показано, что исследуемое уравнение инвариантно относительно преобразований сдвига по пространственной и временной координатам. При дополнительном ограничении на параметры, уравнение также инвариантно относительно преобразования Галилея. Неклассические симметрии рассматриваемого уравнения находятся методом Блюмана и Коула. Изучены регулярный и сингулярный случаи неклассических симметрий. Найдены пять семейств неклассических симметрий, допускаемых исследуемым уравнением. Построены инвариантные редукции, соответствующие данным симметриям. С их помощью найдены семейства точных решений исследуемого уравнения. Полученные решения выражаются через рациональные, тригонометрические и специальные функции
Построение IL-программ ПЛК по LTL-спецификации
Get PDFAn approach to the construction and verification of PLC IL-programs for discrete problems is proposed. For the specification of the program behavior, we use the linear-time temporal logic LTL. Programming is carried out in the IL-language (Instruction List) according to an LTL-specification. The correctness analysis of an LTL-specification is carried out by the symbolic model checking tool Cadence SMV. A new approach to programming and verification of PLC IL-programs is shown by an example. For a discrete problem, we give an IL-program and its LTL-specification.The purpose of the article is to describe an approach to programming PLC, which would provide a possibility of IL-program correctness analysis by the model checking method.Under the proposed approach, the change of the value of each program variable is described by a pair of LTL-formulas. The first LTL-formula describes situations which increase the value of the corresponding variable, the second LTL-formula specifies conditions leading to a decrease of the variable value. The LTL-formulas (used for speci- fication of the corresponding variable behavior) are constructive in the sense that they construct the PLC-program (IL-program), which satisfies temporal properties expressed by these formulas. Thus, the programming of PLC is reduced to the construction of LTLspecification of the behavior of each program variable. In addition, an SMV-model of a PLC IL-program is constructed according to LTL-specification. Then, the SMV-model is analysed by the symbolic model checking tool Cadence SMV
О работе семинара «Нелинейная динамика»
Get PDFВ 2013 году в рамках научно-образовательного центра «Нелинейная динамика» продолжил работу научный семинар, посвященный исследованиям поведения, а также методам анализа динамических систем. За прошедший учебный год на нем было заслушано более тридцати сообщений по тематике исследований научно-образовательного центра. Ниже представлены тезисы наиболее интересных докладов, прозвучавших на семинаре
Синтез моделей процессов по журналам событий с шумом
Get PDFProcess mining is a new emerging discipline related to process management, formal process models, and data mining. One of the main tasks of process mining is the model synthesis (discovery) based on event logs. A wide range of algorithms for process model discovery, analysis, and enhancement is developed. The real-life event logs often contain noise of different types. In this paper we describe the main causes of noise in the event logs and study the effect of noise on the performance of process discovery algorithms. The experimental results of application of the main process discovery algorithms to artificial event logs with noise are provided. Specially generated event logs with noise of different types were processed using the four basic discovery techniques. Although modern algorithms can cope with some types of noise, in most cases, their use does not lead to obtaining a satisfactory result. Thus, there is a need for more sophisticated algorithms to deal with noise of different types
Локальная динамика логистического уравнения, содержащего запаздывание
Get PDFWe considered a logistic equation with delay and studied its local dynamics. The critical cases have been found in the problem of the equilibrium state stability. We applied standard Andronov-Hopf biffurcation methods for delay differential equations and an asymptotic method, developed by one of the authors, based on the construction of special evolution equations that define the local dynamics equations with delay. It is shown that all solutions of the equation tend to an equilibrium state or result in a single stable cycle. The results of numerical modelling are presented in this paper. The study has proved that analytical and numerical modeling results have a good correlation.Рассматривается логистическое уравнение с добавлением слагаемого, ха- рактеризующего запаздывание. Исследуется локальная динамика этого уравнения. Выделены критические случаи в задаче об устойчивости состояния равновесия. Используются стандартные бифуркационные методы Андронова– Хопфа для уравнений с запаздыванием и разработанный одним из авторов асимптотический метод, основанный на построении специальных эволюционных уравнений, которые и определяют локальную динамику уравнений, содержащих запаздывание. Показано, что в зависимости от одного из параметров уравнения либо все решения стремятся к состоянию равновесия, либо выходят на единственный устойчивый цикл. Приведены результаты численного исследования. Отмечено хорошее совпадение результатов численного моделирования с утверждениями аналитического плана
Разработка самоприменимой системы верификации. Теория и практика
Get PDFAs opposed to traditional testing, the deductive verification represents a formal way to examine the program correctness. But what about the correctness of the verification system itself? The theoretical foundations of Hoare’s logic were examined in classical works, and some soundness/completeness theorems are well-known. However, we practically are not aware of implementations of those theoretical methods which were subjected to anything more than testing. In other words, our ultimate goal is a verification system which can be self-applicable (at least partially). In our recent studies we addressed ourselves to the metageneration approach in order to make such a task more feasible.По сравнению с традиционным тестированием дедуктивная верификация предлагает более формальный способ доказательства корректности программ. Но как установить корректность самой системы верификации? Теоретические основы логик Хоара исследовались в классических работах, где были получены различные результаты по непротиворечивости и полноте. Однако нам не известны реализации этих теоретических методов, проверенные чем-либо отличным от обычного тестирования. Иными словами, нас интересует система верификации, которая может быть применена к самой себе (хотя бы частично). В наших исследованиях мы обратились к методу метагенерации, который выглядит многообещающим для этой задачи
Влияние запаздывающей обратной связи на устойчивость периодических орбит
Get PDFIn this paper we solve problems of stabilization of unstable cycle by the delay feedback. We study a model equation with qubic nonlinearity. In this case only one multiplicator is located outside a unit circle. Delay time is proportional to the cycle period. The D-partition of the parameter plane is obtained. The main result is analytically found conditions for parameters of delay control such that the initial cycle is stable. Also, we have found necessary and sufficient conditions of solvability of the stabilization problem. As a consequence, the problem of stablity of the Stuart–Landau equation periodic solution is completely solved.В работе решается задача стабилизации неустойчивого цикла с помощью запаздывающей обратной связи на примере модельного уравнения с кубической нелинейностью. Мы рассматриваем случай, когда в задаче без управления ровно один мультипликатор цикла расположен вне единичной окружности. Время запаздывания выбирается пропорциональным периоду исходного цикла, чтобы в задаче с управлением исходное решение сохранялось без изменений. Для плоскости комплексного коэффициента запаздывающего управления получено D-разбиение. Главный результат состоит в аналитически найденных условиях на параметры запаздывающей обратной связи – коэффициент и время задержки, – при которых исходное периодическое решение становится устойчивым. Также определены необходимые и достаточные условия на собственные параметры задачи, при которых задача стабилизации разрешима. Как следствие, полностью решена задача об устойчивости цикла уравнения Стюарта–Ландау