Verifying nondeterministic probabilistic channel systems against ω-regular linear-time properties

DOI10.1145/1297658.1297663zbMath1367.68181arXivcs/0511023OpenAlexW2083816928MaRDI QIDQ5277794

Nathalie Bertrand, Christel Baier, Philippe Schnoebelen

Publication date: 12 July 2017

Published in: ACM Transactions on Computational Logic (Search for Journal in Brave)

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

zbMATH Keywords

Markov decision processesprobabilistic modelscommunication protocolslossy channels

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)

Symblicit algorithms for mean-payoff and shortest path in monotonic Markov decision processes ⋮ Mixing Lossy and Perfect Fifo Channels ⋮ Computable fixpoints in well-structured symbolic model checking ⋮ Qualitative reachability in stochastic BPA games ⋮ Symbolic Verification of Communicating Systems with Probabilistic Message Losses: Liveness and Fairness ⋮ Stochastic Games with Lossy Channels

This page was built for publication: Verifying nondeterministic probabilistic channel systems against ω-regular linear-time properties