Fair termination for parameterized probabilistic concurrent systems
From MaRDI portal
Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)
Abstract: We consider the problem of automatically verifying that a parameterized family of probabilistic concurrent systems terminates with probability one for all instances against adversarial schedulers. A parameterized family defines an infinite-state system: for each number n, the family consists of an instance with n finite-state processes. In contrast to safety, the parameterized verification of liveness is currently still considered extremely challenging especially in the presence of probabilities in the model. One major challenge is to provide a sufficiently powerful symbolic framework. One well-known symbolic framework for the parameterized verification of non-probabilistic concurrent systems is regular model checking. Although the framework was recently extended to probabilistic systems, incorporating fairness in the framework - often crucial for verifying termination - has been especially difficult due to the presence of an infinite number of fairness constraints (one for each process). Our main contribution is a systematic, regularity-preserving, encoding of finitary fairness (a realistic notion of fairness proposed by Alur & Henzinger) in the framework of regular model checking for probabilistic parameterized systems. Our encoding reduces termination with finitary fairness to verifying parameterized termination without fairness over probabilistic systems in regular model checking (for which a verification framework already exists). We show that our algorithm could verify termination for many interesting examples from distributed algorithms (Herman's protocol) and evolutionary biology (Moran process, cell cycle switch), which do not hold under the standard notion of fairness. To the best of our knowledge, our algorithm is the first fully-automatic method that can prove termination for these examples.
Recommendations
Cites work
- scientific article; zbMATH DE number 3148873 (Why is no real title available?)
- scientific article; zbMATH DE number 3972158 (Why is no real title available?)
- scientific article; zbMATH DE number 1832220 (Why is no real title available?)
- scientific article; zbMATH DE number 5585443 (Why is no real title available?)
- Abstract regular tree model checking
- Accelerating tree-automatic relations
- Algorithmic metatheorems for decidable LTL model checking over infinite systems
- Analysis of probabilistic basic parallel processes
- Automata, logics, and infinite games. A guide to current research
- Automated Technology for Verification and Analysis
- Checking NFA equivalence with bisimulations up to congruence
- Deductive proofs of almost sure persistence and recurrence properties
- Distributed algorithms. An intuitive approach
- Explicit fair scheduling for dynamic control
- Fairness for dynamic control
- Iterating transducers in the large (extended abstract)
- Liveness of randomised parameterised systems under arbitrary schedulers
- Minimum and maximum delay problems in real-time systems
- On the verification of qualitative properties of probabilistic processes under fairness constraints.
- Parameterized verification of many identical probabilistic timed processes
- Probabilistic self-stabilization
- Probabilistic termination: soundness, completeness, and compositionality
- Proving time bounds for randomized distributed algorithms
- Temporal logics for the specification of performance and reliability
- Termination of Probabilistic Concurrent Program
- The Power of Hybrid Acceleration
- Verification of multiprocess probabilistic protocols
- Weakest precondition reasoning for expected run-times of probabilistic programs
- When simulation meets antichains. (On checking language inclusion of nondeterministic finite (tree) automata)
Cited in
(12)- Probabilistic Analysis of Binary Sessions
- Fair termination revisited - with delay
- Automated termination analysis of polynomial probabilistic programs
- Progress measures and stack assertions for fair termination
- Regular model checking revisited
- On the complexity of deciding fair termination of probabilistic concurrent finite-state programs
- Promptness and bounded fairness in concurrent and parameterized systems
- scientific article; zbMATH DE number 7649941 (Why is no real title available?)
- The complexity of verifying population protocols
- scientific article; zbMATH DE number 3982496 (Why is no real title available?)
- P^5: planner-less proofs of probabilistic parameterized protocols
- Population protocols: beyond runtime analysis
This page was built for publication: Fair termination for parameterized probabilistic concurrent systems
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3303911)
