13 citations · 62 across the 26 of their papers we have counts for
31 papers
dtControl2+: Trading Optimality for Explainability in MDPs via Decision Trees
Tereza Kinská, Jan Křetínský, Tobias Meggendorfer +2
Over the past decade, decision trees have been used to represent controllers (a.k.a. policies) in an explainable way, with dtControl2 as a current state-of-the-art tool. However, f…
DOMtutor: Automated Autograding for Logic in Computer Science
Tobias Meggendorfer
Teaching computer science at universities is often structured rather classically and theory oriented. The former refers to "transmission"-style lectures accompanied by exercises wh…
Confidence Sequences for Online Statistical Model Checking of Markov Decision Processes
Konstantin Kueffner, Tobias Meggendorfer, Maximilian Weininger +1
Markov decision processes (MDPs) are a classic model of decision making under uncertainty, exhibiting both non-deterministic choice as well as probabilistic uncertainty. Traditiona…
UMB: A Unified Markov Binary Format for Probabilistic Model Checking (extended version)
Roman Andriushchenko, Arnd Hartmanns, Joshua Jeppson +5
This paper presents the unified Markov binary (UMB) format, an efficient, extensible, and well-supported explicit-state file format for representing a wide range of probabilistic s…
SemML 2.0: Synthesizing Controllers for LTL
Jan Křetínský, Tobias Meggendorfer, Maximilian Prokop
Synthesizing a reactive system from specifications given in linear temporal logic (LTL) is a classical problem, finding its applications in safety-critical systems design. These sy…
Statistical Model Checking Beyond Means: Quantiles, CVaR, and the DKW Inequality (extended version)
Carlos E. Budde, Arnd Hartmanns, Tobias Meggendorfer +2
Statistical model checking (SMC) randomly samples probabilistic models to approximate quantities of interest with statistical error guarantees. It is traditionally used to estimate…
Multiplicative Rewards in Markovian Models
Christel Baier, Krishnendu Chatterjee, Tobias Meggendorfer +1
This paper studies the expected value of multiplicative rewards, where rewards obtained in each step are multiplied (instead of the usual addition), in Markov chains (MCs) and Mark…
SemML: Enhancing Automata-Theoretic LTL Synthesis with Machine Learning
Jan Kretinsky, Tobias Meggendorfer, Maximilian Prokop +1
Synthesizing a reactive system from specifications given in linear temporal logic (LTL) is a classical problem, finding its applications in safety-critical systems design. We prese…
Solving Robust Markov Decision Processes: Generic, Reliable, Efficient
Tobias Meggendorfer, Maximilian Weininger, Patrick Wienhöft
Markov decision processes (MDP) are a well-established model for sequential decision-making in the presence of probabilities. In robust MDP (RMDP), every action is associated with…
Sound Statistical Model Checking for Probabilities and Expected Rewards (extended version)
Carlos E. Budde, Arnd Hartmanns, Tobias Meggendorfer +2
Statistical model checking estimates probabilities and expectations of interest in probabilistic system models by using random simulations. Its results come with statistical guaran…
Tools at the Frontiers of Quantitative Verification
Roman Andriushchenko, Alexander Bork, Carlos E. Budde +20
The analysis of formal models that include quantitative aspects such as timing or probabilistic choices is performed by quantitative verification tools. Broad and mature tool suppo…
Playing Games with your PET: Extending the Partial Exploration Tool to Stochastic Games
Tobias Meggendorfer, Maximilian Weininger
We present version 2.0 of the Partial Exploration Tool (PET), a tool for verification of probabilistic systems. We extend the previous version by adding support for stochastic game…
Certified Policy Verification and Synthesis for MDPs under Distributional Reach-avoidance Properties
S. Akshay, Krishnendu Chatterjee, Tobias Meggendorfer +1
Markov Decision Processes (MDPs) are a classical model for decision making in the presence of uncertainty. Often they are viewed as state transformers with planning objectives defi…
What Are the Odds? Improving the foundations of Statistical Model Checking
Tobias Meggendorfer, Maximilian Weininger, Patrick Wienhöft
Markov decision processes (MDPs) are a fundamental model for decision making under uncertainty. They exhibit non-deterministic choice as well as probabilistic uncertainty. Traditio…
Learning Algorithms for Verification of Markov Decision Processes
Tomáš Brázdil, Krishnendu Chatterjee, Martin Chmelik +6
We present a general framework for applying learning algorithms and heuristical guidance to the verification of Markov decision processes (MDPs). The primary goal of our techniques…
Reachability Poorman Discrete-Bidding Games
Guy Avni, Tobias Meggendorfer, Suman Sadhukhan +2
We consider {\em bidding games}, a class of two-player zero-sum {\em graph games}. The game proceeds as follows. Both players have bounded budgets. A token is placed on a vertex of…
Entropic Risk for Turn-Based Stochastic Games
Christel Baier, Krishnendu Chatterjee, Tobias Meggendorfer +1
Entropic risk (ERisk) is an established risk measure in finance, quantifying risk by an exponential re-weighting of rewards. We study ERisk for the first time in the context of tur…
MDPs as Distribution Transformers: Affine Invariant Synthesis for Safety Objectives
S. Akshay, Krishnendu Chatterjee, Tobias Meggendorfer +1
Markov decision processes can be viewed as transformers of probability distributions. While this view is useful from a practical standpoint to reason about trajectories of distribu…
Guessing Winning Policies in LTL Synthesis by Semantic Learning
Jan Kretinsky, Tobias Meggendorfer, Maximilian Prokop +1
We provide a learning-based technique for guessing a winning strategy in a parity game originating from an LTL synthesis problem. A cheaply obtained guess can be useful in several…
Stopping Criteria for Value Iteration on Stochastic Games with Quantitative Objectives
Jan Křetínský, Tobias Meggendorfer, Maximilian Weininger
A classic solution technique for Markov decision processes (MDP) and stochastic games (SG) is value iteration (VI). Due to its good practical performance, this approximative approa…
Correct Approximation of Stationary Distributions
Tobias Meggendorfer
A classical problem for Markov chains is determining their stationary (or steady-state) distribution. This problem has an equally classical solution based on eigenvectors and linea…
Satisfiability Bounds for -Regular Properties in Bounded-Parameter Markov Decision Processes
Jan Křetínský, Tobias Meggendorfer, Maximilian Weininger
We consider the problem of computing minimum and maximum probabilities of satisfying an -regular property in a bounded-parameter Markov decision process (BMDP). BMDP arise from…
Risk-aware Stochastic Shortest Path
Tobias Meggendorfer
We treat the problem of risk-aware control for stochastic shortest path (SSP) on Markov decision processes (MDP). Typically, expectation is considered for SSP, which however is obl…
Anytime Guarantees for Reachability in Uncountable Markov Decision Processes
Kush Grover, Jan Křetínský, Tobias Meggendorfer +1
We consider the problem of approximating the reachability probabilities in Markov decision processes (MDP) with uncountable (continuous) state and action spaces. While there are al…