51 citations · 122 across the 7 of their papers we have counts for
10 papers
dtControl 2.0: Explainable Strategy Representation via Decision Tree Learning Steered by Experts
Pranav Ashok, Mathias Jackermeier, Jan Křetínský +3
Recent advances have shown how decision trees are apt data structures for concisely representing strategies (or controllers) satisfying various objectives. Moreover, they also make…
DeepAbstract: Neural Network Abstraction for Accelerating Verification
Pranav Ashok, Vahid Hashemi, Jan Křetínský +1
While abstraction is a classic tool of verification to scale it up, it is not used very often for verifying neural networks. However, it can help with the still open task of scalin…
dtControl: Decision Tree Learning Algorithms for Controller Representation
Pranav Ashok, Mathias Jackermeier, Pushpak Jagtap +3
Decision tree learning is a popular classification technique most commonly used in machine learning applications. Recent work has shown that decision trees can be used to represent…
Approximating Values of Generalized-Reachability Stochastic Games
Pranav Ashok, Krishnendu Chatterjee, Jan Kretinsky +2
Simple stochastic games are turn-based 2.5-player games with a reachability objective. The basic question asks whether one player can ensure reaching a given target with at least a…
Strategy Representation by Decision Trees with Linear Classifiers
Pranav Ashok, Tomáš Brázdil, Krishnendu Chatterjee +3
Graph games and Markov decision processes (MDPs) are standard models in reactive synthesis and verification of probabilistic systems with nondeterminism. The class of -regular w…
SOS: Safe, Optimal and Small Strategies for Hybrid Markov Decision Processes
Pranav Ashok, Jan Křetínský, Kim Guldstrand Larsen +3
For hybrid Markov decision processes, UPPAAL Stratego can compute strategies that are safe for a given safety property and (in the limit) optimal for a given cost function. Unfortu…
PAC Statistical Model Checking for Markov Decision Processes and Stochastic Games
Pranav Ashok, Jan Křetínský, Maximilian Weininger
Statistical model checking (SMC) is a technique for analysis of probabilistic systems that may be (partially) unknown. We present an SMC algorithm for (unbounded) reachability yiel…
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…
Continuous-Time Markov Decisions based on Partial Exploration
Pranav Ashok, Yuliya Butkova, Holger Hermanns +1
We provide a framework for speeding up algorithms for time-bounded reachability analysis of continuous-time Markov decision processes. The principle is to find a small, but almost…
Value Iteration for Long-run Average Reward in Markov Decision Processes
Pranav Ashok, Krishnendu Chatterjee, Przemyslaw Daca +2
Markov decision processes (MDPs) are standard models for probabilistic systems with non-deterministic behaviours. Long-run average rewards provide a mathematically elegant formalis…