About | Contact Us | Register | Login
ProceedingsSeriesJournalsSearchEAI
9th EAI International Conference on Performance Evaluation Methodologies and Tools

Research Article

Equivalence and Minimization for Model Checking Labeled Markov Chains

Cite
BibTeX Plain Text
  • @INPROCEEDINGS{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},
        proceedings={9th EAI International Conference on Performance Evaluation Methodologies and Tools},
        publisher={ACM},
        proceedings_a={VALUETOOLS},
        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
    VALUETOOLS
    ICST
    DOI: 10.4108/eai.14-12-2015.2262622
Peter Buchholz1, Jan Kriege1, Dimitri Scheftelowitsch1,*
  • 1: TU Dortmund
*Contact email: dimitri.scheftelowitsch@cs.tu-dortmund.de

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.

Keywords
model checking labeled markov chains equivalence
Published
2016-01-04
Publisher
ACM
http://dx.doi.org/10.4108/eai.14-12-2015.2262622
Copyright © 2015–2025 ICST
EBSCOProQuestDBLPDOAJPortico
EAI Logo

About EAI

  • Who We Are
  • Leadership
  • Research Areas
  • Partners
  • Media Center

Community

  • Membership
  • Conference
  • Recognition
  • Sponsor Us

Publish with EAI

  • Publishing
  • Journals
  • Proceedings
  • Books
  • EUDL