Advertisement

Separating Fairness and Well-Foundedness for the Analysis of Fair Discrete Systems

  • Amir Pnueli
  • Andreas Podelski
  • Andrey Rybalchenko
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3440)

Abstract

Fair discrete systems (FDSs) are a computational model of concurrent programs where fairness assumptions are specified in terms of sets of states. The analysis of fair discrete systems involves a non-trivial interplay between fairness and well-foundedness (ranking functions). This interplay has been an obstacle for automation. The contribution of this paper is a new analysis of temporal properties of FDSs. The analysis uses a domain of binary relations over states labeled by sets of indices of fairness requirements. The use of labeled relations separates the reasoning on well-foundedness and fairness.

References

  1. 1.
    Colón, M., Sipma, H.: Synthesis of linear ranking functions. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 67–81. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  2. 2.
    Cousot, P.: Partial completeness of abstract fixpoint checking. In: Choueiry, B.Y., Walsh, T. (eds.) SARA 2000. LNCS (LNAI), vol. 1864, pp. 1–15. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  3. 3.
    Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proc. of POPL 1977: Principles of Programming Languages, pp. 238–252. ACM Press, New York (1977)Google Scholar
  4. 4.
    Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: Proc. of POPL 1979: Principles of Programming Languages, pp. 269–282. ACM Press, New York (1979)Google Scholar
  5. 5.
    Fang, Y., Piterman, N., Pnueli, A., Zuck, L.D.: Liveness with incomprehensible ranking. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 482–496. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  6. 6.
    Fang, Y., Piterman, N., Pnueli, A., Zuck, L.D.: Liveness with invisible ranking. In: Steffen, Levi (eds.) [21], pp. 223–238.Google Scholar
  7. 7.
    Holzbaur, C.: OFAI clp(q,r) Manual, edn. 1.3.3, Vienna. Austrian Research Institute for Artificial Intelligence (1995) TR-95-09 Google Scholar
  8. 8.
    Kesten, Y., Pnueli, A., Raviv, L.: Algorithmic verification of linear temporal logic specifications. In: Larsen, K.G., Skyum, S., Winskel, G. (eds.) ICALP 1998. LNCS, vol. 1443, pp. 1–16. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  9. 9.
    Klarlund, N.: Progress measures and stack assertions for fair termination. In: Proc. of PODC 1992: Principles of Distributed Computing, pp. 229–240. ACM Press, New York (1992)Google Scholar
  10. 10.
    T.I.S. Laboratory. SICStus Prolog User’s Manual. Swedish Institute of Computer Science, PO Box 1263 SE-164 29 Kista, Sweden (October 2001) (Release 3.8.7)Google Scholar
  11. 11.
    Lamport, L.: A new solution of Dijkstra’s concurrent programming problem. Communications of the ACM 17(8), 453–455 (1974)zbMATHCrossRefMathSciNetGoogle Scholar
  12. 12.
    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
  13. 13.
    Lichtenstein, O., Pnueli, A.: Checking that finite state concurrent programs satisfy their linear specification. In: Proc. of POPL 1985: Principles of Programming Languages, pp. 97–107. ACM Press, New York (1985)Google Scholar
  14. 14.
    Manna, Z., Pnueli, A.: Completing the temporal picture. Theoretical Computer Science 83(1), 91–130 (1991)CrossRefGoogle Scholar
  15. 15.
    Manna, Z., Pnueli, A.: Temporal verification of reactive systems: Safety. Springer, Heidelberg (1995)Google Scholar
  16. 16.
    Manna, Z., Pnueli, A.: Temporal verification of reactive systems: Progress. Draft (1996)Google Scholar
  17. 17.
    Podelski, A., Rybalchenko, A.: A complete method for the synthesis of linear ranking functions. In: Steffen, Levi (eds.) [21], pp. 239–251.Google Scholar
  18. 18.
    Podelski, A., Rybalchenko, A.: Transition invariants. In: Proc. of LICS 2004: Logic in Computer Science, pp. 32–41. IEEE, Los Alamitos (2004)CrossRefGoogle Scholar
  19. 19.
    Podelski, A., Rybalchenko, A.: Transition predicate abstraction and fair termination. In: Proc. of POPL 2005: Principles of Programming Languages. ACM Press, New York (2005) (to appear)Google Scholar
  20. 20.
    Ramsey, F.P.: On a problem of formal logic. In: Proc. London Math. Soc., vol. 30, pp. 264–285 (1930)Google Scholar
  21. 21.
    Steffen, B., Levi, G. (eds.): VMCAI 2004. LNCS, vol. 2937. Springer, Heidelberg (2004)zbMATHGoogle Scholar
  22. 22.
    Tiwari, A.: Termination of linear programs. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 70–82. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  23. 23.
    Vardi, M.Y.: Verification of concurrent programs — the automata-theoretic framework. Annals of Pure and Applied Logic 51, 79–98 (1991)zbMATHCrossRefMathSciNetGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Amir Pnueli
    • 1
  • Andreas Podelski
    • 2
  • Andrey Rybalchenko
    • 2
  1. 1.New York UniversityNew York
  2. 2.Max-Planck-Institut für InformatikSaarbrücken

Personalised recommendations