Advertisement

Fundamental structures in Well-Structured infinite Transition Systems

  • Alain Finkel
  • Philippe Schnoebelen
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1380)

Abstract

We suggest a simple and clean definition for Well-Structured Transition Systems [20, 1], a general class of infinite state systems for which decidability results exist. As a consequence we can (1) generalize the definition in many ways, (2) find examples of (general) WSTS's in many fields, and (3) present new decidability results.

Keywords

Transition System Decidability Result Fundamental Structure Finite State Automaton Finite Basis 
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.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    P. A. Abdulla, K. čerāns, B. Jonsson, and T. Yih-Kuen. General decidability theorems for infinite-state systems. In Proc. 11th IEEE Symp. Logic in Computer Science (LICS'96), New Brunswick, NJ, USA, July 1996, pages 313–321, 1996.Google Scholar
  2. 2.
    P. A. Abdulla and B. Jonsson. Verifying programs with unreliable channels. In Proc. 8th IEEE Symp. Logic in Computer Science (LICS'93), Montreal, Canada, June 1993, pages 160–170, 1993.Google Scholar
  3. 3.
    P. A. Abdulla and B. Jonsson. Undecidability of verifying programs with unreliable channels. In Proc. 21st Int. Coll. Automata, Languages, and Programming (ICALP'94), Jerusalem, Israel, July 1994, volume 820 of Lecture Notes in Computer Science, pages 316–327. Springer-Verlag, 1994.Google Scholar
  4. 4.
    P. A. Abdulla and B. Jonsson. Model-checking through constraint solving. In Methods and Tools for the Verification of Infinite State Systems, Proceedings of the Grenoble-Alpe d'Huez European School of Computer Science, May 23–25, Grenoble, France. VERIMAG, St-Martin d'Hères, France, 1997.Google Scholar
  5. 5.
    J. C. M. Baeten, J. A. Bergstra, and J. W. Klop. Decidability of bisimulation equivalence for processes generating context-free languages. In Proc. Parallel Architectures and Languages Europe (PARLE'87), Eindhoven, NL, June 1987, vol. II: Parallel Languages, volume 259 of Lecture Notes in Computer Science, pages 94–111. Springer-Verlag, 1987.Google Scholar
  6. 6.
    M. C. Browne, E. M. Clarke, and O. Grümberg. Characterizing finite Kripke structures in propositional temporal logic. Theoretical Computer Science, 59(1–2):115–131, 1988.CrossRefMathSciNetGoogle Scholar
  7. 7.
    J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, and L. J. Hwang. Symbolic model checking: 1020 states and beyond. Information and Computation, 98(2):142–170, 1992.CrossRefMathSciNetGoogle Scholar
  8. 8.
    G. von Bochmann. Finite state description of communication protocols. Computer Networks and ISDN Systems, 2:361–372, 1978.Google Scholar
  9. 9.
    A. Bonchatbonrat. Concise Holmesian proofs for elementary Moncher-Watson problems. In A. Mycroft, editor, Proc. 3rd Int. Conf. Theor. Crim. Deduction, London, November 1894.Google Scholar
  10. 10.
    G. Cécé. Etat de l'art des techniques d'analyse des automates finis communicants. Rapport de DEA, Université de Paris-Sud, Orsay, France, September 1993.Google Scholar
  11. 11.
    K. čerāns. Deciding properties of integral relational automata. In Proc. 21st Int. Coll. Automata, Languages, and Programming (ICALP'94), Jerusalem, Israel, July 1994, volume 820 of Lecture Notes in Computer Science, pages 35–46. Springer-Verlag, 1994.Google Scholar
  12. 12.
    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, 1995.CrossRefGoogle Scholar
  13. 13.
    S. Christensen. Decidability and decomposition in process algebras. PhD thesis CST-105-93, Dept. of Computer Science, University of Edinburgh, UK, 1993.Google Scholar
  14. 14.
    G. Ciardo. Petri nets with marking-dependent arc cardinality: Properties and analysis. In Proc. 15th Int. Conf. Applications and Theory of Petri Nets, Zaragoza, Spain, June 1994, volume 815 of Lecture Notes in Computer Science, pages 179–198. Springer-Verlag, 1994.Google Scholar
  15. 15.
    J. Esparza. More infinite results. In Proc. 1st Int. Workshop on Verification of Infinite State Systems (INFINITY'96), Pisa, Italy, Aug. 1996, volume 5 of Electronic Notes in Theor. Comp. Sci. Elsevier, 1997.Google Scholar
  16. 16.
    A. Finkel and A. Choquet. Fifo nets without order deadlock. Acta Informatica, 25(1):15–36, 1987.CrossRefMathSciNetGoogle Scholar
  17. 17.
    A. Finkel. About monogeneous fifo Petri nets. In Proc. 3rd European Workshop on Applications and Theory of Petri Nets, Varenna, Italy, Sep. 1982, pages 175–192, 1982.Google Scholar
  18. 18.
    A. Finkel. A generalization of the procedure of Karp and Miller to well structured transition systems. In Proc. 14th Int. Coll. Automata, Languages, and Programming (ICALP'87), Karlsruhe, FRG, July 1987, volume 267 of Lecture Notes in Computer Science, pages 499–508. Springer-Verlag, 1987.Google Scholar
  19. 19.
    A. Finkel. Well structured transition systems. Research Report 365, Lab. de Recherche en Informatique (LRI), Univ. Paris-Sud, Orsay, August 1987.Google Scholar
  20. 20.
    A. Finkel. Reduction and covering of infinite reachability trees. Information and Computation, 89(2):144–179, 1990.zbMATHCrossRefMathSciNetGoogle Scholar
  21. 21.
    A. Finkel. The minimal coverability graph algorithm. In Advances in Petri Nets 1993, volume 674 of Lecture Notes in Computer Science, pages 210–243. Springer-Verlag, 1993.Google Scholar
  22. 22.
    A. Finkel. Decidability of the termination problem for completely specificied protocols. Distributed Computing, 7:129–135, 1994.CrossRefGoogle Scholar
  23. 23.
    M. G. Gouda and L. E. Rosier. Synchronizable networks of communicating finite state machines. Unpublished manuscript, 1985.Google Scholar
  24. 24.
    M. Hennessy and R. Milner. Algebraic laws for nondeterminism and concurrency. Journal of the ACM, 32(1):137–161, 1985.CrossRefMathSciNetGoogle Scholar
  25. 25.
    O. Kouchnarenko and Ph. Schnoebelen. A model for recursive-parallel programs. In Proc. 1st Int. Workshop on Verification of Infinite State Systems (INFINITY'96), Pisa, Italy, Aug. 1996, volume 5 of Electronic Notes in Theor. Comp. Sci. Elsevier, 1997.Google Scholar
  26. 26.
    C. Lakos and S. Christensen. A general approach to arc extensions for coloured Petri nets. In Proc. 15th Int. Conf. Applications and Theory of Petri Nets, Zaragoza, Spain, June 1994, volume 815 of Lecture Notes in Computer Science, pages 338–357. Springer-Verlag, 1994.Google Scholar
  27. 27.
    E. Mäkinen. On permutation grammars generating context-free languages. BIT, 25:604–610, 1985.zbMATHCrossRefMathSciNetGoogle Scholar
  28. 28.
    F. Moller. Infinite results. In Proc. 7th Int. Conf. Concurrency Theory (CONCUR'96), Pisa, Italy, Aug. 1996, volume 1119 of Lecture Notes in Computer Science, pages 195–216. Springer-Verlag, 1996.Google Scholar
  29. 29.
    R. Valk. Self-modifying nets, a natural extension of Petri nets. In Proc. 5th Int. Coll. Automata, Languages, and Programming (ICALP'78), Udine, Italy, Jul. 1978, volume 62 of Lecture Notes in Computer Science, pages 464–476. Springer-Verlag, 1978.Google Scholar
  30. 30.
    R. Valk and M. Jantzen. The residue of vector sets with applications to decidability problems in Petri nets. Acta Informatica, 21:643–674, 1985.CrossRefMathSciNetGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1998

Authors and Affiliations

  • Alain Finkel
    • 1
  • Philippe Schnoebelen
    • 1
  1. 1.Lab. Specification and VerificationENS de Cachan & CNRS URA 2236Cachan CedexFrance

Personalised recommendations