maisМоделирование и анализ информационных системModeling and Analysis of Information Systems1818-10152313-5417Yaroslavl State University10.18255/1818-1015-2024-1-54-77mais-1838Research ArticleTheory of ComputingО применении исчисления позитивно-образованных формул для исследования управляемых дискретно-событийных системOn the application of the calculus of positively constructed formulas for the study of controlled discrete-event systemshttps://orcid.org/0000-0002-8703-3096ДавыдовАртем ВасильевичDavydovArtem Васильевичartem@icc.ruhttps://orcid.org/0000-0001-7116-9338ЛарионовАлександр АлександровичLarionovAleksandr A.bootfrost@zoho.comhttps://orcid.org/0000-0003-1439-3274НагулНадежда ВладимировнаNagulNadezhda V.sapling@icc.ruИнститут динамики систем и теории управления им. В.М. Матросова СО РАНРоссияMatrosov Institute for System Dynamics and Control Theory SB RASRussian Federation2024280320243115477Copyright © Давыдов А.В., Ларионов А.А., Нагул Н.В., 20242024Давыдов А.В., Ларионов А.А., Нагул Н.В.Davydov A.В., Larionov A.A., Nagul N.V.Данная работа распространяется под лицензией Creative Commons Attribution 4.0.This work is licensed under a Creative Commons Attribution 4.0 License.https://www.mais-journal.ru/jour/article/view/1838

Статья посвящена разработке подхода к решению основных задач теории супервизорного управления логическими дискретно-событийными системами (ДСС), основанного на представлении их в виде позитивно-образованных формул (ПОФ). Рассматриваются логические ДСС в автоматной форме, понимаемые как генераторы некоторых регулярных языков. Язык ПОФ представляет собой полный язык первого порядка, формулы которого имеют регулярную структуру из чередующихся типовых кванторов и не содержат в синтаксисе оператора отрицания. Ранее было доказано, что любая формула классического исчисления предикатов первого порядка может быть представлена в виде ПОФ. ПОФ имеют наглядное древовидное представление и естественную вопросно-ответную процедуру поиска вывода с помощью единственного правила вывода. Показано, как разработанное в 1990-х годах для решения некоторых задач управления динамическими системами исчисление ПОФ позволяет решать базовые задачи теории супервизорного управления, такие как проверка критериев существования супервизорного управления, автоматическая модификация ограничений на поведение управляемой системы и реализация супервизора. Благодаря некоторым особенностям исчисления ПОФ существует возможность применения немонотонного вывода. Продемонстрировано, как представленный метод на основе ПОФ позволяет выполнять дополнительную обработку событий во время логического вывода. Также представлена программная система Bootfrost, или так называемый прувер, разработанный для опровержения полученных ПОФ, кратко описываются особенности его реализации. В качестве иллюстративного примера рассматривается задача управления автономным мобильным роботом.

The article is devoted to the development of an approach to solving the main problems of the theory of supervisory control of logical discrete-event systems (DES), based on their representation in the form of positively constructed formulas (PCF). We consider logical DESs in automata form, understood as generators of some regular languages. The PCF language is a complete first-order language, the formulas of which have a regular structure of alternating type quantifiers and do not contain a negation operator in the syntax. It was previously proven that any formula of the classical first-order predicate calculus can be represented as a PCF. PCFs have a visual tree representation and a natural question-and-answer procedure for searching for an inference using a single inference rule. It is shown how the PCF calculus, developed in the 1990s to solve some problems of control of dynamic systems, makes it possible to solve basic problems of the theory of supervisory control, such as checking the criteria for the existence of supervisory control, automatically modifying restrictions on the behavior of the controlled system, and implementing a supervisor. Due to some features of the PCF calculus, it is possible to use a non-monotonic inference. It is demonstrated how the presented PCF-based method allows for additional event processing during inference. The Bootfrost software system, or the so-called prover, designed to refute the obtained PCFs is also presented, and the features of its implementation are briefly described. As an illustrative example, we consider the problem of controlling an autonomous mobile robot.

позитивно-образованная формулаавтоматическое доказательство теоремпрувердискретно-событийная системасупервизорное управлениеpositively constructed formulaautomated theorem provingproverdiscrete event systemsupervisory controlМинистерство науки и высшего образования РФ (121032400051-9).Ministry of Science and Higher Education of the Russian Federation (121032400051-9).ReferencesS. 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.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.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.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.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.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.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.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.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.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.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.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.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.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.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. Gross, “Supervisory control theory applied to swarm robotics,” Swarm Intelligence, vol. 10, no. 1, pp. 65–97, 2016.Y. K. Lopes, S. M. Trenkwalder, A. B. Leal, T. J. Dodd, and R. Gross, “Supervisory control theory applied to swarm robotics,” Swarm Intelligence, vol. 10, no. 1, pp. 65–97, 2016.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.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: doi:10.1017/fmp.2017.1.T. Hales et al., “A formal proof of the Kepler conjecture,” in Forum of mathematics, Pi, 2017, vol. 5, p. e2, doi: 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. 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.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.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.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.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.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.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.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.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.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.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.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 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.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.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.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.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, “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.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. Bjorner and L. Nachmanson, “Navigating the Universe of Z3 Theory Solvers,” in Formal Methods: Foundations and Applications, 2020, pp. 8–24, doi: https://doi.org/10.1007/978-3-030-63882-5_2.N. Bjorner and L. Nachmanson, “Navigating the Universe of Z3 Theory Solvers,” in Formal Methods: Foundations and Applications, 2020, pp. 8–24, doi: https://doi.org/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.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.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.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.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.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.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.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.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.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. 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.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.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.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.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.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.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. 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.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.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.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.

The authors declare that there are no conflicts of interest present.