?
Petri nets behavioral equivalence checking in SMV
.
Drozdov D., Dubinin V., Кулагин В. П.
This paper proposes an approach to k-bounded Petri nets behavioral equivalence checking using the model checking method and mainstream verifier nuSMV. For the comparison of behavior of two nets, an add-in net is introduced which performs a supervisory control of these two nets. The approach uses an implicit word-to-word comparison of labeled Petri net languages with invisible transitions when computing CTL temporal logic formulas. The technique of Petri nets equivalence checking in SMV is briefly discussed followed by a simple case study.
В книге
M. : HSE, 2016
Berlin : Springer, 2014
This book constitutes the proceedings of the 35th International Conference on Application and Theory of Petri Nets and Concurrency, PETRI NETS 2014, held in Tunis, Tunisia, in June 2014. The 15 regular papers and 4 tool papers presented in this volume were carefully reviewed and selected from 48 submissions. In addition the book contains 3 ...
Добавлено: 3 июля 2014 г.
Switzerland : Springer, 2017
This book constitutes the proceedings of the 38th International Conference on Application and Theory of Petri Nets and Concurrency, PETRI NETS 2017, held in Zaragoza, Spain, in June 2017. Petri Nets 2017 is co-located with the Application of Concurrency to System Design Conference, ACSD 2017.
The 16 papers, 9 theory papers, 4 application papers, and 3 tool papers, ...
Добавлено: 6 мая 2017 г.
-, 2016
The issue contains papers accepted for presentation at the 10th Spring/Summer Young Researchers’ Colloquium on Software Engineering (SYRCoSE 2016) held in Krasnovidovo, Mozhaysky District, Moscow Oblast, Russia on May 30-June 1, 2016. The paper selection was based on originality and contributions to the field. Each paper was peer-reviewed by at least three referees.
The colloquium’s topics ...
Добавлено: 5 июня 2016 г.
Дворянский Л. В., Михайлов В. Е., Proceedings of the Institute for System Programming of the RAS 2017 Vol. 29 No. 4 P. 175-190
Вполне структурированные системы переходов являются хорошо известным инструментом для доказательства разрешимости свойств покрываемости и ограниченности. Каждый год появляются новые формализмы, которые оказываются вполне структурированными системами переходов. Несмотря на большой объем теоретической работы, существует большая потребность в эмпирических изучении вполне структурированных систем переходов. В данной работе представлен инструмент для анализа таких систем. Мы предлагаем расширение высокоуровневого ...
Добавлено: 1 октября 2017 г.
Захаров В. А., Винарский Е. М., В кн. : Материалы XIII Международного семинара "Дискретная математика и ее приложения" имени академика О.Б. Лупанова (Москва, МГУ, 17-22 июня 2019). : М. : Изд-во механико-математического факультета МГУ, 2019. С. 257-260.
Конечные автоматы Мили, представляющие собой простейшую математическую модель преобразования потоковых данных, широко используются во многих областях информатики. Но для некоторых приложений большое значение имеют не только значения обрабатываемых данных и порядок их следования, но также интервалы времени, которые отделяют события, присходящие по ходу вычисления автомата. Такие свойства уже не описывается явно средствами классической теории конечных ...
Добавлено: 17 октября 2019 г.
Ломазова И. А., Popova-Zeugmann L., Fundamenta Informaticae 2016 Vol. 143 No. 1-2 P. 101-112
Добавлено: 12 октября 2015 г.
Vladimir A. Bashkin, Ломазова И. А., Fundamenta Informaticae 2012 Vol. 120 No. 3-4 P. 243-257
Автоматы, управляемые ресурсами, (RDA) представляют собой конечные автоматы, которые располагаются в узлах конечной системной сети и асинхронно потребляют/производят через порты (дуги системной сети) некоторые общие ресурсы. При этом RDA сами могут служить ресурсами друг для друга, что делает модель весьма гибкой. Ранее было доказано, что RDA-сети эквивалентны по выразительности сетям Петри.
В этой работе вводится новый ...
Добавлено: 28 ноября 2012 г.
Bouajjani A., Monniaux D., Cham : Springer, 2016
This book constitutes the refereed proceedings of the 18th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2017, held in Paris, France, in January 2017. The 27 full papers together with 3 invited keynotes presented were carefully reviewed and selected from 60 submissions. VMCAI provides topics including: program verification, model checking, abstract interpretation ...
Добавлено: 29 марта 2017 г.
K.G. Serebrennikov, Proceedings of the Institute for System Programming of the RAS 2019 Vol. 31 No. 4 P. 163-174
Добавлено: 24 октября 2019 г.
Ломазова И. А., Романов И. В., , in : Concurrency, Specification and Programming. CS&P’2012. Berlin, September 26 – September 28, 2012. Volume 2. Vol. 2. Issue 225.: Berlin : Humboldt University of Berlin, 2012. P. 239-250.
Работа посвящена моделированию сервисов с помощью модулей потоков работ, которые представляют собой специальный подкласс сетей Петри. Проблема совместимости сервисов состоит в проверке того, что два Веб-сервиса подходят друг другу, т.е. что их композиция является бездефектной. Исследуется задача проверки комплиментарности ресурсов производимых/потребляемых сервисами, что является необходимым условием совместимости сервисов. Ресурсы, производимые/потребляемые сервисами, описываются как языки мультимножеств. ...
Добавлено: 19 ноября 2012 г.
Кулагин В. П., Информатизация образования и науки 2015 № 4(28) С. 133-147
В статье рассматриваются методы построения тензоров преобразования (ТП), применяемых при анализе и синтезе сетевых моделей сложных систем, представленных в различных системах координат. Рассмотрен общий метод построения ТП, а также метод построения ТП для сетевых моделей, представленных множеством автоматно- синхронизационных сетей и в виде примитивной системы. Показано, что сложность предложенных методов построения ТП линейна и определяется ...
Добавлено: 25 февраля 2016 г.
Карраскель Г. Х., Ломазова И. А., Rivkin A., , in : Proceedings of the International Workshop on Petri Nets and Software Engineering co-located with 41st International Conference on Application and Theory of Petri Nets and Concurrency (PETRI NETS 2020). Vol. 2651: CEUR Workshop Proceedings.: CEUR-WS.org, 2020. P. 118-137.
Добавлено: 19 октября 2020 г.
Vladimir A. Bashkin, Ломазова И. А., Novikova Y., , in : Parallel Computing Technologies. 12th International Conference, PaCT 2013, St. Petersburg, Russia, September 30-October 4, 2013, Proceedings. Vol. 7979: Lecture Notes in Computer Science.: Berlin, Heidelberg : Springer, 2013. P. 13-25.
The paper presents a formalism and a tool for modelling and analysis of distributed real-time systems of mobile agents. For that we use a time extension of our Resource Driven Automata Nets (TRDA-nets) formalism. A TRDA-net is a two-level system. The upper level represents distributed environment locations with a net of active resources. On the ...
Добавлено: 1 октября 2013 г.
Мицюк А. А., Ломазова И. А., ван дер Аалст В., Automatic Control and Computer Sciences 2017 Vol. 51 No. 7 P. 709-723
Добавлено: 1 декабря 2017 г.
Dordrecht, L., Heidelberg, NY : Springer, 2013
This volume constitutes the proceedings of the 34th International Conference on Application and Theory of Petri Nets and Concurrency (PETRI NETS 2013). The Petri Net conferences serve as annual meeting places to discuss the progress in the field of Petri nets and related models of concurrency. They provide a forum for researchers to present and discuss both applications and ...
Добавлено: 3 ноября 2013 г.
Гнатенко А. Р., Захаров В. А., В кн. : Дискретные модели в теории управляющих систем: Х Международная конференция, Москва и Подмосковье, 23-25 мая 2018 г. : Труды. : МГУ, МАКС Пресс, 2018. С. 131-133.
Проведено сравнение выразительных возможностей темпоральной логики LP-CTL*. В этой логике были выделены два класса формул (фрагмента) LP-1-LTL и LP-n-LTL и показано, что фрагмент LP-1-LTL превосходит по выразительным возможностям известную темпоральную логику линейного времени LTL, а фрагмент LP-n-LTL имеет такие же выразительные возможности, что и монадическая логика второго порядка с одной функцией следования S1S. ...
Добавлено: 14 июня 2018 г.
Ломазова И. А., Popova-Zeugmann L., Bartels A., , in : International Conference on Control, Decision and Information Technologies, CoDIT 2017, Barcelona, Spain, April 5-7, 2017. : IEEE, 2017. P. 0236-0241.
Добавлено: 10 ноября 2017 г.
Петровский Д. В., Кокурин Д. И., Логистика и управление цепями поставок 2017 № 6 С. 125-132
В данной статье рассматривается применение аппарата стохастических сетей Петри при анализе цепей поставок. Основным анализируемым объектом являлся складской модуль и модуль производства, и их взаимодействие с другими элементами системы. Изучаемая логистическая система была представлена в виде стохастической сети Петри, затем были созданы две модели одной системы с разными начальными характеристиками с целью их дальнейшего сравнения. ...
Добавлено: 28 ноября 2017 г.
Гнатенко А. Р., Захаров В. А., Proceedings of the Institute for System Programming of the RAS 2018 Vol. 30 No. 3 P. 303-324
Добавлено: 14 июня 2018 г.
Ломазова И. А., , in : Application and Theory of Petri Nets and Concurrency. 38th International Conference, PETRI NETS 2017, Zaragoza, Spain, June 25–30, 2017, Proceedings. Vol. 10258: Lecture Notes in Computer Science.: Switzerland : Springer, 2017. P. 19-34.
Добавлено: 6 мая 2017 г.
Ломазова И. А., Romanov I., Fundamenta Informaticae 2013 Vol. 128 No. 1-2 P. 129-141
In this work we consider modeling of services with workflow modules, which form a Petri net subclass. The service compatibility problem is to answer the question, whether two services fit together, i.e. whether the composed system is correct. We study complementarity of resources, produced/consumed by two services—a necessary condition for the service compatibility. Resources, which ...
Добавлено: 18 ноября 2013 г.
Дворянский Л. В., Formal Methods in System Design (Нидерланды, целевой журнал) 2020
Вложенные сети Петри (NP-сети) - это формализм, удобный для моделирования систем, которые состоят из распределенных мобильных агентов с индивидуальным поведением. Выразительность формализма NP-сетей больше, чем у классических сетей Петри. Формализм позволяет моделировать открытые многоагентные системы с появлением, исчезновением, и клонированием агентов.
Несколько методов проверки, основанных на структурном анализе и методах проверки моделей, были
разработан для формализма. Но один из основных методов ...
Добавлено: 2 ноября 2019 г.
Мицюк А. А., Шугуров И. С., Моделирование и анализ информационных систем 2014 Т. 21 № 4 С. 181-198
Извлечение процессов (process mining) -- новая и активно развивающаяся область исследований, тесно связанная с управлением процессами, формальными моделями процессов и извлечением данных (data mining). Одна из основных задач извлечения процессов -- синтез (извлечение) модели процесса на основании анализа журнала событий. Разработан широкий спектр алгоритмов для извлечения, анализа и усовершенствования моделей процессов. Журналы событий реальных систем ...
Добавлено: 20 октября 2014 г.
Кулагин В. П., Перспективы науки и образования 2013 № 6 С. 26-30
Раскрываются формирования информационных ресурсов на основе параллельных вычислений. Раскрыта проблема семантического разрыва. Отмечен антропологический подход оценки производительности вычислительных систем. Показана целесообразность применения тензорных методов и сетей Петри для формирования информационных ресурсов. ...
Добавлено: 26 марта 2015 г.