Maximally permissive controlled system synthesis for non-determinism and modal logic

A. C. van Hulst, M.A. Reniers, W. J. Fokkink

Research output: Contribution to JournalArticleAcademicpeer-review

Abstract

We propose a new technique for controlled system synthesis on non-deterministic automata for requirements in modal logic. Synthesis, as defined in this paper, restricts a behavioral specification of the uncontrolled system such that it satisfies a given logical expression, while adhering to the rules dictated by supervisory control such as maximal permissiveness and controllability. The applied requirement formalism extends Hennessy-Milner logic with the invariant and reachability modalities from Gödel-Löb logic, and is therefore able to express a broad range of control requirements, such as marker state reachability and deadlock-freeness. This paper contributes to the field of control synthesis by achieving maximal permissiveness in a non-deterministic context for control requirements in modal logic, and treatment of controllability via partial bisimulation. We present a well-defined and complete derivation of the synthesis result, which is supported further by computer-verified proofs created using the Coq proof assistant. The synthesis method is also presented in algorithmic form, including an analysis of its computational complexity. We show that the proposed synthesis theory allows full expressibility of Ramadge-Wonham supervisory control theory and we illustrate its applicability in two small industrial case studies, including an analysis with regard to scalability.

Original languageEnglish
Pages (from-to)109-142
Number of pages34
JournalDiscrete Event Dynamic Systems
Volume27
Issue number1
DOIs
Publication statusPublished - 1 Mar 2017

Fingerprint

Nondeterminism
Modal Logic
Synthesis
Supervisory Control
Requirements
Reachability
Controllability
Logic
Bisimulation
Deadlock
Control theory
Control Theory
Modality
Automata
Scalability
Well-defined
Computational complexity
Computational Complexity
Express
Specification

Keywords

  • Controllability
  • Controlled system synthesis
  • Maximal permissiveness
  • Modal logic
  • Non-determinism
  • Partial bisimulation

Cite this

@article{85e582187b144f4c813a852e6858ceac,
title = "Maximally permissive controlled system synthesis for non-determinism and modal logic",
abstract = "We propose a new technique for controlled system synthesis on non-deterministic automata for requirements in modal logic. Synthesis, as defined in this paper, restricts a behavioral specification of the uncontrolled system such that it satisfies a given logical expression, while adhering to the rules dictated by supervisory control such as maximal permissiveness and controllability. The applied requirement formalism extends Hennessy-Milner logic with the invariant and reachability modalities from G{\"o}del-L{\"o}b logic, and is therefore able to express a broad range of control requirements, such as marker state reachability and deadlock-freeness. This paper contributes to the field of control synthesis by achieving maximal permissiveness in a non-deterministic context for control requirements in modal logic, and treatment of controllability via partial bisimulation. We present a well-defined and complete derivation of the synthesis result, which is supported further by computer-verified proofs created using the Coq proof assistant. The synthesis method is also presented in algorithmic form, including an analysis of its computational complexity. We show that the proposed synthesis theory allows full expressibility of Ramadge-Wonham supervisory control theory and we illustrate its applicability in two small industrial case studies, including an analysis with regard to scalability.",
keywords = "Controllability, Controlled system synthesis, Maximal permissiveness, Modal logic, Non-determinism, Partial bisimulation",
author = "{van Hulst}, {A. C.} and M.A. Reniers and Fokkink, {W. J.}",
year = "2017",
month = "3",
day = "1",
doi = "10.1007/s10626-016-0231-8",
language = "English",
volume = "27",
pages = "109--142",
journal = "Discrete Event Dynamic Systems",
issn = "0924-6703",
publisher = "Springer Netherlands",
number = "1",

}

Maximally permissive controlled system synthesis for non-determinism and modal logic. / van Hulst, A. C.; Reniers, M.A.; Fokkink, W. J.

In: Discrete Event Dynamic Systems, Vol. 27, No. 1, 01.03.2017, p. 109-142.

Research output: Contribution to JournalArticleAcademicpeer-review

TY - JOUR

T1 - Maximally permissive controlled system synthesis for non-determinism and modal logic

AU - van Hulst, A. C.

AU - Reniers, M.A.

AU - Fokkink, W. J.

PY - 2017/3/1

Y1 - 2017/3/1

N2 - We propose a new technique for controlled system synthesis on non-deterministic automata for requirements in modal logic. Synthesis, as defined in this paper, restricts a behavioral specification of the uncontrolled system such that it satisfies a given logical expression, while adhering to the rules dictated by supervisory control such as maximal permissiveness and controllability. The applied requirement formalism extends Hennessy-Milner logic with the invariant and reachability modalities from Gödel-Löb logic, and is therefore able to express a broad range of control requirements, such as marker state reachability and deadlock-freeness. This paper contributes to the field of control synthesis by achieving maximal permissiveness in a non-deterministic context for control requirements in modal logic, and treatment of controllability via partial bisimulation. We present a well-defined and complete derivation of the synthesis result, which is supported further by computer-verified proofs created using the Coq proof assistant. The synthesis method is also presented in algorithmic form, including an analysis of its computational complexity. We show that the proposed synthesis theory allows full expressibility of Ramadge-Wonham supervisory control theory and we illustrate its applicability in two small industrial case studies, including an analysis with regard to scalability.

AB - We propose a new technique for controlled system synthesis on non-deterministic automata for requirements in modal logic. Synthesis, as defined in this paper, restricts a behavioral specification of the uncontrolled system such that it satisfies a given logical expression, while adhering to the rules dictated by supervisory control such as maximal permissiveness and controllability. The applied requirement formalism extends Hennessy-Milner logic with the invariant and reachability modalities from Gödel-Löb logic, and is therefore able to express a broad range of control requirements, such as marker state reachability and deadlock-freeness. This paper contributes to the field of control synthesis by achieving maximal permissiveness in a non-deterministic context for control requirements in modal logic, and treatment of controllability via partial bisimulation. We present a well-defined and complete derivation of the synthesis result, which is supported further by computer-verified proofs created using the Coq proof assistant. The synthesis method is also presented in algorithmic form, including an analysis of its computational complexity. We show that the proposed synthesis theory allows full expressibility of Ramadge-Wonham supervisory control theory and we illustrate its applicability in two small industrial case studies, including an analysis with regard to scalability.

KW - Controllability

KW - Controlled system synthesis

KW - Maximal permissiveness

KW - Modal logic

KW - Non-determinism

KW - Partial bisimulation

UR - http://www.scopus.com/inward/record.url?scp=84988699966&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84988699966&partnerID=8YFLogxK

U2 - 10.1007/s10626-016-0231-8

DO - 10.1007/s10626-016-0231-8

M3 - Article

VL - 27

SP - 109

EP - 142

JO - Discrete Event Dynamic Systems

JF - Discrete Event Dynamic Systems

SN - 0924-6703

IS - 1

ER -