publication . Article . Preprint . 2007

Decisive Markov Chains

Abdulla, Parosh Aziz; Henda, Noomene Ben; Mayr, Richard;
Open Access English
  • Published: 18 Jun 2007
Abstract
We consider qualitative and quantitative verification problems for infinite-state Markov chains. We call a Markov chain decisive w.r.t. a given set of target states F if it almost certainly eventually reaches either F or a state from which F can no longer be reached. While all finite Markov chains are trivially decisive (for every set F), this also holds for many classes of infinite Markov chains. Infinite Markov chains which contain a finite attractor are decisive w.r.t. every set F. In particular, this holds for probabilistic lossy channel systems (PLCS). Furthermore, all globally coarse Markov chains are decisive. This class includes probabilistic vector addi...
Subjects
free text keywords: Computer Science - Discrete Mathematics, D.2.4, Computer Science - Logic in Computer Science, F.4.1, G.3
40 references, page 1 of 3

[ABIJ00] P. Abdulla, C. Baier, P. Iyer, and B. Jonsson. Reasoning about probabilistic lossy channel systems. In Proc. of CONCUR 2000, volume 1877 of LNCS, 2000.

[AC05] E. Asarin and P. Collins. Noisy Turing machines. In Proc. ICALP '05, 32. International Colloquium on Automata, Languages, and Programming, pages 1031-1042, 2005.

[ACˇ JYK00] P. Abdulla, K. Cˇ er¯ans, B. Jonsson, and T. Yih-Kuen. Algorithmic analysis of programs with well quasi-ordered domains. Information and Computation, 160:109-127, 2000.

[AHM05] P. Abdulla, N.B. Henda, and R. Mayr. Verifying infinite Markov chains with a finite attractor or the global coarseness property. In Twentieth Annual IEEE Symposium on Logic in Computer Science (LICS 2005). IEEE, 2005.

[AJ96] P. Abdulla and B. Jonsson. Verifying programs with unreliable channels. Information and Computation, 127(2):91-101, 1996. [OpenAIRE]

[AR03] P. Abdulla and A. Rabinovich. Verification of probabilistic systems with faulty communication. In Proc. FOSSACS03, Conf. on Foundations of Software Science and Computation Structures, volume 2620, 2003.

[BE99] C. Baier and B. Engelen. Establishing qualitative properties for probabilistic lossy channel systems. In Katoen, editor, ARTS'99, Formal Methods for Real-Time and Probabilistic Systems, 5th Int. AMAST Workshop, volume 1601 of LNCS, pages 34-52. Springer Verlag, 1999. [OpenAIRE]

[BS03] N. Bertrand and Ph. Schnoebelen. Model checking lossy channels systems is probably decidable. In Proc. FOSSACS03, Conf. on Foundations of Software Science and Computation Structures, volume 2620, 2003. [OpenAIRE]

[BS04] N. Bertrand and Ph. Schnoebelen. Verifying nondeterministic channel systems with probabilistic message losses. In R. Bharadwaj, editor, Proc. of the 3rd Int. Workshop on Automated Verification of Infinite-State Systems (AVIS'04), ENTCS. Elsevier, 2004.

[BZ83] D. Brand and P. Zafiropulo. On communicating finite-state machines. Journal of the ACM, 2(5):323-342, April 1983.

[CFI96] G. C´ec´e, A. Finkel, and P. Iyer. Unreliable channels are easier to verify than perfect channels. Information and Computation, 124(1):20-31, 10 January 1996. [OpenAIRE]

[CGP99] E.M. Clarke, O. Grumberg, and D. Peled. Model Checking. MIT Press, Dec. 1999.

[Cou91] B. Courcelle. On constructing obstruction sets of words. Bulletin of the EATCS, 44:178-185, June 1991.

[CSS03] J.-M. Couvreur, N. Saheb, and G. Sutre. An optimal automata approach to LTL model checking of probabilistic systems. In Proc. LPAR'2003, volume 2850 of LNCS, pages 361-375, 2003.

[CY88] C. Courcoubetis and M. Yannakakis. Verifying temporal properties of finite-state probabilistic programs. In Proc. 29. Annual Symp. Foundations of Computer Science, pages 338-345, 1988.

40 references, page 1 of 3
Abstract
We consider qualitative and quantitative verification problems for infinite-state Markov chains. We call a Markov chain decisive w.r.t. a given set of target states F if it almost certainly eventually reaches either F or a state from which F can no longer be reached. While all finite Markov chains are trivially decisive (for every set F), this also holds for many classes of infinite Markov chains. Infinite Markov chains which contain a finite attractor are decisive w.r.t. every set F. In particular, this holds for probabilistic lossy channel systems (PLCS). Furthermore, all globally coarse Markov chains are decisive. This class includes probabilistic vector addi...
Subjects
free text keywords: Computer Science - Discrete Mathematics, D.2.4, Computer Science - Logic in Computer Science, F.4.1, G.3
40 references, page 1 of 3

[ABIJ00] P. Abdulla, C. Baier, P. Iyer, and B. Jonsson. Reasoning about probabilistic lossy channel systems. In Proc. of CONCUR 2000, volume 1877 of LNCS, 2000.

[AC05] E. Asarin and P. Collins. Noisy Turing machines. In Proc. ICALP '05, 32. International Colloquium on Automata, Languages, and Programming, pages 1031-1042, 2005.

[ACˇ JYK00] P. Abdulla, K. Cˇ er¯ans, B. Jonsson, and T. Yih-Kuen. Algorithmic analysis of programs with well quasi-ordered domains. Information and Computation, 160:109-127, 2000.

[AHM05] P. Abdulla, N.B. Henda, and R. Mayr. Verifying infinite Markov chains with a finite attractor or the global coarseness property. In Twentieth Annual IEEE Symposium on Logic in Computer Science (LICS 2005). IEEE, 2005.

[AJ96] P. Abdulla and B. Jonsson. Verifying programs with unreliable channels. Information and Computation, 127(2):91-101, 1996. [OpenAIRE]

[AR03] P. Abdulla and A. Rabinovich. Verification of probabilistic systems with faulty communication. In Proc. FOSSACS03, Conf. on Foundations of Software Science and Computation Structures, volume 2620, 2003.

[BE99] C. Baier and B. Engelen. Establishing qualitative properties for probabilistic lossy channel systems. In Katoen, editor, ARTS'99, Formal Methods for Real-Time and Probabilistic Systems, 5th Int. AMAST Workshop, volume 1601 of LNCS, pages 34-52. Springer Verlag, 1999. [OpenAIRE]

[BS03] N. Bertrand and Ph. Schnoebelen. Model checking lossy channels systems is probably decidable. In Proc. FOSSACS03, Conf. on Foundations of Software Science and Computation Structures, volume 2620, 2003. [OpenAIRE]

[BS04] N. Bertrand and Ph. Schnoebelen. Verifying nondeterministic channel systems with probabilistic message losses. In R. Bharadwaj, editor, Proc. of the 3rd Int. Workshop on Automated Verification of Infinite-State Systems (AVIS'04), ENTCS. Elsevier, 2004.

[BZ83] D. Brand and P. Zafiropulo. On communicating finite-state machines. Journal of the ACM, 2(5):323-342, April 1983.

[CFI96] G. C´ec´e, A. Finkel, and P. Iyer. Unreliable channels are easier to verify than perfect channels. Information and Computation, 124(1):20-31, 10 January 1996. [OpenAIRE]

[CGP99] E.M. Clarke, O. Grumberg, and D. Peled. Model Checking. MIT Press, Dec. 1999.

[Cou91] B. Courcelle. On constructing obstruction sets of words. Bulletin of the EATCS, 44:178-185, June 1991.

[CSS03] J.-M. Couvreur, N. Saheb, and G. Sutre. An optimal automata approach to LTL model checking of probabilistic systems. In Proc. LPAR'2003, volume 2850 of LNCS, pages 361-375, 2003.

[CY88] C. Courcoubetis and M. Yannakakis. Verifying temporal properties of finite-state probabilistic programs. In Proc. 29. Annual Symp. Foundations of Computer Science, pages 338-345, 1988.

40 references, page 1 of 3
Powered by OpenAIRE Open Research Graph
Any information missing or wrong?Report an Issue
publication . Article . Preprint . 2007

Decisive Markov Chains

Abdulla, Parosh Aziz; Henda, Noomene Ben; Mayr, Richard;