Model Checking for Imprecise Markov Chains

Troffaes, Matthias C.M.; Skulj, Damjan

Abstract

We extend probabilistic computational tree logic for expressing properties of Markov chains to imprecise Markov chains, and provide an efficient algorithm for model checking of imprecise Markov chains. Thereby, we provide a formal framework to answer a very wide range of questions about imprecise Markov chains, in a systematic and computationally efficient way.

Citation

Troffaes, M. C., & Skulj, D. (2013). Model Checking for Imprecise Markov Chains. In F. Cozman, T. Denoeux, S. Destercke, & T. Seidenfeld (Eds.), ISIPTA ’13 : proceedings of the eighth international symposium on imprecise probability : theories and applications July 2-5 2013, Compiègne, France (337-344)

• Presentation Conference Type: Conference Paper (Published)
• Conference Name: ISIPTA'13: Proceedings of the Eighth International Symposium on Imprecise Probability: Theories and Applications
• Publication Date: Jul 5, 2013
• Deposit Date: May 29, 2013
• Publicly Available Date: Oct 22, 2014
• Pages: 337-344
• Book Title: ISIPTA ’13 : proceedings of the eighth international symposium on imprecise probability : theories and applications July 2-5 2013, Compiègne, France.
• Keywords: Imprecise Markov chain, Model checking, Parse tree, Logic, Computation.
• Public URL: https://durham-repository.worktribe.com/output/1155467
• Publisher URL: http://www.sipta.org/isipta13/index.php?id=paper&paper=034.html
• Additional Information: 2-5 July 2013