Abstract
Lossy channel systems (LCSs) are models for communicating systems where the subprocesses are linked via unbounded FIFO channels which might lose messages. Link protocols, such as the Alternating Bit Protocol and HDLC can be modelled with these systems. The decidability of several verification problems of LCSs has been investigated by Abdulla & Jonsson [AJ93], AJ94], e.g. they have shown that the reach-ability problem for LCSs is decidable while LTL model checking is not. In this paper, we consider probabilistic LCSs (which are LCSs where the transitions are augmented with appropriate probabilities) as introduced by [IN97] and show that the question of whether or not a linear time property holds with probability 1 is decidable. More precisely, we show how LTL ∖X model checking for (certain types of) probabilistic LCSs can be reduced to a reachability problem in a (non-probabilistic) LCS where the latter can be solved with the methods of [AJ93].
The second author is sponsored by the DFG-Project MA 794/3-1.
Here, LTL ∖X denotes standard linear time logic without next step.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
P. Abdulla, A. Bouajjani, and B. Jonsson. On-the-fly analysis of systems with unbounded, lossy FIFO channels. LNCS, 1427:305–318, 1998.
P. Abdulla and B. Jonsson. Verifying programs with unreliable channels. Proc. LICS’93, pages 160–170, 1993. The full version with the same title has been published in Information and Computation, 127:91–101, 1996.
P. Abdulla and B. Jonsson. Undecidable verification problems for programs with unreliable channels. LNCS, 820:316–327, 1994. The full version with the same title has been published in Information and Computation, 130:71–90, 1996.
P. Abdulla and M. Kindahl. Decidability of simulation and bisimulation between lossy channel systems and finite state systems. LNCS, 962:333–347, 1995.
P. Abdulla, M. Kindahl, and D. Peled. An improved search strategy for lossy channel systems. In PSTV/FORTE. Chapman-Hall, 1997.
A. Aziz, V. Singhal, R. Brayton, and A. Sangiovanni-Vincentelli. It usually works: The temporal logic of stochastic systems. Proc. CAV’95, 939:155–165, 1995.
J. Baeten, J. Bergstra, and S. Smolka. Axiomatizing probabilistic processes: ACP with generative probabilities (extended abstract). CONCUR’92, 630:472–485, 1992. The full version with the same title has been published in Information and Computation, 122:234–255, 1995.
M. Browne, E. Clarke, and O. Grumberg. Characterizing finite Kripke structures in propositional temporal logic. Theoretical Computer Science, 59:115–131, 1988.
A. Bianco and L. de Alfaro. Model checking of probabilistic and nondeterministic systems. LNCS, 1026:499–513, 1995.
C. Baier, B. Engelen, and M. Roggenbach. Establishing Qualitative Properties for Probabilistic Lossy Channel Systems. Technical Report 3/99, Universität Mannheim, Fakultät für Mathematik und Informatik, 1999.
C. Baier and H. Hermanns. Weak bisimulation for fully probabilistic processes. LNCS, 1254:119–130, 1997.
C. Baier and M. Kwiatkowska. Model checking for a probabilistic branching time logic with fairness. Distributed Computing, 11:125–155, 1998.
A. Bouajjani and R. Mayr. Model checking lossy vector addition systems. 1998. To appear in Proc. STACS’99, LNCS.
L. Breiman. Probability. Addison-Wesley Publishing Company, 1968.
K. Bartlett, R. Scantlebury, and P. Wilkinson. A note on reliable full-duplex transmission over half-duplex links. Communications of the ACM, 12(5):260–261, 1969.
D. Brand and P. Zafiropulo. On communicating finite-state machines. Journal of the ACM, 30(2):323–342, 1983.
L. Christoff and I. Christoff. Efficient algorithms for verification of equivalences for probabilistic processes. Proc. CAV’91, LNCS, 575:310–321, 1991.
L. Christoff and I. Christoff. Reasoning about safety and liveness properties for probabilistic processes. Proc. 12th Conference on Foundations of Software Technology and Theoretical Computer Science, LNCS, 652:342–355, 1992.
E. Clarke, E. Emerson, and A. Sistla. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems, 8(2):244–263, 1986.
G. Cécé, A. Finkel, and S. Iyer. Unreliable channels are easier to verify than perfect channels. Information and Computation, 124(1):20–31, 1996.
C. Courcoubetis and M. Yannakakis. Verifying temporal properties of finite-state probabilistic programs. Proc. FOCS’88, pages 338–345, 1988.
C. Courcoubetis and M. Yannakakis. The complexity of probabilistic verification. Journal of the ACM, 42(4):857–907, 1995.
L. de Alfaro. Temporal logics for the specification of performance and reliability. Proc. STACS’97, LNCS, 1200:165–176, 1997.
E. Emerson. Temporal and modal logic. Handbook of Theoretical Computer Science, B:995–1072, 1990.
W. Feller. An Introduction to Probability Theory and its Application. John Wiley and Sons, New York, 1968.
A. Finkel. Decidability of the termination problem for completely specified protocols. Distributed Computing, 7(3):129–135, 1994.
H. Hansson and B. Jonsson. A logic for reasoning about time and reliability. Formal Aspects of Computing, 6(5):512–535, 1994.
S. Hart and M. Sharir. Probabilistic propositional temporal logics. Information and Control, 70(2/3):97–155, 1986. This is the extended version of “Probabilistic Temporal Logics for Finite and Bounded Models”. In Proc. STOCS’84, 1–13, 1984.
S. Hart, M. Sharir, and A. Pnueli. Termination of probabilistic concurrent program. ACM Transactions on Programming Languages and Systems, 5(3):356–380, 1983.
T. Huynh and L. Tian. On some equivalence relations for probabilistic processes. Fundamenta Informaticae, 17:211–234, 1992.
P. Iyer and M. Narasimha. “Almost always” and “sometime definitely” are not enough: Probabilistic quantifiers and probabilistic model-checking. Technical Report TR-96-16, Department of Computer Science, North Carolina State University, 1996.
P. Iyer and M. Narasimha. Probabilistic lossy channel systems. Proc. TAPSOFT’97, LNCS, 1214:667–681, 1997.
ISO. Data communications-HDLC procedures-elements of procedures. Technical Report TR-ISO-4335, International Standards Organization, Geneva, 1979.
C. Jou and S. Smolka. Equivalences, congruences, and complete axiomatizations for probabilistic processes. In Proc. CONCUR’90, LNCS, 458:367–383, 1990.
D. Lehmann and S. Shelah. Reasoning about time and chance. Information and Control, 53(3):165–198, 1982.
K. Larsen and A. Skou. Compositional verification of probabilistic processes. In CONCUR’92, LNCS, 630:456–471, 1992.
N. Lynch and M. Tuttle. Hierarchical Correctness Proofs For Distributed Algorithms. PODC’87, pages 137–151, 1987.
N. Lynch. Distributed Algorithms. Morgan Kaufmann Series in Data Management Systems. Morgan Kaufmann Publishers, 1995.
Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems-Specification. Springer-Verlag, 1992.
A. Pnueli and L. Zuck. Probabilistic Verification. Information and Computation, 103(1):1–29, 1993. This is the extended version of “Probabilistic Verification by Tableaux”. In Proc. LICS’86, 322–331, 1986.
S. Safra. On the complexity of ω-automata. FOCS’88, pages 319–327, 1988.
R. Segala. Modeling and Verification of Randomized Distributed Real-Time Systems. PhD thesis, Massachusetts Institute of Technology, 1995.
W. Thomas. Automata on infinite objects. Handbook of Theoretical Computer Science, B:133–191, 1990.
M. Vardi. Automatic verification of probabilistic concurrent finite-state programs. FOCS’85, pages 327–338, 1985.
M. Vardi. An automata-theoretic approach to linear temporal logic. LNCS, 1043:238–266, 1996.
M. Vardi and P. Wolper. An automata-theoretic approach to automatic program verification. LICS’ 86, pages 332–345, 1986.
M. Vardi and P. Wolper. Reasoning about infinite computations. Information and Computation, 115(1):1–37, 1994.
P. Wolper, M. Vardi, and A. Sistla. Reasoning about infinite computation paths (extended abstract). FOCS’83, pages 185–194, 1983.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Baier, C., Engelen, B. (1999). Establishing Qualitative Properties for Probabilistic Lossy Channel Systems. In: Katoen, JP. (eds) Formal Methods for Real-Time and Probabilistic Systems. ARTS 1999. Lecture Notes in Computer Science, vol 1601. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48778-6_3
Download citation
DOI: https://doi.org/10.1007/3-540-48778-6_3
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-66010-1
Online ISBN: 978-3-540-48778-4
eBook Packages: Springer Book Archive