Fair Termination for Parameterized Probabilistic Concurrent Systems

DOI10.1007/978-3-662-54577-5_29zbMath1452.68127arXiv1710.10756OpenAlexW2598547732MaRDI QIDQ3303911

Rupak Majumdar, Philipp Rümmer, Ondřej Lengál, Anthony Widjaja Lin

Publication date: 5 August 2020

Published in: Tools and Algorithms for the Construction and Analysis of Systems (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1710.10756

zbMATH Keywords

Markov decision processregular languagefairness constraintatomic propositionfairness condition

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87)

Related Items (6)

Regular model checking revisited ⋮ Unnamed Item ⋮ Population protocols: beyond runtime analysis ⋮ Automated termination analysis of polynomial probabilistic programs ⋮ The complexity of verifying population protocols ⋮ Probabilistic Analysis of Binary Sessions

Uses Software

• PRISM
• FAST

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Minimum and maximum delay problems in real-time systems
• Probabilistic self-stabilization
• Verification of multiprocess probabilistic protocols
• Automata, logics, and infinite games. A guide to current research
• Deductive proofs of almost sure persistence and recurrence properties
• On the verification of qualitative properties of probabilistic processes under fairness constraints.
• Weakest Precondition Reasoning for Expected Run–Times of Probabilistic Programs
• Probabilistic Termination
• Checking NFA equivalence with bisimulations up to congruence
• Accelerating tree-automatic relations
• When Simulation Meets Antichains
• Fairness for Dynamic Control
• Algorithmic Metatheorems for Decidable LTL Model Checking over Infinite Systems
• Liveness of Randomised Parameterised Systems under Arbitrary Schedulers
• Termination of Probabilistic Concurrent Program
• Temporal logics for the specification of performance and reliability
• Explicit Fair Scheduling for Dynamic Control
• Proving time bounds for randomized distributed algorithms
• Analysis of Probabilistic Basic Parallel Processes
• Automated Technology for Verification and Analysis
• The Power of Hybrid Acceleration
• Computer Aided Verification

This page was built for publication: Fair Termination for Parameterized Probabilistic Concurrent Systems