Modelirovanie i Analiz Informatsionnykh Sistem
RUS  ENG    JOURNALS   PEOPLE   ORGANISATIONS   CONFERENCES   SEMINARS   VIDEO LIBRARY   PACKAGE AMSBIB  
General information
Latest issue
Archive
Impact factor

Search papers
Search references

RSS
Latest issue
Current issues
Archive issues
What is RSS



Model. Anal. Inform. Sist.:
Year:
Volume:
Issue:
Page:
Find






Personal entry:
Login:
Password:
Save password
Enter
Forgotten password?
Register


Modelirovanie i Analiz Informatsionnykh Sistem, 2024, Volume 31, Number 1, Pages 54–77
DOI: https://doi.org/10.18255/1818-1015-2024-1-54-77
(Mi mais815)
 

Theory of computing

On the application of the calculus of positively constructed formulas for the study of controlled discrete-event systems

A. V. Davydov, A. A. Larionov, N. V. Nagul

Matrosov Institute for System Dynamics and Control Theory SB RAS
References:
Abstract: 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.
Funding agency Grant number
Ministry of Science and Higher Education of the Russian Federation 121032400051-9
Ministry of Science and Higher Education of the Russian Federation (121032400051-9).
Received: 02.02.2024
Revised: 08.02.2024
Accepted: 14.02.2024
Document Type: Article
UDC: 004.832.3
MSC: 68V15, 93C65
Language: Russian
Citation: 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”, Model. Anal. Inform. Sist., 31:1 (2024), 54–77
Citation in format AMSBIB
\Bibitem{DavLarNag24}
\by A.~V.~Davydov, A.~A.~Larionov, N.~V.~Nagul
\paper On the application of the calculus of positively constructed formulas for the study of controlled discrete-event systems
\jour Model. Anal. Inform. Sist.
\yr 2024
\vol 31
\issue 1
\pages 54--77
\mathnet{http://mi.mathnet.ru/mais815}
\crossref{https://doi.org/10.18255/1818-1015-2024-1-54-77}
Linking options:
  • https://www.mathnet.ru/eng/mais815
  • https://www.mathnet.ru/eng/mais/v31/i1/p54
  • Citing articles in Google Scholar: Russian citations, English citations
    Related articles in Google Scholar: Russian articles, English articles
    Моделирование и анализ информационных систем
    Statistics & downloads:
    Abstract page:38
    Full-text PDF :26
    References:13
     
      Contact us:
     Terms of Use  Registration to the website  Logotypes © Steklov Mathematical Institute RAS, 2024