Supremal Marker-Controllable Subformula of a Given Canonical Temporal-Safety Formula
The existence of marker-progressive supervisory control – about ensuring constant marker progress under specified temporal safety for a class of fair discrete-event systems (DES’s) – is a new control problem formulation that has been studied in terms of DES marker-co...
| Main Author: | |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
IEEE
2022-01-01
|
| Series: | IEEE Access |
| Subjects: | |
| Online Access: | https://ieeexplore.ieee.org/document/9796506/ |
| _version_ | 1811332798829559808 |
|---|---|
| author | Kiam Tian Seow |
| author_facet | Kiam Tian Seow |
| author_sort | Kiam Tian Seow |
| collection | DOAJ |
| description | The existence of marker-progressive supervisory control – about ensuring constant marker progress under specified temporal safety for a class of fair discrete-event systems (DES’s) – is a new control problem formulation that has been studied in terms of DES marker-controllability of a linear-time temporal logic (LTL) safety formula given in canonical form. In this paper, provided it exists, the supremal marker-controllable subformula of a given canonical temporal-safety formula for the fair DES model considered is characterized as the weakest fixpoint of some monotone operator <inline-formula> <tex-math notation="LaTeX">$\Omega $ </tex-math></inline-formula>. In the case where the DES model is finite state and the complete specification for constant marker progress under temporal safety is a formula of a decidable LTL fragment, it is shown that this fixpoint can be computed as the limit of the (finite) sequence of iterations of computing operator <inline-formula> <tex-math notation="LaTeX">$\Omega $ </tex-math></inline-formula> in the syntax of LTL. Marker-progressive control synthesis by fixpoint computation can therefore be made in the same natural-language motivated algebra of LTL as writing the specification, providing the unique opportunity to exploit not only the role of fair events in DES’s, but also the human readability of LTL formulas and the associated, syntax-based calculational approach that is transparent; such fixpoint computation is illustrated with four examples. A discussion examines and illuminates the significance of this paper and its potential impact on the logic foundation of supervisory control; it includes making comparisons with related work, and explaining a straightforward generalization of DES marker-controllability that directly extends the proposed fixpoint computation to cover the full specification hierarchy of canonical LTL. |
| first_indexed | 2024-04-13T16:42:23Z |
| format | Article |
| id | doaj.art-ffabbb2a8e5e4a33b74f11d95c8b33fe |
| institution | Directory Open Access Journal |
| issn | 2169-3536 |
| language | English |
| last_indexed | 2024-04-13T16:42:23Z |
| publishDate | 2022-01-01 |
| publisher | IEEE |
| record_format | Article |
| series | IEEE Access |
| spelling | doaj.art-ffabbb2a8e5e4a33b74f11d95c8b33fe2022-12-22T02:39:12ZengIEEEIEEE Access2169-35362022-01-0110663006632010.1109/ACCESS.2022.31831989796506Supremal Marker-Controllable Subformula of a Given Canonical Temporal-Safety FormulaKiam Tian Seow0https://orcid.org/0000-0001-5784-1132Robot Intelligence Technology Laboratory, School of Electrical Engineering, KAIST, Daejeon, South KoreaThe existence of marker-progressive supervisory control – about ensuring constant marker progress under specified temporal safety for a class of fair discrete-event systems (DES’s) – is a new control problem formulation that has been studied in terms of DES marker-controllability of a linear-time temporal logic (LTL) safety formula given in canonical form. In this paper, provided it exists, the supremal marker-controllable subformula of a given canonical temporal-safety formula for the fair DES model considered is characterized as the weakest fixpoint of some monotone operator <inline-formula> <tex-math notation="LaTeX">$\Omega $ </tex-math></inline-formula>. In the case where the DES model is finite state and the complete specification for constant marker progress under temporal safety is a formula of a decidable LTL fragment, it is shown that this fixpoint can be computed as the limit of the (finite) sequence of iterations of computing operator <inline-formula> <tex-math notation="LaTeX">$\Omega $ </tex-math></inline-formula> in the syntax of LTL. Marker-progressive control synthesis by fixpoint computation can therefore be made in the same natural-language motivated algebra of LTL as writing the specification, providing the unique opportunity to exploit not only the role of fair events in DES’s, but also the human readability of LTL formulas and the associated, syntax-based calculational approach that is transparent; such fixpoint computation is illustrated with four examples. A discussion examines and illuminates the significance of this paper and its potential impact on the logic foundation of supervisory control; it includes making comparisons with related work, and explaining a straightforward generalization of DES marker-controllability that directly extends the proposed fixpoint computation to cover the full specification hierarchy of canonical LTL.https://ieeexplore.ieee.org/document/9796506/Fair discrete-event systemslinear-time temporal logicsupervisory control |
| spellingShingle | Kiam Tian Seow Supremal Marker-Controllable Subformula of a Given Canonical Temporal-Safety Formula IEEE Access Fair discrete-event systems linear-time temporal logic supervisory control |
| title | Supremal Marker-Controllable Subformula of a Given Canonical Temporal-Safety Formula |
| title_full | Supremal Marker-Controllable Subformula of a Given Canonical Temporal-Safety Formula |
| title_fullStr | Supremal Marker-Controllable Subformula of a Given Canonical Temporal-Safety Formula |
| title_full_unstemmed | Supremal Marker-Controllable Subformula of a Given Canonical Temporal-Safety Formula |
| title_short | Supremal Marker-Controllable Subformula of a Given Canonical Temporal-Safety Formula |
| title_sort | supremal marker controllable subformula of a given canonical temporal safety formula |
| topic | Fair discrete-event systems linear-time temporal logic supervisory control |
| url | https://ieeexplore.ieee.org/document/9796506/ |
| work_keys_str_mv | AT kiamtianseow supremalmarkercontrollablesubformulaofagivencanonicaltemporalsafetyformula |