Joachim Klein

Compositional Synthesis and Most General Controllers

Dokumente und Dateien


Bitte nutzen Sie beim Zitieren immer folgende Url:

Kurzfassung in Englisch

Given a formal model of the behavior of a system, an objective and some notion of control the goal of controller synthesis 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 P_1, P_2, ..., P_k in an online manner. We iteratively construct a controller C_1 for system A enforcing P_1, then a controller C_2 enforcing P_2 for the parallel composition of the first controller with the system, and so on. It is crucial for this approach that each controller C_i enforces P_i in a most general manner, being as permissive as possible. Otherwise, behavior that is needed to enforce subsequent objectives could be prematurely removed.

Standard notions of strategies and controllers only allow the most general treatment for the limited class of safety objectives. We introduce a novel concept of most general strategies and controllers suited for the compositional treatment of objectives beyond safety. We demonstrate the existence of most general controllers for all enforceable, observation-based omega-regular objectives and provide algorithms for the construction of such most general controllers, with specialized variants for the subclass of safety and co-safety objectives.

We furthermore adapt and apply our general framework for the compositional synthesis of most general controllers to the setting of exogenous coordination in the context of the channel-based coordination language Reo and the constraint automata framework and report on our implementation in the verification toolset Vereofy.

The construction of most general controllers in Vereofy for omega-regular objectives relies on our tool ltl2dstar for generating deterministic omega-automata from Linear Temporal Logic (LTL) formulas. We introduce a generic improvement for exploiting insensitiveness to stuttering during the determinization construction and evaluate its effectiveness in practice. We further investigate the performance of recently proposed variants of Safra\'s determinization construction in practice.

weitere Metadaten

Synthese, kompositionell, allgemeinst, Controller, LTL, Determinisierung, Reo, CARML, RSL
synthesis, compositional, most general, controller, LTL, determinization, Reo, CARML, RSL
DDC Klassifikation004
RVK KlassifikationST 130
HochschuleTechnische Universität Dresden
FakultätFakultät Informatik
ProfessurProfessur für Algebraische und logische Grundlagen der Informatik
BetreuerProf. Dr. rer. nat. Christel Baier
GutachterProf. Dr. rer. nat. Christel Baier
Prof. Dr.-Ing. Martin Steffen
Tag d. Einreichung (bei der Fakultät)04.01.2013
Tag d. Verteidigung / Kolloquiums / Prüfung22.02.2013
Veröffentlichungsdatum (online)18.12.2013
persistente URNurn:nbn:de:bsz:14-qucosa-130654

Hinweis zum Urheberrecht

Diese Website ist eine Installation von Qucosa - Quality Content of Saxony!
Sächsische Landesbibliothek Staats- und Universitätsbibliothek Dresden