Skip to main content
SpringerLink
Log in

Undecidable verification problems for programs with unreliable channels

  • Conference paper
  • First Online:
Automata, Languages and Programming (ICALP 1994)

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

Included in the following conference series:

Abstract

We consider the verification of a particular class of infinite-state systems, namely systems consisting of finite-state processes that communicate via unbounded lossy FIFO channels. This class is able to model e.g. link protocols such as the Alternating Bit Protocol and HDLC. In an earlier paper, we showed that several interesting verification problems are decidable for this class of systems, namely (1) the reachability problem: is a set of states reachable from some other state of the system, (2) safety property over traces formulated as regular sets of allowed finite traces, and (3) eventuality properties: do all computations of a system eventually reach a given set of states. In this paper, we show that the following problems are undecidable, namely

  • The model checking problem in propositional temporal logics such as Propositional Linear Time Logic (PTL) and Computation Tree Logic (CTL).

  • The problem of deciding eventuality properties with fair channels: do all computations eventually reach a given set of states if the unreliable channels are fair in the sense that they deliver infinitely many messages if infinitely many messages are transmitted. This problem can model the question of whether a link protocol, such as HDLC, will eventually reliably transfer messages across a medium that is not permanently broken.

The results are obtained through a reduction from a variant of Post's Correspondence Problem.

Supported in part by the Swedish Board for Industrial and Technical Development (NUTEK) as part of ESPRIT BRA project No. 6021 (REACT), and by the Swedish Research Council for Engineering Sciences (TFR) under contract No. 92-814.

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

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. R. Alur, C. Courcoubetis, and D. Dill. Model-checking for real-time systems. In Proc. 5th IEEE Int. Symp. on Logic in Computer Science, pages 414–425, Philadelphia, 1990.

    Google Scholar 

  2. Parosh Aziz Abdulla and Bengt Jonsson. Verifying programs with unreliable channels. In Proc. 8th IEEE Int. Symp. on Logic in Computer Science, 1993.

    Google Scholar 

  3. Parosh Aziz Abdulla and Bengt Jonsson. Undecidable verification problems for programs with unreliable channels. Technical Report 94/47, Dept. of Computer Systems, Uppsala University, Sweden, 1994.

    Google Scholar 

  4. J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill, and L.J. Hwang. Symbolic model checking: 1020 states and beyond. In Proc. 5th IEEE Int. Symp. on Logic in Computer Science, 1990.

    Google Scholar 

  5. K. Bartlett, R. Scantlebury, and P. Wilkinson. A note on reliable full-duplex transmissions over half duplex lines. Communications of the ACM, 2(5):260–261, 1969.

    Google Scholar 

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

    Google Scholar 

  7. K. Cerans. Decidability of bisimulation equivalence for parallel timer processes. In Proc. Workshop on Computer Aided Verification, volume 663 of Lecture Notes in Computer Science, pages 302–315, 1992.

    Google Scholar 

  8. E.M. Clarke, E.A. Emerson, and A.P. Sistla. Automatic verification of finite-state concurrent systems using temporal logic specification. ACM Trans. on Programming Languages and Systems, 8(2):244–263, April 1986.

    Google Scholar 

  9. A. Choquet and A. Finkel. Simulation of linear FIFO nets having a structured set of terminal markings. In Proc. 8th European Workshop on Applications and Theory of Petri Nets, 1987.

    Google Scholar 

  10. E. M. Clarke and O. Grumberg. Avoiding the state explosion problem in temporal logic model checking algorithms. In Proc. 6th ACM Symp. on Principles of Distributed Computing, Vancouver, Canada, pages 294–303, 1987.

    Google Scholar 

  11. A. Finkel. A new class of analyzable CFSMs with unbounded FIFO channels. In Protocol Specification, Testing, and Verification VIII, pages 1–12, Atlantic City, USA, 1988. IFIP WG 6.1, North-Holland.

    Google Scholar 

  12. A. Finkel. Decidability of the termination problem for completely specified protocols. Technical Report 463, LRI, University Paris-Sud, 1989. Also accepted for publication in the Distributed Computing Journal.

    Google Scholar 

  13. M.G. Gouda, E.M. Gurari, T.-H. Lai, and L.E. Rosier. On deadlock detection in systems of communicating finite state machines. Computers and Artificial Intelligence, 6(3):209–228, 1987.

    Google Scholar 

  14. S. M. German and A. P. Sistla. Reasoning about systems with many processes. Journal of the ACM, 39(3):675–735, 1992.

    Google Scholar 

  15. G.J. Holzmann. Design and Validation of Computer Protocols. Prentice Hall, 1991.

    Google Scholar 

  16. ISO. Data communications — HDLC procedures — elements of procedures. Technical Report ISO 4335, International Standards Organization, Geneva, Switzerland, 1979.

    Google Scholar 

  17. B. Jonsson and J. Parrow. Deciding bisimulation equivalences for a class of non-finite-state programs. In Monien and Cori, editors, Proc. 6th Symposium on Theoretical Aspects of Computer Science, volume 349 of Lecture Notes in Computer Science, pages 421–433. Springer Verlag, 1989. Revised version to appear in Information and Computation.

    Google Scholar 

  18. R.M. Karp and R.E. Miller. Parallel program schemata. Journal of Computer and Systems Sciences, 3(2):147–195, May 1969.

    Google Scholar 

  19. J.K. Pachl. Protocol description and analysis based on a state transition model with channel expressions. In Protocol Specification, Testing, and Verification VII, May 1987.

    Google Scholar 

  20. W. Peng and S. Purushothaman. Data flow analysis of communicating finite state machines. ACM Trans. on Programming Languages and Systems, 13(3):399–442, July 1991.

    Google Scholar 

  21. K. Ruohonen. On some variants of Post's correspondence problem. Acta Informatica, (19):357–367, 1983.

    Google Scholar 

  22. L.E. Rosier and H-C. Yen. Boundedness, empty channel detection and synchronization for communicating finite automata. Theoretical Computer Science, 44:69–105, 1986.

    Google Scholar 

  23. Z. Shtadler and O. Grumberg. Network grammars, communication behaviours and automatic verification. In Sifakis, editor, Proc. Workshop on Computer Aided Verification, volume 407 of Lecture Notes in Computer Science, pages 151–165. Springer Verlag, 1990.

    Google Scholar 

  24. A.P. Sistla and L.D. Zuck. Automatic temporal verification of buffer systems. In Larsen and Skou, editors, Proc. Workshop on Computer Aided Verification, volume 575 of Lecture Notes in Computer Science. Springer Verlag, 1991.

    Google Scholar 

  25. M. Y. Vardi and P. Wolper. An automata-theoretic approach to automatic program verification. In Proc. 1st IEEE Int. Symp. on Logic in Computer Science, pages 332–344, June 1986.

    Google Scholar 

  26. Pierre Wolper. Expressing interesting properties of programs in propositional temporal logic (extended abstract). In Proc. 13th ACM Symp. on Principles of Programming Languages, pages 184–193, Jan. 1986.

    Google Scholar 

  27. Wang Yi. CCS + Time = an interleaving model for real time systems. In Leach Albert, Monien, and Rodriguez Artalejo, editors, Proc. ICALP '91, volume 510 of Lecture Notes in Computer Science. Springer Verlag, 1991.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Dept. of Computer Systems, Uppsala University, P.O. Box 325, 751 05, Uppsala, Sweden

    Parosh Aziz Abdulla & Bengt Jonsson

Authors
  1. Parosh Aziz Abdulla
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Bengt Jonsson
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Serge Abiteboul Eli Shamir

Rights and permissions

Reprints and permissions

Copyright information

© 1994 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Abdulla, P.A., Jonsson, B. (1994). Undecidable verification problems for programs with unreliable channels. In: Abiteboul, S., Shamir, E. (eds) Automata, Languages and Programming. ICALP 1994. Lecture Notes in Computer Science, vol 820. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-58201-0_78

Download citation

  • DOI: https://doi.org/10.1007/3-540-58201-0_78

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-58201-4

  • Online ISBN: 978-3-540-48566-7

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation