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

2011 ◽  
Author(s):  
Henri Hansen ◽  
Marta Kwiatkowska ◽  
Hongyang Qu
Keyword(s):  
Model Checking ◽  
Partial Order ◽  
Markov Decision Processes ◽  
Order Reduction ◽  
Decision Processes ◽  
Partial Order Reduction ◽  
Markov Decision

Controlled Markov set-chains with discounting

1998 ◽  
Vol 35 (2) ◽  
pp. 293-302 ◽  
Author(s):  
Masami Kurano ◽  
Jinjie Song ◽  
Masanori Hosaka ◽  
Youqiang Huang
Keyword(s):  
Partial Order ◽  
Markov Decision Processes ◽  
Transition Probability ◽  
Decision Processes ◽  
New Model ◽  
Numerical Example ◽  
Markov Decision ◽  
Theoretical Results

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.

scholarly journals Partial-Order Reduction for Parity Games with an Application on Parameterised Boolean Equation Systems

2020 ◽  
pp. 307-324 ◽  
Author(s):  
Thomas Neele ◽  
Tim A. C. Willemse ◽  
Wieger Wesselink
Keyword(s):  
Fixed Point ◽  
Model Checking ◽  
Partial Order ◽  
Order Reduction ◽  
Partial Order Reduction ◽  
State Space Explosion ◽  
Boolean Equation ◽  
Parity Games ◽  
High Level ◽  
Established Technique

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