О ПРИМЕНЕНИИ ИСЧИСЛЕНИЯ ПОЗИТИВНО-ОБРАЗОВАННЫХ ФОРМУЛ ДЛЯ ИССЛЕДОВАНИЯ УПРАВЛЯЕМЫХ ДИСКРЕТНО-СОБЫТИЙНЫХ СИСТЕМ (2024)
Статья посвящена разработке подхода к решению основных задач теории супервизорного управления логическими дискретно-событийными системами (ДСС), основанного на представлении их в виде позитивно-образованных формул (ПОФ). Рассматриваются логические ДСС в автоматной форме, понимаемые как генераторы некоторых регулярных языков. Язык ПОФ представляет собой полный язык первого порядка, формулы которого имеют регулярную структуру из чередующихся типовых кванторов и не содержат в синтаксисе оператора отрицания. Ранее было доказано, что любая формула классического исчисления предикатов первого порядка может быть представлена в виде ПОФ. ПОФ имеют наглядное древовидное представление и естественную вопросно-ответную процедуру поиска вывода с помощью единственного правила вывода. Показано, как разработанное в 1990-х годах для решения некоторых задач управления динамическими системами исчисление ПОФ позволяет решать базовые задачи теории супервизорного управления, такие как проверка критериев существования супервизорного управления, автоматическая модификация ограничений на поведение управляемой системы и реализация супервизора. Благодаря некоторым особенностям исчисления ПОФ существует возможность применения немонотонного вывода. Продемонстрировано, как представленный метод на основе ПОФ позволяет выполнять дополнительную обработку событий во время логического вывода. Также представлена программная система Bootfrost, или так называемый прувер, разработанный для опровержения полученных ПОФ, кратко описываются особенности его реализации. В качестве иллюстративного примера рассматривается задача управления автономным мобильным роботом.
Идентификаторы и классификаторы
- eLIBRARY ID
- 63159423
Класс дискретно-событийных систем (ДСС) — это широкий класс моделей, как правило, используемых для представления сложных технических и технологических систем, таких как производственные и сборочные процессы, коммуникационные протоколы, транспортные системы, системы управления базами данных, в которых смена дискретных состояний системы происходит вследствие возникновения некоторых дискретных событий [1—3].
Для описания таких систем используются различные формализмы, которые могут включать или не включать явное указание времени, например, конечные автоматы, сети Петри, диоидные алгебры, темпоральные логики и др. Если важна только последовательность событий, а не время их возникновения и длительность, говорят о логических ДСС. Два формализма наиболее часто применяются для исследования логических ДСС: конечные автоматы, являющиеся самыми наглядными моделями, подверженными, однако, проклятию размерности, и сети Петри, обладающие компактностью представления и достаточной выразительностью.
Список литературы
-
S. Lafortune, “Discrete event systems: Modeling, observation, and control”, Annual Review of Control, Robotics, and Autonomous Systems, vol. 2, pp. 141-159, 2019,. DOI: 10.1146/annurev-control-053018-023659
-
C. Seatzu, M. Silva, and J. H. Van Schuppen, Eds., Control of discrete-event systems. Springer London, 2013.
-
W. M. Wonham and K. Cai, Supervisory Control of Discrete-Event Systems. Springer International Publishing, 2019.
-
P. J. Ramadge and W. M. Wonham, “Supervisory control of a class of discrete event processes”, SIAM Journal on Control and Optimization, vol. 25, no. 1, pp. 206-230, 1987,. DOI: 10.1137/0325013
-
C. G. Cassandras and S. Lafortune, Introduction to Discrete Event Systems. Springer Cham, 2021.
-
W. M. Wonham, K. Cai, and K. Rudie, “Supervisory control of discrete-event systems: A brief history”, Annual Reviews in Control, vol. 45, pp. 250-256, 2018,. DOI: 10.1016/j.arcontrol.2018.03.002
-
A. Jayasiri, G. K. Mann, and R. G. Gosine, “Behavior coordination of mobile robotics using supervisory control of fuzzy discrete event systems”, IEEE Transactions on Systems, Man, and Cybernetics, Part B (Cybernetics), vol. 41, no. 5, pp. 1224-1238, 2011.
-
C. R. C. Torrico, A. B. Leal, and A. T. Y. Watanabe, “Modeling and Supervisory Control of Mobile Robots: A Case of a Sumo Robot”, IFAC-Papers OnLine, vol. 49, no. 32, pp. 240-245, 2016.
-
X. Dai, L. Jiang, and Y. Zhao, “Cooperative exploration based on supervisory control of multi-robot systems”, Applied Intelligence, vol. 45, no. 1, pp. 18-29, 2016. EDN: ICBFQW
-
A. Tsalatsanis, A. Yalcin, and K. P. Valavanis, "Dynamic task allocation in cooperative robot teams", Robotica, vol. 30, no. 5, pp. 721-730, 2012,. DOI: 10.1017/S0263574711000920 EDN: RQYRUP -
R. C. Hill and S. Lafortune, "Scaling the formal synthesis of supervisory control software for multiple robot systems", in 2017 American Control Conference (ACC), 2017, pp. 3840-3847,. DOI: 10.23919/ACC.2017.7963543 -
G. W. Gamage, G. K. I. Mann, and R. G. Gosine, "Discrete Event Systems Based Formation Control Framework to Coordinate Multiple Nonholonomic Mobile Robots", in Proceedings of the 2009 IEEE RSJ International Conference on Intelligent Robots and Systems, 2009, pp. 4831-4836. -
Y. K. Lopes, S. M. Trenkwalder, A. B. Leal, T. J. Dodd, and R. Gro\ss, "Supervisory control theory applied to swarm robotics", Swarm Intelligence, vol. 10, no. 1, pp. 65-97, 2016. EDN: JRJBQL -
F. J. Mendiburu, M. R. A. Morais, and A. M. N. Lima, "Behavior coordination in multi-robot systems", in 2016 IEEE International Conference on Automatica (ICA-ACCA), 2016, pp. 1-7. -
T. Hales et al., "A formal proof of the Kepler conjecture", in Forum of mathematics, Pi, 2017, vol. 5, p. e2,. DOI: 10.1017/fmp.2017.1 -
G. Klein et al., "seL4: Formal verification of an OS kernel", in Proceedings of the ACM SIGOPS 22nd symposium on Operating systems principles, 2009, pp. 207-220. -
G. Gonthier and others, "Formal proof-the four-color theorem", Notices of the AMS, vol. 55, no. 11, pp. 1382-1393, 2008. -
X. Leroy, "Formal verification of a realistic compiler", Communications of the ACM, vol. 52, no. 7, pp. 107-115, 2009. -
D. A. Kondratyev and A. V. Promsky, "The Complex Approach of the C-lightVer System to the Automated Error Localization in C-Programs", Automatic Control and Computer Sciences, vol. 54, no. 7, pp. 728-739, 2020,. DOI: 10.3103/S0146411620070093 EDN: OQPQSY -
J. S. Moore, "Milestones from the Pure Lisp theorem prover to ACL2", Formal Aspects of Computing, vol. 31, no. 6, pp. 699-732, 2019,. DOI: 10.1007/s00165-019-00490-3 -
E. Karpas and D. Magazzeni, "Automated planning for robotics", Annual Review of Control, Robotics, and Autonomous Systems, vol. 3, pp. 417-439, 2020. -
Z. Zombori, J. Urban, and C. E. Brown, "Prolog technology reinforcement learning prover", in International Joint Conference on Automated Reasoning, 2020, pp. 489-507. -
M. Schader and S. Luke, "Planner-Guided Robot Swarms", in International Conference on Practical Applications of Agents and Multi-Agent Systems, 2020, pp. 224-237. -
W. Li, A. Miyazawa, P. Ribeiro, A. Cavalcanti, J. Woodcock, and J. Timmis, "From formalised state machines to implementations of robotic controllers", in Distributed Autonomous Robotic Systems: the 13th International Symposium, 2018, pp. 517-529. -
S. N. Vassilyev, "Machine synthesis of mathematical theorems", The Journal of Logic Programming, vol. 9, no. 2-3, pp. 235-266, 1990,. DOI: 10.1016/0743-1066(90)90042-4 -
A. K. Zherlov, S. N. Vassilyev, E. A. Fedosov, and B. E. Fedunov, Intelligent control of dynamic systems. Fizmatlit, 2000. -
S. N. Vassilyev and G. M. Ponomarev, "Automation methods for logical derivation and their application in the control of dynamic and intelligent systems", Proceedings of the Steklov Institute of Mathematics, vol. 276, pp. 161-179, 2012. -
S. N. Vassilyev and A. A. Galyaev, "Logical-optimization approach to pursuit problems for a group of targets", Doklady Mathematics, vol. 95, no. 3, pp. 299-304, 2017. EDN: XNVVXF -
F. F. H. Reijnen, T. R. Erens, J. M. van de Mortel-Fronczak, and J. E. Rooda, "Supervisory controller synthesis and implementation for safety PLCs", Discrete Event Dynamic Systems, vol. 32, no. 1, pp. 115-141, 2022. EDN: KKKGRC -
D. Bohlender and S. Kowalewski, "Compositional Verification of PLC Software using Horn Clauses and Mode Abstraction", IFAC-PapersOnLine, vol. 51, pp. 428-433, Jan. 2018,. DOI: 10.1016/j.ifacol.2018.06.336 -
D. Bohlender and S. Kowalewski, "Leveraging Horn clause solving for compositional verification of PLC software", Discrete Event Dynamic Systems, vol. 30, no. 1, pp. 1-24, 2020,. DOI: 10.1007/s10626-019-00296-8 -
N. Bj\orner and L. Nachmanson, "Navigating the Universe of Z3 Theory Solvers", in Formal Methods: Foundations and Applications, 2020, pp. 8-24,. DOI: 10.1007/978-3-030-63882-5_2 -
A. D. Vieira, E. A. P. Santos, M. H. de Queiroz, A. B. Leal, A. D. de Paula Neto, and J. E. R. Cury, "A Method for PLC Implementation of Supervisory Control of Discrete Event Systems", IEEE Transactions on Control Systems Technology, vol. 25, no. 1, pp. 175-191, 2017,. DOI: 10.1109/TCST.2016.2544702 -
J. G. Thistle and W. M. Wonham, "Control problems in a temporal logic framework", International Journal of Control, vol. 44, no. 4, pp. 943-976, 1986,. DOI: 10.1080/00207178608933645 -
B. C. Rawlings, S. Lafortune, and B. E. Ydstie, "Supervisory Control of Labeled Transition Systems Subject to Multiple Reachability Requirements via Symbolic Model Checking", IEEE Transactions on Control Systems Technology, vol. 28, no. 2, pp. 644-652, 2020,. DOI: 10.1109/TCST.2018.2877621 -
K. T. Seow, "Supervisory Control of Fair Discrete-Event Systems: A Canonical Temporal Logic Foundation", IEEE Transactions on Automatic Control, vol. 66, no. 11, pp. 5269-5282, 2021,. DOI: 10.1109/TAC.2020.3037156 EDN: CVTFTG -
S. Jiang and R. Kumar, "Supervisory Control of Discrete Event Systems with CTL* Temporal Logic Specifications", SIAM Journal on Control and Optimization, vol. 44, no. 6, pp. 2079-2103, 2006,. DOI: 10.1137/S0363012902409982 -
G. Aucher, "Supervisory Control Theory in Epistemic Temporal Logic", in Proceedings of the 2014 international conference on Autonomous agents and multi-agent systems, 2014, pp. 333-340. -
K. Ritsuka and K. Rudie, "Do what you know: coupling knowledge with action in discrete-event systems", Discrete Event Dynamic Systems, vol. 33, pp. 257-277, 2023,. DOI: 10.1007/s10626-023-00381-z -
X. Geng, D. Ouyang, and C. Han, "Verifying Diagnosability of Discrete Event System with Logical Formula", Chinese Journal of Electronics, vol. 29, pp. 304-311, 2020,. DOI: 10.1049/cje.2020.01.008 -
L. Feng and W. M. Wonham, "TCT: A computation tool for supervisory control synthesis", in Proceedings of the 8th International Workshop on Discrete Event Systems, 2006, pp. 388-389. -
L. Ricker, S. Lafortune, and S. Genc, "DESUMA: A Tool Integrating GIDDES and UMDES", in 2006 8th International Workshop on Discrete Event Systems, 2006, pp. 392-393,. DOI: 10.1109/WODES.2006.382402 -
R. Malik, K. \AAkesson, H. Flordal, and M. Fabian, "Supremica - An Efficient Tool for Large-Scale Discrete Event Systems", IFAC-PapersOnLine, vol. 50, no. 1, pp. 5794-5799, 2017,. DOI: 10.1016/j.ifacol.2017.08.427 -
K. \AAkesson, H. Flordal, and M. Fabian, "Exploiting modularity for synthesis and verification of supervisors", IFAC Proceedings Volumes, vol. 35, no. 1, pp. 175-180, 2002. -
B. A. Brandin, R. Malik, and P. Malik, "Incremental verification and synthesis of discrete-event systems guided by counter examples", IEEE Transactions on Control Systems Technology, vol. 12, no. 3, pp. 387-401, 2004. -
S. Mohajerani, R. Malik, and M. Fabian, "A framework for compositional synthesis of modular nonblocking supervisors", IEEE Transactions on Automatic Control, vol. 59, no. 1, pp. 150-162, 2013. -
N. Bourbaki, Theory of Sets. Hermann, 1968. -
A. Larionov, A. Davydov, and E. Cherkashin, "The method for translating first-order logic formulas into positively constructed formulas", Software & Systems, vol. 32, no. 4, pp. 556-564, 2019,. DOI: 10.15827/0236-235X.128.556-564 -
A. Davydov, A. Larionov, and E. Cherkashin, "On the calculus of positively constructed formulas for automated theorem proving", Automatic Control and Computer Sciences, vol. 45, no. 7, pp. 402-407, 2011,. DOI: 10.3103/s0146411611070054 EDN: PEQNGP -
S. Ulyanov, I. Bychkov, and N. Maksimkin, "Event-Based Path-Planning and Path-Following in Unknown Environments for Underactuated Autonomous Underwater Vehicles", Applied Sciences, vol. 10, no. 21, p. 7894, 2020,. DOI: 10.3390/app10217894 EDN: THDUVN
Выпуск
Другие статьи выпуска
В статье рассматриваются неориентированные кратные графы произвольной натуральной кратности k>1. Кратный граф содержит ребра трех типов: обычные, кратные и мультиребра. Ребра последних двух типов представляют собой объединение k связанных ребер, которые соединяют 2 или (k+1) вершину соответственно. Связанные ребра могут использоваться только согласованно. Если вершина инцидентна кратному ребру, то она может быть инцидентна другим кратным ребрам, а также она может быть общим концом k связанных ребер мультиребра. Если вершина является общим концом мультиребра, то она не может быть общим концом никакого другого мультиребра. Рассматривается задача об эйлеровом маршруте (цикле или цепи) в кратном графе, которая обобщает классическую задачу для обычного графа. Доказывается, что задача о кратном эйлеровом маршруте в варианте распознавания является NP-полной. Для этого предварительно обосновывается NP-полнота вспомогательной задачи о покрывающих цепях с заданными концами в обычном графе.
В работе исследуются автоматические методы классификации русскоязычных предложений на два класса: содержащие и не содержащие ироничный посыл. Рассматриваемые методы могут быть разделены на три категории: классификаторы на основе эмбеддингов языковых моделей, классификаторы с использованием информации о тональности и классификаторы с обучением эмбеддингов обнаружению иронии. Составными элементами классификаторов являются нейронные сети, такие как BERT, RoBERTa, BiLSTM, CNN, а также механизм внимания и полносвязные слои. Эксперименты по обнаружению иронии проводились с использованием двух корпусов русскоязычных предложений: первый корпус составлен из публицистических текстов из открытого корпуса OpenCorpora, второй корпус является расширением первого и дополнен ироничными предложениями с ресурса Wiktionary. Лучшие результаты продемонстрировала группа классификаторов на основе чистых эмбеддингов языковых моделей с максимальным значением F-меры 0.84, достигнутым связкой из RoBERTa, BiLSTM, механизма внимания и пары полносвязных слоев в ходе экспериментов на расширенном корпусе. В целом использование расширенного корпуса давало результаты на 2-5% выше результатов на базовом корпусе. Достигнутые результаты являются лучшими для рассматриваемой задачи в случае русского языка и сравнимы с лучшими для английского.
В статье рассматривается теория и алгоритмы, необходимые для построения минимального покрытия обобщенных типизированных зависимостей включения. Традиционно аппарат построения минимальных покрытий используется для всех видов зависимостей с целью получения не избыточного и непротиворечивого проекта базы данных. Обобщенные зависимости включения соответствуют ссылочным ограничениям целостности, когда в одном ограничении участвуют несколько главных и несколько внешних отношений, что соответствует ребру ультраграфа. В предыдущей работе на основе исследования свойств зависимостей представлена система аксиом с доказательством непротиворечивости и полноты. В данной работе проведены исследования замыканий для обобщенных типизированных зависимостей включения. Разработан алгоритм построения замыканий, доказана его корректность. Полученные результаты далее используются для разработки алгоритма построения минимального покрытия. В конце статьи представлены примеры, которые демонстрируют работу алгоритмов.
Процесс-ориентированное программирование - один из подходов к разработке управляющего программного обеспечения. Процесс-ориентированная программа определяется как последовательность процессов. Каждый процесс представляется набором именованных состояний, содержащих программный код, которые задают логику поведения процесса. Выполнение программы заключается в последовательном исполнении этих процессов в их текущих состояниях на каждой итерации цикла управления. Процессы могут взаимодействовать через изменение состояний друг друга и через разделяемые переменные. Статья является развитием метода классификации темпоральных требований к процесс-ориентированным программам с целью упростить и автоматизировать дедуктивную верификацию таких программ. Метод состоит из следующих шагов. На первом шаге требования формализуются на специализированном языке DV-TRL, варианте типизированной логики предикатов первого порядка с набором интерпретированных типов и предикатных и функциональных символов, позволяющем отражать специфические понятия систем управления в процесс-ориентированной парадигме. На втором шаге формализованные требования разбиваются на классы, каждый из которых определяется шаблоном - параметрической формулой языка DV-TRL, причем условия корректности, порождаемые для процесс-ориентированных программ относительно требований, удовлетворяющих одному шаблону, имеют одну и ту же схему доказательства. На третьем шаге разрабатываются соответствующие схемы доказательства. В статье мы сначала даём краткое введение в язык poST, процесс-ориентированное расширение языка ST стандарта МЭК 61131-3. Далее определяется язык DV-TRL. Мы также приводим коллекцию требований на естественном языке для нескольких систем управления. Затем мы определяем шаблоны, позволяющие полностью покрыть все требования этой коллекции и для каждого из шаблонов приводим пример формализованного требования из коллекции и описываем схему доказательства условий корректности для этого шаблона. Статистика распределения требований из коллекции по шаблонам выявляет наиболее востребованные шаблоны. Мы также провели анализ связанных работ.
Издательство
- Издательство
- ЯрГУ им. П.Г. Демидова
- Регион
- Россия, Ярославль
- Почтовый адрес
- 150003, Ярославль, Советская, 14,
- Юр. адрес
- 150003, Ярославль, Советская, 14,
- ФИО
- Иванчин Артем Владимирович (Ректор)
- E-mail адрес
- rectorat@uniyar.ac.ru
- Контактный телефон
- +7 (485) 2797702