MULTI-OBJECTIVE MODEL CHECKING OF MARKOV DECISION PROCESSES
We study and provide efficient algorithms for multi-objective model checking problems for Markov Decision Processes (MDPs). Given an MDP, M, and given multiple linear-time (ω-regular or LTL) properties φi, and probabilities ri ∈ [0,1], i=1,...,k, we ask whether there exists a strategy σ for the cont...
| Main Authors: | , , , |
|---|---|
| Format: | Journal article |
| Language: | English |
| Published: |
2008
|
| _version_ | 1826258727277166592 |
|---|---|
| author | Etessami, K Kwiatkowska, M Vardi, M Yannakakis, M |
| author_facet | Etessami, K Kwiatkowska, M Vardi, M Yannakakis, M |
| author_sort | Etessami, K |
| collection | OXFORD |
| description | We study and provide efficient algorithms for multi-objective model checking problems for Markov Decision Processes (MDPs). Given an MDP, M, and given multiple linear-time (ω-regular or LTL) properties φi, and probabilities ri ∈ [0,1], i=1,...,k, we ask whether there exists a strategy σ for the controller such that, for all i, the probability that a trajectory of M controlled by σ satisfies φi is at least ri. We provide an algorithm that decides whether there exists such a strategy and if so produces it, and which runs in time polynomial in the size of the MDP. Such a strategy may require the use of both randomization and memory. We also consider more general multi-objective ω-regular queries, which we motivate with an application to assume-guarantee compositional reasoning for probabilistic systems. Note that there can be trade-offs between different properties: satisfying property φ1 with high probability may necessitate satisfying φ2 with low probability. Viewing this as a multi-objective optimization problem, we want information about the "trade-off curve" or Pareto curve for maximizing the probabilities of different properties. We show that one can compute an approximate Pareto curve with respect to a set of ω-regular properties in time polynomial in the size of the MDP. Our quantitative upper bounds use LP methods. We also study qualitative multi-objective model checking problems, and we show that these can be analysed by purely graph-theoretic methods, even though the strategies may still require both randomization and memory. © K. Etessami, M. Kwiatkowska, M. Y. Vardi, and M. Yannakakis. |
| first_indexed | 2024-03-06T18:38:32Z |
| format | Journal article |
| id | oxford-uuid:0c1f87a1-3b54-4267-89c0-2fb91afc46cf |
| institution | University of Oxford |
| language | English |
| last_indexed | 2024-03-06T18:38:32Z |
| publishDate | 2008 |
| record_format | dspace |
| spelling | oxford-uuid:0c1f87a1-3b54-4267-89c0-2fb91afc46cf2022-03-26T09:33:09ZMULTI-OBJECTIVE MODEL CHECKING OF MARKOV DECISION PROCESSESJournal articlehttp://purl.org/coar/resource_type/c_dcae04bcuuid:0c1f87a1-3b54-4267-89c0-2fb91afc46cfEnglishSymplectic Elements at Oxford2008Etessami, KKwiatkowska, MVardi, MYannakakis, MWe study and provide efficient algorithms for multi-objective model checking problems for Markov Decision Processes (MDPs). Given an MDP, M, and given multiple linear-time (ω-regular or LTL) properties φi, and probabilities ri ∈ [0,1], i=1,...,k, we ask whether there exists a strategy σ for the controller such that, for all i, the probability that a trajectory of M controlled by σ satisfies φi is at least ri. We provide an algorithm that decides whether there exists such a strategy and if so produces it, and which runs in time polynomial in the size of the MDP. Such a strategy may require the use of both randomization and memory. We also consider more general multi-objective ω-regular queries, which we motivate with an application to assume-guarantee compositional reasoning for probabilistic systems. Note that there can be trade-offs between different properties: satisfying property φ1 with high probability may necessitate satisfying φ2 with low probability. Viewing this as a multi-objective optimization problem, we want information about the "trade-off curve" or Pareto curve for maximizing the probabilities of different properties. We show that one can compute an approximate Pareto curve with respect to a set of ω-regular properties in time polynomial in the size of the MDP. Our quantitative upper bounds use LP methods. We also study qualitative multi-objective model checking problems, and we show that these can be analysed by purely graph-theoretic methods, even though the strategies may still require both randomization and memory. © K. Etessami, M. Kwiatkowska, M. Y. Vardi, and M. Yannakakis. |
| spellingShingle | Etessami, K Kwiatkowska, M Vardi, M Yannakakis, M MULTI-OBJECTIVE MODEL CHECKING OF MARKOV DECISION PROCESSES |
| title | MULTI-OBJECTIVE MODEL CHECKING OF MARKOV DECISION PROCESSES |
| title_full | MULTI-OBJECTIVE MODEL CHECKING OF MARKOV DECISION PROCESSES |
| title_fullStr | MULTI-OBJECTIVE MODEL CHECKING OF MARKOV DECISION PROCESSES |
| title_full_unstemmed | MULTI-OBJECTIVE MODEL CHECKING OF MARKOV DECISION PROCESSES |
| title_short | MULTI-OBJECTIVE MODEL CHECKING OF MARKOV DECISION PROCESSES |
| title_sort | multi objective model checking of markov decision processes |
| work_keys_str_mv | AT etessamik multiobjectivemodelcheckingofmarkovdecisionprocesses AT kwiatkowskam multiobjectivemodelcheckingofmarkovdecisionprocesses AT vardim multiobjectivemodelcheckingofmarkovdecisionprocesses AT yannakakism multiobjectivemodelcheckingofmarkovdecisionprocesses |