Back to Search
Start Over
Analysis and Control of Partially Observed Discrete-Event Systems via Positively Constructed Formulas
- 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