Scenario-Based Verification of Uncertain MDPs
Murat Cubuktepe
1 , Nils Jansen
2 , Sebastian Junges
3 ,
Joost-Pieter Katoen
3 , Ufuk Topcu
1
1 The University of Texas at Austin, Austin, USA
2 Radboud University Nijmegen, Nijmegen, The Netherlands
3 RWTH Aachen University, Aachen, Germany
Abstract. We consider Markov decision processes (MDPs) in which
the transition probabilities and rewards belong to an uncertainty set
parametrized by a collection of random variables. The probability distributions for these random parameters are unknown. The problem is to
compute the probability to satisfy a temporal logic specification within
any MDP that corresponds to a sample from these unknown distributions.
In general, this problem is undecidable, and we resort to techniques from
so-called scenario optimization. Based on a finite number of samples of
the uncertain parameters, each of which induces an MDP, the proposed
method estimates the probability of satisfying the specification by solving
a finite-dimensional convex optimization problem. The number of samples
required to obtain a high confidence on this estimate is independent from
the number of states and the number of random parameters. Experiments
on a large set of benchmarks show that a few thousand samples suffice to
obtain high-quality confidence bounds with a high probability.
Keywords: MDP, Uncertainty, Verification, Scenario optimisation
1 Introduction
MDPs. Markov decision processes (MDPs) model sequential decision-making
problems in stochastic dynamic environments [51]. They are widely used in
areas like planning [52], reinforcement learning [53], formal verification [48], and
robotics [24]. Mature model checking tools like PRISM [21] and Storm [35]
employ efficient algorithms to verify the correctness of MDPs against temporal
logic specifications [2] provided all transition probabilities and cost functions
are exactly known. In many applications, however, this assumption may be
unrealistic, as certain system parameters are typically not exactly known and
under control by external sources.
Supported by the grants ARL # ACC-APG-RTP W911NF, NASA #
80NSSC19K0209, NSF # 1646522, and NSF # 1652113.
c
The Author(s) 2020
A. Biere and D. Parker (Eds.): TACAS 2020, LNCS 12078, pp. 287–305, 2020.
https://doi.org/10.1007/978-3-030-45190-5 16
Murat Cubuktepe
1 , Nils Jansen
2 , Sebastian Junges
3 ,
Joost-Pieter Katoen
3 , Ufuk Topcu
1
1 The University of Texas at Austin, Austin, USA
2 Radboud University Nijmegen, Nijmegen, The Netherlands
3 RWTH Aachen University, Aachen, Germany
Abstract. We consider Markov decision processes (MDPs) in which
the transition probabilities and rewards belong to an uncertainty set
parametrized by a collection of random variables. The probability distributions for these random parameters are unknown. The problem is to
compute the probability to satisfy a temporal logic specification within
any MDP that corresponds to a sample from these unknown distributions.
In general, this problem is undecidable, and we resort to techniques from
so-called scenario optimization. Based on a finite number of samples of
the uncertain parameters, each of which induces an MDP, the proposed
method estimates the probability of satisfying the specification by solving
a finite-dimensional convex optimization problem. The number of samples
required to obtain a high confidence on this estimate is independent from
the number of states and the number of random parameters. Experiments
on a large set of benchmarks show that a few thousand samples suffice to
obtain high-quality confidence bounds with a high probability.
Keywords: MDP, Uncertainty, Verification, Scenario optimisation
1 Introduction
MDPs. Markov decision processes (MDPs) model sequential decision-making
problems in stochastic dynamic environments [51]. They are widely used in
areas like planning [52], reinforcement learning [53], formal verification [48], and
robotics [24]. Mature model checking tools like PRISM [21] and Storm [35]
employ efficient algorithms to verify the correctness of MDPs against temporal
logic specifications [2] provided all transition probabilities and cost functions
are exactly known. In many applications, however, this assumption may be
unrealistic, as certain system parameters are typically not exactly known and
under control by external sources.
Supported by the grants ARL # ACC-APG-RTP W911NF, NASA #
80NSSC19K0209, NSF # 1646522, and NSF # 1652113.
c
The Author(s) 2020
A. Biere and D. Parker (Eds.): TACAS 2020, LNCS 12078, pp. 287–305, 2020.
https://doi.org/10.1007/978-3-030-45190-5 16