Advertisement

Localized Fairness: A Rewriting Semantics

  • José Meseguer
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3467)

Abstract

Fairness is a rich phenomenon: we have weak and strong fairness, and many different variants of those concepts: transition fairness, object/process fairness, actor fairness, position fairness, and so on, associated with specific models or languages, but lacking a common theoretical framework. This work uses rewriting semantics as a common theoretical framework for fairness. A common thread tying together the different fairness variants is the notion of localization: fairness must often be localized to specific entities in a system. For systems specified as rewrite theories localization can be formalized by making explicit the subset of variables in a rule corresponding to the items that must be localized. In this way, localized fairness becomes a parametric notion, that can be easily specialized to model a very wide range of fairness phenomena. After formalizing these concepts and proving basic results, the paper studies in detail both a relative and an absolute LTL semantics for rewrite theories with localized fairness requirements, and shows that it is always possible to pass from the relative to the absolute semantics by means of a theory transformation. This allows using a standard LTL model checker to check properties under fairness assumptions.

Keywords

Kripke Structure Linear Time Temporal Logic Dine Philosopher Position Justice Springer LNCS 
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.
    Agha, G.: Actors. MIT Press, Cambridge (1986)Google Scholar
  2. 2.
    Bruni, R., Meseguer, J.: Generalized rewrite theories. In: Baeten, J.C.M., Lenstra, J.K., Parrow, J., Woeginger, G.J. (eds.) ICALP 2003. LNCS, vol. 2719, pp. 252–266. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  3. 3.
    Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (2001)Google Scholar
  4. 4.
    Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Talcott, C.: Maude 2.0 Manual (June 2003), http://maude.cs.uiuc.edu
  5. 5.
    Eker, S., Meseguer, J., Sridharanarayanan, A.: The Maude LTL model checker. In: Gadducci, F., Montanari, U. (eds.) Proc. 4th. Intl. Workshop on Rewriting Logic and its Applications. ENTCS, Elsevier, Amsterdam (2002)Google Scholar
  6. 6.
    Francez, N.: Fairness. Springer, Heidelberg (1986)zbMATHGoogle Scholar
  7. 7.
    Gyuris, V., Sistla, A.: On-the-fly model-checking under fairness that exploits symmetry. Formal Methods in System Design (to appear)Google Scholar
  8. 8.
    Lamport, L.: A temporal logic of actions. ACM Trans. on Prog. Lang. and Systems 16(3), 872–923 (1994)CrossRefGoogle Scholar
  9. 9.
    Latvala, T., Heljanko, K.: Coping with strong fairness. Fundamenta Informaticae 34, 1–19 (2000)MathSciNetGoogle Scholar
  10. 10.
    Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems – Specification. Springer, Heidelberg (1992)Google Scholar
  11. 11.
    Martí-Oliet, N., Meseguer, J.: Rewriting logic: roadmap and bibliography. Theoretical Computer Science 285, 121–154 (2002)zbMATHCrossRefMathSciNetGoogle Scholar
  12. 12.
    Meseguer, J.: Localized fairness. Manuscript, UIUC (February 2005), http://maude.cs.uiuc.edu
  13. 13.
    Meseguer, J.: Conditional rewriting logic as a unified model of concurrency. Theoretical Computer Science 96(1), 73–155 (1992)zbMATHCrossRefMathSciNetGoogle Scholar
  14. 14.
    Meseguer, J.: A logical theory of concurrent objects and its realization in the Maude language. In: Agha, G., Wegner, P., Yonezawa, A. (eds.) Research Directions in Concurrent Object-Oriented Programming, pp. 314–390. MIT Press, Cambridge (1993)Google Scholar
  15. 15.
    Meseguer, J.: Membership algebra as a logical framework for equational specification. In: Parisi-Presicce, F. (ed.) WADT 1997. LNCS, vol. 1376, pp. 18–61. Springer, Heidelberg (1998)Google Scholar
  16. 16.
    Misra, J.: A Discipline of Multiprogramming. Springer, Heidelberg (2001)zbMATHCrossRefGoogle Scholar
  17. 17.
    Pnueli, A., Kesten, Y.: Algorithmic and deductive verification methods for CTL∗. In: Broy, M., Pizka, M. (eds.) Models, Algebras, and Logic of Engineering Software, NATO Advanced Study Institute, Marktoberdorf, Germany, July 30– August 11, pp. 109–131. IOS Press, Amsterdam (2003)Google Scholar
  18. 18.
    Porat, S., Francez, N.: Fairness in term rewriting systems. In: Jouannaud, J.-P. (ed.) RTA 1985. LNCS, vol. 202, pp. 287–300. Springer, Heidelberg (1985)Google Scholar
  19. 19.
    Porat, S., Francez, N.: Full communication and fair termination in equational (and combined) term-rewriting systems. In: Siekmann, J.H. (ed.) CADE 1986. LNCS, vol. 230, pp. 21–41. Springer, Heidelberg (1986)Google Scholar
  20. 20.
    Tison, S.: Fair termination is decidable for ground systems. In: Dershowitz, N. (ed.) RTA 1989. LNCS, vol. 355, pp. 462–476. Springer, Heidelberg (1989)Google Scholar
  21. 21.
    Viry, P.: Equational rules for rewriting logic. Theoretical Computer Science 285, 487–517 (2002)zbMATHCrossRefMathSciNetGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • José Meseguer
    • 1
  1. 1.CS DepartmentUniversity of Illinois at Urbana-ChampaignUSA

Personalised recommendations