hide
Free keywords:
Mathematics, Optimization and Control, math.OC,cs.SY
Abstract:
Symbolic approaches to the control design over complex systems employ the
construction of finite-state models that are related to the original control
systems, then use techniques from finite-state synthesis to compute controllers
satisfying specifications given in a temporal logic, and finally translate the
synthesized schemes back as controllers for the concrete complex systems. Such
approaches have been successfully developed and implemented for the synthesis
of controllers over non-probabilistic control systems. In this paper, we extend
the technique to probabilistic control systems modeled by controlled stochastic
differential equations. We show that for every stochastic control system
satisfying a probabilistic variant of incremental input-to-state stability, and
for every given precision $\varepsilon>0$, a finite-state transition system can
be constructed, which is $\varepsilon$-approximately bisimilar (in the sense of
moments) to the original stochastic control system. Moreover, we provide
results relating stochastic control systems to their corresponding finite-state
transition systems in terms of probabilistic bisimulation relations known in
the literature. We demonstrate the effectiveness of the construction by
synthesizing controllers for stochastic control systems over rich
specifications expressed in linear temporal logic. The discussed technique
enables a new, automated, correct-by-construction controller synthesis approach
for stochastic control systems, which are common mathematical models employed
in many safety critical systems subject to structured uncertainty and are thus
relevant for cyber-physical applications.