8 citations · 25 across the 17 of their papers we have counts for
8 papers · 1 filter
Monte Carlo Tree Search for Verifying Reachability in Markov Decision Processes
Pranav Ashok, Tomáš Brázdil, Jan Křetínský +1
The maximum reachability probabilities in a Markov decision process can be computed using value iteration (VI). Recently, simulation-based heuristic extensions of VI have been intr…
LTL Store: Repository of LTL formulae from literature and case studies
Jan Křetínský, Tobias Meggendorfer, Salomon Sickert
This continuously extended technical report collects and compares commonly used formulae from the literature and provides them in a machine readable way.
The Satisfiability Problem for Unbounded Fragments of Probabilistic CTL
Jan Křetínský, Alexej Rotar
We investigate the satisfiability and finite satisfiability problem for probabilistic computation-tree logic (PCTL) where operators are not restricted by any step bounds. We establ…
Conditional Value-at-Risk for Reachability and Mean Payoff in Markov Decision Processes
Jan Křetínský, Tobias Meggendorfer
We present the conditional value-at-risk (CVaR) in the context of Markov chains and Markov decision processes with reachability and mean-payoff objectives. CVaR quantifies risk by…
One Theorem to Rule Them All: A Unified Translation of LTL into ω-Automata
Javier Esparza, Jan Kretinsky, Salomon Sickert
We present a unified translation of LTL formulas into deterministic Rabin automata, limit-deterministic Büchi automata, and nondeterministic Büchi automata. The translations yield…
Value Iteration for Simple Stochastic Games: Stopping Criterion and Learning Algorithm
Edon Kelmendi, Julia Krämer, Jan Kretinsky +1
Simple stochastic games can be solved by value iteration (VI), which yields a sequence of under-approximations of the value of the game. This sequence is guaranteed to converge to…