A Compositional Framework for Controller Synthesis

Christel BaierChristel Baier, Joachim KleinJoachim Klein, Sascha KlüppelholzSascha Klüppelholz

DOI Link

Christel Baier, Joachim Klein, Sascha Klüppelholz
A Compositional Framework for Controller Synthesis
Proc. of the 22nd International Conference on Concurrency Theory (CONCUR'11), volume 6901 of Lecture Notes in Computer Science, 512--527, 2011. Springer

Details
Bibtex

KurzfassungAbstract
Given a system A and objective Φ, the general task of controller synthesis is to design a decision making policy that ensures Φ to be satisfied. This paper deals with LTS-like system models and controllers that make their decisions based on the observables of the actions performed so far. Our main contribution is a compositional framework for treating multiple linear-time objectives inductively. For this purpose, we introduce a novel notion of strategies that serve as generators for observation-based decision functions. Our compositional approach will rely on most general (i.e., most permissive) strategies generating all decision functions that guarantee the objective under consideration. Finally we show that for safety and co-safety objectives Φ, most general strategies are realizable by finite-state controllers that exogenously enforce Φ.
Forschungsgruppe:Research Group: Verifikation und formale quantitative Analyse„Verifikation und formale quantitative Analyse“ befindet sich nicht in der Liste (Computational Logic, Automatentheorie, Wissensverarbeitung, Knowledge-Based Systems, Knowledge Systems, Wissensbasierte Systeme, Logische Programmierung und Argumentation, Algebra und Diskrete Strukturen, Knowledge-aware Artificial Intelligence, Algebraische und logische Grundlagen der Informatik) zulässiger Werte für das Attribut „Forschungsgruppe“.Algebraic and Logical Foundations of Computer Science

The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-642-23217-6_34.

@inproceedings{BKK2011,
  author    = {Christel Baier and Joachim Klein and Sascha Kl{\"{u}}ppelholz},
  title     = {A Compositional Framework for Controller Synthesis},
  booktitle = {Proc. of the 22nd International Conference on Concurrency Theory
               (CONCUR'11)},
  series    = {Lecture Notes in Computer Science},
  volume    = {6901},
  publisher = {Springer},
  year      = {2011},
  pages     = {512--527},
  doi       = {10.1007/978-3-642-23217-6_34}
}