Game-Based Probabilistic Predicate Abstraction in PRISM

DOI10.1016/J.ENTCS.2008.11.016MaRDI QIDQ5415661zbMATH OpenOpenAlexFDO

Authors

Publication date 13 May 2014

Published in Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.entcs.2008.11.016

zbMATH Keywords

automatic verificationMarkov modelspredicate abstractionprobabilistic model checking

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87)

Recommendations

• Probabilistic game semantics
• Compositional Predicate Abstraction from Game Semantics
• Towards a probabilistic interpretation of game logic
• Tight game abstractions of probabilistic automata
• PRISM-games: a model checker for stochastic multi-player games
• Verification and refutation of probabilistic specifications via games
• The concurrent game semantics of probabilistic PCF
• Probabilistic quantifiers and games
• scientific article; zbMATH DE number 7445154

Cites work

• Computer Aided Verification
• Game-Based Probabilistic Predicate Abstraction in PRISM
• scientific article; zbMATH DE number 2006656 (Why is no real title available?)
• scientific article; zbMATH DE number 1863173 (Why is no real title available?)
• scientific article; zbMATH DE number 1884411 (Why is no real title available?)
• scientific article; zbMATH DE number 3240812 (Why is no real title available?)
• Magnifying-Lens Abstraction for Markov Decision Processes
• Model checking of probabilistic and nondeterministic systems
• Model Checking Software
• On finite-state approximants for probabilistic computation tree logic
• Predicate abstraction of ANSI-C programs using SAT

Cited in

(10)

• Lifted model checking for relational MDPs
• Model checking single agent behaviours by fluid approximation
• Verification and refutation of probabilistic specifications via games
• Tight game abstractions of probabilistic automata
• Compositional Predicate Abstraction from Game Semantics
• Compositional abstraction for stochastic systems
• Game-Based Probabilistic Predicate Abstraction in PRISM
• A game-based abstraction-refinement framework for Markov decision processes
• Quantitative aspects of programming languages and systems over the past 2⁴ years and beyond
• Probabilistic model checking of biological systems with uncertain kinetic rates

Describes a project that uses

Uses Software

• PRISM
• LiQuor

This page was built for publication: Game-Based Probabilistic Predicate Abstraction in PRISM

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5415661)