Advertisement

Weakest Congruence Results Concerning “Any-Lock”

  • Antti Puhakka
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2215)

Abstract

In process algebras the weakest congruences that preserve interesting properties of systems are of theoretical and practical importance. A system can stop executing visible actions in two ways: by deadlocking or livelocking. The weakest deadlock-preserving congruence was published in [20]. The weakest livelock-preserving congruence and the weakest congruence that preserves all traces of visible actions leading to a livelock were published in [17]. In this paper we will equate deadlock and livelock. We introduce the weakest congruence that preserves the predicate “any-lock” which distinguishes those systems that can stop executing visible actions from those that cannot. We also present the weakest congruence that preserves all traces after which the system can stop executing visible actions. Finally, we give two simple weakest-congruence characterisations for the CSP failures-divergences equivalence, one of which is a minimal characterisation in a well-defined sense. However, we also show that there is no minimum (least) characterisation.

Keywords

Semantic Model Linear Temporal Logic Parallel Composition Visible Action Label Transition System 
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.
    Bergstra, J. A., Klop, J. W. & Olderog, E.-R.: “Failures without Chaos: A New Process Semantics for Fair Abstraction”. Formal Description of Programming Concepts III, North-Holland 1987, pp. 77–103.Google Scholar
  2. 2.
    Bolognesi, T. & Brinksma, E.: “Introduction to the ISO Specification Language LOTOS”. Computer Networks and ISDN Systems 14, 1987, pp. 25–59.CrossRefGoogle Scholar
  3. 3.
    Boreale, M., De Nicola, R. & Pugliese, R.: “Basic Observables for Processes”. Information and Computation 149 (1999), pp. 77–98.zbMATHCrossRefMathSciNetGoogle Scholar
  4. 4.
    Brinksma, E., Rensink, A. & Vogler, W.: “Fair Testing”. Proc. CONCUR’95, 6th International Conference on Concurrency Theory, Lecture Notes in Computer Science 962, Springer-Verlag 1995, pp. 313–327.Google Scholar
  5. 5.
    Brookes, S. D. & Roscoe, A. W.: “An Improved Failures Model for Communicating Sequential Processes”. Proc. NSF-SERC Seminar on Concurrency, Lecture Notes in Computer Science 197, Springer-Verlag 1985, pp. 281–305.Google Scholar
  6. 6.
    De Nicola, R. & Hennessy, M.: “Testing Equivalences for Processes”. Theoretical Computer Science 34 (1984), pp. 83–133.zbMATHCrossRefMathSciNetGoogle Scholar
  7. 7.
    Fournet, C. & Gonthier, G.: “A Hierarchy of Equivalences for Asynchronous Calculi”. Proc. ICALP’98, 25th International Colloquium on Automata, Languages and Programming, Lecture Notes in Computer Science 1443, Springer-Verlag 1998, pp. 844–855.CrossRefGoogle Scholar
  8. 8.
    Hennessy, M.: “Synchronous and Asynchronous Experiments on processes”. Information and Control 59(1983), pp. 36–83.zbMATHCrossRefMathSciNetGoogle Scholar
  9. 9.
    Hoare, C. A. R.: Communicating Sequential Processes. Prentice-Hall 1985, 256 p.Google Scholar
  10. 10.
    Kaivola, R. & Valmari, A.: “The Weakest Compositional Semantic Equivalence Preserving Nexttime-less Linear Temporal Logic”. Proc. CONCUR’92, Third International Conference on Concurrency Theory, Lecture Notes in Computer Science 630, Springer-Verlag 1992, pp. 207–221.Google Scholar
  11. 11.
    Leduc, G.: “Failure-based Congruences, Unfair Divergences and New Testing Theory”. Proc. Protocol Specification, Testing and Verification, XIV, Chapman & Hall, London (1995), pp. 252–267.Google Scholar
  12. 12.
    Manna, Z. & Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems, Volume I: Specification. Springer-Verlag 1992, 427 p.Google Scholar
  13. 13.
    Milner, R.: Communication and Concurrency. Prentice-Hall 1989, 260 p.Google Scholar
  14. 14.
    Milner, R.: “The polyadic π-calculus: a tutorial”. In Bauer, F. L., Brauer, W. & Schwichtenberg, H. (editors), Logic and Algebra of Specification, Springer-Verlag 1993, pp. 203–246.Google Scholar
  15. 15.
    Milner, R. & Sangiorgi, D.: “Barbed Bisimulation”. Proc. ICALP92, 19th International Colloquium on Automata, Languages and Programming, Lecture Notes in Computer Science 623, Springer-Verlag 1992, pp. 685–695.Google Scholar
  16. 16.
    Older, S.: “Strong Fairness and Full Abstraction for Communicating Processes”. Information and Computation 163 (2000), pp. 471–509.zbMATHCrossRefMathSciNetGoogle Scholar
  17. 17.
    Puhakka, A. & Valmari, A.: “Weakest-Congruence Results for Livelock-Preserving Equivalences”. Proc. CONCUR’99, 10th International Conference on Concurrency Theory, Lecture Notes in Computer Science 1664, Springer-Verlag 1999, pp. 510–524.CrossRefGoogle Scholar
  18. 18.
    Puhakka, A. & Valmari, A.: “Liveness and Fairness in Process-Algebraic Verification”. To appear in Proc. CONCUR’01, 12th International Conference on Concurrency Theory, Lecture Notes in Computer Science, Springer-Verlag.Google Scholar
  19. 19.
    Roscoe, A. W.: The Theory and Practice of Concurrency. Prentice-Hall 1998, 565 p.Google Scholar
  20. 20.
    Valmari, A.: “The Weakest Deadlock-Preserving Congruence”. Information Processing Letters 53 (1995), pp. 341–346.zbMATHCrossRefMathSciNetGoogle Scholar
  21. 21.
    Valmari, A.: “Failure-based Equivalences Are Faster Than Many Believe”. Proc. Structures in Concurrency Theory 1995, Springer-Verlag “Workshops in Computing” series, 1995, pp. 326–340.Google Scholar
  22. 22.
    Valmari, A.: “The State Explosion Problem”. Lectures on Petri Nets I: Basic Models, Lecture Notes in Computer Science 1491, Springer-Verlag 1998, pp. 429–528.Google Scholar
  23. 23.
    Valmari, A. & Tienari, M.: “Compositional Failure-Based Semantic Models for Basic LOTOS”. Formal Aspects of Computing 7 (1995), pp. 440–468.zbMATHCrossRefGoogle Scholar
  24. 24.
    Vogler, W.: “Failures Semantics and Deadlocking of Modular Petri Nets”. Acta Informatica 26 (1989), pp. 333–348.zbMATHMathSciNetGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2001

Authors and Affiliations

  • Antti Puhakka
    • 1
  1. 1.Software Systems LaboratoryTampere University of TechnologyTampereFinland

Personalised recommendations