CONTROLLER SYNTHESIS FOR PROBABILISTIC SYSTEMS

摘要

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 probabil-ism 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.