Assume-Guarantee (A/G) contracts are a well established paradigm for dealing with large-scale decentralized systems and have a longstanding history and well established theoretical foundations. Its main idea is to decouple dependent decentralized processes, or subsystems, by making use of a set of compatible local contracts consisting of an assumption and a guarantee. If the rest of the system fulfills a process’ assumption, this process must ensure its local guarantee holds, which in turn implies that the corresponding assumptions induced on the others also hold. The implications of this methodology are very appealing from a practical perspective, as they allow for (i) efficient design, i.e., local controllers can be synthesized in a decentralized and concurrent fashion; (ii) information integrity, meaning that, apart from what is specified by the contracts, no detailed information about a local behavior is shared with the rest of the plant; and (iii) decoupled maintenance, as contract-compatible adaptations in a component do not affect others.
Motivated by these desirable features, we develop an assume-guarantee synthesis framework for supervisory control of decentralized discrete event systems. The setting of decentralized supervisory control uses a substantially different model of process synchronization than reactive synthesis (see this page for our work on the connection between supervisory control and reactive synthesis for monolithic synthesis).
In particular, this line of works uses synchronized deterministic finite automata (DFA) over finite words as system models, compared to input/output ω-automata over infinite words. Here, the synchronisation of DFA ensures that liveness requirements, encoded by marked states in the involved automata, must be enforced by all subsystems at the same time. Furthermore, synchronisation of automata leads to blocking situations in a decentralized setting – which requires special attention – while interacting input/output ω-automata never block.
Group Members Involved:
Publications:
- A. M. Mainhardt and A.-K. Schmuck. Synthesis of Decentralized Supervisory Control via Contract Negotiation. 2023. (journal version, under review, PrePrint)
- A. Mainhardt and A.-K. Schmuck. Assume-Guarantee Synthesis of Decentralized Supervisory Control. WODES’22. 2022. (extended version) (best student paper award)