Symbolic algorithms for qualitative analysis of Markov decision processes with Büchi objectives
Chatterjee K, Henzinger MH, Joglekar M, Shah N. 2013. Symbolic algorithms for qualitative analysis of Markov decision processes with Büchi objectives. Formal Methods in System Design. 42(3), 301–327.
Download (ext.)
http://arxiv.org/abs/1104.3348
[Preprint]
Journal Article
| Published
| English
Scopus indexed
Author
Department
Grant
Abstract
We consider Markov decision processes (MDPs) with Büchi (liveness) objectives. We consider the problem of computing the set of almost-sure winning states from where the objective can be ensured with probability 1. Our contributions are as follows: First, we present the first subquadratic symbolic algorithm to compute the almost-sure winning set for MDPs with Büchi objectives; our algorithm takes O(n · √ m) symbolic steps as compared to the previous known algorithm that takes O(n 2) symbolic steps, where n is the number of states and m is the number of edges of the MDP. In practice MDPs have constant out-degree, and then our symbolic algorithm takes O(n · √ n) symbolic steps, as compared to the previous known O(n 2) symbolic steps algorithm. Second, we present a new algorithm, namely win-lose algorithm, with the following two properties: (a) the algorithm iteratively computes subsets of the almost-sure winning set and its complement, as compared to all previous algorithms that discover the almost-sure winning set upon termination; and (b) requires O(n · √ K) symbolic steps, where K is the maximal number of edges of strongly connected components (scc's) of the MDP. The win-lose algorithm requires symbolic computation of scc's. Third, we improve the algorithm for symbolic scc computation; the previous known algorithm takes linear symbolic steps, and our new algorithm improves the constants associated with the linear number of steps. In the worst case the previous known algorithm takes 5×n symbolic steps, whereas our new algorithm takes 4×n symbolic steps.
Publishing Year
Date Published
2013-06-01
Journal Title
Formal Methods in System Design
Publisher
Springer
Volume
42
Issue
3
Page
301 - 327
IST-REx-ID
Cite this
Chatterjee K, Henzinger MH, Joglekar M, Shah N. Symbolic algorithms for qualitative analysis of Markov decision processes with Büchi objectives. Formal Methods in System Design. 2013;42(3):301-327. doi:10.1007/s10703-012-0180-2
Chatterjee, K., Henzinger, M. H., Joglekar, M., & Shah, N. (2013). Symbolic algorithms for qualitative analysis of Markov decision processes with Büchi objectives. Formal Methods in System Design. Springer. https://doi.org/10.1007/s10703-012-0180-2
Chatterjee, Krishnendu, Monika H Henzinger, Manas Joglekar, and Nisarg Shah. “Symbolic Algorithms for Qualitative Analysis of Markov Decision Processes with Büchi Objectives.” Formal Methods in System Design. Springer, 2013. https://doi.org/10.1007/s10703-012-0180-2.
K. Chatterjee, M. H. Henzinger, M. Joglekar, and N. Shah, “Symbolic algorithms for qualitative analysis of Markov decision processes with Büchi objectives,” Formal Methods in System Design, vol. 42, no. 3. Springer, pp. 301–327, 2013.
Chatterjee K, Henzinger MH, Joglekar M, Shah N. 2013. Symbolic algorithms for qualitative analysis of Markov decision processes with Büchi objectives. Formal Methods in System Design. 42(3), 301–327.
Chatterjee, Krishnendu, et al. “Symbolic Algorithms for Qualitative Analysis of Markov Decision Processes with Büchi Objectives.” Formal Methods in System Design, vol. 42, no. 3, Springer, 2013, pp. 301–27, doi:10.1007/s10703-012-0180-2.
All files available under the following license(s):
Copyright Statement:
This Item is protected by copyright and/or related rights. [...]
Link(s) to Main File(s)
Access Level
Open Access
Material in ISTA:
Earlier Version
Export
Marked PublicationsOpen Data ISTA Research Explorer
Sources
arXiv 1104.3348