scholarly journals Partial Order Reduction for Model Checking Markov Decision Processes under Unconditional Fairness

Author(s):  
Henri Hansen ◽  
Marta Kwiatkowska ◽  
Hongyang Qu
1998 ◽  
Vol 35 (2) ◽  
pp. 293-302 ◽  
Author(s):  
Masami Kurano ◽  
Jinjie Song ◽  
Masanori Hosaka ◽  
Youqiang Huang

In the framework of discounted Markov decision processes, we consider the case that the transition probability varies in some given domain at each time and its variation is unknown or unobservable.To this end we introduce a new model, named controlled Markov set-chains, based on Markov set-chains, and discuss its optimization under some partial order.Also, a numerical example is given to explain the theoretical results and the computation.


Author(s):  
Thomas Neele ◽  
Tim A. C. Willemse ◽  
Wieger Wesselink

Abstract Partial-order reduction (POR) is a well-established technique to combat the problem of state-space explosion. We propose POR techniques that are sound for parity games, a well-established formalism for solving a variety of decision problems. As a consequence, we obtain the first POR method that is sound for model checking for the full modal $$\mu $$-calculus. Our technique is applied to, and implemented for the fixed point logic called parameterised Boolean equation systems, which provides a high-level representation of parity games. Experiments indicate that substantial reductions can be achieved.


Sign in / Sign up

Export Citation Format

Share Document