Showing 1–23 of 23 results for author: Weininger, M

Tools at the Frontiers of Quantitative Verification

Authors: Roman Andriushchenko, Alexander Bork, Carlos E. Budde, Milan Češka, Kush Grover, Ernst Moritz Hahn, Arnd Hartmanns, Bryant Israelsen, Nils Jansen, Joshua Jeppson, Sebastian Junges, Maximilian A. Köhl, Bettina Könighofer, Jan Křetínský, Tobias Meggendorfer, David Parker, Stefan Pranger, Tim Quatmann, Enno Ruijters, Landon Taylor, Matthias Volk, Maximilian Weininger, Zhen Zhang

Abstract: 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 support is available for computing basic properties such as expected rewards on basic models such as Markov chains. Previous editions of QComp, the comparison of tools for the analysis of quantitative formal models, focused o… ▽ More 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 support is available for computing basic properties such as expected rewards on basic models such as Markov chains. Previous editions of QComp, the comparison of tools for the analysis of quantitative formal models, focused on this setting. Many application scenarios, however, require more advanced property types such as LTL and parameter synthesis queries as well as advanced models like stochastic games and partially observable MDPs. For these, tool support is in its infancy today. This paper presents the outcomes of QComp 2023: a survey of the state of the art in quantitative verification tool support for advanced property types and models. With tools ranging from first research prototypes to well-supported integrations into established toolsets, this report highlights today's active areas and tomorrow's challenges in tool-focused research for quantitative verification. △ Less

Submitted 22 May, 2024; originally announced May 2024.

Playing Games with your PET: Extending the Partial Exploration Tool to Stochastic Games

Authors: Tobias Meggendorfer, Maximilian Weininger

Abstract: 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 games, based on a recent unified framework for sound value iteration algorithms. Thereby, PET2 is the first tool implementing a sound and efficient approach for solving stochastic games with objectives of the type reachabili… ▽ More 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 games, based on a recent unified framework for sound value iteration algorithms. Thereby, PET2 is the first tool implementing a sound and efficient approach for solving stochastic games with objectives of the type reachability/safety and mean payoff. We complement this approach by develo** and implementing a partial-exploration based variant for all three objectives. Our experimental evaluation shows that PET2 offers the most efficient partial-exploration based algorithm and is the most viable tool on SGs, even outperforming unsound tools. △ Less

Submitted 13 May, 2024; v1 submitted 6 May, 2024; originally announced May 2024.

What Are the Odds? Improving the foundations of Statistical Model Checking

Authors: Tobias Meggendorfer, Maximilian Weininger, Patrick Wienhöft

Abstract: Markov decision processes (MDPs) are a fundamental model for decision making under uncertainty. They exhibit non-deterministic choice as well as probabilistic uncertainty. Traditionally, verification algorithms assume exact knowledge of the probabilities that govern the behaviour of an MDP. As this assumption is often unrealistic in practice, statistical model checking (SMC) was developed in the p… ▽ More Markov decision processes (MDPs) are a fundamental model for decision making under uncertainty. They exhibit non-deterministic choice as well as probabilistic uncertainty. Traditionally, verification algorithms assume exact knowledge of the probabilities that govern the behaviour of an MDP. As this assumption is often unrealistic in practice, statistical model checking (SMC) was developed in the past two decades. It allows to analyse MDPs with unknown transition probabilities and provide probably approximately correct (PAC) guarantees on the result. Model-based SMC algorithms sample the MDP and build a model of it by estimating all transition probabilities, essentially for every transition answering the question: ``What are the odds?'' However, so far the statistical methods employed by the state of the art SMC algorithms are quite naive. Our contribution are several fundamental improvements to those methods: On the one hand, we survey statistics literature for better concentration inequalities; on the other hand, we propose specialised approaches that exploit our knowledge of the MDP. Our improvements are generally applicable to many kinds of problem statements because they are largely independent of the setting. Moreover, our experimental evaluation shows that they lead to significant gains, reducing the number of samples that the SMC algorithm has to collect by up to two orders of magnitude. △ Less

Submitted 8 April, 2024; originally announced April 2024.

Stop** Criteria for Value Iteration on Stochastic Games with Quantitative Objectives

Authors: Jan Křetínský, Tobias Meggendorfer, Maximilian Weininger

Abstract: 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 approach is typically preferred over exact techniques, even though no practical bounds on the imprecision of the result could be given until recently. As a consequence, even the most used model checkers could return arbitraril… ▽ More 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 approach is typically preferred over exact techniques, even though no practical bounds on the imprecision of the result could be given until recently. As a consequence, even the most used model checkers could return arbitrarily wrong results. Over the past decade, different works derived stop** criteria, indicating when the precision reaches the desired level, for various settings, in particular MDP with reachability, total reward, and mean payoff, and SG with reachability. In this paper, we provide the first stop** criteria for VI on SG with total reward and mean payoff, yielding the first anytime algorithms in these settings. To this end, we provide the solution in two flavours: First through a reduction to the MDP case and second directly on SG. The former is simpler and automatically utilizes any advances on MDP. The latter allows for more local computations, heading towards better practical efficiency. Our solution unifies the previously mentioned approaches for MDP and SG and their underlying ideas. To achieve this, we isolate objective-specific subroutines as well as identify objective-independent concepts. These structural concepts, while surprisingly simple, form the very essence of the unified solution. △ Less

Submitted 19 April, 2023; originally announced April 2023.

A Practitioner's Guide to MDP Model Checking Algorithms

Authors: Arnd Hartmanns, Sebastian Junges, Tim Quatmann, Maximilian Weininger

Abstract: Model checking undiscounted reachability and expected-reward properties on Markov decision processes (MDPs) is key for the verification of systems that act under uncertainty. Popular algorithms are policy iteration and variants of value iteration; in tool competitions, most participants rely on the latter. These algorithms generally need worst-case exponential time. However the problem can equally… ▽ More Model checking undiscounted reachability and expected-reward properties on Markov decision processes (MDPs) is key for the verification of systems that act under uncertainty. Popular algorithms are policy iteration and variants of value iteration; in tool competitions, most participants rely on the latter. These algorithms generally need worst-case exponential time. However the problem can equally be formulated as a linear program, solvable in polynomial time. In this paper, we give a detailed overview of today's state-of-the-art algorithms for MDP model checking with a focus on performance and correctness. We highlight their fundamental differences, and describe various optimisations and implementation variants. We experimentally compare floating-point and exact-arithmetic implementations of all algorithms on three benchmark sets using two probabilistic model checkers. Our results show that (optimistic) value iteration is a sensible default, but other algorithms are preferable in specific settings. This paper thereby provides a guide for MDP verification practitioners -- tool builders and users alike. △ Less

Submitted 24 January, 2023; originally announced January 2023.

Algebraically Explainable Controllers: Decision Trees and Support Vector Machines Join Forces

Authors: Florian Jüngermann, Jan Křetínský, Maximilian Weininger

Abstract: Recently, decision trees (DT) have been used as an explainable representation of controllers (a.k.a. strategies, policies, schedulers). Although they are often very efficient and produce small and understandable controllers for discrete systems, complex continuous dynamics still pose a challenge. In particular, when the relationships between variables take more complex forms, such as polynomials,… ▽ More Recently, decision trees (DT) have been used as an explainable representation of controllers (a.k.a. strategies, policies, schedulers). Although they are often very efficient and produce small and understandable controllers for discrete systems, complex continuous dynamics still pose a challenge. In particular, when the relationships between variables take more complex forms, such as polynomials, they cannot be obtained using the available DT learning procedures. In contrast, support vector machines provide a more powerful representation, capable of discovering many such relationships, but not in an explainable form. Therefore, we suggest to combine the two frameworks in order to obtain an understandable representation over richer, domain-relevant algebraic predicates. We demonstrate and evaluate the proposed method experimentally on established benchmarks. △ Less

Submitted 29 August, 2022; v1 submitted 26 August, 2022; originally announced August 2022.

Optimistic and Topological Value Iteration for Simple Stochastic Games

Authors: Muqsit Azeem, Alexandros Evangelidis, Jan Křetínský, Alexander Slivinskiy, Maximilian Weininger

Abstract: While value iteration (VI) is a standard solution approach to simple stochastic games (SSGs), it suffered from the lack of a stop** criterion. Recently, several solutions have appeared, among them also "optimistic" VI (OVI). However, OVI is applicable only to one-player SSGs with no end components. We lift these two assumptions, making it available to general SSGs. Further, we utilize the idea i… ▽ More While value iteration (VI) is a standard solution approach to simple stochastic games (SSGs), it suffered from the lack of a stop** criterion. Recently, several solutions have appeared, among them also "optimistic" VI (OVI). However, OVI is applicable only to one-player SSGs with no end components. We lift these two assumptions, making it available to general SSGs. Further, we utilize the idea in the context of topological VI, where we provide an efficient precise solution. In order to compare the new algorithms with the state of the art, we use not only the standard benchmarks, but we also design a random generator of SSGs, which can be biased towards various types of models, aiding in understanding the advantages of different algorithms on SSGs. △ Less

Submitted 28 July, 2022; originally announced July 2022.

Satisfiability Bounds for $ω$-Regular Properties in Bounded-Parameter Markov Decision Processes

Authors: Jan Křetínský, Tobias Meggendorfer, Maximilian Weininger

Abstract: 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 Markov decision processes (MDP) by allowing for uncertainty on the transition probabilities in the form of intervals where the actual probabilities are unknown. $ω$-regular languages form a large class of properties, exp… ▽ More 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 Markov decision processes (MDP) by allowing for uncertainty on the transition probabilities in the form of intervals where the actual probabilities are unknown. $ω$-regular languages form a large class of properties, expressible as, e.g., Rabin or parity automata, encompassing rich specifications such as linear temporal logic. In a BMDP the probability to satisfy the property depends on the unknown transitions probabilities as well as on the policy. In this paper, we compute the extreme values. This solves the problem specifically suggested by Dutreix and Coogan in CDC 2018, extending their results on interval Markov chains with no adversary. The main idea is to reinterpret their work as analysis of interval MDP and accordingly the BMDP problem as analysis of an $ω$-regular stochastic game, where a solution is provided. This method extends smoothly further to bounded-parameter stochastic games. △ Less

Submitted 27 July, 2022; originally announced July 2022.

Stochastic Games with Disjunctions of Multiple Objectives

Authors: Tobias Winkler, Maximilian Weininger

Abstract: Stochastic games combine controllable and adversarial non-determinism with stochastic behavior and are a common tool in control, verification and synthesis of reactive systems facing uncertainty. Multi-objective stochastic games are natural in situations where several - possibly conflicting - performance criteria like time and energy consumption are relevant. Such conjunctive combinations are the… ▽ More Stochastic games combine controllable and adversarial non-determinism with stochastic behavior and are a common tool in control, verification and synthesis of reactive systems facing uncertainty. Multi-objective stochastic games are natural in situations where several - possibly conflicting - performance criteria like time and energy consumption are relevant. Such conjunctive combinations are the most studied multi-objective setting in the literature. In this paper, we consider the dual disjunctive problem. More concretely, we study turn-based stochastic two-player games on graphs where the winning condition is to guarantee at least one reachability or safety objective from a given set of alternatives. We present a fine-grained overview of strategy and computational complexity of such disjunctive queries (DQs) and provide new lower and upper bounds for several variants of the problem, significantly extending previous works. We also propose a novel value iteration-style algorithm for approximating the set of Pareto optimal thresholds for a given DQ. △ Less

Submitted 16 September, 2021; originally announced September 2021.

Comments: In Proceedings GandALF 2021, arXiv:2109.07798. arXiv admin note: substantial text overlap with arXiv:2108.04604

Journal ref: EPTCS 346, 2021, pp. 83-100

Stochastic Games with Disjunctions of Multiple Objectives (Technical Report)

Authors: Tobias Winkler, Maximilian Weininger

Abstract: Stochastic games combine controllable and adversarial non-determinism with stochastic behavior and are a common tool in control, verification and synthesis of reactive systems facing uncertainty. Multi-objective stochastic games are natural in situations where several - possibly conflicting - performance criteria like time and energy consumption are relevant. Such conjunctive combinations are the… ▽ More Stochastic games combine controllable and adversarial non-determinism with stochastic behavior and are a common tool in control, verification and synthesis of reactive systems facing uncertainty. Multi-objective stochastic games are natural in situations where several - possibly conflicting - performance criteria like time and energy consumption are relevant. Such conjunctive combinations are the most studied multi-objective setting in the literature. In this paper, we consider the dual disjunctive problem. More concretely, we study turn-based stochastic two-player games on graphs where the winning condition is to guarantee at least one reachability or safety objective from a given set of alternatives. We present a fine-grained overview of strategy and computational complexity of such \emph{disjunctive queries} (DQs) and provide new lower and upper bounds for several variants of the problem, significantly extending previous works. We also propose a novel value iteration-style algorithm for approximating the set of Pareto optimal thresholds for a given DQ. △ Less

Submitted 6 September, 2021; v1 submitted 10 August, 2021; originally announced August 2021.

Comments: Technical report including appendix with detailed proofs, 29 pages

dtControl 2.0: Explainable Strategy Representation via Decision Tree Learning Steered by Experts

Authors: Pranav Ashok, Mathias Jackermeier, Jan Křetínský, Christoph Weinhuber, Maximilian Weininger, Mayank Yadav

Abstract: Recent advances have shown how decision trees are apt data structures for concisely representing strategies (or controllers) satisfying various objectives. Moreover, they also make the strategy more explainable. The recent tool dtControl had provided pipelines with tools supporting strategy synthesis for hybrid systems, such as SCOTS and Uppaal Stratego. We present dtControl 2.0, a new version wit… ▽ More Recent advances have shown how decision trees are apt data structures for concisely representing strategies (or controllers) satisfying various objectives. Moreover, they also make the strategy more explainable. The recent tool dtControl had provided pipelines with tools supporting strategy synthesis for hybrid systems, such as SCOTS and Uppaal Stratego. We present dtControl 2.0, a new version with several fundamentally novel features. Most importantly, the user can now provide domain knowledge to be exploited in the decision tree learning process and can also interactively steer the process based on the dynamically provided information. To this end, we also provide a graphical user interface. It allows for inspection and re-computation of parts of the result, suggesting as well as receiving advice on predicates, and visual simulation of the decision-making process. Besides, we interface model checkers of probabilistic systems, namely Storm and PRISM and provide dedicated support for categorical enumeration-type state variables. Consequently, the controllers are more explainable and smaller. △ Less

Submitted 4 May, 2021; v1 submitted 15 January, 2021; originally announced January 2021.

Journal ref: TACAS (2) (pp. 326-345). Springer. 2021

Online Monitoring $ω$-Regular Properties in Unknown Markov Chains

Authors: Javier Esparza, Stefan Kiefer, Jan Kretinsky, Maximilian Weininger

Abstract: We study runtime monitoring of $ω$-regular properties. We consider a simple setting in which a run of an unknown finite-state Markov chain $\mathcal M$ is monitored against a fixed but arbitrary $ω$-regular specification $\varphi$. The purpose of monitoring is to keep aborting runs that are "unlikely" to satisfy the specification until $\mathcal M$ executes a correct run. We design controllers for… ▽ More We study runtime monitoring of $ω$-regular properties. We consider a simple setting in which a run of an unknown finite-state Markov chain $\mathcal M$ is monitored against a fixed but arbitrary $ω$-regular specification $\varphi$. The purpose of monitoring is to keep aborting runs that are "unlikely" to satisfy the specification until $\mathcal M$ executes a correct run. We design controllers for the reset action that (assuming that $\varphi$ has positive probability) satisfy the following property w.p.1: the number of resets is finite, and the run executed by $\mathcal M$ after the last reset satisfies $\varphi$. △ Less

Submitted 16 October, 2020; originally announced October 2020.

Comparison of Algorithms for Simple Stochastic Games

Authors: Jan Křetínský, Emanuel Ramneantu, Alexander Slivinskiy, Maximilian Weininger

Abstract: Simple stochastic games are turn-based 2.5-player zero-sum graph games with a reachability objective. The problem is to compute the winning probability as well as the optimal strategies of both players. In this paper, we compare the three known classes of algorithms -- value iteration, strategy iteration and quadratic programming -- both theoretically and practically. Further, we suggest several… ▽ More Simple stochastic games are turn-based 2.5-player zero-sum graph games with a reachability objective. The problem is to compute the winning probability as well as the optimal strategies of both players. In this paper, we compare the three known classes of algorithms -- value iteration, strategy iteration and quadratic programming -- both theoretically and practically. Further, we suggest several improvements for all algorithms, including the first approach based on quadratic programming that avoids transforming the stochastic game to a stop** one. Our extensive experiments show that these improvements can lead to significant speed-ups. We implemented all algorithms in PRISM-games 3.0, thereby providing the first implementation of quadratic programming for solving simple stochastic games. △ Less

Submitted 22 September, 2020; originally announced September 2020.

Comments: In Proceedings GandALF 2020, arXiv:2009.09360

Journal ref: EPTCS 326, 2020, pp. 131-148

Comparison of Algorithms for Simple Stochastic Games (Full Version)

Authors: Jan Kretinsky, Emanuel Ramneantu, Alexander Slivinskiy, Maximilian Weininger

Abstract: Simple stochastic games are turn-based 2.5-player zero-sum graph games with a reachability objective. The problem is to compute the winning probability as well as the optimal strategies of both players. In this paper, we compare the three known classes of algorithms -- value iteration, strategy iteration and quadratic programming -- both theoretically and practically. Further, we suggest several i… ▽ More Simple stochastic games are turn-based 2.5-player zero-sum graph games with a reachability objective. The problem is to compute the winning probability as well as the optimal strategies of both players. In this paper, we compare the three known classes of algorithms -- value iteration, strategy iteration and quadratic programming -- both theoretically and practically. Further, we suggest several improvements for all algorithms, including the first approach based on quadratic programming that avoids transforming the stochastic game to a stop** one. Our extensive experiments show that these improvements can lead to significant speed-ups. We implemented all algorithms in PRISM-games 3.0, thereby providing the first implementation of quadratic programming for solving simple stochastic games. △ Less

Submitted 25 August, 2020; v1 submitted 21 August, 2020; originally announced August 2020.

Anytime Guarantees for Reachability in Uncountable Markov Decision Processes

Authors: Kush Grover, Jan Křetínský, Tobias Meggendorfer, Maximilian Weininger

Abstract: We consider the problem of approximating the reachability probabilities in Markov decision processes (MDP) with uncountable (continuous) state and action spaces. While there are algorithms that, for special classes of such MDP, provide a sequence of approximations converging to the true value in the limit, our aim is to obtain an algorithm with guarantees on the precision of the approximation. As… ▽ More We consider the problem of approximating the reachability probabilities in Markov decision processes (MDP) with uncountable (continuous) state and action spaces. While there are algorithms that, for special classes of such MDP, provide a sequence of approximations converging to the true value in the limit, our aim is to obtain an algorithm with guarantees on the precision of the approximation. As this problem is undecidable in general, assumptions on the MDP are necessary. Our main contribution is to identify sufficient assumptions that are as weak as possible, thus approaching the "boundary" of which systems can be correctly and reliably analyzed. To this end, we also argue why each of our assumptions is necessary for algorithms based on processing finitely many observations. We present two solution variants. The first one provides converging lower bounds under weaker assumptions than typical ones from previous works concerned with guarantees. The second one then utilizes stronger assumptions to additionally provide converging upper bounds. Altogether, we obtain an anytime algorithm, i.e. yielding a sequence of approximants with known and iteratively improving precision, converging to the true value in the limit. Besides, due to the generality of our assumptions, our algorithms are very general templates, readily allowing for various heuristics from literature in contrast to, e.g., a specific discretization algorithm. Our theoretical contribution thus paves the way for future practical improvements without sacrificing correctness guarantees. △ Less

Submitted 12 July, 2022; v1 submitted 10 August, 2020; originally announced August 2020.

Stochastic Games with Lexicographic Reachability-Safety Objectives

Authors: Krishnendu Chatterjee, Joost-Pieter Katoen, Maximilian Weininger, Tobias Winkler

Abstract: We study turn-based stochastic zero-sum games with lexicographic preferences over reachability and safety objectives. Stochastic games are standard models in control, verification, and synthesis of stochastic reactive systems that exhibit both randomness as well as angelic and demonic non-determinism. Lexicographic order allows to consider multiple objectives with a strict preference order over th… ▽ More We study turn-based stochastic zero-sum games with lexicographic preferences over reachability and safety objectives. Stochastic games are standard models in control, verification, and synthesis of stochastic reactive systems that exhibit both randomness as well as angelic and demonic non-determinism. Lexicographic order allows to consider multiple objectives with a strict preference order over the satisfaction of the objectives. To the best of our knowledge, stochastic games with lexicographic objectives have not been studied before. We establish determinacy of such games and present strategy and computational complexity results. For strategy complexity, we show that lexicographically optimal strategies exist that are deterministic and memory is only required to remember the already satisfied and violated objectives. For a constant number of objectives, we show that the relevant decision problem is in NP $\cap$ coNP, matching the current known bound for single objectives; and in general the decision problem is PSPACE-hard and can be solved in NEXPTIME $\cap$ coNEXPTIME. We present an algorithm that computes the lexicographically optimal strategies via a reduction to computation of optimal strategies in a sequence of single-objectives games. We have implemented our algorithm and report experimental results on various case studies. △ Less

Submitted 13 May, 2020; v1 submitted 8 May, 2020; originally announced May 2020.

Comments: Full version (33 pages) of CAV20 conference paper; including an appendix with technical proofs

Automata Tutor v3

Authors: Loris D'Antoni, Martin Helfrich, Jan Kretinsky, Emanuel Ramneantu, Maximilian Weininger

Abstract: Computer science class enrollments have rapidly risen in the past decade. With current class sizes, standard approaches to grading and providing personalized feedback are no longer possible and new techniques become both feasible and necessary. In this paper, we present the third version of Automata Tutor, a tool for hel** teachers and students in large courses on automata and formal languages.… ▽ More Computer science class enrollments have rapidly risen in the past decade. With current class sizes, standard approaches to grading and providing personalized feedback are no longer possible and new techniques become both feasible and necessary. In this paper, we present the third version of Automata Tutor, a tool for hel** teachers and students in large courses on automata and formal languages. The second version of Automata Tutor supported automatic grading and feedback for finite-automata constructions and has already been used by thousands of users in dozens of countries. This new version of Automata Tutor supports automated grading and feedback generation for a greatly extended variety of new problems, including problems that ask students to create regular expressions, context-free grammars, pushdown automata and Turing machines corresponding to a given description, and problems about converting between equivalent models - e.g., from regular expressions to nondeterministic finite automata. Moreover, for several problems, this new version also enables teachers and students to automatically generate new problem instances. We also present the results of a survey run on a class of 950 students, which shows very positive results about the usability and usefulness of the tool. △ Less

Submitted 14 May, 2020; v1 submitted 4 May, 2020; originally announced May 2020.

dtControl: Decision Tree Learning Algorithms for Controller Representation

Authors: Pranav Ashok, Mathias Jackermeier, Pushpak Jagtap, Jan Křetínský, Maximilian Weininger, Majid Zamani

Abstract: 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 provably-correct controllers concisely. Compared to representations using lookup tables or binary decision diagrams, decision trees are smaller and more explainable. We present dtControl, an easily extensible tool for r… ▽ More 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 provably-correct controllers concisely. Compared to representations using lookup tables or binary decision diagrams, decision trees are smaller and more explainable. We present dtControl, an easily extensible tool for representing memoryless controllers as decision trees. We give a comprehensive evaluation of various decision tree learning algorithms applied to 10 case studies arising out of correct-by-construction controller synthesis. These algorithms include two new techniques, one for using arbitrary linear binary classifiers in the decision tree learning, and one novel approach for determinizing controllers during the decision tree construction. In particular the latter turns out to be extremely efficient, yielding decision trees with a single-digit number of decision nodes on 5 of the case studies. △ Less

Submitted 12 February, 2020; originally announced February 2020.

Approximating Values of Generalized-Reachability Stochastic Games

Authors: Pranav Ashok, Krishnendu Chatterjee, Jan Kretinsky, Maximilian Weininger, Tobias Winkler

Abstract: 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 given probability. A natural extension is games with a conjunction of such conditions as objective. Despite a plethora of recent results on the analysis of systems with multiple objectives, the decidability of this basi… ▽ More 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 given probability. A natural extension is games with a conjunction of such conditions as objective. Despite a plethora of recent results on the analysis of systems with multiple objectives, the decidability of this basic problem remains open. In this paper, we present an algorithm approximating the Pareto frontier of the achievable values to a given precision. Moreover, it is an anytime algorithm, meaning it can be stopped at any time returning the current approximation and its error bound. △ Less

Submitted 27 April, 2020; v1 submitted 14 August, 2019; originally announced August 2019.

SOS: Safe, Optimal and Small Strategies for Hybrid Markov Decision Processes

Authors: Pranav Ashok, Jan Křetínský, Kim Guldstrand Larsen, Adrien Le Coënt, Jakob Haahr Taankvist, Maximilian Weininger

Abstract: 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. Unfortunately, these strategies cannot be exported easily since they are computed as a very long list. In this paper, we demonstrate methods to learn compact representations of the strategies in the form of decision trees. Thes… ▽ More 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. Unfortunately, these strategies cannot be exported easily since they are computed as a very long list. In this paper, we demonstrate methods to learn compact representations of the strategies in the form of decision trees. These decision trees are much smaller, more understandable, and can easily be exported as code that can be loaded into embedded systems. Despite the size compression and actual differences to the original strategy, we provide guarantees on both safety and optimality of the decision-tree strategy. On the top, we show how to obtain yet smaller representations, which are still guaranteed safe, but achieve a desired trade-off between size and optimality. △ Less

Submitted 25 June, 2019; originally announced June 2019.

PAC Statistical Model Checking for Markov Decision Processes and Stochastic Games

Authors: Pranav Ashok, Jan Křetínský, Maximilian Weininger

Abstract: 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 yielding probably approximately correct (PAC) guarantees on the results. We consider both the setting (i) with no knowledge of the transition function (with the only quantity required a bound on the minimum transition probab… ▽ More 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 yielding probably approximately correct (PAC) guarantees on the results. We consider both the setting (i) with no knowledge of the transition function (with the only quantity required a bound on the minimum transition probability) and (ii) with knowledge of the topology of the underlying graph. On the one hand, it is the first algorithm for stochastic games. On the other hand, it is the first practical algorithm even for Markov decision processes. Compared to previous approaches where PAC guarantees require running times longer than the age of universe even for systems with a handful of states, our algorithm often yields reasonably precise results within minutes, not requiring the knowledge of mixing time or the topology of the whole model. △ Less

Submitted 1 February, 2021; v1 submitted 10 May, 2019; originally announced May 2019.

Value Iteration for Simple Stochastic Games: Stop** Criterion and Learning Algorithm

Authors: Edon Kelmendi, Julia Krämer, Jan Kretinsky, Maximilian Weininger

Abstract: 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 the value only in the limit. Since no stop** criterion is known, this technique does not provide any guarantees on its results. We provide the first stop** criterion for VI on simple stochastic games. It is achieved… ▽ More 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 the value only in the limit. Since no stop** criterion is known, this technique does not provide any guarantees on its results. We provide the first stop** criterion for VI on simple stochastic games. It is achieved by additionally computing a convergent sequence of over-approximations of the value, relying on an analysis of the game graph. Consequently, VI becomes an anytime algorithm returning the approximation of the value and the current error bound. As another consequence, we can provide a simulation-based asynchronous VI algorithm, which yields the same guarantees, but without necessarily exploring the whole game graph. △ Less

Submitted 13 April, 2018; originally announced April 2018.

Comments: CAV2018

Index appearance record for transforming Rabin automata into parity automata

Authors: Jan Křetínský, Tobias Meggendorfer, Clara Waldmann, Maximilian Weininger

Abstract: Transforming deterministic $ω$-automata into deterministic parity automata is traditionally done using variants of appearance records. We present a more efficient variant of this approach, tailored to Rabin automata, and several optimizations applicable to all appearance records. We compare the methods experimentally and find out that our method produces smaller automata than previous approaches.… ▽ More Transforming deterministic $ω$-automata into deterministic parity automata is traditionally done using variants of appearance records. We present a more efficient variant of this approach, tailored to Rabin automata, and several optimizations applicable to all appearance records. We compare the methods experimentally and find out that our method produces smaller automata than previous approaches. Moreover, the experiments demonstrate the potential of our method for LTL synthesis, using LTL-to-Rabin translators. It leads to significantly smaller parity automata when compared to state-of-the-art approaches on complex formulae. △ Less

Submitted 20 January, 2017; originally announced January 2017.