On the refinement of liveness properties of distributed systems
From MaRDI portal
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
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
Cites work
- scientific article; zbMATH DE number 4110131 (Why is no real title available?)
- scientific article; zbMATH DE number 42752 (Why is no real title available?)
- scientific article; zbMATH DE number 52331 (Why is no real title available?)
- scientific article; zbMATH DE number 1296290 (Why is no real title available?)
- scientific article; zbMATH DE number 1479642 (Why is no real title available?)
- scientific article; zbMATH DE number 194539 (Why is no real title available?)
- Completing the temporal picture
- Eventually-serializable data services
- Forward and backward simulations. I. Untimed Systems
- Generalized temporal verification diagrams
- Grammar Analysis and Parsing by Abstract Interpretation
- Hybrid I/O automata.
- Liveness in timed and untimed systems
- On verifying that a concurrent program satisfies a nondeterministic specification
- Proving Liveness Properties of Concurrent Programs
- Proving correctness with respect to nondeterministic safety specifications
- Proving the Correctness of Multiprocess Programs
- Recognizing safety and liveness
- Safety, liveness and fairness in temporal logic
- The Online Transportation Problem
- The existence of refinement mappings
- Verification by augmented abstraction: The automata-theoretic view
- Verification by augmented finitary abstraction
- Verification of concurrent programs: The automata-theoretic framework
- Verifying temporal properties without temporal logic
Cited in
(22)- Liveness by Invisible Invariants
- Processes with local and global liveness requirements
- Safety-liveness exclusion in distributed computing
- Proving liveness of fair transition systems
- Off-the-shelf automated analysis of liveness properties for just paths
- Dynamic input/output automata: a formal and compositional model for dynamic systems
- Polynomial-time optimal liveness enforcement for guidepath-based transport systems
- From states to histories relating state and history views onto systems
- Auxiliary constructs for proving liveness in compassion discrete systems
- Justness. A completeness criterion for capturing liveness properties (extended abstract)
- Splitting forward simulations to cope with liveness
- A short counterexample property for safety and liveness verification of fault-tolerant distributed algorithms
- scientific article; zbMATH DE number 177525 (Why is no real title available?)
- Syntax directed analysis of liveness properties of while programs
- Liveness characterization for GFC systems. II
- Simulating liveness by reduction strategies
- Local safety and local liveness for distributed systems
- Categorical liveness checking by corecursive algebras
- Processes with infinite liveness requirements
- Ensuring liveness properties of distributed systems: open problems
- The coarsest precongruences respecting safety and liveness properties
- An axiomatic approach to liveness for differential equations
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)
