Quantitative automata-based controller synthesis for non-autonomous stochastic hybrid systems

Conference item

This work deals with Markov processes that are defined over an uncountable state space (possibly hybrid) and embedding non-determinism in the shape of a control structure. The contribution looks at the problem of optimization, over the set of allowed controls, of probabilistic specifications defined by automata - in particular, the focus is on deterministic finite-state automata. This problem can be reformulated as an optimization of a probabilistic reachability property over a product process obtained from the model for the specification and the model of the system. Optimizing over automata-based specifications thus leads to maximal or minimal probabilistic reachability properties. For both setups, the contribution shows that these problems can be sufficiently tackled with history-independent Markov policies. This outcome has relevant computational repercussions: in particular, the work develops a discretization procedure leading into standard optimization problems over Markov decision processes. Such procedure is associated with exact error bounds and is experimentally tested on a case study. Copyright © 2013 ACM.

Authors: Tkachev, I; Abate, A; Mereacre, A; Katoen, J

• Host title: HSCC 2013 - Proceedings of the 16th International Conference on Hybrid Systems: Computation and Control, Part of CPSWeek 2013
• Volume: 1
• Pages: 293-302
• Publication date: 2012-01-01
• DOI: 10.1145/2461328.2461373