Advertisement

Using Fairness Constraints in Process-Algebraic Verification

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

Abstract

Although liveness and fairness have been used for a long time in classical model checking, with process-algebraic methods they have seen far less use. One problem is that it is difficult to combine fairness constraints with the compositionality of process algebra. Here we show how a class of fairness constraints can be applied in a consistent way to processes in the compositional setting. We use only ordinary, but possibly infinite, LTSs as our models of processes. In many cases the infinite LTSs are part of a larger system, which can again be represented as a finite LTS. We show how this finiteness can be recovered, namely, we present an algorithm that checks whether a finite representation exists and, if it does, constructs a finite LTS that is equivalent to the infinite system. Even in the negative case, the system produced by the algorithm is a conservative estimate of the infinite system. Such a finite representation can be placed as a component in further compositional analysis just like any other LTS.

Keywords

Temporal Logic 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.
    Aho, A.V., Hopcroft, J.E., Ullman, J.D.: The Design and Analysis of Computer Algorithms, p. 470. Addison-Wesley Publishing Company, Reading (1974)zbMATHGoogle Scholar
  2. 2.
    Alpern, B., Schneider, F.: Defining Liveness. Information Processing Letters 21(4), 181–185 (1985)zbMATHCrossRefMathSciNetGoogle Scholar
  3. 3.
    Apt, K., Francez, N., Katz, S.: Appraising Fairness in Languages for Distributed Programming. Distributed Computing 2(4), 226–241 (1988)zbMATHCrossRefGoogle Scholar
  4. 4.
    Bartlett, K.A., Scantlebury, R.A., Wilkinson, P.T.: A Note on Reliable Full-Duplex Transmission Over Half-Duplex Links. Communications of the ACM 12(5), 260–261 (1969)CrossRefGoogle Scholar
  5. 5.
    Brinksma, E., Rensink, A., Vogler, W.: Fair Testing. In: Lee, I., Smolka, S.A. (eds.) CONCUR 1995. LNCS, vol. 962, pp. 313–327. Springer, Heidelberg (1995)Google Scholar
  6. 6.
    Clarke, E.M., Emerson, E.A.: Synthesis of [2] Synchronization Skeletons for Branching Time Temporal Logic. In: Kozen, D. (ed.) Logic of Programs 1981. LNCS, vol. 131, pp. 52–71. Springer, Heidelberg (1982)CrossRefGoogle Scholar
  7. 7.
    Cleaveland, R., Lüttgen, G.: A Semantic Theory for Heterogeneous System Design. In: Kapoor, S., Prasad, S. (eds.) FST TCS 2000. LNCS, vol. 1974, pp. 312–324. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  8. 8.
    Costa, G., Stirling, C.: A Fair Calculus of Communicating Systems. Acta Informatica 21(1), 417–441 (1984)zbMATHCrossRefMathSciNetGoogle Scholar
  9. 9.
    Francez, N.: Fairness, p. 295. Springer, Heidelberg (1986)zbMATHGoogle Scholar
  10. 10.
    Gerth, R., Peled, D., Vardi, M.Y., Wolper, P.: Simple On-the-fly Automatic Verification of Linear Temporal Logic. In: Proc. Fifteenth IFIP International Symposium on Protocol Specification, Testing and Verification. IFIP Conference Proceedings 38, pp. 3–18 (1995)Google Scholar
  11. 11.
    Hennessy, M.: An Algebraic Theory of Fair Asynchronous Communicating Processes. Theoretical Computer Science 49(2,3), 121–143 (1987)zbMATHCrossRefMathSciNetGoogle Scholar
  12. 12.
    Hoare, C.A.R.: Communicating Sequential Processes, p. 256. Prentice-Hall, Englewood Cliffs (1985)zbMATHGoogle Scholar
  13. 13.
    Kaivola, R., Valmari, A.: The Weakest Compositional Semantic Equivalence Preserving Nexttime-less Linear Temporal Logic. In: Cleaveland, W.R. (ed.) CONCUR 1992. LNCS, vol. 630, pp. 207–221. Springer, Heidelberg (1992)CrossRefGoogle Scholar
  14. 14.
    Lehmann, D., Pnueli, A., Stavi, J.: Impartiality, Justice and Fairness: The Ethics of Concurrent Termination. In: Even, S., Kariv, O. (eds.) ICALP 1981. LNCS, vol. 115, pp. 264–277. Springer, Heidelberg (1981)Google Scholar
  15. 15.
    Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems, Specification, vol. I, p. 427. Springer, Heidelberg (1992)Google Scholar
  16. 16.
    Milner, R.: Communication and Concurrency, 260 p. Prentice-Hall, Englewood Cliffs (1989)zbMATHGoogle Scholar
  17. 17.
    Older, S.: Strong Fairness and Full Abstraction for Communicating Processes. Information and Computation 163(2), 471–509 (2000)zbMATHCrossRefMathSciNetGoogle Scholar
  18. 18.
    Parrow, J.: Fairness Properties in Process Algebra with Applications in Communication Protocol Verification. Ph.D. thesis, Uppsala University, 176 p. (1985)Google Scholar
  19. 19.
    Pnueli, A.: A Temporal Logic of Concurrent Programs. Theoretical Computer Science 13, 45–60 (1981)zbMATHCrossRefMathSciNetGoogle Scholar
  20. 20.
    Puhakka, A.: Using Fairness in Process-Algebraic Verification. Tampere University of Technology, Institute of Software Systems Report 24 (2003), http://www.cs.tut.fi/ohj/VARG/publications/
  21. 21.
    Puhakka, A., Valmari, A.: Liveness and Fairness in Process-Algebraic Verification. In: Larsen, K.G., Nielsen, M. (eds.) CONCUR 2001. LNCS, vol. 2154, pp. 202–217. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  22. 22.
    Queille, J.P., Sifakis, J.: Specification and Verification of Concurrent Systems in CESAR. In: Dezani-Ciancaglini, M., Montanari, U. (eds.) Programming 1982. LNCS, vol. 137, pp. 337–351. Springer, Heidelberg (1982)Google Scholar
  23. 23.
    Roscoe, A.W.: The Theory and Practice of Concurrency, p. 565. Prentice-Hall, Englewood Cliffs (1998)Google Scholar
  24. 24.
    Sistla, A.P., Vardi, M.Y., Wolper, P.: The Complementation Problem for Büchi Automata with Applications to Temporal Logic. Theoretical Computer Science 49(2,3), 217–237 (1987)zbMATHCrossRefMathSciNetGoogle Scholar
  25. 25.
    Thomas, W.: Automata on Infinite Objects. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, vol. B, pp. 133–191. Elsevier, Amsterdam (1990)Google Scholar
  26. 26.
    Valmari, A.: A Chaos-Free Failures Divergences Semantics with Applications to Verification. In: Millennial Perspectives in Computer Science: Proceedings of the 1999 Oxford–Microsoft Symposium in honour of Sir Tony Hoare. Palgrave ”Cornerstones of Computing” series, pp. 365–382 (2000)Google Scholar
  27. 27.
    Valmari, A., Tienari, M.: Compositional Failure-Based Semantic Models for Basic LOTOS. Formal Aspects of Computing 7(4), 440–468 (1995)zbMATHCrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Antti Puhakka
    • 1
  1. 1.Institute of Software SystemsTampere University of TechnologyTampereFinland

Personalised recommendations