Specification revision for Markov decision processes with optimal trade-off
Optimal control policy synthesis for probabilistic systems from high-level specifications is increasingly often studied. One major question that is commonly faced, however, is what to do when the optimal probability of achieving the specification is not satisfactory? We address this question by view...
| Main Authors: | , |
|---|---|
| Format: | Conference item |
| Published: |
Institute of Electrical and Electronics Engineers
2016
|
| _version_ | 1797079770488373248 |
|---|---|
| author | Lahijanian, M Kwiatkowska, M |
| author_facet | Lahijanian, M Kwiatkowska, M |
| author_sort | Lahijanian, M |
| collection | OXFORD |
| description | Optimal control policy synthesis for probabilistic systems from high-level specifications is increasingly often studied. One major question that is commonly faced, however, is what to do when the optimal probability of achieving the specification is not satisfactory? We address this question by viewing the specification as a soft constraint and present a synthesis framework for MDPs that encodes and automates specification revision in a trade-off for higher probability. The method uses co-safe LTL as the specification language and quantifies the revisions to the specification according to userdefined proposition costs. The framework computes a control policy that optimizes the trade-off between the probability of satisfaction and the cost of specification revision. The key idea of the method is a rule for the composition of the MDP, the automaton representing the specification, and the proposition costs such that all possible specification revisions along with their costs and probabilities of satisfaction are captured in one structure. The problem is then reduced to multi-objective optimization on an MDP. The power of the method is illustrated though simulations of a complex robotic scenario. |
| first_indexed | 2024-03-07T00:50:31Z |
| format | Conference item |
| id | oxford-uuid:863e4a92-6a07-40bc-a7d8-dc3331718bf3 |
| institution | University of Oxford |
| last_indexed | 2024-03-07T00:50:31Z |
| publishDate | 2016 |
| publisher | Institute of Electrical and Electronics Engineers |
| record_format | dspace |
| spelling | oxford-uuid:863e4a92-6a07-40bc-a7d8-dc3331718bf32022-03-26T22:02:38ZSpecification revision for Markov decision processes with optimal trade-offConference itemhttp://purl.org/coar/resource_type/c_5794uuid:863e4a92-6a07-40bc-a7d8-dc3331718bf3Symplectic Elements at OxfordInstitute of Electrical and Electronics Engineers2016Lahijanian, MKwiatkowska, MOptimal control policy synthesis for probabilistic systems from high-level specifications is increasingly often studied. One major question that is commonly faced, however, is what to do when the optimal probability of achieving the specification is not satisfactory? We address this question by viewing the specification as a soft constraint and present a synthesis framework for MDPs that encodes and automates specification revision in a trade-off for higher probability. The method uses co-safe LTL as the specification language and quantifies the revisions to the specification according to userdefined proposition costs. The framework computes a control policy that optimizes the trade-off between the probability of satisfaction and the cost of specification revision. The key idea of the method is a rule for the composition of the MDP, the automaton representing the specification, and the proposition costs such that all possible specification revisions along with their costs and probabilities of satisfaction are captured in one structure. The problem is then reduced to multi-objective optimization on an MDP. The power of the method is illustrated though simulations of a complex robotic scenario. |
| spellingShingle | Lahijanian, M Kwiatkowska, M Specification revision for Markov decision processes with optimal trade-off |
| title | Specification revision for Markov decision processes with optimal trade-off |
| title_full | Specification revision for Markov decision processes with optimal trade-off |
| title_fullStr | Specification revision for Markov decision processes with optimal trade-off |
| title_full_unstemmed | Specification revision for Markov decision processes with optimal trade-off |
| title_short | Specification revision for Markov decision processes with optimal trade-off |
| title_sort | specification revision for markov decision processes with optimal trade off |
| work_keys_str_mv | AT lahijanianm specificationrevisionformarkovdecisionprocesseswithoptimaltradeoff AT kwiatkowskam specificationrevisionformarkovdecisionprocesseswithoptimaltradeoff |