Modeling and Analysis of Information Systems / Моделирование и анализ информационных систем (МАИС)
Not a member yet
782 research outputs found
Sort by
О верификации моделей и проверке выполнимости формул одного параметрического расширения темпоральной логики линейного времени
Get PDFSequential reactive systems are computer programs or hardware devices which process the flows of input data or control signals and output the streams of instructions or responses. When designing such systems one needs formal specification languages capable of expressing the relationships between the input and output flows. Previously, we introduced a family of such specification languages based on temporal logics , and combined with regular languages. A characteristic feature of these new extensions of conventional temporal logics is that temporal operators and basic predicates are parameterized by regular languages. In our early papers, we estimated the expressive power of the new temporal logic - and introduced a model checking algorithm for -, -, and -. The main issue which still remains unclear is the complexity of decision problems for these logics. In the paper, we give a complete solution to satisfiability checking and model checking problems for - and prove that both problems are Pspace-complete. The computational hardness of the problems under consideration is easily proved by reducing to them the intersection emptyness problem for the families of regular languages. The main result of the paper is an algorithm for reducing the satisfiability of checking - formulas to the emptiness problem for Buchi automata of relatively small size and a description of a technique that allows one to check the emptiness of the obtained automata within space polynomial of the size of input formulas.К последовательным реагирующим системам относятся компьютерные программы и вычислительные устройства, которые обрабатывают потоки входных данных или сигналов управления и генерируют на выходе последовательности команд или результатов вычислений. Для проектирования таких систем полезно иметь формальные языки спецификаций, способные выражать отношения между входными и выходными потоками данных. В предшествующих работах нами было предложено семейство таких языков спецификаций, представляющих собой расширение темпоральных логик , и за счет использования регулярных языков в качестве параметров темпоральных операторов. Мы провели сравнительный анализ выразительных возможностей нового расширения темпоральной логики линейного времени - и предложили алгоритмы верификации моделей для новых расширений логик -, -, и -. Однако вопрос о сложности задач верификации моделей и проверки выполнимости формул указанных логик оставался открытым. В этой статье мы восполняем этот пробел в наших исследованиях и показываем, что для темпоральной логики - обе задачи являются Pspace-полными. Вычислительная трудность рассматриваемых задач легко доказывается сведением к ним проблемы пустоты пересечения семейств регулярных языков. Основным результатом статьи является алгоритм сведения задачи проверки выполнимости формул логики - к проблеме пустоты автоматов Бюхи сравнительно небольшого размера и описание стратегии, позволяющей проверять пустоту полученных автоматов с использованием объема памяти, полиномального относительно размера исходных формул
Анализ влияния стилометрических характеристик разного уровня на верификацию авторов художественных произведений
Get PDFThis article is dedicated to the analysis of various stylometric characteristics combinations of different levels for the quality of verification of authorship of Russian, English and French prose texts. The research was carried out for both low-level stylometric characteristics based on words and symbols and higher-level structural characteristics.All stylometric characteristics were calculated automatically with the help of the ProseRhythmDetector program. This approach gave a possibility to analyze the works of a large volume and of many writers at the same time. During the work, vectors of stylometric characteristics of the level of symbols, words and structure were compared to each text. During the experiments, the sets of parameters of these three levels were combined with each other in all possible ways. The resulting vectors of stylometric characteristics were applied to the input of various classifiers to perform verification and identify the most appropriate classifier for solving the problem. The best results were obtained with the help of the AdaBoost classifier. The average F-score for all languages turned out to be more than 92 %. Detailed assessments of the quality of verification are given and analyzed for each author. Use of high-level stylometric characteristics, in particular, frequency of using N-grams of POS tags, offers the prospect of a more detailed analysis of the style of one or another author. The results of the experiments show that when the characteristics of the structure level are combined with the characteristics of the level of words and / or symbols, the most accurate results of verification of authorship for literary texts in Russian, English and French are obtained. Additionally, the authors were able to conclude about a different degree of impact of stylometric characteristics for the quality of verification of authorship for different languages.Данная статья посвящена анализу влияния различных комбинаций стилометрических характеристик разного уровня на качество верификации авторства русских, английских и французских прозаических текстов. Исследование проводилось как для низкоуровневых стилометрических характеристик, основанных на словах и символах, так и для более высокоуровневых – структурных.Подсчёт всех стилометрических характеристик был выполнен автоматически с помощью программы ProseRhythmDetector. Такой подход позволил провести анализ произведений большого объёма и многих писателей одновременно. В ходе работы каждому тексту были сопоставлены векторы стилометрических характеристик уровня символов, слов и структуры. При проведении экспериментов наборы параметров этих трёх уровней были скомбинированы между собой всеми возможными способами. Полученные векторы стилометрических характеристик были поданы на вход различным классификаторам для выполнения верификации и выявления наиболее подходящего классификатора для решения поставленной задачи. Лучшие результаты были получены с помощью классификатора AdaBoost. Средняя F-мера для всех языков оказалась более 92%. Детальные оценки качества верификации приведены для каждого автора и проанализированы. Использование высокоуровневых стилометрических характеристик, в частности, частоты использования N-грамм POS-тегов открывает перспективу более детального анализа стиля того или иного автора. Результаты экспериментов показывают, что при соединении характеристик уровня структуры с характеристиками уровня слов и/или символов получаются наиболее точные результаты верификации авторства для художественных текстов на русском, английском и французском языках. Дополнительно авторам удалось сделать вывод о разной степени влияния стилометрических характеристик на качество верификации авторства для различных языков
Исследование нелинейных полиномиальных систем управления
Get PDFThe paper considers methods for estimating stability using Lyapunov functions, which are used for nonlinear polynomial control systems. The apparatus of the Gro¨bner basis method is used to assess the stability of a dynamical system. A description of the Gro¨bner basis method is given. To apply the method, the canonical relations of the nonlinear system are approximated by polynomials of the components of the state and control vectors. To calculate the Gro¨bner basis, the Buchberger algorithm is used, which is implemented in symbolic computation programs for solving systems of nonlinear polynomial equations. The use of the Gro¨bner basis for finding solutions of a nonlinear system of polynomial equations is considered, similar to the application of the Gauss method for solving a system of linear equations. The equilibrium states of a nonlinear polynomial system are determined as solutions of a nonlinear system of polynomial equations. An example of determining the equilibrium states of a nonlinear polynomial system using the Gro¨bner basis method is given. An example of finding the critical points of a nonlinear polynomial system using the Gro¨bner basis method and the Wolfram Mathematica application software is given. The Wolfram Mathematica program uses the function of determining the reduced Gro¨bner basis. The application of the Gro¨bner basis method for estimating the attraction domain of a nonlinear dynamic system with respect to the equilibrium point is considered. To determine the scalar potential, the vector field of the dynamic system is decomposed into gradient and vortex components. For the gradient component, the scalar potential and the Lyapunov function in polynomial form are determined by applying the homotopy operator. The use of Gro¨bner bases in the gradient method for finding the Lyapunov function of a nonlinear dynamical system is considered. The coordination of input-output signals of the system based on the construction of Gro¨bner bases is considered.В работе рассматриваются методы оценивания устойчивости с помощью функций Ляпунова, применяемые для нелинейных полиномиальных систем управления. Для оценивания устойчивости используется аппарат метода базисов Грёбнера. Приводится описание метода базисов Грёбнера. Для применения метода канонические соотношении нелинейной системы аппроксимируются полиномами компонент векторов состоянии и управления. Для вычисления базиса Грёбнера применяется алгоритм Бухбергера, который реализован в программах символьных вычислений для решения систем нелинейных полиномиальных уравнений. Рассматривается использование базиса Грёбнера при нахождения решений нелинейной системы полиномиальных уравнений аналогично применению метода Гаусса для решения системы линейных уравнений. Определяются равновесные состояния нелинейной полиномиальной системы как решения нелинейной системы полиномиальных уравнений. Приводится пример определения равновесных состояний нелинейной полиномиальной системы с использованием метода базисов Грёбнера. Приводится пример нахождения критических точек нелинейной полиномиальной системы с использованием метода базисов Грёбнера и прикладного программного обеспечения Wolfram Mathematica. При использовании прикладного программного обеспечения Wolfram Mathematica применяется функция определения редуцированного базиса Грёбнера. Рассматривается применение метода базиса Грёбнера для оценивания области притяжения нелинейной динамической системы относительно точки равновесия. Для определения скалярного потенциала векторное поле динамической системы декомпозируется на градиентную и вихревую компоненты. По градиентному компоненту скалярный потенциал и функция Ляпунова в полиномиальной форме определяются на основе применения оператора гомотопии. Рассмотрено использование базисов Грёбнера при градиентном методе нахождения функции Ляпунова нелинейной динамической системы. Рассмотрено согласование сигналов ввода-вывода системы на основе построения базисов Грёбнера
Выделение условий разрешимости NP-полных задач для класса предфрактальных графов
Get PDFModern network systems (unmanned aerial vehicles groups, social networks, network production chains, transport and logistics networks, communication networks, cryptocurrency networks) are distinguished by their multi-element nature and the dynamics of connections between its elements. A number of discrete problems on the construction of optimal substructures of network systems described in the form of various classes of graphs are NP-complete problems. In this case, the variability and dynamism of the structures of network systems leads to an "additional" complication of the search for solutions to discrete optimization problems. At the same time, for some subclasses of dynamical graphs, which are used to model the structures of network systems, conditions for the solvability of a number of NP-complete problems can be distinguished. This subclass of dynamic graphs includes pre-fractal graphs. The article investigates NP-complete problems on pre-fractal graphs: a Hamiltonian cycle, a skeleton with the maximum number of pendant vertices, a monochromatic triangle, a clique, an independent set. The conditions under which for some problems it is possible to obtain an answer about the existence and to construct polynomial (when fixing the number of seed vertices) algorithms for finding solutions are identified.Современные сетевые системы (группы БПЛА, социальные сети, сетевые производственные цепочки, транспортно-логистические сети, сети связи, криптовалютные сети) отличаются многоэлементностью и динамикой связей между ее элементами. Ряд дискретных задач по построению оптимальных подструктур сетевых систем, описываемых в виде различных классов графов относятся к NP-полным задачам. При этом изменчивость и динамичность структур сетевых систем приводит к «дополнительному» усложнению поиска решения задач дискретной оптимизации. Вместе с тем для некоторых подклассов динамических графов, которыми моделируются структуры сетевых систем, можно выделить условия разрешимости ряда NP-полных задач. К такому подклассу динамических графов относятся предфрактальные графы. В статье исследованы NP-полные задачи на предфрактальных графах: гамильтонов цикл, остов с максимальным числом висячих вершин, монохроматический треугольник, клика, независимое множество. Выделены условия, при которых для некоторых задач возможно получить ответ о существовании и построить полиномиальные (при фиксировании числа вершин затравки) алгоритмы поиска решений
Алгоритмы поиска с возвратом для построения гамильтонова разложения 4-регулярного мультиграфа
Get PDFWe consider a Hamiltonian decomposition problem of partitioning a regular graph into edge-disjoint Hamiltonian cycles. It is known that verifying vertex non-adjacency in the 1-skeleton of the symmetric and asymmetric traveling salesperson polytopes is an NP-complete problem. On the other hand, a suffcient condition for two vertices to be non-adjacent can be formulated as a combinatorial problem of finding a Hamiltonian decomposition of a 4-regular multigraph. We present two backtracking algorithms for verifying vertex non-adjacency in the 1-skeleton of the traveling salesperson polytope and constructing a Hamiltonian decomposition: an algorithm based on a simple path extension and an algorithm based on the chain edge fixing procedure. Based on the results of the computational experiments for undirected multigraphs, both backtracking algorithms lost to the known heuristic general variable neighborhood search algorithm. However, for directed multigraphs, the algorithm based on chain fixing of edges showed comparable results with heuristics on instances with existing solutions, and better results on instances of the problem where the Hamiltonian decomposition does not exist.Рассматривается задача построения гамильтонова разложения регулярного мультиграфа на гамильтоновы циклы без общих рёбер. Известно, что проверка несмежности вершин в полиэдральных графах симметричного и асимметричного многогранников коммивояжёра является NP-полной задачей. С другой стороны, достаточное условие несмежности вершин можно сформулировать в виде комбинаторной задачи построения гамильтонова разложения 4-регулярного мультиграфа. В статье представлены два алгоритма поиска с возвратом для проверки несмежности вершин в полиэдральном графе коммивояжёра и построения гамильтонова разложения 4-регулярного мультиграфа: алгоритм на основе последовательного расширения простого пути и алгоритм на основе процедуры цепного фиксирования рёбер. По результатам вычислительных экспериментов для неориентированных мультиграфов оба переборных алгоритма проиграли известному эвристическому алгоритму поиска с переменными окрестностями. Однако для ориентированных мультиграфов алгоритм на основе цепного фиксирования рёбер показал сопоставимые результаты с эвристиками на экземплярах задачи, имеющих решение, и лучшие результаты на экземплярах задачи, для которых гамильтонова разложения не существует
Алгоритм оценивания частоты сигнала на выходе канала с управляемым информационным потоком в условиях фазового шума
Get PDFResearch in the field of efficient frequency estimation algorithms is of great interest. The reason for this is the redistribution of the role of additive and phase noise in many modern radio-engineering applications. An example is the area of measuring radio devices, which usually operate at high signal-to-noise ratios (SNR). The estimation error is largely determined not by the broadband noise, but by the frequency and phase noise of the local oscillators of the receiving and transmitting devices. In particular, earlier works \\cite{Nikiforov} proposed an efficient computational algorithm for estimating the frequency of a quasi-harmonic signal based on the iterative calculation of the autocorrelation sequence (ACS). In \\cite{Volkov}, this algorithm was improved and its proximity to the Rao-Cramer boundary was shown (the sources of this noise are master oscillators and frequency synthesizers). Possibilities of frequency estimation in radio channels make it possible to significantly expand the functionality of the entire radio network. This can include, for example, the problem of adaptive distribution of information flows of a radio network. This also includes the tasks of synchronization and coherent signal processing. For these reasons, more research is needed on this algorithm, the calculation of theoretical boundaries and their comparison with the simulation results.Большой интерес вызывают исследования в области эффективных алгоритмов оценивания частоты. Причиной этому является перераспределение во многих современных радиотехнических приложениях роли аддитивного и фазового шумов. Примером может служить область измерительных радиоприборов, работающих, как правило, при высоких отношениях сигнал/шум (ОСШ). Ошибка оценки в большей степени определяется не широкополосным шумом, а частотными и фазовыми шумами гетеродинов приемных и передающих устройств. В частности, в более ранних работах [1] предложен эффективный вычислительный алгоритм оценивания частоты квазигармонического сигнала, основанный на итерационном вычислении АКП. В [2] этот алгоритм доработан и показана его близость к границе Рао-Крамера (источниками этих шумов являются задающие генераторы и синтезаторы частоты). Возможности оценивания частоты в радиоканалах позволяют существенно расширить функционал всей радиосети. Сюда можно отнести, например, задачу адаптивного распределения информационных потоков радиосети. Сюда же можно отнести задачи синхронизации и когерентной обработки сигналов. По этим причинам необходимы дополнительные исследования этого алгоритма, расчет теоретических границ и их сравнение с результатами моделирования
Простой алгоритм отыскания неотрицательного базисного решения системы линейных алгебраических уравнений
Get PDFThis article describes an algorithm for obtaining a non-negative basic solution of a system of linear algebraic equations. This problem, which undoubtedly has an independent interest, in particular, is the most time-consuming part of the famous simplex method for solving linear programming problems.Unlike the artificial basis Orden’s method used in the classical simplex method, the proposed algorithm does not attract artificial variables and economically consumes computational resources.The algorithm consists of two stages, each of which is based on Gaussian exceptions. The first stage coincides with the main part of the Gaussian complete exclusion method, in which the matrix of the system is reduced to the form with an identity submatrix. The second stage is an iterative cycle, at each of the iterations of which, according to some rules, a resolving element is selected, and then a Gaussian elimination step is performed, preserving the matrix structure obtained at the first stage. The cycle ends either when the absence of non-negative solutions is established, or when one of them is found.Two rules for choosing a resolving element are given. The more primitive of them allows for ambiguity of choice and does not exclude looping (but in very rare cases). Use of the second rule ensures that there is no looping.В данной статье описывается алгоритм получения неотрицательного базисного решения системы линейных алгебраических уравнений. Эта задача, в частности, является наиболее трудоемким этапом знаменитого симплекс-метода решения задач линейного программирования, хотя бесспорно представляет и самостоятельный интерес. В отличии от метода искусственного базиса Ордена, применяемого в классическом симплекс-методе, предлагаемый алгоритм не использует искусственных переменных и экономно расходует вычислительные ресурсы.Алгоритм состоит из двух этапов, основу каждого из которых составляют Гауссовы исключения. Первый этап совпадает с основной частью метода полных исключений Гаусса, в котором матрица системы приводится к виду с единичной подматрицей. Второй этап представляет из себя итерационный цикл, на каждой из итераций которого по некоторым правилам выбирается разрешающий элемент, а затем выполняется шаг исключения Гаусса, сохраняющий структуру матрицы, полученную на первом этапе. Цикл завершается, либо когда будет установлено отсутствие неотрицательных решений, либо когда будет найдено одно из них.Приводятся два правила выбора разрешающего элемента. Более примитивное из них допускает неоднозначность выбора и не исключает зацикливания (но в очень редких случаях). Использование второго правила гарантирует отсутствие зацикливания
Трансформация функционально-потоковых параллельных программ в императивные
Get PDFFunctional dataflow programming languages are designed to create parallel portable programs. The source code of such programs is translated into a set of graphs that reflect information and control dependencies. The main way of their execution is interpretation, which does not allow to perform calculations efficiently on real parallel computing systems and leads to poor performance. To run programs directly on existing computing systems, you need to use specific optimization and transformation methods that take into account the features of both the programming language and the architecture of the system. Currently, the most common is the Von Neumann architecture, however, parallel programming for it in most cases is carried out using imperative languages with a static type system. For different architectures of parallel computing systems, there are various approaches to writing parallel programs. The transformation of dataflow parallel programs into imperative programs allows to form a framework of imperative code fragments that directly display sequential calculations. In the future, this framework can be adapted to a specific parallel architecture. The paper considers an approach to performing this type of transformation, which consists in allocating fragments of dataflow parallel programs as templates, which are subsequently replaced by equivalent fragments of imperative languages. The proposed transformation methods allow generating program code, to which various optimizing transformations can be applied in the future, including parallelization taking into account the target architecture.Функционально-потоковая парадигма параллельного программирования ориентирована на разработку параллельных переносимых программ. Исходный код функционально-потоковых программ транслируется в набор графов, отражающих информационные и управляющие зависимости. Основным способом их исполнения является интерпретация, что не позволяет эффективно выполнять вычисления на реальных параллельных вычислительных системах и ведет к низкой производительности. Для непосредственного выполнения программ на существующих вычислительных системах требуется использование специфических методов оптимизации и трансформации, учитывающих особенности как языка программирования, так и архитектуры исполнителя. В настоящее время наиболее распространенной является архитектура Фон-Неймана, параллельное программирование для которой в большинстве случаев осуществляется с использованием языков, поддерживающих императивный стиль и ориентированных на статическую систему типов. Для различных архитектур параллельных вычислительных систем существуют разнообразные подходы к написанию параллельных программ. Трансформация функционально-потоковых параллельных программ в императивные позволяет сформировать общий каркас из фрагментов императивного кода, непосредственно отображающих последовательные вычисления, который в дальнейшем может быть адаптирован к конкретной параллельной архитектуре. В работе рассматривается подход к выполнению такого типа трансформации, заключающийся в выделении фрагментов функционально-потоковых параллельных программ в качестве шаблонов, заменяемых впоследствии на эквивалентные фрагменты императивных языков. Предлагаемые методы трансформации позволяют порождать программный код, к которому в дальнейшем можно применять различные оптимизирующие преобразования, включая распараллеливание с учетом целевой архитектуры
О характеристиках символьного исполнения в задаче оценки качества обфусцирующих преобразований
Get PDFObfuscation is used to protect programs from analysis and reverse engineering. There are theoretically effective and resistant obfuscation methods, but most of them are not implemented in practice yet. The main reasons are large overhead for the execution of obfuscated code and the limitation of application only to a specific class of programs. On the other hand, a large number of obfuscation methods have been developed that are applied in practice. The existing approaches to the assessment of such obfuscation methods are based mainly on the static characteristics of programs. Therefore, the comprehensive (taking into account the dynamic characteristics of programs) justification of their effectiveness and resistance is a relevant task. It seems that such a justification can be made using machine learning methods, based on feature vectors that describe both static and dynamic characteristics of programs. In this paper, it is proposed to build such a vector on the basis of characteristics of two compared programs: the original and obfuscated, original and deobfuscated, obfuscated and deobfuscated. In order to obtain the dynamic characteristics of the program, a scheme based on a symbolic execution is constructed and presented in this paper. The choice of the symbolic execution is justified by the fact that such characteristics can describe the difficulty of comprehension of the program in dynamic analysis. The paper proposes two implementations of the scheme: extended and simplified. The extended scheme is closer to the process of analyzing a program by an analyst, since it includes the steps of disassembly and translation into intermediate code, while in the simplified scheme these steps are excluded. In order to identify the characteristics of symbolic execution that are suitable for assessing the effectiveness and resistance of obfuscation based on machine learning methods, experiments with the developed schemes were carried out. Based on the obtained results, a set of suitable characteristics is determined.Обфускация применяется для защиты программ от анализа и обратного проектирования. Несмотря на то, что в настоящее время существуют теоретически стойкие методы обфускации, эти методы пока не могут применяться на практике. В основном это связано либо с затратностью по ресурсам на исполнение обфусцированного кода, либо с ограничением на применение только к конкретному классу программ. С другой стороны, разработано большое количество методов обфускации, которые применяются на практике. Существующие подходы к оценке таких обфусцирующих преобразований в большей степени основаны на статических характеристиках программ. Однако актуальна задача комплексного (учитывающего и динамические характеристики программ) обоснования их эффективности и стойкости. Представляется, что такое обоснование может быть выполнено с помощью методов машинного обучения на основе векторов признаков, описывающих как статические, так и динамические характеристики программ. В настоящей работе такой вектор предлагается строить на основе характеристик пар сравниваемых программ: исходной и обфусцированной, исходной и деобфусцированной, обфусцированной и деобфусцированной. Для получения динамических характеристик программы в работе построена схема, основанная на символьном исполнении. Выбор символьного исполнения обосновывается тем, что такие характеристики могут описать сложность понимания программы при динамическом анализе. В работе предлагается две реализации схемы: расширенная и упрощенная. Расширенная схема приближена к процессу анализа программы аналитиком, так как включает в себя этапы дизассемблирования и трансляции в промежуточный код, в то время как в упрощенной схеме эти этапы исключены. С разработанными схемами проведены эксперименты с целью выявления характеристик символьного исполнения, подходящих для оценки эффективности и стойкости обфускации на основе методов машинного обучения. На основе полученных результатов определен набор подходящих характеристик