Back to Search Start Over

Analysis and Control of Partially Observed Discrete-Event Systems via Positively Constructed Formulas

Authors :
Artem Davydov
Aleksandr Larionov
Nadezhda Nagul
Source :
Computation, Vol 12, Iss 5, p 95 (2024)
Publication Year :
2024
Publisher :
MDPI AG, 2024.

Abstract

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.

Details

Language :
English
ISSN :
20793197
Volume :
12
Issue :
5
Database :
Directory of Open Access Journals
Journal :
Computation
Publication Type :
Academic Journal
Accession number :
edsdoj.fdb8eeb5e319407282acfd41f0583d95
Document Type :
article
Full Text :
https://doi.org/10.3390/computation12050095