Abstract
Lossy channel systems (LCS’s) are systems of finite state automata that communicate via unreliable unbounded fifo channels. We propose a new probabilistic model for these systems, where losses of messages are seen as faults occurring with some given probability, and where the internal behavior of the system remains nondeterministic, giving rise to a reactive Markov chains semantics. We then investigate the verification of linear-time properties on this new model.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
P. A. Abdulla, A. Annichini, and A. Bouajjani. Symbolic verification of lossy channel systems: Application to the bounded retransmission protocol. In Proc. 5th Int. Conf. Tools and Algorithms for the Construction and Analysis of Systems (TACAS’99), vol. 1579 of Lect. Notes Comp. Sci., pages 208–222. Springer, 1999.
P. A. Abdulla, C. Baier, S. Purushothaman Iyer, and B. Jonsson. Reasoning about probabilistic lossy channel systems. In Proc. 11th Int. Conf. Concurrency Theory (CONCUR’2000), vol. 1877 of Lect. Notes in Computer Sci., pages 320–333. Springer, 2000.
P. A. Abdulla and B. Jonsson. Undecidable verification problems for programs with unreliable channels. Information and Computation, 130(1):71–90, 1996.
P. A. Abdulla and B. Jonsson. Verifying programs with unreliable channels. Information and Computation, 127(2):91–101, 1996.
P. A. Abdulla and A. Rabinovich. Verification of probabilistic systems with faulty communication. In Proc. FOSSACS’2003 (this volume). Springer, 2003.
C. Baier and B. Engelen. Establishing qualitative properties for probabilistic lossy channel systems: An algorithmic approach. In Proc. 5th Int. AMAST Workshop Formal Methods for Real-Time and Probabilistic Systems (ARTS’99), vol. 1601 of Lect. Notes Comp. Sci., pages 34–52. Springer, 1999.
C. Baier, J.-P. Katoen, and H. Hermanns. Approximate symbolic model checking of continuous-time Markov chains. In Proc. 26th Int. Coll. Automata, Languages, and Programming (ICALP’99), vol. 1644 of Lect. Notes Comp. Sci., pages 142–162. Springer, 1999.
D. Brand and P. Zafiropulo. On communicating finite-state machines. Journal of the ACM, 30(2):323–342, 1983.
G. Cécé, A. Finkel, and S. Purushothaman Iyer. Unreliable channels are easier to verify than perfect channels. Information and Computation, 124(1):20–31, 1996.
C. Courcoubetis and M. Yannakakis. The complexity of probabilistic verification. Journal of the ACM, 42(4):857–907, 1995.
C. Derman. Finite-State Markovian Decision Processes. Academic Press, 1970.
A. Finkel. Decidability of the termination problem for completely specificied protocols. Distributed Computing, 7(3):129–135, 1994.
S. Hart, M. Sharir, and A. Pnueli. Termination of probabilistic concurrent programs. ACM Transactions on Programming Languages and Systems, 5(3):356–380, 1983.
R. Mayr. Undecidable problems in unreliable computations. In Proc. 4th Latin American Symposium on Theoretical Informatics (LATIN’2000), vol. 1776 of Lect. Notes Comp. Sci., pages 377–386. Springer, 2000.
B. Masson and Ph. Schnoebelen. On verifying fair lossy channel systems. In Proc. 27th Int. Symp. Math. Found. Comp. Sci. (MFCS’2002), vol. 2420 of Lect. Notes Comp. Sci., pages 543–555. Springer, 2002.
P. Panangaden. Measure and probability for concurrency theorists. Theoretical Computer Sci., 253(2):287–309, 2001.
S. Purushothaman Iyer and M. Narasimha. Probabilistic lossy channel systems. In Proc. 7th Int. Joint Conf. Theory and Practice of Software Development (TAPSOFT’97), vol. 1214 of Lect. Notes Comp. Sci., pages 667–681. Springer, 1997.
Ph. Schnoebelen. Bisimulation and other undecidable equivalences for lossy channel systems. In Proc. 4th Int. Symp. Theoretical Aspects of Computer Software (TACS’2001), vol. 2215 of Lect. Notes Comp. Sci., pages 385–399. Springer, 2001.
Ph. Schnoebelen. Verifying lossy channel systems has nonprimitive recursive complexity. Information Processing Letters, 83(5):251–261, 2002.
M. Y. Vardi. Automatic verification of probabilistic concurrent finite-state programs. In Proc. 26th IEEE Symp. Foundations of Computer Science (FOCS’85), pages 327–338, 1985.
M. Y. Vardi. Probabilistic linear-time model checking: An overview of the automata-theoretic approach. In Proc. 5th Int. AMAST Workshop Formal Methods for Real-Time and Probabilistic Systems (ARTS’99), vol. 1601 of Lect. Notes Comp. Sci., pages 265–276. Springer, 1999.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bertrand, N., Schnoebelen, P. (2003). Model Checking Lossy Channels Systems Is Probably Decidable. In: Gordon, A.D. (eds) Foundations of Software Science and Computation Structures. FoSSaCS 2003. Lecture Notes in Computer Science, vol 2620. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-36576-1_8
Download citation
DOI: https://doi.org/10.1007/3-540-36576-1_8
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-00897-2
Online ISBN: 978-3-540-36576-1
eBook Packages: Springer Book Archive