Formal Methods in System Design

, Volume 28, Issue 1, pp 57–84 | Cite as

Model Checking with Strong Fairness

  • Yonit Kesten
  • Amir Pnueli
  • Li-On Raviv
  • Elad Shahar


In this paper we present a coherent framework for symbolic model checking of linear-time temporal logic (ltl) properties over finite state reactive systems, taking full fairness constraints into consideration. We use the computational model of a fair discrete system (fds) which takes into account both justice (weak fairness) and compassion (strong fairness). The approach presented here reduces the model-checking problem into the question of whether a given fds is feasible (i.e. has at least one computation).

The contribution of the paper is twofold: On the methodological level, it presents a direct self-contained exposition of full ltl symbolic model checking without resorting to reductions to either μ-calculus or ctl. On the technical level, it extends previous methods by dealing with compassion at the algorithmic level instead of either adding it to the specification, or transforming compassion to justice.

Finally, we extend ctl with past operators, and show that the basic symbolic feasibility algorithm presented here, can be used to model check an arbitrary ctl formula over an fds with full fairness constraints.


model checking temporal logic LTL CTL fairness fair discrete systems temporal testers 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill, and L.J. Hwang, “Symbolic model checking: 1020 states and beyond,” Inf. and Comp., Vol. 98, No. 2, pp. 142–170, 1992.MathSciNetGoogle Scholar
  2. 2.
    E.M. Clarke and E.A. Emerson, “Design and synthesis of synchronization skeletons using branching time temporal logic,” in Proc. IBM Workshop on Logics of Programs, Volume 131 of Lect. Notes in Comp. Sci., Springer-Verlag, 1981, pp. 52–71.Google Scholar
  3. 3.
    E.M. Clarke, O. Grumberg, and K. Hamaguchi, “Another look at ltl model checking,” Formal Methods in System Design, Vol. 10, No. 1, 1997.Google Scholar
  4. 4.
    E.M. Clarke, O. Grumberg, D.E. Long, and X. Zhao, “Efficient generation of counterexamples and witnesses in symbolic model checking,” in Proc. Design Automation Conference 95 (DAC95), 1995.Google Scholar
  5. 5.
    E.A. Emerson and C.L. Lei, “Efficient model-checking in fragments of the propositional modal μ-calculus,” in Proc. First IEEE Symp. Logic in Comp. Sci., pp. 267–278, 1986.Google Scholar
  6. 6.
    E.A. Emerson and C. Lei, “Modalities for model checking: Branching time logic strikes back,” Science of Computer Programming, Vol. 8, pp. 275–306, 1987.MathSciNetGoogle Scholar
  7. 7.
    N. Francez, Fairness, Springer-Verlag, 1986.Google Scholar
  8. 8.
    D. Gabbay, A. Pnueli, S. Shelah, and J. Stavi, “On the temporal analysis of fairness,” in Proc. 7th ACM Symp. Princ. of Prog. Lang., pp. 163–173, 1980.Google Scholar
  9. 9.
    R.H. Hardin, R.P. Kurshan, S.K. Shukla, and M.Y. Vardi, “A new heuristic for bad cycle detection using BDDs,” in O. Grumberg and O. Grumberg (Eds.), Proc. 9th Intl. Conference on Computer Aided Verification, (CAV'97), Volume 1254 of Lect. Notes in Comp. Sci., Springer-Verlag, 1997, pp. 268–278.Google Scholar
  10. 10.
    M.R. Henzinger and J.A. Telle, “Faster algorithms for the nonemptiness of street automata and for communication protocol prunning,” in Proceedings of the 5th Scandina vian Workshop on Algorithn Theory, 1996, pp. 10–20.Google Scholar
  11. 11.
    R. Hojati, H. Touati, R.P. Kurshan, and R.K. Brayton, “Efficient ω-regular language containment,” in G.V. Bochmann and D.K. Probst (Eds.), Proc. 4th Intl. Conference on Computer Aided Verification (CAV'92), Volume 697 of Lect. Notes in Comp. Sci., Springer-Verlag, number 663 in Lect. Notes in Comp. Sci., SPringer-Verlag, 1992, pp. 396–409.Google Scholar
  12. 12.
    Y. Kesten and A. Pnueli, “Verification by augmented finitary abstraction, Inf. and Comp., Vol. 163, pp. 203–243, 2000.MathSciNetGoogle Scholar
  13. 13.
    Y. Kesten, A. Pnueli, and L. Raviv, “Algorithmic verification of linear temporal logic specifications,” in K.G. Larsen, S. Skyum, and G. Winskel (Eds.), Proc, 25th Int. Col-loq. Aut. Lang. Prog., Volume 1443 of Lect. Notes in Comp. Sci., Springer-Verlag, 1998, pp. 1–16.Google Scholar
  14. 14.
    R.P. Kurshan, Computer Aided Verification of Coordinating Processes, Princeton University Press, Princeton, New Jersey, 1995.Google Scholar
  15. 15.
    O. Lichtenstein, “Decidability, completeness, and extensions of linear time temporal logic,” PhD thesis, Weizmann Institute of Science, 1991.Google Scholar
  16. 16.
    O. Lichtenstein and A. Pnueli, “Checking that finite state concurrent programs satisfy their linear specification,” in Proc. 12th ACM Symp. Princ. of Prog. Lang., 1985, pp. 97–107.Google Scholar
  17. 17.
    D. Lehmann, A. Pnueli, and J. Stavi, “Impartiality, justice and fairness: The ethics of concurrent termination,” in Proc. 8th Int. Colloq. Aut. Lang. Prog., Volume 115 of Lect. Notes in Comp. Sci., Springer-Verlag, 1981, pp. 264–277.Google Scholar
  18. 18.
    O. Lichtenstein, A. Pnueli, and L. Zuck, “The glory of the past,” in Proc. Conf. Logics of Programs, Volume 193 of Lect. Notes in Comp. Sci., Springer-Verlag, 1985, pp. 196–218.Google Scholar
  19. 19.
    Z. Manna and A. Pnueli, “Completing the temporal picture,” Theor. Comp. Sci., Vol. 83, No. 1, pp. 97–130, 1991.CrossRefGoogle Scholar
  20. 20.
    Z. Manna and A. Pnueli, Temporal Logic of Reactive and Concurrent Systems: Specification, Springer-Verlag, New York, 1991.Google Scholar
  21. 21.
    Z. Manna and A. Pnueli, Temporal Verification of Reactive Systems: Safety, Springer-Verlag, New York, 1995.Google Scholar
  22. 22.
    A. Pnueli and E. Shahar, “A platform for combining deductive with algorithmic verification,” in R. Alur and T. Henzinger, R. Alur and T. Henzinger (Eds.), Proc. 8th Intl. Conference on Computer Aided Verification (CAV'96), Volume 1102 of Led. Notes in Comp. Sci., Springer- Verlag, 1996, pp. 184–195.Google Scholar
  23. 23.
    J.P. Queille and J. Sifakis, “Specification and verification of concurrent systems,” in cesar in M. Dezani-Ciancaglini and M. Montanari (Eds.), International Symposium on Programming, Volume 137 of Lect. Notes in Comp. Sci., Springer-Verlag, 1982, pp. 337–351.Google Scholar
  24. 24.
    K. Ravi, R. Bloem, and F. Somenzi, “A comparative study of symbolic algorithms for the computation of fair cycles,” in W.A. Hunt, Jr. and S.D. Johnson (Eds.), Formal Methods in Computer Aided Design, Volume 1954 of Lect. Notes in Comp. Sci., Springer-Verlag, 2000, pp. 143–160.Google Scholar
  25. 25.
    F.A. Stomp, W.-P. de Roever, and R.T. Gerth, “The μ-calculus as an assertion language for fairness arguments,” Inf. and Comp., Vol. 82, pp. 278–322, 1989.MathSciNetGoogle Scholar
  26. 26.
    M.Y. Vardi and P. Wolper, “An automata-theoretic approach to automatic program verification,” in Proc. First IEEE Symp. Logic in Comp. Sci., 1986, pp. 332–344.Google Scholar
  27. 27.
    Z. Yang, “Performance analysis of symbolic reachability algorithms in model checking,” Master's thesis, Rice University, 1999.Google Scholar

Copyright information

© Springer Science + Business Media, Inc. 2006

Authors and Affiliations

  • Yonit Kesten
    • 1
  • Amir Pnueli
    • 2
  • Li-On Raviv
    • 2
  • Elad Shahar
    • 2
  1. 1.Ben Gurion UniversityIsrael
  2. 2.Weizmann Institute of ScienceIsrael

Personalised recommendations