Maximally permissive controlled system synthesis for modal logic

Allan C. van Hulst, Michel A. Reniers, Wan Fokkink

Research output: Chapter in Book / Report / Conference proceedingConference contributionAcademicpeer-review

Abstract

We propose a new method for controlled system synthesis on non-deterministic automata, which includes the synthesis for deadlock-freeness, as well as invariant and reachability expressions. Our technique restricts the behavior of a Kripke-structure with labeled transitions, representing the uncontrolled system, such that it adheres to a given requirement specification in an expressive modal logic, while all non-invalidating behavior is retained. This induces maximal permissiveness in the context of supervisory control. Research presented in this paper allows a system model to be constrained according to a broad set of liveness, safety and fairness specifications of desired behavior, and embraces most concepts from Ramadge-Wonham supervisory control, including controllability and marker-state reachability. The synthesis construction is formally verified using the Coq proof assistant.
Original languageEnglish
Title of host publicationSOFSEM 2015: Theory and Practice of Computer Science - 41st International Conference on Current Trends in Theory and Practice of Computer Science
PublisherSpringer/Verlag
Pages230-241
Number of pages12
Volume8939
ISBN (Electronic)9783662460771
Publication statusPublished - 2015
Event41st International Conference on Current Trends in Theory and Practice of Computer Science, SOFSEM 2015 - Pec pod Sněžkou, Czech Republic
Duration: 24 Jan 201529 Jan 2015

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume8939
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference41st International Conference on Current Trends in Theory and Practice of Computer Science, SOFSEM 2015
CountryCzech Republic
CityPec pod Sněžkou
Period24/01/1529/01/15

Fingerprint Dive into the research topics of 'Maximally permissive controlled system synthesis for modal logic'. Together they form a unique fingerprint.

Cite this