Research Article
Equivalence and Minimization for Model Checking Labeled Markov Chains
@ARTICLE{10.4108/eai.14-12-2015.2262622, author={Peter Buchholz and Jan Kriege and Dimitri Scheftelowitsch}, title={Equivalence and Minimization for Model Checking Labeled Markov Chains}, journal={EAI Endorsed Transactions on Scalable Information Systems}, volume={3}, number={11}, publisher={ACM}, journal_a={SIS}, year={2016}, month={1}, keywords={model checking, labeled markov chains, equivalence}, doi={10.4108/eai.14-12-2015.2262622} }- Peter Buchholz
Jan Kriege
Dimitri Scheftelowitsch
Year: 2016
Equivalence and Minimization for Model Checking Labeled Markov Chains
SIS
EAI
DOI: 10.4108/eai.14-12-2015.2262622
Abstract
Model checking of Markov chains using logics like CSL or asCSL proves whether a logical formula holds for a state of the Markov chain. It has been developed in the last decade to a widely used approach to express performance and dependability quantities for models from a wide range of application areas. In this paper, model checking is extended to prove formulas for distributions rather than single states. This is a very natural way to express certain performance or dependability measures that depend on the state of the system rather than on a specific state in the state space of the Markov chain. It is shown that the mentioned logics can be easily extended from states to distributions and model checking algorithms can also be easily adopted. Furthermore, new equivalences will be introduced that are weaker than bisimulation but still characterize the extended logics.
Copyright © 2015 D. Scheftelowitsch et al., licensed to EAI. This is an open access article distributed under the terms of the Creative Commons Attribution licence (http://creativecommons.org/licenses/by/3.0/), which permits unlimited use, distribution and reproduction in any medium so long as the original work is properly cited.
