A lattice-theoretic characterization of safety and liveness

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

A lattice-theoretic characterization of safety and liveness

Full text

Pdf (778 KB)

Source

Annual ACM Symposium on Principles of Distributed Computing archive
Proceedings of the twenty-second annual symposium on Principles of distributed computing table of contents

Boston, Massachusetts

Pages: 325 - 333

Year of Publication: 2003

ISBN:1-58113-708-7

Authors

Panagiotis Manolios	Georgia Institute of Technology, Atlanta, Georgia
Richard Trefler	University of Waterloo 200 Waterloo, Ontario, Canada

Sponsors

SIGOPS: ACM Special Interest Group on Operating Systems
SIGACT: ACM Special Interest Group on Algorithms and Computation Theory

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 6, Downloads (12 Months): 34, Citation Count: 1

Additional Information:

abstract references cited by index terms collaborative colleagues

Tools and Actions:	Request Permissions Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/872035.872083 What is a DOI?

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

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked 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