Controller synthesis for reactive systems in distributed, real-time and hybrid settings

We investigate controller synthesis in distributed, real-time and hybrid settings. In distributed setting, we prove that the monadic second order theory of the event structure unfolding of every system of connectedly communicating processes (CCP) is decidable. With this, we show that the distributed controller synthesis problem with CCPs is decidable for robust linear time specifications. And if distributed controllers exist, then finite state ones can be effectively synthesized. In real-time setting, we establish the decidability of admission controller synthesis with the preemptive EDF scheduling policy on a single processor; for both linear time temporal logic (LTL) or quantified propositional LTL (QPLTL) specifications. In hybrid setting, we show the decidability of controller synthesis for restricted differential hybrid automata (with no sensing delay), for both LTL and QPLTL specifications. In both real-time and hybrid settings, we prove that, if controllers exist, then finite state ones can be effectively synthesized.

Author dc:creator

• YANG SHAOFA

• open systems, controller synthesis, distributed systems, logic for concurrency, real-time systems, hybrid systems