{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T01:04:39Z","timestamp":1760144679403,"version":"build-2065373602"},"reference-count":54,"publisher":"MDPI AG","issue":"5","license":[{"start":{"date-parts":[[2024,5,9]],"date-time":"2024-05-09T00:00:00Z","timestamp":1715212800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100012190","name":"Ministry of Science and Higher Education of the Russian Federation","doi-asserted-by":"publisher","award":["121032400051-9"],"award-info":[{"award-number":["121032400051-9"]}],"id":[{"id":"10.13039\/501100012190","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Computation"],"abstract":"<jats:p>This paper establishes a connection between control theory for partially observed discrete-event systems (DESs) and automated theorem proving (ATP) in the calculus of positively constructed formulas (PCFs). The language of PCFs is a complete first-order language providing a powerful tool for qualitative analysis of dynamical systems. Based on ATP in the PCF calculus, a new technique is suggested for checking observability as a property of formal languages, which is necessary for the existence of supervisory control of DESs. In the case of violation of observability, words causing a conflict can also be extracted with the help of a specially designed PCF. With an example of the problem of path planning by a robot in an unknown environment, we show the application of our approach at one of the levels of a robot control system. The prover Bootfrost developed to facilitate PCF refutation is also presented. The tests show positive results and perspectives for the presented approach.<\/jats:p>","DOI":"10.3390\/computation12050095","type":"journal-article","created":{"date-parts":[[2024,5,10]],"date-time":"2024-05-10T05:25:47Z","timestamp":1715318747000},"page":"95","update-policy":"https:\/\/doi.org\/10.3390\/mdpi_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Analysis and Control of Partially Observed Discrete-Event Systems via Positively Constructed Formulas"],"prefix":"10.3390","volume":"12","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-8703-3096","authenticated-orcid":false,"given":"Artem","family":"Davydov","sequence":"first","affiliation":[{"name":"Matrosov Institute for System Dynamics and Control Theory of the Siberian Branch of the Russian Academy of Sciences, 134 Lermontov St., 664033 Irkutsk, Russia"}]},{"given":"Aleksandr","family":"Larionov","sequence":"additional","affiliation":[{"name":"Matrosov Institute for System Dynamics and Control Theory of the Siberian Branch of the Russian Academy of Sciences, 134 Lermontov St., 664033 Irkutsk, Russia"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1439-3274","authenticated-orcid":false,"given":"Nadezhda","family":"Nagul","sequence":"additional","affiliation":[{"name":"Matrosov Institute for System Dynamics and Control Theory of the Siberian Branch of the Russian Academy of Sciences, 134 Lermontov St., 664033 Irkutsk, Russia"}]}],"member":"1968","published-online":{"date-parts":[[2024,5,9]]},"reference":[{"key":"ref_1","doi-asserted-by":"crossref","unstructured":"Cassandras, C.G., and Lafortune, S. (2021). Introduction to Discrete Event Systems, Springer.","DOI":"10.1007\/978-3-030-72274-6"},{"key":"ref_2","doi-asserted-by":"crossref","first-page":"141","DOI":"10.1146\/annurev-control-053018-023659","article-title":"Discrete Event Systems: Modeling, Observation, and Control","volume":"2","author":"Lafortune","year":"2019","journal-title":"Annu. Rev. Control Robot. Auton. Syst."},{"key":"ref_3","doi-asserted-by":"crossref","unstructured":"Seatzu, C., Silva, M., and van Schuppen, J.H. (2013). Control of Discrete-Event Systems, Springer.","DOI":"10.1007\/978-1-4471-4276-8"},{"key":"ref_4","doi-asserted-by":"crossref","first-page":"206","DOI":"10.1137\/0325013","article-title":"Supervisory control of a class of discrete event processes","volume":"25","author":"Ramadge","year":"1987","journal-title":"SIAM J. Control Optim."},{"key":"ref_5","doi-asserted-by":"crossref","first-page":"18","DOI":"10.1007\/s10489-015-0741-3","article-title":"Cooperative exploration based on supervisory control of multi-robot systems","volume":"45","author":"Dai","year":"2016","journal-title":"Appl. Intell."},{"key":"ref_6","doi-asserted-by":"crossref","first-page":"65","DOI":"10.1007\/s11721-016-0119-0","article-title":"Supervisory control theory applied to swarm robotics","volume":"10","author":"Lopes","year":"2016","journal-title":"Swarm Intell."},{"key":"ref_7","doi-asserted-by":"crossref","unstructured":"Hill, R.C., and Lafortune, S. (2017, January 24\u201326). Scaling the formal synthesis of supervisory control software for multiple robot systems. Proceedings of the 2017 American Control Conference (ACC), Seattle, WA, USA.","DOI":"10.23919\/ACC.2017.7963543"},{"key":"ref_8","doi-asserted-by":"crossref","unstructured":"Wonham, W.M., and Cai, K. (2019). Supervisory Control of Discrete-Event Systems, Springer International Publishing.","DOI":"10.1007\/978-3-319-77452-7"},{"key":"ref_9","doi-asserted-by":"crossref","first-page":"250","DOI":"10.1016\/j.arcontrol.2018.03.002","article-title":"Supervisory control of discrete-event systems: A brief history","volume":"45","author":"Wonham","year":"2018","journal-title":"Annu. Rev. Control"},{"key":"ref_10","doi-asserted-by":"crossref","first-page":"e2","DOI":"10.1017\/fmp.2017.1","article-title":"A formal proof of the kepler conjecture","volume":"5","author":"Hales","year":"2017","journal-title":"Forum Math. Pi"},{"key":"ref_11","doi-asserted-by":"crossref","first-page":"107","DOI":"10.1145\/1743546.1743574","article-title":"SeL4: Formal Verification of an Operating-System Kernel","volume":"53","author":"Klein","year":"2010","journal-title":"Commun. ACM"},{"key":"ref_12","first-page":"1382","article-title":"Formal Proof\u2014The Four-Color Theorem","volume":"11","author":"Gonthier","year":"2008","journal-title":"Not. Am. Math. Soc."},{"key":"ref_13","doi-asserted-by":"crossref","first-page":"107","DOI":"10.1145\/1538788.1538814","article-title":"Formal Verification of a Realistic Compiler","volume":"52","author":"Leroy","year":"2009","journal-title":"Commun. ACM"},{"key":"ref_14","doi-asserted-by":"crossref","first-page":"417","DOI":"10.1146\/annurev-control-082619-100135","article-title":"Automated planning for robotics","volume":"3","author":"Karpas","year":"2020","journal-title":"Annu. Rev. Control Robot. Auton. Syst."},{"key":"ref_15","doi-asserted-by":"crossref","unstructured":"Zombori, Z., Urban, J., and Brown, C.E. (2020, January 1\u20134). Prolog technology reinforcement learning prover. Proceedings of the International Joint Conference on Automated Reasoning, Paris, France.","DOI":"10.1007\/978-3-030-51054-1_33"},{"key":"ref_16","doi-asserted-by":"crossref","unstructured":"Schader, M., and Luke, S. (2020, January 7\u20139). Planner-Guided Robot Swarms. Proceedings of the International Conference on Practical Applications of Agents and Multi-Agent Systems, L\u2019Aquila, Italy.","DOI":"10.1007\/978-3-030-49778-1_18"},{"key":"ref_17","doi-asserted-by":"crossref","unstructured":"Gro\u00df, R., Kolling, A., Berman, S., Frazzoli, E., Martinoli, A., Matsuno, F., and Gauci, M. (2018). Distributed Autonomous Robotic Systems: The 13th International Symposium, Springer International Publishing.","DOI":"10.1007\/978-3-319-73008-0"},{"key":"ref_18","doi-asserted-by":"crossref","first-page":"235","DOI":"10.1016\/0743-1066(90)90042-4","article-title":"Machine synthesis of mathematical theorems","volume":"9","author":"Vassilyev","year":"1990","journal-title":"J. Log. Program."},{"key":"ref_19","doi-asserted-by":"crossref","first-page":"402","DOI":"10.3103\/S0146411611070054","article-title":"On the calculus of positively constructed formulas for automated theorem proving","volume":"45","author":"Davydov","year":"2011","journal-title":"Autom. Control Comput. Sci."},{"key":"ref_20","unstructured":"Kumar, A.N., and Russell, I. (1999, January 1\u20135). New Logics for Intelligent Control. Proceedings of the Twelfth International Florida Artificial Intelligence Research Society Conference, Orlando, FL, USA."},{"key":"ref_21","unstructured":"Zherlov, A.K., Vassilyev, S.N., Fedosov, E.A., and Fedunov, B.E. (2000). Intelligent Control of Dynamic Systems, Fizmatlit. (In Russian)."},{"key":"ref_22","doi-asserted-by":"crossref","first-page":"299","DOI":"10.1134\/S1064562417030267","article-title":"Logical-optimization approach to pursuit problems for a group of targets","volume":"95","author":"Vassilyev","year":"2017","journal-title":"Dokl. Math."},{"key":"ref_23","doi-asserted-by":"crossref","first-page":"161","DOI":"10.1134\/S0081543812020137","article-title":"Automation methods for logical derivation and their application in the control of dynamic and intelligent systems","volume":"276","author":"Vassilyev","year":"2012","journal-title":"Proc. Steklov Inst. Math."},{"key":"ref_24","unstructured":"Larionov, A. (2024, April 26). Bootfrost. Available online: https:\/\/github.com\/snigavik\/bootfrost."},{"key":"ref_25","first-page":"20150404","article-title":"Provably trustworthy systems","volume":"375","author":"Klein","year":"2017","journal-title":"Philos. Trans. R. Soc. Math. Phys. Eng. Sci."},{"key":"ref_26","first-page":"68","article-title":"The construction of controllable sublanguage of specification for DES via PCFs based inference","volume":"Volume 2638","author":"Bychkov","year":"2020","journal-title":"Proceedings of the 2nd International Workshop on Information, Computation, and Control Systems for Distributed Environments, ICCS-DE 2020"},{"key":"ref_27","doi-asserted-by":"crossref","first-page":"177","DOI":"10.1007\/BF02088297","article-title":"Supremal and maximal sublanguages arising in supervisor synthesis problems with partial observations","volume":"22","author":"Cho","year":"1989","journal-title":"Math. Syst. Theory"},{"key":"ref_28","doi-asserted-by":"crossref","first-page":"151","DOI":"10.1007\/BF01215843","article-title":"An algebraic approach to supervisory control","volume":"5","author":"Inan","year":"1992","journal-title":"Math. Control Signals Syst."},{"key":"ref_29","doi-asserted-by":"crossref","first-page":"361","DOI":"10.1016\/0167-6911(90)90059-4","article-title":"The infimal prefix-closed and observable superlanguange of a given language","volume":"15","author":"Rudie","year":"1990","journal-title":"Syst. Control Lett."},{"key":"ref_30","doi-asserted-by":"crossref","unstructured":"Feng, L., and Wonham, W.M. (2006, January 10\u201312). TCT: A computation tool for supervisory control synthesis. Proceedings of the 2006 8th International Workshop on Discrete Event Systems, Ann Arbor, MI, USA.","DOI":"10.1109\/WODES.2006.382399"},{"key":"ref_31","unstructured":"Lafortune, S. (2024, April 15). Desuma. Available online: https:\/\/gitlab.eecs.umich.edu\/wikis\/desuma."},{"key":"ref_32","doi-asserted-by":"crossref","unstructured":"Ricker, L., Lafortune, S., and Genc, S. (2006, January 10\u201312). DESUMA: A Tool Integrating GIDDES and UMDES. Proceedings of the 2006 8th International Workshop on Discrete Event Systems, Ann Arbor, MI, USA.","DOI":"10.1109\/WODES.2006.382402"},{"key":"ref_33","unstructured":"\u00c5kesson, K., Fabian, M., Flordal, H., Vahidi, A., and Malik, R. (2024, April 05). Supremica. Available online: https:\/\/supremica.org\/."},{"key":"ref_34","doi-asserted-by":"crossref","first-page":"5794","DOI":"10.1016\/j.ifacol.2017.08.427","article-title":"Supremica\u2013An Efficient Tool for Large-Scale Discrete Event Systems","volume":"50","author":"Malik","year":"2017","journal-title":"IFAC-PapersOnLine"},{"key":"ref_35","doi-asserted-by":"crossref","first-page":"175","DOI":"10.3182\/20020721-6-ES-1901.00517","article-title":"Exploiting modularity for synthesis and verification of supervisors","volume":"35","author":"Flordal","year":"2002","journal-title":"IFAC Proc. Vol."},{"key":"ref_36","doi-asserted-by":"crossref","first-page":"387","DOI":"10.1109\/TCST.2004.824795","article-title":"Incremental verification and synthesis of discrete-event systems guided by counter examples","volume":"12","author":"Brandin","year":"2004","journal-title":"IEEE Trans. Control Syst. Technol."},{"key":"ref_37","doi-asserted-by":"crossref","first-page":"150","DOI":"10.1109\/TAC.2013.2283109","article-title":"A Framework for Compositional Synthesis of Modular Nonblocking Supervisors","volume":"59","author":"Mohajerani","year":"2014","journal-title":"IEEE Trans. Autom. Control"},{"key":"ref_38","first-page":"556","article-title":"The method for translating first-order logic formulas into positively constructed formulas","volume":"4","author":"Larionov","year":"2019","journal-title":"Softw. Syst."},{"key":"ref_39","unstructured":"Larionov, A., Davydov, A., and Cherkashin, E. (2013, January 20\u201324). The calculus of positively constructed formulas, its features, strategies and implementation. Proceedings of the 2013 36th International Convention on Information and Communication Technology, Electronics and Microelectronics (MIPRO), Opatija, Croatia."},{"key":"ref_40","doi-asserted-by":"crossref","first-page":"483","DOI":"10.1007\/s10817-017-9407-7","article-title":"The TPTP Problem Library and Associated Infrastructure. From CNF to TH0, TPTP v6.4.0","volume":"59","author":"Sutcliffe","year":"2017","journal-title":"J. Autom. Reason."},{"key":"ref_41","doi-asserted-by":"crossref","unstructured":"Ulyanov, S., Bychkov, I., and Maksimkin, N. (2020). Event-Based Path-Planning and Path-Following in Unknown Environments for Underactuated Autonomous Underwater Vehicles. Appl. Sci., 10.","DOI":"10.3390\/app10217894"},{"key":"ref_42","doi-asserted-by":"crossref","first-page":"012001","DOI":"10.1088\/1742-6596\/1864\/1\/012001","article-title":"Hierarchical event-based control of multi-robot systems in unstructured environments","volume":"1864","author":"Bychkov","year":"2021","journal-title":"J. Phys. Conf. Ser."},{"key":"ref_43","doi-asserted-by":"crossref","first-page":"1734","DOI":"10.1016\/j.oceaneng.2006.10.019","article-title":"Nonlinear path-following control of an AUV","volume":"34","author":"Lapierre","year":"2007","journal-title":"Ocean Eng."},{"key":"ref_44","doi-asserted-by":"crossref","unstructured":"Yan, Z., Li, J., Zhang, G., and Wu, Y. (2018). A Real-Time Reaction Obstacle Avoidance Algorithm for Autonomous Underwater Vehicles in Unknown Environments. Sensors, 18.","DOI":"10.3390\/s18020438"},{"key":"ref_45","doi-asserted-by":"crossref","first-page":"497","DOI":"10.2307\/2372560","article-title":"On Curves of Minimal Length with a Constraint on Average Curvature, and with Prescribed Initial and Terminal Positions and Tangents","volume":"79","author":"Dubins","year":"1957","journal-title":"Am. J. Math."},{"key":"ref_46","doi-asserted-by":"crossref","unstructured":"Kostylev, D., Tolstikhin, A., and Ulyanov, S. (2019, January 20\u201324). Development of the complex modelling system for intelligent control algorithms testing. Proceedings of the 2019 42nd International Convention on Information and Communication Technology, Electronics and Microelectronics (MIPRO), Opatija, Croatia.","DOI":"10.23919\/MIPRO.2019.8757003"},{"key":"ref_47","doi-asserted-by":"crossref","first-page":"304","DOI":"10.1049\/cje.2020.01.008","article-title":"Verifying Diagnosability of Discrete Event System with Logical Formula","volume":"29","author":"Geng","year":"2020","journal-title":"Chin. J. Electron."},{"key":"ref_48","doi-asserted-by":"crossref","first-page":"115","DOI":"10.1007\/s10626-021-00350-4","article-title":"Supervisory controller synthesis and implementation for safety PLCs","volume":"32","author":"Reijnen","year":"2022","journal-title":"Discret. Event Dyn. Syst."},{"key":"ref_49","doi-asserted-by":"crossref","first-page":"5269","DOI":"10.1109\/TAC.2020.3037156","article-title":"Supervisory Control of Fair Discrete-Event Systems: A Canonical Temporal Logic Foundation","volume":"66","author":"Seow","year":"2021","journal-title":"IEEE Trans. Autom. Control"},{"key":"ref_50","doi-asserted-by":"crossref","first-page":"943","DOI":"10.1080\/00207178608933645","article-title":"Control problems in a temporal logic framework","volume":"44","author":"Thistle","year":"1986","journal-title":"Int. J. Control"},{"key":"ref_51","doi-asserted-by":"crossref","first-page":"644","DOI":"10.1109\/TCST.2018.2877621","article-title":"Supervisory Control of Labeled Transition Systems Subject to Multiple Reachability Requirements via Symbolic Model Checking","volume":"28","author":"Rawlings","year":"2020","journal-title":"IEEE Trans. Control Syst. Technol."},{"key":"ref_52","doi-asserted-by":"crossref","first-page":"2079","DOI":"10.1137\/S0363012902409982","article-title":"Supervisory Control of Discrete Event Systems with CTL* Temporal Logic Specifications","volume":"44","author":"Jiang","year":"2006","journal-title":"SIAM J. Control Optim."},{"key":"ref_53","unstructured":"Aucher, G. (2014, January 5\u20139). Supervisory Control Theory in Epistemic Temporal Logic. Proceedings of the International Conference on Autonomous Agents and Multi-Agent Systems, Paris, France."},{"key":"ref_54","doi-asserted-by":"crossref","first-page":"257","DOI":"10.1007\/s10626-023-00381-z","article-title":"Do what you know: Coupling knowledge with action in discrete-event systems","volume":"33","author":"Ritsuka","year":"2023","journal-title":"Discret. Event Dyn. Syst."}],"container-title":["Computation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.mdpi.com\/2079-3197\/12\/5\/95\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,10]],"date-time":"2025-10-10T14:43:01Z","timestamp":1760107381000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.mdpi.com\/2079-3197\/12\/5\/95"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,5,9]]},"references-count":54,"journal-issue":{"issue":"5","published-online":{"date-parts":[[2024,5]]}},"alternative-id":["computation12050095"],"URL":"https:\/\/doi.org\/10.3390\/computation12050095","relation":{},"ISSN":["2079-3197"],"issn-type":[{"type":"electronic","value":"2079-3197"}],"subject":[],"published":{"date-parts":[[2024,5,9]]}}}