
LTLConstrained SteadyState Policy Synthesis
Decisionmaking policies for agents are often synthesized with the const...
read it

dtControl 2.0: Explainable Strategy Representation via Decision Tree Learning Steered by Experts
Recent advances have shown how decision trees are apt data structures fo...
read it

Comparison of Algorithms for Simple Stochastic Games
Simple stochastic games are turnbased 2.5player zerosum graph games w...
read it

Comparison of Algorithms for Simple Stochastic Games (Full Version)
Simple stochastic games are turnbased 2.5player zerosum graph games w...
read it

Formalizing and Guaranteeing* HumanRobot Interaction
Robot capabilities are maturing across domains, from selfdriving cars, ...
read it

DeepAbstract: Neural Network Abstraction for Accelerating Verification
While abstraction is a classic tool of verification to scale it up, it i...
read it

dtControl: Decision Tree Learning Algorithms for Controller Representation
Decision tree learning is a popular classification technique most common...
read it

Stopping Criteria for Value and Strategy Iteration on Concurrent Stochastic Reachability Games
We consider concurrent stochastic games played on graphs with reachabili...
read it

Approximating Values of GeneralizedReachability Stochastic Games
Simple stochastic games are turnbased 2.5player games with a reachabil...
read it

Semantic Labelling and Learning for Parity Game Solving in LTL Synthesis
We propose "semantic labelling" as a novel ingredient for solving games ...
read it

SOS: Safe, Optimal and Small Strategies for Hybrid Markov Decision Processes
For hybrid Markov decision processes, UPPAAL Stratego can compute strate...
read it

Strategy Representation by Decision Trees with Linear Classifiers
Graph games and Markov decision processes (MDPs) are standard models in ...
read it

Of Cores: A PartialExploration Framework for Markov Decision Processes
We introduce a framework for approximate analysis of Markov decision pro...
read it

SemiQuantitative Abstraction and Analysis of Chemical Reaction Networks
Analysis of large continuoustime stochastic systems is a computationall...
read it

PAC Statistical Model Checking for Markov Decision Processes and Stochastic Games
Statistical model checking (SMC) is a technique for analysis of probabil...
read it

Monte Carlo Tree Search for Verifying Reachability in Markov Decision Processes
The maximum reachability probabilities in a Markov decision process can ...
read it

ContinuousTime Markov Decisions based on Partial Exploration
We provide a framework for speeding up algorithms for timebounded reach...
read it

LTL Store: Repository of LTL formulae from literature and case studies
This continuously extended technical report collects and compares common...
read it

The Satisfiability Problem for Unbounded Fragments of Probabilistic CTL
We investigate the satisfiability and finite satisfiability problem for ...
read it

Conditional ValueatRisk for Reachability and Mean Payoff in Markov Decision Processes
We present the conditional valueatrisk (CVaR) in the context of Markov...
read it

One Theorem to Rule Them All: A Unified Translation of LTL into ωAutomata
We present a unified translation of LTL formulas into deterministic Rabi...
read it

LearningBased MeanPayoff Optimization in an Unknown MDP under OmegaRegular Constraints
We formalize the problem of maximizing the meanpayoff value with high p...
read it

Value Iteration for Simple Stochastic Games: Stopping Criterion and Learning Algorithm
Simple stochastic games can be solved by value iteration (VI), which yie...
read it

Strategy Representation by Decision Trees in Reactive Synthesis
Graph games played by two players over finitestate graphs are central i...
read it

Efficient Strategy Iteration for Mean Payoff in Markov Decision Processes
Markov decision processes (MDPs) are standard models for probabilistic s...
read it
Jan Křetínský
is this you? claim profile