Controller Synthesis for Probabilistic Systems

Christel BaierChristel Baier, Marcus GrößerMarcus Größer, Martin LeuckerMartin Leucker, Benedikt BolligBenedikt Bollig, Frank CiesinskiFrank Ciesinski

DOI Link

Christel Baier, Marcus Größer, Martin Leucker, Benedikt Bollig, Frank Ciesinski
Controller Synthesis for Probabilistic Systems
Exploring New Frontiers of Theoretical Informatics, IFIP 18th World Computer Congress, TC1 3rd International Conference on Theoretical Computer Science (TCS2004), volume 155 of IFIP, 493--506, 2004. Kluwer/Springer

Details
Bibtex

KurzfassungAbstract
Controller synthesis addresses the question of how to limit the internal behavior of a given implementation to meet its specification, regardless of the behavior enforced by the environment. In this paper, we consider a model with probabilism and nondeterminism where the nondeterministic choices in some states are assumed to be controllable, while the others are under the control of an unpredictable environment. We first consider probabilistic computation tree logic as specification formalism, discuss the role of strategy-types for the controller and show the NP-hardness of the controller synthesis problem. The second part of the paper presents a controller synthesis algorithm for automata-specifications which relies on a reduction to the synthesis problem for PCTL with fairness.
Forschungsgruppe:Research Group: Algebraische und logische Grundlagen der InformatikAlgebraic and Logical Foundations of Computer Science

@inproceedings{BGLBC2004,
  author    = {Christel Baier and Marcus Gr{\"{o}}{\ss}er and Martin Leucker and
               Benedikt Bollig and Frank Ciesinski},
  title     = {Controller Synthesis for Probabilistic Systems},
  booktitle = {Exploring New Frontiers of Theoretical Informatics, {IFIP} 18th
               World Computer Congress, {TC1} 3rd International Conference on
               Theoretical Computer Science (TCS2004)},
  series    = {IFIP},
  volume    = {155},
  publisher = {Kluwer/Springer},
  year      = {2004},
  pages     = {493--506},
  doi       = {10.1007/1-4020-8141-3_38}
}