Geodesic
On the application of the calculus of positively constructed formulas for the study of controlled discrete-event systems
Modelirovanie i analiz informacionnyh sistem, Tome 31 (2024) no. 1, pp. 54-77

Voir la notice de l'article provenant de la source Math-Net.Ru

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.
Keywords: positively constructed formula, automated theorem proving, prover, discrete event system, supervisory control. 
@article{MAIS_2024_31_1_a2,
     author = {A. V. Davydov and A. A. Larionov and N. V. Nagul},
     title = {On the application of the calculus of positively constructed formulas for the study of controlled discrete-event systems},
     journal = {Modelirovanie i analiz informacionnyh sistem},
     pages = {54--77},
     publisher = {mathdoc},
     volume = {31},
     number = {1},
     year = {2024},
     language = {ru},
     url = {http://geodesic.mathdoc.fr/item/MAIS_2024_31_1_a2/}
}
TY  - JOUR
AU  - A. V. Davydov
AU  - A. A. Larionov
AU  - N. V. Nagul
TI  - On the application of the calculus of positively constructed formulas for the study of controlled discrete-event systems
JO  - Modelirovanie i analiz informacionnyh sistem
PY  - 2024
SP  - 54
EP  - 77
VL  - 31
IS  - 1
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/MAIS_2024_31_1_a2/
LA  - ru
ID  - MAIS_2024_31_1_a2
ER  - 
%0 Journal Article
%A A. V. Davydov
%A A. A. Larionov
%A N. V. Nagul
%T On the application of the calculus of positively constructed formulas for the study of controlled discrete-event systems
%J Modelirovanie i analiz informacionnyh sistem
%D 2024
%P 54-77
%V 31
%N 1
%I mathdoc
%U http://geodesic.mathdoc.fr/item/MAIS_2024_31_1_a2/
%G ru
%F MAIS_2024_31_1_a2
A. V. Davydov; A. A. Larionov; N. V. Nagul. On the application of the calculus of positively constructed formulas for the study of controlled discrete-event systems. Modelirovanie i analiz informacionnyh sistem, Tome 31 (2024) no. 1, pp. 54-77. http://geodesic.mathdoc.fr/item/MAIS_2024_31_1_a2/