Skip to main content
SpringerLink
Log in

Establishing Qualitative Properties for Probabilistic Lossy Channel Systems

An Algorithmic Approach

  • Conference paper
  • First Online:
Formal Methods for Real-Time and Probabilistic Systems (ARTS 1999)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 1601))

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.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. P. Abdulla, A. Bouajjani, and B. Jonsson. On-the-fly analysis of systems with unbounded, lossy FIFO channels. LNCS, 1427:305–318, 1998.

    MathSciNet  Google Scholar 

  2. 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.

    Google Scholar 

  3. 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.

    MathSciNet  MATH  Google Scholar 

  4. P. Abdulla and M. Kindahl. Decidability of simulation and bisimulation between lossy channel systems and finite state systems. LNCS, 962:333–347, 1995.

    Google Scholar 

  5. P. Abdulla, M. Kindahl, and D. Peled. An improved search strategy for lossy channel systems. In PSTV/FORTE. Chapman-Hall, 1997.

    Google Scholar 

  6. 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.

    Google Scholar 

  7. 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.

    MATH  Google Scholar 

  8. M. Browne, E. Clarke, and O. Grumberg. Characterizing finite Kripke structures in propositional temporal logic. Theoretical Computer Science, 59:115–131, 1988.

    Article  MathSciNet  MATH  Google Scholar 

  9. A. Bianco and L. de Alfaro. Model checking of probabilistic and nondeterministic systems. LNCS, 1026:499–513, 1995.

    MathSciNet  MATH  Google Scholar 

  10. 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.

    Google Scholar 

  11. C. Baier and H. Hermanns. Weak bisimulation for fully probabilistic processes. LNCS, 1254:119–130, 1997.

    Google Scholar 

  12. C. Baier and M. Kwiatkowska. Model checking for a probabilistic branching time logic with fairness. Distributed Computing, 11:125–155, 1998.

    Article  Google Scholar 

  13. A. Bouajjani and R. Mayr. Model checking lossy vector addition systems. 1998. To appear in Proc. STACS’99, LNCS.

    Google Scholar 

  14. L. Breiman. Probability. Addison-Wesley Publishing Company, 1968.

    Google Scholar 

  15. 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.

    Article  Google Scholar 

  16. D. Brand and P. Zafiropulo. On communicating finite-state machines. Journal of the ACM, 30(2):323–342, 1983.

    Article  MathSciNet  MATH  Google Scholar 

  17. L. Christoff and I. Christoff. Efficient algorithms for verification of equivalences for probabilistic processes. Proc. CAV’91, LNCS, 575:310–321, 1991.

    Google Scholar 

  18. 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.

    Chapter  Google Scholar 

  19. 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.

    Article  MATH  Google Scholar 

  20. 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.

    Article  MathSciNet  MATH  Google Scholar 

  21. C. Courcoubetis and M. Yannakakis. Verifying temporal properties of finite-state probabilistic programs. Proc. FOCS’88, pages 338–345, 1988.

    Google Scholar 

  22. C. Courcoubetis and M. Yannakakis. The complexity of probabilistic verification. Journal of the ACM, 42(4):857–907, 1995.

    Article  MathSciNet  MATH  Google Scholar 

  23. L. de Alfaro. Temporal logics for the specification of performance and reliability. Proc. STACS’97, LNCS, 1200:165–176, 1997.

    Google Scholar 

  24. E. Emerson. Temporal and modal logic. Handbook of Theoretical Computer Science, B:995–1072, 1990.

    MathSciNet  MATH  Google Scholar 

  25. W. Feller. An Introduction to Probability Theory and its Application. John Wiley and Sons, New York, 1968.

    MATH  Google Scholar 

  26. A. Finkel. Decidability of the termination problem for completely specified protocols. Distributed Computing, 7(3):129–135, 1994.

    Article  Google Scholar 

  27. H. Hansson and B. Jonsson. A logic for reasoning about time and reliability. Formal Aspects of Computing, 6(5):512–535, 1994.

    Article  MATH  Google Scholar 

  28. 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.

    Article  MathSciNet  MATH  Google Scholar 

  29. S. Hart, M. Sharir, and A. Pnueli. Termination of probabilistic concurrent program. ACM Transactions on Programming Languages and Systems, 5(3):356–380, 1983.

    Article  MATH  Google Scholar 

  30. T. Huynh and L. Tian. On some equivalence relations for probabilistic processes. Fundamenta Informaticae, 17:211–234, 1992.

    MathSciNet  MATH  Google Scholar 

  31. 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.

    Google Scholar 

  32. P. Iyer and M. Narasimha. Probabilistic lossy channel systems. Proc. TAPSOFT’97, LNCS, 1214:667–681, 1997.

    Google Scholar 

  33. ISO. Data communications-HDLC procedures-elements of procedures. Technical Report TR-ISO-4335, International Standards Organization, Geneva, 1979.

    Google Scholar 

  34. C. Jou and S. Smolka. Equivalences, congruences, and complete axiomatizations for probabilistic processes. In Proc. CONCUR’90, LNCS, 458:367–383, 1990.

    Google Scholar 

  35. D. Lehmann and S. Shelah. Reasoning about time and chance. Information and Control, 53(3):165–198, 1982.

    Article  MathSciNet  MATH  Google Scholar 

  36. K. Larsen and A. Skou. Compositional verification of probabilistic processes. In CONCUR’92, LNCS, 630:456–471, 1992.

    Google Scholar 

  37. N. Lynch and M. Tuttle. Hierarchical Correctness Proofs For Distributed Algorithms. PODC’87, pages 137–151, 1987.

    Google Scholar 

  38. N. Lynch. Distributed Algorithms. Morgan Kaufmann Series in Data Management Systems. Morgan Kaufmann Publishers, 1995.

    Google Scholar 

  39. Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems-Specification. Springer-Verlag, 1992.

    Google Scholar 

  40. 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.

    Article  MathSciNet  MATH  Google Scholar 

  41. S. Safra. On the complexity of ω-automata. FOCS’88, pages 319–327, 1988.

    Google Scholar 

  42. R. Segala. Modeling and Verification of Randomized Distributed Real-Time Systems. PhD thesis, Massachusetts Institute of Technology, 1995.

    Google Scholar 

  43. W. Thomas. Automata on infinite objects. Handbook of Theoretical Computer Science, B:133–191, 1990.

    MathSciNet  MATH  Google Scholar 

  44. M. Vardi. Automatic verification of probabilistic concurrent finite-state programs. FOCS’85, pages 327–338, 1985.

    Google Scholar 

  45. M. Vardi. An automata-theoretic approach to linear temporal logic. LNCS, 1043:238–266, 1996.

    Google Scholar 

  46. M. Vardi and P. Wolper. An automata-theoretic approach to automatic program verification. LICS’ 86, pages 332–345, 1986.

    Google Scholar 

  47. M. Vardi and P. Wolper. Reasoning about infinite computations. Information and Computation, 115(1):1–37, 1994.

    Article  MathSciNet  MATH  Google Scholar 

  48. P. Wolper, M. Vardi, and A. Sistla. Reasoning about infinite computation paths (extended abstract). FOCS’83, pages 185–194, 1983.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Fakultät für Mathematik & Informatik, D7, 27, Universität Mannheim, 68131, Mannheim, Germany

    Christel Baier & Bettina Engelen

Authors
  1. Christel Baier
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Bettina Engelen
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Lehrstuhl für Informatik, University of Erlangen-Nürnberg, Martensstr. 3, D-91058, Erlangen, Germany

    Joost-Pieter Katoen

  2. Formal Methods and Tools Group, University of Twente, P.O. Box 217, 7500 AE, Enschede, The Netherlands

    Joost-Pieter Katoen

Rights and permissions

Reprints 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

Publish with us

Policies and ethics

Search

Navigation