Quantitative automata-based controller synthesis for non-autonomous stochastic hybrid systems
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...
| Main Authors: | , , , |
|---|---|
| Format: | Conference item |
| Published: |
2012
|
| _version_ | 1797050845331718144 |
|---|---|
| author | Tkachev, I Abate, A Mereacre, A Katoen, J |
| author_facet | Tkachev, I Abate, A Mereacre, A Katoen, J |
| author_sort | Tkachev, I |
| collection | OXFORD |
| description | 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. |
| first_indexed | 2024-03-06T18:11:14Z |
| format | Conference item |
| id | oxford-uuid:0317821e-5076-4baf-a53d-5074ebacf8e6 |
| institution | University of Oxford |
| last_indexed | 2024-03-06T18:11:14Z |
| publishDate | 2012 |
| record_format | dspace |
| spelling | oxford-uuid:0317821e-5076-4baf-a53d-5074ebacf8e62022-03-26T08:44:11ZQuantitative automata-based controller synthesis for non-autonomous stochastic hybrid systemsConference itemhttp://purl.org/coar/resource_type/c_5794uuid:0317821e-5076-4baf-a53d-5074ebacf8e6Symplectic Elements at Oxford2012Tkachev, IAbate, AMereacre, AKatoen, JThis 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. |
| spellingShingle | Tkachev, I Abate, A Mereacre, A Katoen, J Quantitative automata-based controller synthesis for non-autonomous stochastic hybrid systems |
| title | Quantitative automata-based controller synthesis for non-autonomous stochastic hybrid systems |
| title_full | Quantitative automata-based controller synthesis for non-autonomous stochastic hybrid systems |
| title_fullStr | Quantitative automata-based controller synthesis for non-autonomous stochastic hybrid systems |
| title_full_unstemmed | Quantitative automata-based controller synthesis for non-autonomous stochastic hybrid systems |
| title_short | Quantitative automata-based controller synthesis for non-autonomous stochastic hybrid systems |
| title_sort | quantitative automata based controller synthesis for non autonomous stochastic hybrid systems |
| work_keys_str_mv | AT tkachevi quantitativeautomatabasedcontrollersynthesisfornonautonomousstochastichybridsystems AT abatea quantitativeautomatabasedcontrollersynthesisfornonautonomousstochastichybridsystems AT mereacrea quantitativeautomatabasedcontrollersynthesisfornonautonomousstochastichybridsystems AT katoenj quantitativeautomatabasedcontrollersynthesisfornonautonomousstochastichybridsystems |