A lattice-theoretic characterization of safety and liveness

ABSTRACT

The distinction between safety and liveness properties is due to Lamport who gave the following informal characterization. Safety properties assert that nothing bad ever happens while liveness properties assert that something good happens eventually. In a well-known paper Alpern and Schneider gave a topological characterization of safety and liveness for the linear time framework. Gumm has stated these notions in the more abstract setting of V-complete Boolean algebras. Recently, we characterized safety and liveness for the branching time framework and found that neither the topological characterization nor Gumm's characterization were general enough for our needs. We present a lattice theoretic characterization that allows us to unify previous results on safety and liveness, including the results for the linear time and branching time frameworks and for w-regular string and tree languages.

REFERENCES

• 1: Martín Abadi , Leslie Lamport, The existence of refinement mappings, Theoretical Computer Science, v.82 n.2, p.253-284, May 31, 1991 [doi>10.1016/0304-3975(91)90224-P]
• 2: Parosh Aziz Abdulla , Kārlis Čerāns , Bengt Jonsson , Yih-Kuen Tsay, Algorithmic analysis of programs with well quasi-ordered domains, Information and Computation, v.160 n.1-2, p.109-127, July 10/Aug. 1, 2000 [doi>10.1006/inco.1999.2843]
• 3: B. Alpern and F. B. Schneider. Defining liveness. Information Processing Letters, 21(4):181--185, Oct. 1985.
• 4: B. Alpern and F. B. Schneider. Recognizing safety and liveness. Distributed Computing, 2(3):117--126, 1987.
• 5: Edmund M. Clarke , E. Allen Emerson, Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic, Logic of Programs, Workshop, p.52-71, May 01, 1981
• 6: E. Allen Emerson, Temporal and modal logic, Handbook of theoretical computer science (vol. B): formal models and semantics, MIT Press, Cambridge, MA, 1991
• 7: E. Allen Emerson , Joseph Y. Halpern, “Sometimes” and “not never” revisited: on branching versus linear time temporal logic, Journal of the ACM (JACM), v.33 n.1, p.151-178, Jan. 1986 [doi>10.1145/4904.4999]
• 8: H. Peter Gumm, Another glance at the Alpern-Schneider characterization of safety and liveness in concurrent executions, Information Processing Letters, v.47 n.6, p.291-294, Oct. 18, 1993 [doi>10.1016/0020-0190(93)90074-J]
• 9: D. Harel , A. Pnueli, On the development of reactive systems, Logics and models of concurrent systems, Springer-Verlag New York, Inc., New York, NY, 1989
• 10: E. Kindler. Safety and liveness properties: A survey. EATCS-BuUetin, 53:268--272, June 1994.
• 11: D. Kozen. Results on the propositional Mu-Calculus. Theoretical Computer Science, pages 334--354, December 1983.
• 12: Orna Kupferman , Moshe Y. Vardi, Model Checking of Safety Properties, Proceedings of the 11th International Conference on Computer Aided Verification, p.172-183, July 06-10, 1999
• 13: L. Lamport. Proving the correctness of multiprocess programs. IEEE Transactions on Software Engineering SE-3, 2:125--143, Mar. 1977.
• 14: Panagiotis Manolios , Richard Trefler, Safety and Liveness in Branching Time, Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science, p.366, June 16-19, 2001
• 15: R. Milner, Communication and concurrency, Prentice-Hall, Inc., Upper Saddle River, NJ, 1989
• 16: Susan Owicki , Leslie Lamport, Proving Liveness Properties of Concurrent Programs, ACM Transactions on Programming Languages and Systems (TOPLAS), v.4 n.3, p.455-495, July 1982 [doi>10.1145/357172.357178]
• 17: A. Pnueli. The temporal logic of programs. In 18th Annual Symposium on Foundations of Computer Science, pages 46--57, Providence, Rhode Island, 1977. IEEE.
• 18: Jean-Pierre Queille , Joseph Sifakis, Specification and verification of concurrent systems in CESAR, Proceedings of the 5th Colloquium on International Symposium on Programming, p.337-351, April 06-08, 1982
• 19: Martin Rem, A personal perspective of Alphern-Schneider characterization of safety and liveness, Beauty is our business: a birthday salute to Edsger W. Dijkstra, Springer-Verlag New York, Inc., New York, NY, 1990
• 20: Fred B. Schneider, Enforceable security policies, ACM Transactions on Information and System Security (TISSEC), v.3 n.1, p.30-50, Feb. 2000 [doi>10.1145/353323.353382]
• 21: A. P. Sistla. Safety, liveness and fairness in temporal logic. Formal Aspects of Computing, 6:495--511, 1994.
• 22: W. Thomas. Automata on infinite objects. In van Leeuwen {23}, pages 135--192.
• 23: Jan van Leeuwen, Handbook of theoretical computer science (vol. B): formal models and semantics, MIT Press, Cambridge, MA, 1991

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs