On the refinement of liveness properties of distributed systems
From MaRDI portal
Publication:763239
DOI10.1007/S10703-011-0117-1zbMATH Open1233.68160arXiv0801.0949OpenAlexW2008807688MaRDI QIDQ763239FDOQ763239
Authors: Paul C. Attie 
Publication date: 9 March 2012
Published in: Formal Methods in System Design (Search for Journal in Brave)
Abstract: 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
Full work available at URL: https://arxiv.org/abs/0801.0949
Recommendations
- Ensuring liveness properties of distributed systems: open problems
- On Liveness Enforcement of Distributed Petri Net Systems
- Local safety and local liveness for distributed systems
- A short counterexample property for safety and liveness verification of fault-tolerant distributed algorithms
- Checking qualitative liveness properties of replicated systems with stochastic scheduling
- On liveness in extended non self-controlling nets
- Safety-liveness exclusion in distributed computing
- A complete characterization of deterministic regular liveness properties
- Liveness in timed and untimed systems
Formal languages and automata (68Q45) Logic in computer science (03B70) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)
Cites Work
- Title not available (Why is that?)
- Forward and backward simulations. I. Untimed Systems
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- The existence of refinement mappings
- Grammar Analysis and Parsing by Abstract Interpretation
- Title not available (Why is that?)
- Safety, liveness and fairness in temporal logic
- Eventually-serializable data services
- The Online Transportation Problem
- Liveness in timed and untimed systems
- Hybrid I/O automata.
- Proving the Correctness of Multiprocess Programs
- Recognizing safety and liveness
- Proving Liveness Properties of Concurrent Programs
- Verification by augmented finitary abstraction
- Completing the temporal picture
- Generalized temporal verification diagrams
- Proving correctness with respect to nondeterministic safety specifications
- Verification of concurrent programs: The automata-theoretic framework
- On verifying that a concurrent program satisfies a nondeterministic specification
- Verifying temporal properties without temporal logic
- Title not available (Why is that?)
- Verification by augmented abstraction: The automata-theoretic view
Cited In (14)
- Liveness by Invisible Invariants
- Processes with local and global liveness requirements
- Safety-liveness exclusion in distributed computing
- Dynamic input/output automata: a formal and compositional model for dynamic systems
- Polynomial-time optimal liveness enforcement for guidepath-based transport systems
- Auxiliary constructs for proving liveness in compassion discrete systems
- From states to histories relating state and history views onto systems
- Splitting forward simulations to cope with liveness
- A short counterexample property for safety and liveness verification of fault-tolerant distributed algorithms
- Title not available (Why is that?)
- Syntax directed analysis of liveness properties of while programs
- Liveness characterization for GFC systems. II
- Local safety and local liveness for distributed systems
- The coarsest precongruences respecting safety and liveness properties
Uses Software
This page was built for publication: On the refinement of liveness properties of distributed systems
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q763239)
