@article{21413, abstract = {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 is to improve performance by avoiding an exhaustive exploration of the state space, instead focussing on particularly relevant areas of the system, guided by heuristics. Our work builds on the previous results of Br{á}zdil et al., significantly extending it as well as refining several details and fixing errors. The presented framework focuses on probabilistic reachability, which is a core problem in verification, and is instantiated in two distinct scenarios. The first assumes that full knowledge of the MDP is available, in particular precise transition probabilities. It performs a heuristic-driven partial exploration of the model, yielding precise lower and upper bounds on the required probability. The second tackles the case where we may only sample the MDP without knowing the exact transition dynamics. Here, we obtain probabilistic guarantees, again in terms of both the lower and upper bounds, which provides efficient stopping criteria for the approximation. In particular, the latter is an extension of statistical model-checking (SMC) for unbounded properties in MDPs. In contrast to other related approaches, we do not restrict our attention to time-bounded (finite-horizon) or discounted properties, nor assume any particular structural properties of the MDP.}, author = {Brázdil, Tomáš and Chatterjee, Krishnendu and Chmelik, Martin and Forejt, Vojtěch and Kretinsky, Jan and Kwiatkowska, Marta and Meggendorfer, Tobias and Parker, David and Ujma, Mateusz}, issn = {2751-4838}, journal = {TheoretiCS}, publisher = {TheoretiCS Foundation}, title = {{Learning algorithms for verification of Markov decision processes}}, doi = {10.46298/theoretics.25.10}, volume = {4}, year = {2025}, } @inproceedings{19375, abstract = {Despite the advances in probabilistic model checking, the scalability of the verification methods remains limited. In particular, the state space often becomes extremely large when instantiating parameterized Markov decision processes (MDPs) even with moderate values. Synthesizing policies for such huge MDPs is beyond the reach of available tools. We propose a learning-based approach to obtain a reasonable policy for such huge MDPs. The idea is to generalize optimal policies obtained by model-checking small instances to larger ones using decision-tree learning. Consequently, our method bypasses the need for explicit state-space exploration of large models, providing a practical solution to the state-space explosion problem. We demonstrate the efficacy of our approach by performing extensive experimentation on the relevant models from the quantitative verification benchmark set. The experimental results indicate that our policies perform well, even when the size of the model is orders of magnitude beyond the reach of state-of-the-art analysis tools.}, author = {Azeem, Muqsit and Chakraborty, Debraj and Kanav, Sudeep and Kretinsky, Jan and Mohagheghi, Mohammadsadegh and Mohr, Stefanie and Weininger, Maximilian}, booktitle = {26th International Conference on Verification, Model Checking, and Abstract Interpretation}, isbn = {9783031827020}, issn = {1611-3349}, location = {Denver, CO, United States}, pages = {97--120}, publisher = {Springer Nature}, title = {{1–2–3–Go! Policy synthesis for parameterized Markov decision processes via decision-tree learning and generalization}}, doi = {10.1007/978-3-031-82703-7_5}, volume = {15530}, year = {2025}, } @inproceedings{20688, abstract = {We consider two-player zero-sum concurrent stochastic games (CSGs) played on graphs with reachability and safety objectives. These include degenerate classes such as Markov decision processes or turn-based stochastic games, which can be solved by linear or quadratic programming; however, in practice, value iteration (VI) outperforms the other approaches and is the most implemented method. Similarly, for CSGs, this practical performance makes VI an attractive alternative to the standard theoretical solution via the existential theory of reals.VI starts with an under-approximation of the sought values for each state and iteratively updates them, traditionally terminating once two consecutive approximations are ϵ-close. However, this stopping criterion lacks guarantees on the precision of the approximation, which is the goal of this work. We provide bounded (a.k.a. interval) VI for CSGs: it complements standard VI with a converging sequence of over-approximations and terminates once the over- and under-approximations are ϵ-close.}, author = {Grobelna, Marta and Kretinsky, Jan and Weininger, Maximilian}, booktitle = {2025 40th Annual ACM/IEEE Symposium on Logic in Computer Science}, location = {Singapore, Singapore}, pages = {568--580}, publisher = {IEEE}, title = {{Stopping criteria for value iteration on concurrent stochastic reachability and safety games}}, doi = {10.1109/lics65433.2025.00049}, year = {2025}, } @inproceedings{18600, 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 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.}, author = {Andriushchenko, Roman and Bork, Alexander and Budde, Carlos E. and Češka, Milan and Grover, Kush and Hahn, Ernst Moritz and Hartmanns, Arnd and Israelsen, Bryant and Jansen, Nils and Jeppson, Joshua and Junges, Sebastian and Köhl, Maximilian A. and Könighofer, Bettina and Kretinsky, Jan and Meggendorfer, Tobias and Parker, David and Pranger, Stefan and Quatmann, Tim and Ruijters, Enno and Taylor, Landon and Volk, Matthias and Weininger, Maximilian and Zhang, Zhen}, booktitle = {TOOLympics Challenge 2023}, isbn = {9783031676949}, issn = {1611-3349}, pages = {90--146}, publisher = {Springer Nature}, title = {{Tools at the Frontiers of Quantitative Verification: QComp 2023 Competition Report}}, doi = {10.1007/978-3-031-67695-6_4}, volume = {14550}, year = {2024}, } @inproceedings{14259, abstract = {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 applications. Not only can the guessed strategy be applied as best-effort in cases where the game’s huge size prohibits rigorous approaches, but it can also increase the scalability of rigorous LTL synthesis in several ways. Firstly, checking whether a guessed strategy is winning is easier than constructing one. Secondly, even if the guess is wrong in some places, it can be fixed by strategy iteration faster than constructing one from scratch. Thirdly, the guess can be used in on-the-fly approaches to prioritize exploration in the most fruitful directions. In contrast to previous works, we (i) reflect the highly structured logical information in game’s states, the so-called semantic labelling, coming from the recent LTL-to-automata translations, and (ii) learn to reflect it properly by learning from previously solved games, bringing the solving process closer to human-like reasoning.}, author = {Kretinsky, Jan and Meggendorfer, Tobias and Prokop, Maximilian and Rieder, Sabine}, booktitle = {35th International Conference on Computer Aided Verification}, isbn = {9783031377051}, issn = {1611-3349}, location = {Paris, France}, pages = {390--414}, publisher = {Springer Nature}, title = {{Guessing winning policies in LTL synthesis by semantic learning}}, doi = {10.1007/978-3-031-37706-8_20}, volume = {13964}, year = {2023}, } @inproceedings{13967, 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 arbitrarily wrong results. Over the past decade, different works derived stopping 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 stopping 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.}, author = {Kretinsky, Jan and Meggendorfer, Tobias and Weininger, Maximilian}, booktitle = {38th Annual ACM/IEEE Symposium on Logic in Computer Science}, isbn = {9798350335873}, issn = {1043-6871}, location = {Boston, MA, United States}, publisher = {IEEE}, title = {{Stopping criteria for value iteration on stochastic games with quantitative objectives}}, doi = {10.1109/LICS56636.2023.10175771}, volume = {2023}, year = {2023}, } @article{10602, abstract = {Transforming ω-automata into parity automata is traditionally done using appearance records. We present an efficient variant of this idea, tailored to Rabin automata, and several optimizations applicable to all appearance records. We compare the methods experimentally and show that our method produces significantly smaller automata than previous approaches.}, author = {Kretinsky, Jan and Meggendorfer, Tobias and Waldmann, Clara and Weininger, Maximilian}, issn = {1432-0525}, journal = {Acta Informatica}, keywords = {computer networks and communications, information systems, software}, pages = {585--618}, publisher = {Springer Nature}, title = {{Index appearance record with preorders}}, doi = {10.1007/s00236-021-00412-y}, volume = {59}, year = {2022}, } @inproceedings{12775, 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 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.}, author = {Grover, Kush and Kretinsky, Jan and Meggendorfer, Tobias and Weininger, Maimilian}, booktitle = {33rd International Conference on Concurrency Theory}, issn = {1868-8969}, location = {Warsaw, Poland}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik}, title = {{Anytime guarantees for reachability in uncountable Markov decision processes}}, doi = {10.4230/LIPIcs.CONCUR.2022.11}, volume = {243}, year = {2022}, } @inproceedings{297, abstract = {Graph games played by two players over finite-state graphs are central in many problems in computer science. In particular, graph games with ω -regular winning conditions, specified as parity objectives, which can express properties such as safety, liveness, fairness, are the basic framework for verification and synthesis of reactive systems. The decisions for a player at various states of the graph game are represented as strategies. While the algorithmic problem for solving graph games with parity objectives has been widely studied, the most prominent data-structure for strategy representation in graph games has been binary decision diagrams (BDDs). However, due to the bit-level representation, BDDs do not retain the inherent flavor of the decisions of strategies, and are notoriously hard to minimize to obtain succinct representation. In this work we propose decision trees for strategy representation in graph games. Decision trees retain the flavor of decisions of strategies and allow entropy-based minimization to obtain succinct trees. However, decision trees work in settings (e.g., probabilistic models) where errors are allowed, and overfitting of data is typically avoided. In contrast, for strategies in graph games no error is allowed, and the decision tree must represent the entire strategy. We develop new techniques to extend decision trees to overcome the above obstacles, while retaining the entropy-based techniques to obtain succinct trees. We have implemented our techniques to extend the existing decision tree solvers. We present experimental results for problems in reactive synthesis to show that decision trees provide a much more efficient data-structure for strategy representation as compared to BDDs.}, author = {Brázdil, Tomáš and Chatterjee, Krishnendu and Kretinsky, Jan and Toman, Viktor}, location = {Thessaloniki, Greece}, pages = {385 -- 407}, publisher = {Springer}, title = {{Strategy representation by decision trees in reactive synthesis}}, doi = {10.1007/978-3-319-89960-2_21}, volume = {10805}, year = {2018}, } @inproceedings{13160, 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. 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.}, author = {Kretinsky, Jan and Meggendorfer, Tobias and Waldmann, Clara and Weininger, Maximilian}, booktitle = {Tools and Algorithms for the Construction and Analysis of Systems}, isbn = {9783662545768}, issn = {1611-3349}, location = {Uppsala, Sweden}, pages = {443--460}, publisher = {Springer}, title = {{Index appearance record for transforming Rabin automata into parity automata}}, doi = {10.1007/978-3-662-54577-5_26}, volume = {10205}, year = {2017}, } @article{1407, abstract = {We consider the problem of computing the set of initial states of a dynamical system such that there exists a control strategy to ensure that the trajectories satisfy a temporal logic specification with probability 1 (almost-surely). We focus on discrete-time, stochastic linear dynamics and specifications given as formulas of the Generalized Reactivity(1) fragment of Linear Temporal Logic over linear predicates in the states of the system. We propose a solution based on iterative abstraction-refinement, and turn-based 2-player probabilistic games. While the theoretical guarantee of our algorithm after any finite number of iterations is only a partial solution, we show that if our algorithm terminates, then the result is the set of all satisfying initial states. Moreover, for any (partial) solution our algorithm synthesizes witness control strategies to ensure almost-sure satisfaction of the temporal logic specification. While the proposed algorithm guarantees progress and soundness in every iteration, it is computationally demanding. We offer an alternative, more efficient solution for the reachability properties that decomposes the problem into a series of smaller problems of the same type. All algorithms are demonstrated on an illustrative case study.}, author = {Svoreňová, Mária and Kretinsky, Jan and Chmelik, Martin and Chatterjee, Krishnendu and Cěrná, Ivana and Belta, Cǎlin}, journal = {Nonlinear Analysis: Hybrid Systems}, number = {2}, pages = {230 -- 253}, publisher = {Elsevier}, title = {{Temporal logic control for stochastic linear systems using abstraction refinement of probabilistic games}}, doi = {10.1016/j.nahs.2016.04.006}, volume = {23}, year = {2017}, } @article{471, abstract = {We present a new algorithm for the statistical model checking of Markov chains with respect to unbounded temporal properties, including full linear temporal logic. The main idea is that we monitor each simulation run on the fly, in order to detect quickly if a bottom strongly connected component is entered with high probability, in which case the simulation run can be terminated early. As a result, our simulation runs are often much shorter than required by termination bounds that are computed a priori for a desired level of confidence on a large state space. In comparison to previous algorithms for statistical model checking our method is not only faster in many cases but also requires less information about the system, namely, only the minimum transition probability that occurs in the Markov chain. In addition, our method can be generalised to unbounded quantitative properties such as mean-payoff bounds. }, author = {Daca, Przemyslaw and Henzinger, Thomas A and Kretinsky, Jan and Petrov, Tatjana}, issn = {1529-3785}, journal = {ACM Transactions on Computational Logic}, number = {2}, publisher = {ACM}, title = {{Faster statistical model checking for unbounded temporal properties}}, doi = {10.1145/3060139}, volume = {18}, year = {2017}, } @inproceedings{645, abstract = {Markov decision processes (MDPs) are standard models for probabilistic systems with non-deterministic behaviours. Long-run average rewards provide a mathematically elegant formalism for expressing long term performance. Value iteration (VI) is one of the simplest and most efficient algorithmic approaches to MDPs with other properties, such as reachability objectives. Unfortunately, a naive extension of VI does not work for MDPs with long-run average rewards, as there is no known stopping criterion. In this work our contributions are threefold. (1) We refute a conjecture related to stopping criteria for MDPs with long-run average rewards. (2) We present two practical algorithms for MDPs with long-run average rewards based on VI. First, we show that a combination of applying VI locally for each maximal end-component (MEC) and VI for reachability objectives can provide approximation guarantees. Second, extending the above approach with a simulation-guided on-demand variant of VI, we present an anytime algorithm that is able to deal with very large models. (3) Finally, we present experimental results showing that our methods significantly outperform the standard approaches on several benchmarks.}, author = {Ashok, Pranav and Chatterjee, Krishnendu and Daca, Przemyslaw and Kretinsky, Jan and Meggendorfer, Tobias}, editor = {Majumdar, Rupak and Kunčak, Viktor}, isbn = {978-331963386-2}, location = {Heidelberg, Germany}, pages = {201 -- 221}, publisher = {Springer}, title = {{Value iteration for long run average reward in markov decision processes}}, doi = {10.1007/978-3-319-63387-9_10}, volume = {10426}, year = {2017}, } @article{466, abstract = {We consider Markov decision processes (MDPs) with multiple limit-average (or mean-payoff) objectives. There exist two different views: (i) the expectation semantics, where the goal is to optimize the expected mean-payoff objective, and (ii) the satisfaction semantics, where the goal is to maximize the probability of runs such that the mean-payoff value stays above a given vector. We consider optimization with respect to both objectives at once, thus unifying the existing semantics. Precisely, the goal is to optimize the expectation while ensuring the satisfaction constraint. Our problem captures the notion of optimization with respect to strategies that are risk-averse (i.e., ensure certain probabilistic guarantee). Our main results are as follows: First, we present algorithms for the decision problems which are always polynomial in the size of the MDP. We also show that an approximation of the Pareto-curve can be computed in time polynomial in the size of the MDP, and the approximation factor, but exponential in the number of dimensions. Second, we present a complete characterization of the strategy complexity (in terms of memory bounds and randomization) required to solve our problem. }, author = {Chatterjee, Krishnendu and Křetínská, Zuzana and Kretinsky, Jan}, issn = {1860-5974}, journal = {Logical Methods in Computer Science}, number = {2}, publisher = {International Federation for Computational Logic}, title = {{Unifying two views on multiple mean-payoff objectives in Markov decision processes}}, doi = {10.23638/LMCS-13(2:15)2017}, volume = {13}, year = {2017}, } @inproceedings{1093, abstract = {We introduce a general class of distances (metrics) between Markov chains, which are based on linear behaviour. This class encompasses distances given topologically (such as the total variation distance or trace distance) as well as by temporal logics or automata. We investigate which of the distances can be approximated by observing the systems, i.e. by black-box testing or simulation, and we provide both negative and positive results. }, author = {Daca, Przemyslaw and Henzinger, Thomas A and Kretinsky, Jan and Petrov, Tatjana}, location = {Quebec City; Canada}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik}, title = {{Linear distances between Markov chains}}, doi = {10.4230/LIPIcs.CONCUR.2016.20}, volume = {59}, year = {2016}, } @inproceedings{1234, abstract = {We present a new algorithm for the statistical model checking of Markov chains with respect to unbounded temporal properties, including full linear temporal logic. The main idea is that we monitor each simulation run on the fly, in order to detect quickly if a bottom strongly connected component is entered with high probability, in which case the simulation run can be terminated early. As a result, our simulation runs are often much shorter than required by termination bounds that are computed a priori for a desired level of confidence on a large state space. In comparison to previous algorithms for statistical model checking our method is not only faster in many cases but also requires less information about the system, namely, only the minimum transition probability that occurs in the Markov chain. In addition, our method can be generalised to unbounded quantitative properties such as mean-payoff bounds.}, author = {Daca, Przemyslaw and Henzinger, Thomas A and Kretinsky, Jan and Petrov, Tatjana}, location = {Eindhoven, The Netherlands}, pages = {112 -- 129}, publisher = {Springer}, title = {{Faster statistical model checking for unbounded temporal properties}}, doi = {10.1007/978-3-662-49674-9_7}, volume = {9636}, year = {2016}, } @inproceedings{1499, abstract = {We consider weighted automata with both positive and negative integer weights on edges and study the problem of synchronization using adaptive strategies that may only observe whether the current weight-level is negative or nonnegative. We show that the synchronization problem is decidable in polynomial time for deterministic weighted automata.}, author = {Kretinsky, Jan and Larsen, Kim and Laursen, Simon and Srba, Jiří}, location = {Madrid, Spain}, pages = {142 -- 154}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik}, title = {{Polynomial time decidability of weighted synchronization under partial observability}}, doi = {10.4230/LIPIcs.CONCUR.2015.142}, volume = {42}, year = {2015}, } @inproceedings{1502, abstract = {We extend the theory of input-output conformance with operators for merge and quotient. The former is useful when testing against multiple requirements or views. The latter can be used to generate tests for patches of an already tested system. Both operators can combine systems with different action alphabets, which is usually the case when constructing complex systems and specifications from parts, for instance different views as well as newly defined functionality of a~previous version of the system.}, author = {Beneš, Nikola and Daca, Przemyslaw and Henzinger, Thomas A and Kretinsky, Jan and Nickovic, Dejan}, isbn = {978-1-4503-3471-6}, location = {Montreal, QC, Canada}, pages = {101 -- 110}, publisher = {ACM}, title = {{Complete composition operators for IOCO-testing theory}}, doi = {10.1145/2737166.2737175}, year = {2015}, } @inproceedings{1594, abstract = {Quantitative extensions of temporal logics have recently attracted significant attention. In this work, we study frequency LTL (fLTL), an extension of LTL which allows to speak about frequencies of events along an execution. Such an extension is particularly useful for probabilistic systems that often cannot fulfil strict qualitative guarantees on the behaviour. It has been recently shown that controller synthesis for Markov decision processes and fLTL is decidable when all the bounds on frequencies are 1. As a step towards a complete quantitative solution, we show that the problem is decidable for the fragment fLTL\GU, where U does not occur in the scope of G (but still F can). Our solution is based on a novel translation of such quantitative formulae into equivalent deterministic automata.}, author = {Forejt, Vojtěch and Krčál, Jan and Kretinsky, Jan}, location = {Suva, Fiji}, pages = {162 -- 177}, publisher = {Springer}, title = {{Controller synthesis for MDPs and frequency LTL\GU}}, doi = {10.1007/978-3-662-48899-7_12}, volume = {9450}, year = {2015}, } @inproceedings{1601, abstract = {We propose a flexible exchange format for ω-automata, as typically used in formal verification, and implement support for it in a range of established tools. Our aim is to simplify the interaction of tools, helping the research community to build upon other people’s work. A key feature of the format is the use of very generic acceptance conditions, specified by Boolean combinations of acceptance primitives, rather than being limited to common cases such as Büchi, Streett, or Rabin. Such flexibility in the choice of acceptance conditions can be exploited in applications, for example in probabilistic model checking, and furthermore encourages the development of acceptance-agnostic tools for automata manipulations. The format allows acceptance conditions that are either state-based or transition-based, and also supports alternating automata.}, author = {Babiak, Tomáš and Blahoudek, František and Duret Lutz, Alexandre and Klein, Joachim and Kretinsky, Jan and Mueller, Daniel and Parker, David and Strejček, Jan}, location = {San Francisco, CA, United States}, pages = {479 -- 486}, publisher = {Springer}, title = {{The Hanoi omega-automata format}}, doi = {10.1007/978-3-319-21690-4_31}, volume = {9206}, year = {2015}, }