A theory of desynchronisable closed loop system
Harsh Beohar (TU/e), Pieter Cuijpers (TU/e)

TL;DR
This paper addresses the challenge of implementing supervisory controllers in asynchronous systems by establishing conditions under which synchronous control systems can be accurately refined into asynchronous implementations using process algebra.
Contribution
It introduces a framework for constructing asynchronous closed loop systems from synchronous ones and provides conditions for their behavioral equivalence.
Findings
Established sufficient conditions for branching bisimilarity between synchronous and asynchronous systems
Proposed a process algebraic approach to model asynchronous control systems
Addressed the inexact synchronisation problem in supervisory control implementations
Abstract
The task of implementing a supervisory controller is non-trivial, even though different theories exist that allow automatic synthesis of these controllers in the form of automata. One of the reasons for this discord is due to the asynchronous interaction between a plant and its controller in implementations, whereas the existing supervisory control theories assume synchronous interaction. As a consequence the implementation suffer from the so-called inexact synchronisation problem. In this paper we address the issue of inexact synchronisation in a process algebraic setting, by solving a more general problem of refinement. We construct an asynchronous closed loop system by introducing a communication medium in a given synchronous closed loop system. Our goal is to find sufficient conditions under which a synchronous closed loop system is branching bisimilar to its corresponding…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsPetri Nets in System Modeling · semigroups and automata theory · Formal Methods in Verification
