Modeling and Analysis of Information Systems / Моделирование и анализ информационных систем (МАИС)
Not a member yet
782 research outputs found
Sort by
Исправление к статье: В. В. Васильчиков, «Параллельный алгоритм решения задачи об изоморфизме графов», Моделирование и анализ информационных систем, Том 27, №1, с. 86–94, 2020. DOI: https://doi.org/10.18255/1818-1015-2020-1-86-94
Get PDFIn the article by V. V. Vasilchikov “Parallel Algorithm for Solving the Graph Isomorphism Problem” ( Modeling and analysis of information systems, vol. 27, no. 1, pp. 86–94, 2020; DOI: https://doi.org/10.18255/1818-1015-2020-1-86-94) there was a misprint in the layout. In the Table 1, in the last column of the row “Degree of graph” the value should be 3000 (instead of 300). The corrected “Table 1” is shown below. The editors apologise for the inconvenience.В статье В.В. Васильчикова «Параллельный алгоритм решения задачи об изоморфизме графов» (Моделирование и анализ информационных систем, том 27, №1, с. 86–94, 2020; https://doi.org/10.18255/1818-1015-2020-1-86-94) при вёрстке была допущена опечатка. В таблице 1 в последнем столбце строки «Степень графа» должно быть значение 3000 (вместо 300). Исправленная «Таблица 1» приводится ниже. Редакция приносит извинения за доставленные неудобства
Аппроксимация ресурсных эквивалентностей в сетях Петри с невидимыми переходами
Get PDFTwo resources (submarkings) are called similar if in any marking any one of them can be replaced by another one without affecting the observable behavior of the net (regarding marking bisimulation). It is known that resource similarity is undecidable for general labelled Petri nets. In this paper we study the properties of the resource similarity and resource bisimulation (a subset of complete similarity relation closed under transition firing) in Petri nets with invisible transitions (where some transitions may be labelled with an invisible label (τ) that makes their firings unobservable for an external observer). It is shown that for a proper subclass (p-saturated nets) the resource bisimlation can be effectively checked. For a general class of Petri net with invisible transitions it is possible to construct a sequence of so-called (n, m)-equivalences approximating the largest τ-bisimulation of resources.Два ресурса (подразметки) называются подобными, если в любой разметке любой из них может быть заменен другим, и при этом наблюдаемое поведение сети не изменится (относительно бисимуляции разметок). Известно, что подобие ресурсов неразрешимо для обыкновенных сетей Петри. В этой статье мы изучаем свойства подобия ресурсов и бисимуляции ресурсов (подмножество отношения подобия, замкнутое по срабатыванию переходов) в сетях Петри с невидимыми переходами (где некоторые переходы могут быть помечены специальной меткой (τ), что делает их срабатывания невидимыми для внешнего наблюдателя). Показано, что для собственного подкласса (p-насыщенных сетей) бисимуляция ресурсов может быть эффективно проверена. Для общего класса сетей Петри с невидимыми переходами можно построить последовательность так называемых (n, m)-эквивалентностей, аппроксимирующую наибольшую τ-бисимиляцию ресурсов
Современные методы детектирования и классификации токсичных комментариев с использованием нейронных сетей
Get PDFThe growth of popularity of online platforms which allow users to communicate with each other, share opinions about various events, and leave comments boosted the development of natural language processing algorithms. Tens of millions of messages per day are published by users of a particular social network need to be analyzed in real time for moderation in order to prevent the spread of various illegal or offensive information, threats and other types of toxic comments. Of course, such a large amount of information can be processed quite quickly only automatically. that is why there is a need to and a way to teach computers to “understand” a text written by humans. It is a non-trivial task even if the word “understand” here means only “to classify”. the rapid evolution of machine learning technologies has led to ubiquitous implementation of new algorithms. A lot of tasks, which for many years were considered almost impossible to solve, are now quite successfully solved using deep learning technologies. this article considers algorithms built using deep learning technologies and neural networks which can successfully solve the problem of detection and classification of toxic comments. In addition, the article presents the results of the developed algorithms, as well as the results of the ensemble of all considered algorithms on a large training set collected and tagged by Google and Jigsaw.Рост популярности онлайн-платформ, позволяющих пользователям общаться друг с другом, делиться мнениями о различных событиях, оставлять комментарии, подтолкнул к развитию алгоритмов обработки естественного языка. Десятки миллионов сообщений в день, которые публикуют пользователи отдельно взятой социальной сети, необходимо анализировать в режиме реального времени или близко к тому с целью модерации, чтобы не допустить распространение различной противозаконной или оскорбительной информации, угроз и других видов токсичных комментариев. Разумеется такой большой объем информации может быть обработан достаточно быстро только автоматически. Возникает необходимость научить компьютер «понимать» текст, написанный человеком, что является нетривиальной задачей, пусть даже под «пониманием» текста подразумевается лишь его классификация. Бурное развитие технологий машинного обучения обусловило повсеместное внедрение новых алгоритмов. Многие задачи, в том числе и задачи обработки естественного языка, которые долгие годы считалось практически невозможно решить, сейчас вполне успешно решаются с использованием технологий глубокого обучения. В данной статье будут рассмотрены алгоритмы, построенные с использованием технологий глубокого обучения и нейронных сетей, позволяющие успешно решать задачу распознавания и классификации токсичных комментариев. Помимо этого, в статье будут приведены результаты тестирования как разработанных алгоритмов, так и ансамбля данных алгоритмов на большой обучающей выборке, собранной и размеченной специалистами компаний Google и Jigsaw
Синтез установочных последовательностей для автоматов с временными ограничениями
Get PDFState identification is the well-known problem in the theory of Finite State Machines (FSM) where homing sequences (HS) are used for the identification of a current FSM state, and this fact is widely used in the area of software and hardware testing and verification. For various kinds of FSMs, such as partial, complete, deterministic, non-deterministic, there exist sufficient and necessary conditions for the existence ofpreset and adaptive HS and algorithms for their derivation. Nowadays timed aspects become very important for hardware and software systems and for this reason classical FSMs are extended by clock variables. In this work, we address the problem of checking the existence and derivation of homing sequences for FSMs with timed guards and show that the length estimation for timed homing sequence coincides with that for untimed FSM. The investigation is based on the FSM abstraction of a Timed FSM, i.e. on a classical FSM which describes behavior of corresponding TFSM and inherits some of its properties. When solving state identification problems for timed FSMs, the existing FSM abstraction is properly optimized.Идентификация состояний является хорошо известной задачей теории конечных автоматов, и установочные последовательности, которые позволяют идентифицировать текущее состояние конечного автомата, широко используются в областях тестирования и верификации программного и аппаратного обеспечения. Для автоматов различных классов, полностью определенных и частичных, детерминированных и недетерминированных, установлены необходимые и достаточные условия существования безусловных и адаптивных установочных последовательностей и предложены алгоритмы их синтеза, если такая последовательность существует. В настоящее время при верификации и тестировании программного и аппаратного обеспечения необходимо учитывать временные аспекты, что приводит к расширению автоматных моделей временными переменными. В настоящей работе мы исследуем задачи проверки существования и синтеза безусловных и адаптивных установочных последовательностей для автоматов с временными ограничениями и показываем, что оценки на длину таких последовательностей совпадают с оценками для классических конечных автоматов. Предлагаемый подход основан на использовании конечно-автоматной абстракции временного автомата, то есть описании временного автомата соответствующим конечным автоматом, который сохраняет свойства временного автомата относительно установочных последовательностей
Алгоритмы для BDI-агентов, основанные на знаниях
Get PDFMultiagent algorithm is a knowledge-based distributed algorithm that solves some problems by means of cooperative work of agents. From an individual agent's perspective, a multiagent algorithm is a reactive and proactive knowledge/believe-based rational algorithm aimed to achieve an agent's own desires. In the paper we study a couple of knowledge-based multiagent algorithms. One particular algorithm is for a system consisting of agents that arrive one by one (in a non-deterministic order) to a resource center to rent (for a while) one of available desired resources. Available resources are passive, they form a cloud; each of the available resources is lent on demand if there is no race for this resource and returns to the cloud after use. Agents also form a cloud but leave the cloud immediately when they rent a desired resource. The problem is to design a knowledge-based multiagent algorithm, which allows each arriving agent eventually to rent some of desired resources (without race for these resources).Мультиагентный алгоритм — это распределённый алгоритм, основанный на знаниях, который решает некоторую проблему посредством совместной работы агентов. BDI-агент — это агент, обладающий убеждениями (Belief), желаниями (Desire) и намерениями (Intention). С точки зрения такого агента, мультиагентный алгоритм — это алгоритм, основанный на его знаниях и убеждениях, с помощью которого достигается выполнение его желаний посредством последовательного осуществления намерений. Мы считаем также, что агенты реактивны, проактивны и рациональны. В этой статье мы предлагаем и изучаем два мультиагентных алгоритма, которые основаны на знаниях. В частности, мы предлагаем мультиагентный алгоритм для следующей задачи аренды ресурсов. Система состоит из агентов, которые прибывают один за другим в произвольном порядке в ресурсный центр, чтобы арендовать один из предоставляемыхресурсов. Предоставляемые ресурсы пассивны, они образуют облако. Если за ресурс нет конкуренции, то он предоставляется по запросу, и возвращается в облако после использования. Агенты также образуют облако, но когда арендуют нужный ресурс, то сразу же покидают ресурсный центр. Задача состоит в разработке мультиагентного алгоритма, основанного на знаниях, обладающего следующим свойством корректности: каждый прибывающий в ресурсный центр агент рано или поздно арендует какой-либо из запрашиваемых ресурсов без конкуренции за этот ресурс в данный момент
Темпоральная логика для программируемых логических контроллеров
Get PDFWe address the formal verification of the control software of critical systems, i.e., ensuring the absence of design errors in a system with respect to requirements. Control systems are usually based on industrial controllers, also known as Programmable Logic Controllers (PLCs). A specific feature of a PLC is a scan cycle: 1) the inputs are read, 2) the PLC states change, and 3) the outputs are written. Therefore, in order to formally verify PLC, e.g., by model checking, it is necessary to describe the transition system taking into account this specificity and reason both in terms of state transitions within a cycle and in terms of larger state transitions according to the scan-cyclic semantics. We propose a formal PLC model as a hyperprocess transition system and temporal cycle-LTL logic based on LTL logic for formulating PLC property. A feature of the cycle-LTL logic is the possibility of viewing the scan cycle in two ways: as the effect of the environment (in particular, the control object) on the control system and as the effect of the control system on the environment. For both cases we introduce modified LTL temporal operators. We also define special modified LTL temporal operators to specify inside properties of scan cycles. We describe the translation of formulas of cycle-LTL into formulas of LTL, and prove its correctness. This implies the possibility ofmodel checking requirements expressed in logic cycle-LTL, by using well-known model checking tools with LTL as specification logic, e.g., Spin. We give the illustrative examples of requirements expressed in the cycle-LTL logic.Мы исследуем формальную верификацию управляющего программного обеспечения критических систем, т. е. проверку соответствия функционирования проектируемой системы предъявленным требованиям. Важнейший класс управляющего программного обеспечения составляют программы для программируемых логических контроллеров (ПЛК). Особенностью программ ПЛК является цикл управления: 1) считываются входы, 2) изменяются состояния ПЛК и 3) записываются выходы. Поэтому для формальной верификации программ ПЛК нужна возможность описывать учитывающие эту специфику системы переходов, а также определять свойства систем, моделирующих программы ПЛК, как относительно переходов внутри цикла, так и относительно более крупных переходов в соответствии с семантикой цикла управления. Мы предлагаем формальную модель программы ПЛК как систему переходов гиперпроцессов и темпоральную логику cycle-LTL для формализации свойств ПЛК. Особенностью логики cycle-LTL является возможность рассматривать свойства систем управления двояким образом: воздействие окружения на систему управления и воздействие системы управления на окружение. Мы определяем модификации стандартных темпоральных операторов логики LTL для каждого из этих случаев, а также для свойств внутри цикла управления. Рассмотрены примеры требований, определенных в нашей логике. Описана трансляция формул cycle-LTL в формулы LTL и показана её корректность. Доказана возможность сведения задачи верификации методом проверки моделей для требований, определенных в логике cycle-LTL, к задаче верификации требований, определенных в стандартной логике LTL
Марковская модель совместных киберугроз и ее применение для выбора оптимального набора средств защиты информации
Get PDFIn this work, we study a Markov model of cyber threats that act on a computer system. Within the framework of the model the computer system is considered as a system with failures and recoveries by analogy with models of reliability theory. To estimate functionally-temporal properties of the system we introduce a parameter called the lifetime of the system and defined as the number of transitions of the corresponding Markov chain until the first hit to the final state. Since this random variable plays an important role at evaluating a security level of the computer system, we investigate in detail its random distribution for the case of mutually exclusive cyber threats; in particular, we derive explicit analytical formulae for numerical characteristics of its distribution: expected value and dispersion. Then we generalize substantially the Markov model dropping the assumption that cyber threats acting on the system are mutually exclusive. This modification leads to an extended Markov chain that has (at least qualitatively) the same structure as the original chain. This fact allowed to generalize the above analytical results for the expected value and dispersion of the lifetime to the case of non-mutually exclusive cyber threats. At the end of the work the Markov model for non-mutually exclusive cyber threats is used to state a problem of finding an optimal configuration of security remedies in a given cyber threat space. It is essential that the formulated optimization problems belong to the class of non-linear discrete (Boolean) programming problems. Finally, we consider an example that illustrate the solution of the problem on selecting the optimal set of security remedies for a computer system.В данной работе исследуется марковская модель киберугроз, действующих на компьютерную систему. В рамках данной модели компьютерная система рассматривается как система с отказами и восстанавлениями по аналогии с моделями теории надежности. Для оценки функционально-временных свойств системы мы вводим ее параметр, называемый временем жизни и определяемый как число переходов в соответствующей марковской цепи до первого попадания в финальное состояние. В силу того, что данная случайная величина играет важную роль при оценке уровня защищенности компьютерной системы, мы подробно исследуем ее распределение вероятностей в случае несовместных киберугроз; в частности, мы получаем явные аналитические формулы для ее числовых характеристик: математического ожидания и дисперсии. Затем мы существенно обобщаем рассматриваемую марковскую модель, исключив допущение о несовместности действующих на систему киберугроз. Соответствующая марковская цепь при такой модификации расширяется за счет дополнительных состояний, не меняя своей качественной структуры. Указанный факт позволил обобщить полученные ранее аналитические результаты для математического ожидания и дисперсии времени жизни на случай совместных киберугроз. В заключении работы марковская модель совместных кибеугроз используется для постановки задачи о поиске оптимальной конфигурации средств защиты информации в заданном пространстве киберугроз. Существенно, что сформулированные оптимизационные задачи принадлежат к классу задач нелинейного дискретного (булева) программирования. В заключении работы рассматривается пример, иллюстрирующий решение задачи о выборе оптимального набора средств защиты для компьютерной системы
Динамически изменяющийся параллелизм с асинхронно-последовательными потоками данных
Get PDFA statically typed version of the data driven functional parallel computing model is proposed. It enables a representation of dynamically changing parallelism by means of asynchronous serial data flows. We consider the features of the syntax and semantics of the statically typed data driven functional parallel programming language Smile that supports asynchronous sequential flows. Our main idea is to apply the Hoar concept of communicating sequential processes to the computation control on the data readiness. It is assumed that on the data readiness a control signal is emitted to inform the processes about the occurrence of certain events. The special feature of our approach is that the model is extended with the special asynchronous containers that can generate events on their partial filling. These containers are a stream and a swarm, each of which has its own specifics. A stream is used to process data which have identical type. The data comes sequentially and asynchronously at arbitrary time moments. The number of the incoming data elements is initially unknown, so the processing completes on the signal of the end of the stream. A swarm is used to contain independent data of the same type and may be used for the massive parallel operations performing. Unlike a stream, the swarm’s size is fixed and known in advance. General principles of the operations with the asynchronous sequential flows with an arbitrary order of data arrival are described. The use of the streams and the swarms in various situations is considered. We propose the language constructions which allow us to operate the swarms and streams and describe the specifics of their application. We provide the sample functions to illustrate the use of the different approaches to description of the parallelism: recursive processing of the asynchronous flows, processing of the flows in an arbitrary or predefined order of operations, direct access and access by the reference to the elements of the streams and swarms, pipelining of calculations. We give a preliminary parallelism assessment which depends on the ratio of the rates of data arrival and their processing. The proposed methods can be used in the development of the future languages and tool-kits of architecture-independent parallel programming.Предлагается статически типизированная версия модели функционально-потоковых параллельных вычислений, которая за счет использования асинхронных последовательных потоков обеспечивает представление динамически изменяющегося параллелизма. Рассмотрены особенности синтаксиса и семантики статически типизированного языка функционально-потокового параллельного программирования Smile, обеспечивающие поддержку асинхронных последовательных потоков. Основная идея подхода базируется на использовании концепции взаимодействующих последовательных процессов Т. Хоара применительно к управлению по готовности данных. Предполагается, что готовность данных сопровождается выдачей управляющих сигналов, информирующих процессы о свершении тех или иных событий. Отличительной особенностью подхода является включение в модель специальных асинхронных контейнеров, которые могут порождать события по частичному заполнению. Этими контейнерами являются поток и рой, каждый из которых имеет свою специфику. Поток используется для обработки данных одного типа, поступающих последовательно и асинхронно в произвольные промежутки времени. Размерность поступающих данных изначально неизвестна, поэтому завершение обработки осуществляется по признаку конца потока. Рой используется для описания независимых данных одного типа, над которыми возможно выполнение массовых параллельных операций. В отличие от потока, его размерность фиксирована и известна заранее. В работе описаны общие принципы организации асинхронных последовательных потоков с произвольным поступлением данных. Рассматривается использование потоков и роев в различных ситуациях. Предлагаются языковые конструкции, позволяющие описывать работу с роями и потоками и особенности их применения. Представлены примеры функций, при реализации которых использованы различные подходы к описанию параллелизма: рекурсивная обработка асинхронных потоков, обработка потоков при недетерминированном и упорядоченном выполнении операций, прямое и ссылочное обращение к элементам потоков и роев, конвейеризация вычислений. Дается предварительная оценка параллелизма в зависимости от временных соотношений между темпом поступления данных и скоростью их обработки. Предложенные методы могут быть использованы при разработке перспективных языковых и инструментальных средств архитектурно-независимого параллельного программирования
К вопросу об оценках распределения длин путей между узлами в глобальной сети
Get PDFThe experiment aimed at finding a distribution of path lengths between nodes in the global network and an estimation of parameters of that distribution is described.In particular, the method of measurement of path length with traceroute utility of the GNU/Linux system and limitations on the selection of nodes imposed by traceroute are described. e measurement results are provided and high values of skewness and kurtosis for all resulting distributions are noted. Simulation model of this experiment was developed to test the experiment validity in the determination of distribution parameters in the global network. This model is also described. It is shown that high values of skewness and kurtosis of the measured distributions are not the result of the measurement technique, therefore the global network could not be described by the Barabasi–Albert ´ model. Several most viable hypotheses explaining diffierences in skewness and kurtosis of experimentally obtained pathlength distribution estimations and values derived from the Barabasi–Albert model are listed. Results of diffierent hypotheses ´ simulations are provided. It is shown that the most fitting hypothesis is that definitive influence on skewness and kurtosis of path-length distribution estimations is caused by the quasi pre-fractal structure of the global network.Описан эксперимент по оцениванию распределения длин путей между узлами в глобальной сети и его характеристик. В частности, показана методика измерения длины пути при помощи утилиты GNU/Linux traceroute и ограничения выбора узлов, налагаемые этим инструментом. Приведены результаты измерений, отмечены высокие значения асимметрии и эксцесса для всех полученных распределений. Описана имитационная модель эксперимента, разработанная для проверки корректности полученных оценок распределения длин путей между узлами в глобальной сети. Приведены результаты моделирования измерений. Показано, что высокие значения асимметрии и эксцесса измеренных распределений не обусловлены только методикой измерения, таким образом, глобальная сеть не описывается моделью Барабаши—Альберт. Перечислены основные гипотезы о причинах отличия асимметрии и эксцесса полученных экспериментально оценок распределения длин путей между узлами в глобальной сети от значений, соответствующих модели Барабаши—Альберт. Описаны результаты моделирования различных гипотез. Показано, что наиболее правдоподобной из них является предположение об определяющем влиянии квазипредфрактальной структуры глобальной сети на асимметрию и эксцесс оценок распределения длин путей между узлами
О моделировании последовательных реагирующих систем при помощи автоматов, работающих в реальном времени
Get PDFSequential reactive systems include hardware devices and software programs which operate in continuous interaction with the external environment, from which they receive streams of input signals (data, commands) and in response to them form streams of output signals. Systems of this type include controllers, network switches, program interpreters, system drivers. The behavior of some reactive systems is determined not only by the sequence of values of input signals, but also by the time of their arrival at the inputs of the system and the delays in computing the output signals. These aspects of reactive system computations are taken into account by real-time models of computation which include, in particular, realtime finite state machines (TFSMs). However, in most works where this class of real-time automata is studied a simple variant of TFSM semantics is used: the transduction relation computed by a TFSM is defined so that the elements of an output stream, regardless oftheir timestamps, follow in the same order as the corresponding elements ofthe input stream. This straightforward approach makes the model easier to analyze and manipulate, but it misses many important features of real-time computation. In this paper we study a more realistic semantics of TFSMs and show how to represent it by means of Labeled Transition Systems. The use of the new TFSM model also requires new approaches to the solution of verification problems in the framework of this model. For this purpose, we propose an alternative definition of TFSM computations by means of Labeled Transition Systems and show that the two definitions of semantics for the considered class of real-time finite state machines are in good agreement with each other. The use of TFSM semantics based on Labeled Transition Systems opens up the possibility of adapting well known real-time model checking techniques to the verification ofsequential reactive systems.Последовательные реагирующие системы включают в себя устройства и программы, вычисления которых состоят в непрерывном взаимодействии с внешней средой, от которой они получают потоки входных сигналов (данных, команд) и в ответ на них формируют потоки выходных сигналов. К системам такого вида относятся контроллеры, сетевые коммутаторы, интерпретаторы программ, системные драйверы. Поведение некоторых реагирующих систем определяется не только последовательностью значений входных сигналов, но также временем их поступления на вход системы и задержками вычисления выходных сигналов. Эти особенности вычисления реагирующих систем хорошо учитываются вычислительными моделями реального времени, к числу которых относятся, в частности, конечные автоматы-преобразователи реального времени (Timed Finite State Machines, TFSMs). Однако в большинстве работ, посвященных изучению этой модели вычислений, используется упрощенная семантика TFSMs: элементы выходного потока, независимо от сопутствующих пометок времени, располагаются в том же порядке, в котором следуют соответствующие им элементы входного потока. Такое упрощение семантики делает модель менее адекватной для многих приложений, но зато облегчает решение задач анализа и преобразования таких автоматов. В данной статье мы изучаем модель TFSM с более реалистичной семантикой. Переход к новой модели TFSM требует и новых подходов к решению задачи верификации автоматов в этой модели. Для этой цели мы предлагаем альтернативное определение вычислений TFSM с использованием размеченных систем переходов и показываем, что два определения семантики для рассматриваемого класса автоматов реального времени хорошо взаимосвязаны друг с другом. Использование семантики TFSM, основанной на размеченных системах переходов, открывает возможность применения ранее известных методов верификации систем вычислений реального времени для анализа поведения последовательных реагирующих систем