Author(s):

Chatterjee, Krishnendu; Henzinger, Monika; Joglekar, Manas; Nisarg, Shah

Title: 
Symbolic algorithms for qualitative analysis of Markov decision processes with Büchi objectives

Title Series: 
LNCS

Affiliation 
IST Austria 
Abstract: 
We consider Markov decision processes (MDPs) with ωregular specifications given as parity objectives. We consider the problem of computing the set of almostsure winning states from where the objective can be ensured with probability 1. The algorithms for the computation of the almostsure winning set for parity objectives iteratively use the solutions for the almostsure winning set for Büchi objectives (a special case of parity objectives). Our contributions are as follows: First, we present the first subquadratic symbolic algorithm to compute the almostsure winning set for MDPs with Büchi objectives; our algorithm takes O(nm) 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 often have constant outdegree, and then our symbolic algorithm takes O(nn) symbolic steps, as compared to the previous known O(n 2) symbolic steps algorithm. Second, we present a new algorithm, namely winlose algorithm, with the following two properties: (a) the algorithm iteratively computes subsets of the almostsure winning set and its complement, as compared to all previous algorithms that discover the almostsure winning set upon termination; and (b) requires O(nK) symbolic steps, where K is the maximal number of edges of strongly connected components (scc’s) of the MDP. The winlose 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.

Conference Title:

CAV: Computer Aided Verification

Volume: 
6806

Conference Dates:

July 1420, 2011

Conference Location:

Snowbird, UT, USA

Publisher:

Springer

Date Published:

20110811

Start Page: 
260

End Page:

276

Sponsor: 
FWF NFN Grant S11407N23 (RiSE), Microsoft faculty fellowship

URL: 

DOI: 
10.1007/9783642221101_21

Open access: 
yes (repository) 