Farkas Certificates and Minimal Witnesses for Probabilistic Reachability Constraints
DOI10.1007/978-3-030-45190-5_18OpenAlexW3022578038MaRDI QIDQ5039515
Simon Jantsch, Florian Funke, Christel Baier
Publication date: 13 October 2022
Published in: Tools and Algorithms for the Construction and Analysis of Systems (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/1910.10636
Markov and semi-Markov decision processes (90C40) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17)
Related Items (1)
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Minimal counterexamples for linear-time probabilistic verification
- Certifying algorithms
- A pivoting algorithm for convex hulls and vertex enumeration of arrangements and polyhedra
- The vertex set of a \(0/1\)-polytope is strongly \(\mathcal P\)-enumerable
- Primal-dual methods for vertex and facet enumeration
- On the approximability of minimizing nonzero variables or unsatisfied relations in linear systems
- Efficient enumeration of the vertices of polyhedra associated with network LP's
- Counterexample explanation by learning small strategies in Markov decision processes
- Reverse search for enumeration
- Symbolic model checking for probabilistic timed automata
- Analysis of backtrack algorithms for listing all vertices and all faces of a convex polyhedron.
- Minimal Critical Subsystems for Discrete-Time Markov Models
- A counterexample-guided abstraction-refinement framework for markov decision processes
- Model checking of probabilistic and nondeterministic systems
- Quantitative Multi-objective Verification for Probabilistic Systems
- Hierarchical Counterexamples for Discrete-Time Markov Chains
- The Complexity of Vertex Enumeration Methods
- Counterexample-guided abstraction refinement for symbolic model checking
- Verification of Markov Decision Processes Using Learning Algorithms
- Fast randomized consensus using shared memory
- Extended Directed Search for Probabilistic Timed Reachability
- Probabilistic CEGAR
- Counterexample Generation for Discrete-Time Markov Chains Using Bounded Model Checking
- Multi-Objective Model Checking of Markov Decision Processes
- An Algorithm for Finding All Vertices of Convex Polyhedral Sets
- An algorithm for determining all extreme points of a convex polytope
- Designing programs that check their work
- The complexity of probabilistic verification
- Termination of Probabilistic Concurrent Program
- Reducibility among Combinatorial Problems
- Temporal logics for the specification of performance and reliability
- Counterexample Generation for Discrete-Time Markov Models: An Introductory Survey
- From Model Checking to a Temporal Proof for Partial Models
- Verification: Theory and Practice
- Tools and Algorithms for the Construction and Analysis of Systems
- Programming Languages and Systems
- An Algorithm for Determining Irrelevant Constraints and all Vertices in Systems of Linear Inequalities
- Counterexamples in Probabilistic Model Checking
- Computer Aided Verification
- Generating all vertices of a polyhedron is hard
This page was built for publication: Farkas Certificates and Minimal Witnesses for Probabilistic Reachability Constraints
