On the Refinement of Liveness Properties of Distributed Systems
| dc.creator | Attie, Paul C. | |
| dc.date | 2008-01-07 | |
| dc.date.accessioned | 2026-07-07T08:52:56Z | |
| dc.date.available | 2026-07-07T08:52:56Z | |
| dc.description | We present a new approach for reasoning about liveness properties of distributed systems, represented as automata. Our approach is based on simulation relations, and requires reasoning only over finite execution fragments. Current simulation-relation based methods for reasoning about liveness properties of automata require reasoning over entire executions, since they involve a proof obligation of the form: if a concrete and abstract execution ``correspond'' via the simulation, and the concrete execution is live, then so is the abstract execution. Our contribution consists of (1) a formalism for defining liveness properties, (2) a proof method for liveness properties based on that formalism, and (3) two expressive completeness results: firstly, our formalism can express any liveness property which satisfies a natural ``robustness'' condition, and secondly, our formalism can express any liveness property at all, provided that history variables can be used | |
| dc.description | 54 pages, 12 figures | |
| dc.identifier | https://arxiv.org/abs/0801.0949 | |
| dc.identifier | http://arxiv.org/abs/0801.0949 | |
| dc.identifier.uri | http://salesiana.dossiersoluciones.com/handle/123456789/145450 | |
| dc.subject | Logic in Computer Science | |
| dc.title | On the Refinement of Liveness Properties of Distributed Systems | |
| dc.type | text |