×

Controller synthesis for probabilistic systems (extended abstract). (English) Zbl 1073.93037

Levy, Jean-Jacques (ed.) et al., Exploring new frontiers of theoretical informatics. IFIP 18th world computer congress, TC1 3rd international conference on theoretical computer science (TCS2004), 22–27 August 2004, Toulouse, France. Boston, MA: Kluwer Academic Publishers (ISBN 1-4020-8140-5/hbk). IFIP, International Federation for Information Processing 155, 493-506 (2004).
A practically important task is considered; the goal is to synthesize a controller that limits or controls the behavior of an existing system (plant) in an environment to meet the given specification. One can also understand the controller and environment as two players. The plant constitutes the game board, and controller synthesis becomes the problem of finding a strategy for the controller that satisfies the specification whatever move the environment does.
The requirement specification can either be given internally or externally. Internal specifications impose restrictions, for example, on the number of visits of a state of the plant. Examples for external specifications are temporal logic formulas that are supposed to be satisfied by the controlled plant. The underlying model for the plant are Markov Decision Processes (MDPs) in which states that are under control of the plant are distinguished from those that are under the control of the environment. Quantitative winning criteria stating that the probability to win the game meets a given lower (or upper) probability bound are considered.
In the first part of the paper, the synthesis problem is considered where the specification is provided by means of a formula of probabilistic computation tree logic (PCTL). As for strategies, several choices are discussed: The system or the opponent has to choose deterministically (D) or can choose randomly (R). Furthermore, he or she might choose according to the current state (M), also called Markovian, or is allowed to look at the history of the game played so far (H). From a practical point of view, it would be desirable to be able to synthesize controllers that do not require extra memory to keep track of a history and do not depend on random number generators. However, it is shown that this is not always possible. For the synthesis algorithms, it means that any of the strategy classes HD, HR, MD and MR requires its own synthesis algorithm. The authors show the NP-completeness of the synthesis problem for PCTL and MD-strategies and the NP-hardness of the synthesis problem for PCTL and the strategy classes HD, HR and MR,
The second part of the paper addresses the synthesis problem for linear-time specifications formalized by LTL-formulas. A control synthesis algorithm is presented which relies on a reduction to the synthesis problem for PCTL with fairness.
For the entire collection see [Zbl 1057.68001].

MSC:

93C65 Discrete event control/observation systems
93B50 Synthesis problems
93E03 Stochastic systems in control theory (general)
90C40 Markov and semi-Markov decision processes
91A15 Stochastic games, stochastic differential games
68Q17 Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.)
PDFBibTeX XMLCite