Статья: О ПРИМЕНЕНИИ ИСЧИСЛЕНИЯ ПОЗИТИВНО-ОБРАЗОВАННЫХ ФОРМУЛ ДЛЯ ИССЛЕДОВАНИЯ УПРАВЛЯЕМЫХ ДИСКРЕТНО-СОБЫТИЙНЫХ СИСТЕМ (2024)

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