On Abstraction of Probabilistic Systems

DOI10.1007/978-3-662-45489-3_4zbMath1426.68167OpenAlexW29485814MaRDI QIDQ2937733

David N. Jansen, Daniel Gebler, Michele Volpato, Christian Dehnert

Publication date: 12 January 2015

Published in: Stochastic Model Checking. Rigorous Dependability Analysis Using Model Checking Techniques for Stochastic Systems (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-662-45489-3_4

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

A counter abstraction technique for verifying properties of probabilistic swarm systems, Abstract model repair for probabilistic systems, Automated verification and synthesis of stochastic hybrid systems: a survey

Uses Software

• SIGREF
• PRISM
• PASS
• CEGAR
• PRISM-games

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Three-valued abstraction for probabilistic systems
• A game-based abstraction-refinement framework for Markov decision processes
• Using branching time temporal logic to synthesize synchronization skeletons
• The complexity of stochastic games
• A logic for reasoning about time and reliability
• Approximating labelled Markov processes
• Comparative branching-time semantics for Markov chains
• Minimal Critical Subsystems for Discrete-Time Markov Models
• SMT-Based Bisimulation Minimisation of Markov Models
• A counterexample-guided abstraction-refinement framework for markov decision processes
• Model checking of probabilistic and nondeterministic systems
• Abstract Probabilistic Automata
• Hierarchical Counterexamples for Discrete-Time Markov Chains
• Probabilistic CEGAR
• Symmetry Reduction for Probabilistic Model Checking Using Generic Representatives
• Sigref – A Symbolic Bisimulation Tool Box
• Assume-Guarantee Verification for Probabilistic Systems
• Sliding Window Abstraction for Infinite Markov Chains
• Best Probabilistic Transformers
• Variable Probabilistic Abstraction Refinement
• The Quest for Minimal Quotients for Probabilistic Automata
• PRISM-games: A Model Checker for Stochastic Multi-Player Games
• Magnifying-Lens Abstraction for Markov Decision Processes
• Symmetry Reduction for Probabilistic Model Checking
• Lazy Abstraction with Interpolants
• Bisimulation Minimisation Mostly Speeds Up Probabilistic Model Checking
• Counterexamples in Probabilistic Model Checking
• Model Checking Software