Decomposing Properties into Safety and Liveness

Schneider, Fred B.

Decomposing Properties into Safety and Liveness

File(s)

87-874.ps (147.02 KB)

87-874.pdf (344.66 KB)

Permanent Link(s)

https://hdl.handle.net/1813/6714

Collections

Computer Science Technical Reports

Author

Schneider, Fred B.

Abstract

A new proof is given that every property can be expressed as a conjunction of safety and liveness properties. The proof is in terms of first-order predicate logic.

Date Issued

1987-10

Publisher

Cornell University

Keywords

computer science

•

technical report

Previously Published as

http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cs/TR87-874

Type

technical report