Journal
IEEE TRANSACTIONS ON AUTOMATIC CONTROL
Volume 59, Issue 12, Pages 3135-3150Publisher
IEEE-INST ELECTRICAL ELECTRONICS ENGINEERS INC
DOI: 10.1109/TAC.2014.2351652
Keywords
Automated synthesis; bisimulation; incremental stability; linear temporal logic; stochastic systems
Funding
- European Commission MoVeS [FP7-ICT-2009-5 257005]
- Toyota
Ask authors/readers for more resources
Symbolic approaches for control design construct finite-state abstract models that are related to the original 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 original 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 modelled 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 epsilon > 0, a finite-state transition system can be constructed, which is epsilon-approximately bisimilar 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. Our technique enables automated, correct-by-construction, controller synthesis for stochastic control systems, which are common mathematical models employed in many safety critical systems subject to structured uncertainty.
Authors
I am an author on this paper
Click your name to claim this paper and add it to your profile.
Reviews
Recommended
No Data Available