59 citations · 458 across the 94 of their papers we have counts for
15 papers · 1 filter
Out of Control: Reducing Probabilistic Models by Control-State Elimination
Tobias Winkler, Johannes Lehmann, Joost-Pieter Katoen
State-of-the-art probabilistic model checkers perform verification on explicit-state Markov models defined in a high-level programming formalism like the PRISM modeling language. T…
Relatively Complete Verification of Probabilistic Programs
Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen +1
We study a syntax for specifying quantitative "assertions" - functions mapping program states to numbers - for probabilistic program verification. We prove that our syntax is expre…
Multi-objective Optimization of Long-run Average and Total Rewards
Tim Quatmann, Joost-Pieter Katoen
This paper presents an efficient procedure for multi-objective model checking of long-run average reward (aka: mean pay-off) and total reward objectives as well as their combinatio…
Automated Termination Analysis of Polynomial Probabilistic Programs
Marcel Moosbrugger, Ezio Bartocci, Joost-Pieter Katoen +1
The termination behavior of probabilistic programs depends on the outcomes of random assignments. Almost sure termination (AST) is concerned with the question whether a program ter…
The Complexity of Reachability in Parametric Markov Decision Processes
Sebastian Junges, Joost-Pieter Katoen, Guillermo A. Pérez +1
This article presents the complexity of reachability decision problems for parametric Markov decision processes (pMDPs), an extension to Markov decision processes (MDPs) where tran…
Bayesian Inference by Symbolic Model Checking
Bahare Salmani, Joost-Pieter Katoen
This paper applies probabilistic model checking techniques for discrete Markov chains to inference in Bayesian networks. We present a simple translation from Bayesian networks into…
Generating Functions for Probabilistic Programs
Lutz Klinkenberg, Kevin Batz, Benjamin Lucien Kaminski +3
This paper investigates the usage of generating functions (GFs) encoding measures over the program variables for reasoning about discrete probabilistic programs. To that end, we de…
Verification of indefinite-horizon POMDPs
Alexander Bork, Sebastian Junges, Joost-Pieter Katoen +1
The verification problem in MDPs asks whether, for any policy resolving the nondeterminism, the probability that something bad happens is bounded by some given threshold. This veri…
Weakest Preexpectation Semantics for Bayesian Inference
Marcin Szymczak, Joost-Pieter Katoen
We present a semantics of a probabilistic while-language with soft conditioning and continuous distributions which handles programs diverging with positive probability. To this end…
PrIC3: Property Directed Reachability for MDPs
Kevin Batz, Sebastian Junges, Benjamin Lucien Kaminski +3
IC3 has been a leap forward in symbolic model checking. This paper proposes PrIC3 (pronounced pricy-three), a conservative extension of IC3 to symbolic model checking of MDPs. Our…
Stochastic Games with Lexicographic Reachability-Safety Objectives
Krishnendu Chatterjee, Joost-Pieter Katoen, Maximilian Weininger +1
We study turn-based stochastic zero-sum games with lexicographic preferences over reachability and safety objectives. Stochastic games are standard models in control, verification,…
Various Ways to Quantify BDMPs
Marc Bouissou, Shahid Khan, Joost-Pieter Katoen +1
A Boolean logic driven Markov process (BDMP) is a dependability analysis model that defines a continuous-time Markov chain (CTMC). This formalism has high expressive power, yet it…
Benchmarking Software Model Checkers on Automotive Code
Lukas Westhofen, Philipp Berger, Joost-Pieter Katoen
This paper reports on our experiences with verifying automotive C code by state-of-the-art open source software model checkers. The embedded C code is automatically generated from…
The Probabilistic Model Checker Storm
Christian Hensel, Sebastian Junges, Joost-Pieter Katoen +2
We present the probabilistic model checker Storm. Storm supports the analysis of discrete- and continuous-time variants of both Markov chains and Markov decision processes. Storm h…
Generative Datalog with Continuous Distributions
Martin Grohe, Benjamin Lucien Kaminski, Joost-Pieter Katoen +1
Arguing for the need to combine declarative and probabilistic programming, Bárány et al. (TODS 2017) recently introduced a probabilistic extension of Datalog as a "purely declarati…