12 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…