Liveness in broadcast networks
From MaRDI portal
Publication:2676223
Abstract: We study liveness and model checking problems for broadcast networks, a system model of identical clients communicating via message passing. The first problem that we consider is Liveness Verification. It asks whether there is a computation such that one of the clients visits a final state infinitely often. The complexity of the problem has been open since 2010 when it was shown to be P-hard and solvable in EXPSPACE. We close the gap by a polynomial-time algorithm. The algorithm relies on a characterization of live computations in terms of paths in a suitable graph, combined with a fixed-point iteration to efficiently check the existence of such paths. The second problem is Fair Liveness Verification. It asks for a computation where all participating clients visit a final state infinitely often. We adjust the algorithm to also solve fair liveness in polynomial time. Both problems can be instrumented to answer model checking questions for broadcast networks against linear time temporal logic specifications. The first problem in this context is Fair Model Checking. It demands that for all computations of a broadcast network, all participating clients satisfy the specification. We solve the problem via the Vardi-Wolper construction and a reduction to Liveness Verification. The second problem is Sparse Model Checking. It asks whether each computation has a participating client that satisfies the specification. We reduce the problem to Fair Liveness Verification.
Recommendations
- Liveness of parameterized timed networks
- Proving liveness for networks of communicating finite state machines
- Decidability and complexity results for verification of asynchronous broadcast networks
- scientific article; zbMATH DE number 1863165
- Playing with probabilities in reconfigurable broadcast networks
Cites work
- A short counterexample property for safety and liveness verification of fault-tolerant distributed algorithms
- All You Need Is Compassion
- Applying the Graph Minor Theorem to the Verification of Graph Transformation Systems
- Automata theory and its applications
- Bounds on mobility
- Complexity of Liveness in Parameterized Systems
- Decidability of parameterized verification
- Distributed local strategies in broadcast networks
- Fine-grained complexity of safety verification
- Fine-grained complexity of safety verification
- Forward analysis of depth-bounded processes
- Graph Grammar Modeling and Verification of Ad Hoc Routing Protocols
- scientific article; zbMATH DE number 1670768 (Why is no real title available?)
- scientific article; zbMATH DE number 827979 (Why is no real title available?)
- scientific article; zbMATH DE number 7354705 (Why is no real title available?)
- Keeping a crowd safe: on the complexity of parameterized verification (invited talk)
- Model checking parameterized systems
- On hierarchical communication topologies in the -calculus
- On the complexity of parameterized reachability in reconfigurable broadcast networks
- On the power of cliques in the parameterized verification of ad hoc networks
- Parameterised pushdown systems with non-atomic writes
- Parameterized verification of ad hoc networks
- Parameterized Verification of Asynchronous Shared-Memory Systems
- Parameterized verification of synchronization in constrained reconfigurable broadcast networks
- Parity to safety in polynomial time for pushdown and collapsible pushdown systems
- Playing with probabilities in reconfigurable broadcast networks
- Query-Based Model Checking of Ad Hoc Network Protocols
- Reachability in networks of register protocols under stochastic schedulers
- Tools and Algorithms for the Construction and Analysis of Systems
Cited in
(7)- The meaning of frozen tokens in live nets
- Checking qualitative liveness properties of replicated systems with stochastic scheduling
- Performing work in broadcast networks
- Verification, Model Checking, and Abstract Interpretation
- Parameterized analysis of reconfigurable broadcast networks
- Parameterized broadcast networks with registers: from NP to the frontiers of decidability
- Wait-only broadcast protocols are easier to verify
This page was built for publication: Liveness in broadcast networks
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2676223)
