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. Wh... View more
[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.
[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.
[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.
[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.