Compositional Synthesis and Most General Controllers

Joachim KleinJoachim Klein

Joachim Klein
Compositional Synthesis and Most General Controllers
Phd thesis

Details
Bibtex

KurzfassungAbstract
Given a formal model of the behavior of a system, an objective and some notion of control the goal of controller synthesis [RW87, Won89] is to construct a (finite-state) controller that ensures that the system always satisfies the objective. Often, the controller can base its decisions only on limited observations of the system. This notion of limited observability induces a partial-information game between the controller and the uncontrollable part of the system. A successful controller then realizes an observation-based strategy that enforces the objective. In this thesis we consider the controller synthesis problem in the linear-time setting where the behavior of the system is given as a nondeterministic, labeled transitions system A, where the controller can only partially observe and control the behavior of A. The goal of the thesis is to develop a compositional approach for constructing controllers, suitable to treat conjunctive cascades of linear-time objectives Φ1, Φ2,..., Φk in an online manner. We iteratively construct a controller C1 for system A enforcing Φ1, then a controller C2 enforcing Φ2 for the parallel composition of the first controller with the system, ie, C1⊳⊲ A, and so on. It is crucial for this approach that each controller Ci enforces Φi in a most general manner, being as permissive as possible. Otherwise, behavior that is needed to enforce subsequent objectives could be prematurely removed.
Forschungsgruppe:Research Group: Algebraische und logische Grundlagen der InformatikAlgebraic and Logical Foundations of Computer Science

@phdthesis{K2025,
  author = {Joachim Klein},
  title  = {Compositional Synthesis and Most General Controllers},
  year   = {2025}
}