Computer Science – Logic in Computer Science
Scientific paper
2008-01-07
Computer Science
Logic in Computer Science
54 pages, 12 figures
Scientific paper
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
No associations
LandOfFree
On the Refinement of Liveness Properties of Distributed Systems does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.
If you have personal experience with On the Refinement of Liveness Properties of Distributed Systems, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and On the Refinement of Liveness Properties of Distributed Systems will most certainly appreciate the feedback.
Profile ID: LFWR-SCP-O-654004