Minimal counterexamples for linear-time probabilistic verification

DOI10.1016/j.tcs.2014.06.020zbMath1360.68604OpenAlexW1980206966WikidataQ57800843 ScholiaQ57800843MaRDI QIDQ402125

Nils Jansen, Ralf Wimmer, Joost-Pieter Katoen, Bernd Becker, Erika Ábrahám

Publication date: 27 August 2014

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.tcs.2014.06.020

zbMATH Keywords

counterexampleMarkov chainMarkov decision processmixed integer linear programming\(\omega\)-regular propertySAT-modulo-theories

Mathematics Subject Classification ID

Mixed integer programming (90C11) Applications of Markov chains and discrete-time Markov processes on general state spaces (social mobility, learning theory, industrial processes, etc.) (60J20) Markov and semi-Markov decision processes (90C40) Specification and verification (program logics, model checking, etc.) (68Q60) Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87)

Related Items

Farkas Certificates and Minimal Witnesses for Probabilistic Reachability Constraints, Enforcing almost-sure reachability in POMDPs, Counterexample-guided inductive synthesis for probabilistic systems, Task-Aware Verifiable RNN-Based Policies for Partially Observable Markov Decision Processes

Uses Software

• SCIP
• PRISM
• MRMC
• LiQuor
• CEGAR
• cvc3
• z3
• COMICS
• DiPro
• LTL2BA

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• K\(^{\ast}\): A heuristic search algorithm for finding the \(k\) shortest paths
• SCIP: solving constraint integer programs
• Experiments with deterministic \(\omega\)-automata for formulas of linear temporal logic
• Symmetry breaking in distributed networks
• Symbolic model checking for probabilistic timed automata
• Minimal Critical Subsystems for Discrete-Time Markov Models
• Verification and Refutation of Probabilistic Specifications via Games
• A counterexample-guided abstraction-refinement framework for markov decision processes
• Learning Probabilistic Systems from Tree Samples
• Hierarchical Counterexamples for Discrete-Time Markov Chains
• Counterexamples in Probabilistic LTL Model Checking for Markov Chains
• Counterexample-guided abstraction refinement for symbolic model checking
• Fast randomized consensus using shared memory
• Extended Directed Search for Probabilistic Timed Reachability
• The Birth of Model Checking
• Probabilistic CEGAR
• Counterexample Generation for Discrete-Time Markov Chains Using Bounded Model Checking
• Impossibility of distributed consensus with one faulty process
• Finding the k Shortest Paths
• Markov Chains
• Verification: Theory and Practice
• Model Checking Software
• Computer Aided Verification
• Depth-First Search and Linear Graph Algorithms
• Tools and Algorithms for the Construction and Analysis of Systems