Verifying nondeterministic probabilistic channel systems against ω-regular linear-time properties
From MaRDI portal
Publication:5277794
DOI10.1145/1297658.1297663zbMath1367.68181arXivcs/0511023MaRDI 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
68Q60: Specification and verification (program logics, model checking, etc.)
68Q85: Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
68Q87: Probability in computer science (algorithm analysis, random structures, phase transitions, etc.)
Related Items
Stochastic Games with Lossy Channels, Qualitative reachability in stochastic BPA games, Computable fixpoints in well-structured symbolic model checking, Symblicit algorithms for mean-payoff and shortest path in monotonic Markov decision processes, Mixing Lossy and Perfect Fifo Channels, Symbolic Verification of Communicating Systems with Probabilistic Message Losses: Liveness and Fairness