Maximally Permissive Controlled System Synthesis for Modal Logic

TL;DR

This paper introduces a formal method for synthesizing maximally permissive controlled systems on non-deterministic automata, ensuring adherence to complex modal logic specifications while retaining all non-invalidating behaviors.

Contribution

It presents a novel synthesis technique that guarantees maximal permissiveness under broad modal logic specifications, extending supervisory control concepts to non-deterministic systems.

Findings

Validated correctness using Coq proof assistant

Supports broad set of liveness, safety, and fairness specifications

Ensures maximal permissiveness in controlled system synthesis

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. Synthesis is defined in this paper as a formal construction, which allowed a careful validation of its correctness using the Coq proof assistant.