Author(s):
Davydov Artem Vasilyevich
Position: Research Scientist
Office: Institute for System Dynamics and Control Theory of Siberian Branch of Russian Academy of Sciences
Address: 664033, Russia, Irkutsk, Lermontova st., 134
Phone Office: (3952)453085
E-mail: artem@icc.ru
SPIN-code: 9827-5805

Nagul Nadezhda Vladimirovna
PhD. , Senior Scientist
Position: Senior Research Scientist
Office: Institute for System Dynamics and Control Theory of Siberian Branch of Russian Academy of Sciences
Address: 664033, Russia, Irkutsk, Lermontova st., 134
Phone Office: (3952)453085
E-mail: sapling@icc.ru
SPIN-code: 9851-3181

Larionov Aleksandr Aleksandrovich
Position: Programmer
Office: Institute for System Dynamics and Control Theory of Siberian Branch of Russian Academy of Sciences
Address: 664033, Russia, Irkutsk, Lermontova st., 134
Phone Office: (3952)453085
E-mail: bootfrost@zoho.com
SPIN-code: 9851-3181

References:
[1] Cassandras C.G., Lafortune S. Introduction to discrete event systems. Boston: Springer; 2008: 772.

[2] Seatzu C., Silva M., van Schuppen J.H. (Eds) Control of discrete-event systems. London: Springer; 2013: 480. DOI:10.1007/978-1-4471-4276-8.

[3] Wonham W.M., Cai K. Supervisory control of discrete-event systems. Cham: Springer; 2019: 487.

[4] Vassilyev S.N. Machine synthesis of mathematical theorems. The Journal of Logic Programming. 1990; (9):235–266. DOI:10.1016/0743-1066(90)90042-4.

[5] Zherlov A.K., Vassilyev S.N., Fedosov E.A., Fedunov B.E. Intellektnoe upravlenie dinamicheskimi sistemami [Intelligent control of dynamic systems]. Moscow: Fizmatlit; 2000: 352. (In Russ.)

[6] Davydov A., Larionov A., Cherkashin E. On the calculus of positively constructed formulas for automated theorem proving. Automatic Control and Computer Sciences. 2011; (45):402–407. DOI:10.3103/s0146411611070054.

[7] Davydov A., Larionov A., Cherkashin E. The calculus of positively constructed formulas, its features, strategies and implementation. International Convention on Information and Communication Technology, Electronics and Microelectronics (MIPRO). Opatija; 2013: 1023–1028.

[8] Kov ́acs L., Voronkov A. First-order theorem proving and vampire. Computer Aided Verification. Berlin, Heidelberg: Springer; 2013: 1–35

9] Otten J. Nanocop: a non-clausal connection prover. Proceedings of the 8th International Joint Conference on Automated Reasoning. Berlin, Heidelberg: Springer-Verlag; 2016: 302–312. DOI:10.1007/978-3-319-40229-1 21.

[10] Schulz S., Cruanes S., Vukmirovi ́c P. Faster, higher, stronger: E 2.3. Proc. of the 27th CADE. Natal, Brasil: Springer; 2019: 495–507.

[11] Davydov A., Larionov A. Action planning for robots using the first order logic calculus of positively constructed formulas. 2020 7th International Confer-
ence on Control, Decision and Information Technologies (CoDIT). 2020; (1):727–732. DOI:10.1109/CoDIT49905.2020.9263814.

[12] Karpas E., Magazzeni D. Automated planning for robotics. Annual Review of Control, Robotics, and Autonomous Systems. 2020; (3):417–439.

[13] Zombori Z., Urban J., Brown C.E. Prolog technology reinforcement learning prover. International Joint Conference on Automated Reasoning. Springer; 2020: 489–507.

[14] Schader M., Luke S. Planner-guided robot swarms. International Conference on Practical Applications of Agents and Multi-Agent Systems. Springer; 2020: 224–237.

[15] Geng X., Ouyang D., Han C. Verifying diagnosability of discrete event system with logical formula. Chinese Journal of Electronics. 2020; (29):304–311. DOI:10.1049/cje.2020.01.008.

[16] Davydov A., Larionov A., Nagul N. On checking controllability of specification languages for des. 2020 43rd International Convention on Information, Communication and Electronic Technology (MIPRO). 2020: 1151–1156. DOI:10.23919/MIPRO48935.2020.9245154.

[17] Davydov A., Larionov A., Nagul N. The construction of controllable sublanguage of specification for DES via PCFs based inference. CEUR Workshop Proceedings. 2020; (2638):68–78.

[18] Davydov A., Larionov A., Nagul N. Application of the PCF calculus for solving the problem of nonblocking supervisory control of discrete event systems. Journal of Physics: Conference Series. 2021; (1864):012048. DOI:10.1088/1742-6596/1864/1/012048.

[19] Davydov A., Larionov A., Nagul N. Positively constructed formulas-based approach to mobile robot control using DES. 2021 44th International Convention on Information, Communication and Electronic Technology (MIPRO). 2021: 1064–1069. DOI:10.23919/MIPRO52101.2021.9597024.

[20] de Queiroz M.H., Cury J.E.R. Modular supervisory control of large scale discrete event systems. The Springer International Series in Engineering and Computer Science. 2000; (569):103–110. DOI:10.1007/978-1-4615-4493-7 10.