{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,15]],"date-time":"2026-03-15T22:59:01Z","timestamp":1773615541720,"version":"3.50.1"},"reference-count":50,"publisher":"Allerton Press","issue":"7","license":[{"start":{"date-parts":[[2024,12,1]],"date-time":"2024-12-01T00:00:00Z","timestamp":1733011200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,12,1]],"date-time":"2024-12-01T00:00:00Z","timestamp":1733011200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Aut. Control Comp. Sci."],"published-print":{"date-parts":[[2024,12]]},"DOI":"10.3103\/s0146411624700445","type":"journal-article","created":{"date-parts":[[2025,2,12]],"date-time":"2025-02-12T14:48:46Z","timestamp":1739371726000},"page":"1042-1062","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["On the Application of the Calculus of Positively Constructed Formulas for the Study of Controlled Discrete-Event Systems"],"prefix":"10.3103","volume":"58","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-8703-3096","authenticated-orcid":false,"given":"A. V.","family":"Davydov","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7116-9338","authenticated-orcid":false,"given":"A. A.","family":"Larionov","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1439-3274","authenticated-orcid":false,"given":"N. V.","family":"Nagul","sequence":"additional","affiliation":[]}],"member":"1627","published-online":{"date-parts":[[2025,2,12]]},"reference":[{"key":"7765_CR1","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1146\/annurev-control-053018-023659","volume":"2","author":"S. Lafortune","year":"2019","unstructured":"Lafortune, S., Discrete event systems: Modeling, observation, and control, Annu. Rev. Control, Rob., \n               Auton. Syst., 2019, vol. 2, no. 1, pp. 141\u2013159. https:\/\/doi.org\/10.1146\/annurev-control-053018-023659","journal-title":"Auton. Syst."},{"key":"7765_CR2","doi-asserted-by":"publisher","unstructured":"Control of Discrete-Event Systems: Automata and Petri Net Perspectives, Seatzu, C., Silva, M., and van Schuppen, J.H., Eds., London: Springer, 2013. https:\/\/doi.org\/10.1007\/978-1-4471-4276-8","DOI":"10.1007\/978-1-4471-4276-8"},{"key":"7765_CR3","doi-asserted-by":"publisher","unstructured":"Wonham, W.M. and Cai, K., Supervisory Control of Discrete-Event Systems, Communications and Control Engineering, Cham: Springer, 2019. https:\/\/doi.org\/10.1007\/978-3-319-77452-7","DOI":"10.1007\/978-3-319-77452-7"},{"key":"7765_CR4","doi-asserted-by":"publisher","first-page":"206","DOI":"10.1137\/0325013","volume":"25","author":"P.J. Ramadge","year":"1987","unstructured":"Ramadge, P.J. and Wonham, W.M., Supervisory control of a class of discrete event processes, SIAM J. Control Optim., 1987, vol. 25, no. 1, pp. 206\u2013230. https:\/\/doi.org\/10.1137\/0325013","journal-title":"SIAM J. Control Optim."},{"key":"7765_CR5","doi-asserted-by":"publisher","unstructured":"Cassandras, Ch.G. and Lafortune, S., Introduction to Discrete Event Systems, Cham: Springer, 2021. https:\/\/doi.org\/10.1007\/978-3-030-72274-6","DOI":"10.1007\/978-3-030-72274-6"},{"key":"7765_CR6","doi-asserted-by":"publisher","first-page":"250","DOI":"10.1016\/j.arcontrol.2018.03.002","volume":"45","author":"W.M. Wonham","year":"2018","unstructured":"Wonham, W.M., Cai, K., and Rudie, K., Supervisory control of discrete-event systems: A brief history, Annu. Rev. Control, 2018, vol. 45, pp. 250\u2013256. https:\/\/doi.org\/10.1016\/j.arcontrol.2018.03.002","journal-title":"Annu. Rev. Control"},{"key":"7765_CR7","doi-asserted-by":"publisher","first-page":"1224","DOI":"10.1109\/tsmcb.2011.2119311","volume":"41","author":"A. Jayasiri","year":"2011","unstructured":"Jayasiri, A., Mann, G.K.I., and Gosine, R.G., Behavior coordination of mobile robotics using supervisory control of fuzzy discrete event systems, IEEE Trans. Syst., Man, Cybern., Part B (Cybern.), 2011, vol. 41, no. 5, pp.\u00a01224\u20131238. https:\/\/doi.org\/10.1109\/tsmcb.2011.2119311","journal-title":"IEEE Trans. Syst., Man, Cybern., Part B (Cybern.)"},{"key":"7765_CR8","doi-asserted-by":"publisher","first-page":"240","DOI":"10.1016\/j.ifacol.2016.12.221","volume":"49","author":"C.R.C. Torrico","year":"2016","unstructured":"Torrico, C.R.C., Leal, A.B., and Watanabe, A.T.Y., Modeling and supervisory control of mobile robots: A case of a sumo robot, IFAC-PapersOnLine, 2016, vol. 49, no. 32, pp. 240\u2013245. https:\/\/doi.org\/10.1016\/j.ifacol.2016.12.221","journal-title":"IFAC-PapersOnLine"},{"key":"7765_CR9","doi-asserted-by":"publisher","first-page":"18","DOI":"10.1007\/s10489-015-0741-3","volume":"45","author":"X. Dai","year":"2016","unstructured":"Dai, X., Jiang, L., and Zhao, Ya., Cooperative exploration based on supervisory control of multi-robot systems, Appl. Intell., 2016, vol. 45, no. 1, pp. 18\u201329. https:\/\/doi.org\/10.1007\/s10489-015-0741-3","journal-title":"Appl. Intell."},{"key":"7765_CR10","doi-asserted-by":"publisher","first-page":"721","DOI":"10.1017\/s0263574711000920","volume":"30","author":"A. Tsalatsanis","year":"2012","unstructured":"Tsalatsanis, A., Yalcin, A., and Valavanis, Kimon.P., Dynamic task allocation in cooperative robot teams, Robotica, 2012, vol. 30, no. 5, pp. 721\u2013730. https:\/\/doi.org\/10.1017\/s0263574711000920","journal-title":"Robotica"},{"key":"7765_CR11","doi-asserted-by":"publisher","unstructured":"Hill, R.C. and Lafortune, S., Scaling the formal synthesis of supervisory control software for multiple robot systems, 2017 American Control Conf. (ACC), Seattle, Wash., 2017, IEEE, 2017, pp. 3840\u20133847. https:\/\/doi.org\/10.23919\/acc.2017.7963543","DOI":"10.23919\/acc.2017.7963543"},{"key":"7765_CR12","doi-asserted-by":"publisher","unstructured":"Gamage, G.W., Mann, G.K.I., and Gosine, R.G., Discrete event systems based formation control framework to coordinate multiple nonholonomic mobile robots, 2009 IEEE\/RSJ Int. Conf. on Intelligent Robots and Systems, St. Louis, Mo., 2009, IEEE, 2009, pp. 4831\u20134836. https:\/\/doi.org\/10.1109\/iros.2009.5354788","DOI":"10.1109\/iros.2009.5354788"},{"key":"7765_CR13","doi-asserted-by":"publisher","first-page":"65","DOI":"10.1007\/s11721-016-0119-0","volume":"10","author":"Yu.K. Lopes","year":"2016","unstructured":"Lopes, Yu.K., Trenkwalder, S.M., Leal, A.B., Dodd, T.J., and Gro\u00df, R., Supervisory control theory applied to swarm robotics, Swarm Intell., 2016, vol. 10, no. 1, pp. 65\u201397. https:\/\/doi.org\/10.1007\/s11721-016-0119-0","journal-title":"Swarm Intell."},{"key":"7765_CR14","doi-asserted-by":"publisher","unstructured":"Mendiburu, F.J., Morais, M.R.A., and Lima, A.M.N., Behavior coordination in multi-robot systems, 2016 IEEE Int. Conf. on Automatica (ICA-ACCA), Curico, Chile, 2016, IEEE, 2016, pp. 1\u20137. https:\/\/doi.org\/10.1109\/ica-acca.2016.7778506","DOI":"10.1109\/ica-acca.2016.7778506"},{"key":"7765_CR15","doi-asserted-by":"publisher","unstructured":"Hales, T., Adams, M., Bauer, G., Dang, T.D., Harrison, J., Hoang, L.T., Kaliszyk, C., Magron, V., Mclaughlin, S., Nguyen, T.T., Nguyen, Q.T., Nipkow, T., Obua, S., Pleso, J., Rute, J., Solovyev, A., Ta, T.H.A., Tran, N.T., Trieu, T.D., Urban, J., Vu, K.Y., and Zumkeller, R., A formal proof of the Kepler conjecture, Forum Math., Pi, 2017, vol. 5, p. e2. https:\/\/doi.org\/10.1017\/fmp.2017.1","DOI":"10.1017\/fmp.2017.1"},{"key":"7765_CR16","doi-asserted-by":"publisher","unstructured":"Klein, G., Elphinstone, K., Heiser, G., Andronick, J., Cock, D., and Derrin, Ph., Sel4: Formal verification of an os kernel, Proc. ACM SIGOPS 22nd Symp. on Operating systems principles, Big Sky, Mont., 2009, New York: Association for Computing Machinery, 2009, pp. 207\u2013220. https:\/\/doi.org\/10.1145\/1629575.1629596","DOI":"10.1145\/1629575.1629596"},{"key":"7765_CR17","first-page":"1382","volume":"55","author":"G. Gonthier","year":"2008","unstructured":"Gonthier, G., Formal proof\u2014The four-color theorem, Not. AMS, 2008, vol. 55, no. 11, pp. 1382\u20131393.","journal-title":"Not. AMS"},{"key":"7765_CR18","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1145\/1538788.1538814","volume":"52","author":"X. Leroy","year":"2009","unstructured":"Leroy, X., Formal verification of a realistic compiler, Commun. ACM, 2009, vol. 52, no. 7, pp. 107\u2013115. https:\/\/doi.org\/10.1145\/1538788.1538814","journal-title":"Commun. ACM"},{"key":"7765_CR19","doi-asserted-by":"publisher","first-page":"728","DOI":"10.3103\/s0146411620070093","volume":"54","author":"D.A. Kondratyev","year":"2020","unstructured":"Kondratyev, D.A. and Promsky, A.V., The complex approach of the C-lightVer system to the automated error localization in C-programs, Autom. Control Comput. Sci., 2020, vol. 54, no. 7, pp. 728\u2013739. https:\/\/doi.org\/10.3103\/s0146411620070093","journal-title":"Autom. Control Comput. Sci."},{"key":"7765_CR20","doi-asserted-by":"publisher","first-page":"699","DOI":"10.1007\/s00165-019-00490-3","volume":"31","author":"J.S. Moore","year":"2019","unstructured":"Moore, J.S., Milestones from the Pure Lisp theorem prover to ACL2, Formal Aspects Comput., 2019, vol. 31, no.\u00a06, pp. 699\u2013732. https:\/\/doi.org\/10.1007\/s00165-019-00490-3","journal-title":"Formal Aspects Comput."},{"key":"7765_CR21","doi-asserted-by":"publisher","first-page":"417","DOI":"10.1146\/annurev-control-082619-100135","volume":"3","author":"E. Karpas","year":"2020","unstructured":"Karpas, E. and Magazzeni, D., Automated planning for robotics, Annu. Rev. Control, Rob., \n               Auton. Syst., 2020, vol. 3, no. 1, pp. 417\u2013439. https:\/\/doi.org\/10.1146\/annurev-control-082619-100135","journal-title":"Auton. Syst."},{"key":"7765_CR22","doi-asserted-by":"publisher","unstructured":"Zombori, Z., Urban, J., and Brown, Ch.E., Prolog technology reinforcement learning prover, Automated Reasoning, Peltier, N. and Sofronie-Stokkermans, V., Eds., Lecture Notes in Computer Science, vol. 12167, Cham: Springer, 2020, pp. 489\u2013507. https:\/\/doi.org\/10.1007\/978-3-030-51054-1_33","DOI":"10.1007\/978-3-030-51054-1_33"},{"key":"7765_CR23","doi-asserted-by":"publisher","unstructured":"Schader, M. and Luke, S., Planner-guided robot swarms, Advances in Practical Applications of Agents, Multi-Agent Systems, and Trustworthiness. The PAAMS Collection, Demazeau, Y., Holvoet, T., Corchado, J., and Costantini, S., Eds., Lecture Notes in Computer Science, vol. 12092, Cham: Springer, 2020, pp. 224\u2013237. https:\/\/doi.org\/10.1007\/978-3-030-49778-1_18","DOI":"10.1007\/978-3-030-49778-1_18"},{"key":"7765_CR24","doi-asserted-by":"publisher","unstructured":"Li, W., Miyazawa, A., Ribeiro, P., Cavalcanti, A., Woodcock, J., and Timmis, J., From formalised state machines to implementations of robotic controllers, Distributed Autonomous Robotic Systems, Gro\u00df, R., Kolling, A., Berman, S., Frazzoli, E., Martinoli, A., Matsuno, F., and Gauci, M., Eds., Springer Proceedings in Advanced Robotics, vol. 6, Cham: Springer, 2018, pp. 517\u2013529. https:\/\/doi.org\/10.1007\/978-3-319-73008-0_36","DOI":"10.1007\/978-3-319-73008-0_36"},{"key":"7765_CR25","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1016\/0743-1066(90)90042-4","volume":"9","author":"S.N. Vassilyev","year":"1990","unstructured":"Vassilyev, S.N., Machine synthesis of mathematical theorems, J. Logic Program., 1990, vol. 9, nos. 2\u20133, pp.\u00a0235\u2013266. https:\/\/doi.org\/10.1016\/0743-1066(90)90042-4","journal-title":"J. Logic Program."},{"key":"7765_CR26","volume-title":"Intelligent Control of Dynamic Systems","author":"A.K. Zherlov","year":"2000","unstructured":"Zherlov, A.K., Vassilyev, S.N., Fedosov, E.A., and Fedunov, B.E., Intelligent Control of Dynamic Systems, Moscow: Fizmatlit, 2000."},{"key":"7765_CR27","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1134\/s0081543812020137","volume":"276","author":"S.N. Vassilyev","year":"2012","unstructured":"Vassilyev, S.N. and Ponomarev, G.M., Automation methods for logical derivation and their application in the control of dynamic and intelligent systems, Proc. Steklov Inst. Math., 2012, vol. 276, no. s1, pp. 161\u2013179. https:\/\/doi.org\/10.1134\/s0081543812020137","journal-title":"Proc. Steklov Inst. Math."},{"key":"7765_CR28","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1134\/s1064562417030267","volume":"95","author":"S.N. Vassilyev","year":"2017","unstructured":"Vassilyev, S.N. and Galyaev, A.A., Logical-optimization approach to pursuit problems for a group of targets, Dokl. Math., 2017, vol. 95, no. 3, pp. 299\u2013304. https:\/\/doi.org\/10.1134\/s1064562417030267","journal-title":"Dokl. Math."},{"key":"7765_CR29","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1007\/s10626-021-00350-4","volume":"32","author":"F.F.H. Reijnen","year":"2022","unstructured":"Reijnen, F.F.H., Erens, T.R., Van De Mortel-Fronczak, J.M., and Rooda, J.E., Supervisory controller synthesis and implementation for safety PLCs, Discrete Event Dynamic Syst., 2022, vol. 32, no. 1, pp. 115\u2013141. https:\/\/doi.org\/10.1007\/s10626-021-00350-4","journal-title":"Discrete Event Dynamic Syst."},{"key":"7765_CR30","doi-asserted-by":"publisher","first-page":"428","DOI":"10.1016\/j.ifacol.2018.06.336","volume":"51","author":"D. Bohlender","year":"2018","unstructured":"Bohlender, D. and Kowalewski, S., Compositional verification of PLC software using horn clauses and mode abstraction, IFAC-PapersOnLine, 2018, vol. 51, no. 7, pp. 428\u2013433. https:\/\/doi.org\/10.1016\/j.ifacol.2018.06.336","journal-title":"IFAC-PapersOnLine"},{"key":"7765_CR31","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s10626-019-00296-8","volume":"30","author":"D. Bohlender","year":"2020","unstructured":"Bohlender, D. and Kowalewski, S., Leveraging horn clause solving for compositional verification of PLC software, Discrete Event Dynamic Syst., 2020, vol. 30, no. 1, pp. 1\u201324. https:\/\/doi.org\/10.1007\/s10626-019-00296-8","journal-title":"Discrete Event Dynamic Syst."},{"key":"7765_CR32","doi-asserted-by":"publisher","unstructured":"Bj\u00f8rner, N. and Nachmanson, L., Navigating the universe of Z3 theory solvers, Formal Methods: Foundations and Applications, Carvalho, G. and Stolz, V., Eds., Lecture Notes in Computer Science, vol. 12475, Cham: Springer, 2020, pp. 8\u201324. https:\/\/doi.org\/10.1007\/978-3-030-63882-52_2","DOI":"10.1007\/978-3-030-63882-52_2"},{"key":"7765_CR33","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1109\/tcst.2016.2544702","volume":"25","author":"A.D. Vieira","year":"2017","unstructured":"Vieira, A.D., Santos, E.A.P., de Queiroz, M.H., Leal, A.B., de Paula Neto, A.D., and Cury, J.E.R., A method for PLC implementation of supervisory control of discrete event systems, IEEE Trans. Control Syst. Technol., 2017, vol. 25, no. 1, pp. 175\u2013191. https:\/\/doi.org\/10.1109\/tcst.2016.2544702","journal-title":"IEEE Trans. Control Syst. Technol."},{"key":"7765_CR34","doi-asserted-by":"publisher","first-page":"943","DOI":"10.1080\/00207178608933645","volume":"44","author":"J.G. Thistle","year":"1986","unstructured":"Thistle, J.G. and Wonham, W.M., Control problems in a temporal logic framework, Int. J. Control, 1986, vol.\u00a044, no. 4, pp. 943\u2013976. https:\/\/doi.org\/10.1080\/00207178608933645","journal-title":"Int. J. Control"},{"key":"7765_CR35","doi-asserted-by":"publisher","first-page":"644","DOI":"10.1109\/tcst.2018.2877621","volume":"28","author":"B.C. Rawlings","year":"2020","unstructured":"Rawlings, B.C., Lafortune, S., and Ydstie, B.E., Supervisory control of labeled transition systems subject to multiple reachability requirements via symbolic model checking, IEEE Trans. Control Syst. Technol., 2020, vol.\u00a028, no. 2, pp. 644\u2013652. https:\/\/doi.org\/10.1109\/tcst.2018.2877621","journal-title":"IEEE Trans. Control Syst. Technol."},{"key":"7765_CR36","doi-asserted-by":"publisher","first-page":"5269","DOI":"10.1109\/tac.2020.3037156","volume":"66","author":"K.T. Seow","year":"2021","unstructured":"Seow, K.T., Supervisory control of fair discrete-event systems: A canonical temporal logic foundation, IEEE Trans. Autom. Control, 2021, vol. 66, no. 11, pp. 5269\u20135282. https:\/\/doi.org\/10.1109\/tac.2020.3037156","journal-title":"IEEE Trans. Autom. Control"},{"key":"7765_CR37","doi-asserted-by":"publisher","first-page":"2079","DOI":"10.1137\/s0363012902409982","volume":"44","author":"Sh. Jiang","year":"2006","unstructured":"Jiang, Sh. and Kumar, R., Supervisory control of discrete event systems with CTL* temporal logic specifications, SIAM J. Control Optim., 2006, vol. 44, no. 6, pp. 2079\u20132103. https:\/\/doi.org\/10.1137\/s0363012902409982","journal-title":"SIAM J. Control Optim."},{"key":"7765_CR38","doi-asserted-by":"crossref","unstructured":"Aucher, G., Supervisory control theory in epistemic temporal logic, AAMAS \u201914: Proc. 2014 Int. Conf. on Autonomous Agents and Multi-Agent Systems, Paris, 2014, Richland, S.C.: Int. Foundation for Autonomous Agents and Multiagent Systems, 2014, pp. 333\u2013340.","DOI":"10.65109\/VJQJ8528"},{"key":"7765_CR39","doi-asserted-by":"publisher","first-page":"257","DOI":"10.1007\/s10626-023-00381-z","volume":"33","author":"K. Ritsuka","year":"2023","unstructured":"Ritsuka, K. and Rudie, K., Do what you know: Coupling knowledge with action in discrete-event systems, Discrete Event Dynamic Syst., 2023, vol. 33, no. 3, pp. 257\u2013277. https:\/\/doi.org\/10.1007\/s10626-023-00381-z","journal-title":"Discrete Event Dynamic Syst."},{"key":"7765_CR40","doi-asserted-by":"publisher","first-page":"304","DOI":"10.1049\/cje.2020.01.008","volume":"29","author":"X. Geng","year":"2020","unstructured":"Geng, X., Ouyang, D., and Han, Ch., Verifying diagnosability of discrete event system with logical formula, Chin. J. Electron., 2020, vol. 29, no. 2, pp. 304\u2013311. https:\/\/doi.org\/10.1049\/cje.2020.01.008","journal-title":"Chin. J. Electron."},{"key":"7765_CR41","doi-asserted-by":"publisher","unstructured":"Feng, L. and Wonham, W.M., TCT: A computation tool for supervisory control synthesis, 2006 8th Int. Workshop on Discrete Event Systems, Ann Arbor, Mich., 2006, IEEE, 2006, pp. 388\u2013389. https:\/\/doi.org\/10.1109\/wodes.2006.382399","DOI":"10.1109\/wodes.2006.382399"},{"key":"7765_CR42","doi-asserted-by":"publisher","unstructured":"Ricker, L., Lafortune, S., and Genc, S., DESUMA: A Tool Integrating GIDDES and UMDES, 2006 8th Int. Workshop on Discrete Event Systems, Ann Arbor, Mich., 2006, IEEE, 2006, pp. 392\u2013393. https:\/\/doi.org\/10.1109\/wodes.2006.382402","DOI":"10.1109\/wodes.2006.382402"},{"key":"7765_CR43","doi-asserted-by":"publisher","first-page":"5794","DOI":"10.1016\/j.ifacol.2017.08.427","volume":"50","author":"R. Malik","year":"2017","unstructured":"Malik, R., \u00c5kesson, K., Flordal, H., and Fabian, M., Supremica\u2013An efficient tool for large-scale discrete event systems, IFAC-PapersOnLine, 2017, vol. 50, no. 1, pp. 5794\u20135799. https:\/\/doi.org\/10.1016\/j.ifacol.2017.08.427","journal-title":"IFAC-PapersOnLine"},{"key":"7765_CR44","doi-asserted-by":"publisher","unstructured":"\u00c5kesson, K., Flordal, H., and Fabian, M., Exploiting modularity for synthesis and verification of supervisors, IFAC Proc. Volumes, 2002, vol. 35, no. 1, pp. 175\u2013180. https:\/\/doi.org\/10.3182\/20020721-6-es-1901.00517","DOI":"10.3182\/20020721-6-es-1901.00517"},{"key":"7765_CR45","doi-asserted-by":"publisher","first-page":"387","DOI":"10.1109\/tcst.2004.824795","volume":"12","author":"B.A. Brandin","year":"2004","unstructured":"Brandin, B.A., Malik, R., and Malik, P., Incremental verification and synthesis of discrete-event systems guided by counter examples, IEEE Trans. Control Syst. Technol., 2004, vol. 12, no. 3, pp. 387\u2013401. https:\/\/doi.org\/10.1109\/tcst.2004.824795","journal-title":"IEEE Trans. Control Syst. Technol."},{"key":"7765_CR46","doi-asserted-by":"publisher","first-page":"150","DOI":"10.1109\/tac.2013.2283109","volume":"59","author":"S. Mohajerani","year":"2013","unstructured":"Mohajerani, S., Malik, R., and Fabian, M., A framework for compositional synthesis of modular nonblocking supervisors, IEEE Trans. Autom. Control, 2013, vol. 59, no. 1, pp. 150\u2013162. https:\/\/doi.org\/10.1109\/tac.2013.2283109","journal-title":"IEEE Trans. Autom. Control"},{"key":"7765_CR47","doi-asserted-by":"publisher","unstructured":"Bourbaki, N., Theory of Sets, Hermann, 1968. https:\/\/doi.org\/10.1007\/978-3-642-59309-3","DOI":"10.1007\/978-3-642-59309-3"},{"key":"7765_CR48","doi-asserted-by":"publisher","first-page":"556","DOI":"10.15827\/0236-235X.128.556-564","volume":"32","author":"A. Larionov","year":"2019","unstructured":"Larionov, A., Davydov, A., and Cherkashin, E., The method for translating first-order logic formulas into positively constructed formulas, Software Syst., 2019, vol. 32, no. 4, pp. 556\u2013564. https:\/\/doi.org\/10.15827\/0236-235X.128.556-564","journal-title":"Software Syst."},{"key":"7765_CR49","doi-asserted-by":"publisher","first-page":"402","DOI":"10.3103\/s0146411611070054","volume":"45","author":"A.V. Davydov","year":"2011","unstructured":"Davydov, A.V., Larionov, A.A., and Cherkashin, E.A., On the calculus of positively constructed formulas for automated theorem proving, Autom. Control Comput. Sci., 2011, vol. 45, no. 7, pp. 402\u2013407. https:\/\/doi.org\/10.3103\/s0146411611070054","journal-title":"Autom. Control Comput. Sci."},{"key":"7765_CR50","doi-asserted-by":"publisher","first-page":"7894","DOI":"10.3390\/app10217894","volume":"10","author":"S. Ulyanov","year":"2020","unstructured":"Ulyanov, S., Bychkov, I., and Maksimkin, N., Event-based path-planning and path-following in unknown environments for underactuated autonomous underwater vehicles, Appl. Sci., 2020, vol. 10, no. 21, p. 7894. https:\/\/doi.org\/10.3390\/app10217894","journal-title":"Appl. Sci."}],"container-title":["Automatic Control and Computer Sciences"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.3103\/S0146411624700445.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.3103\/S0146411624700445","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.3103\/S0146411624700445.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,3,15]],"date-time":"2026-03-15T22:01:20Z","timestamp":1773612080000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.3103\/S0146411624700445"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,12]]},"references-count":50,"journal-issue":{"issue":"7","published-print":{"date-parts":[[2024,12]]}},"alternative-id":["7765"],"URL":"https:\/\/doi.org\/10.3103\/s0146411624700445","relation":{},"ISSN":["0146-4116","1558-108X"],"issn-type":[{"value":"0146-4116","type":"print"},{"value":"1558-108X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,12]]},"assertion":[{"value":"2 February 2024","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"8 February 2024","order":2,"name":"revised","label":"Revised","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"14 February 2024","order":3,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"12 February 2025","order":4,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"The authors of this work declare that they have no conflicts of interest.","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"CONFLICT OF INTEREST"}}]}}