Probabilistic Computation Tree Logic (PCTL) is frequently used to formally specify control objectives such as reachability and safety on probabilistic systems [1]. To check the correctness of PCTL specifications on these systems, model checking methods are required [2]. Although model checking PCTL by model-based analysis is theoretically possible [1], it is not preferable in practice when the system model is unknown or large. In these cases, model checking by sampling, i.e. statistical model checking (SMC), is needed [3], [4].
The statistical model checking of PCTL specifications on Markov Decision Processes (MDPs) is frequently encountered in many decision problems – e.g., for a robot in a grid world under probabilistic disturbance, checking whether there exists a feasible control policy such that the probability of reaching certain goal states is greater than a probability threshold [5]–[7]. In these problems, the main challenge is to search for such a feasible policy for the PCTL specification of interest.
To search for feasible policies for temporal logics speci-fications, such as PCTL, on MDPs, one approach is model-based reinforcement learning [8]–[11] – i.e., first inferring the transition probabilities of the MDP by sampling over each state-action pair, and then searching for the feasible policy via model-based analysis. This approach is often inefficient, since not all transition probabilities are relevant to the PCTL
Nima Roohi is with the University of California San Diego, USA nroohi@ucsd.edu. Matthew West, Mahesh Viswanathan, and Geir E. Dullerud are with the University of Illinois at Urbana-Champaign, USA
specification of interest. Here instead, we adopt a model-free reinforcement learning approach [12].
Common model-free reinforcement learning techniques cannot directly handle temporal logic specifications. One solution is to find a surrogate reward function such that the policy learned for this surrogate reward function is the one needed for checking the temporal logic specification of interest. For certain temporal logics interpreted under special semantics (usually involving a metric), the surrogate reward can be found based on that semantics [13]–[15].
For temporal logics under the standard semantics [16], the surrogate reward functions can be derived via constructing the product MDP [7], [17], [18] of the initial MDP and the automaton realizing the temporal logic specification. However, the complexity of constructing the automaton from a general linear temporal logic (LTL) specification is double exponential [16], [19]. For a fraction of LTL, namely LTL/GU, the complexity is exponential [20], [21]. In addition, the size of the product MDP is usually much larger than the initial MDP, although the produce MDP may be constructed on-the-fly to reduce the extra computation cost, as it did in [18].
In this work, we propose a new statistical model checking method for PCTL specifications on MDPs. For a lucid discussion, we only consider non-nested PCTL specifications. PCTL formulas in general form with nested probabilistic operators can be handled in the standard manner using the approach proposed in [22], [23]. Our method uses upper-confidence-bound (UCB) based Q-learning to directly learn the feasible policy of PCTL specifications, without constructing the product MDP. The effectiveness of UCB-based Qlearning has been proven for the K-bandit problem, and has been numerically demonstrated on many decision-learning problems on MDPs (see [24]).
For bounded-time PCTL specifications, we treat the statistical model checking problem as a finite sequence of K-bandit problems and use the UCB-based Q-learning to learn the desirable decision at each time step. For unbounded-time PCTL specifications, we look for a truncation time to reduce it to a bounded-time problem by checking the PCTL specification and its negation at the same time. Our statistical model checking algorithm is online; it terminates with probability 1, and only when the statistical error of the learning result is smaller than a user-specified value.
The rest of the paper is organized as follows. The preliminaries on labeled MDPs and PCTL are given in Section II. In Section III, using the principle of optimism in the face of uncertainty, we design Q-learning algorithms to solve finite-time and infinite-time probabilistic satisfaction, and give finite sample probabilistic guarantees for the correctness of the algorithms. We implement and evaluate the proposed algorithms on several case studies in Section IV. Finally, we conclude this work in Section V.
The set of integers and real numbers are denoted by N and R, respectively. For , let [n] = {1, . . ., n}. The cardinality of a set is denoted by
. The set of finite-length sequences taken from a finite set S is denoted by
.
A. Markov Decision Process
A Markov decision process (MDP) is a finite-state probabilistic system, where the transition probabilities between the states are determined by the control action taken from a given finite set. Each state of the MDP is labeled by a set of atomic propositions indicating the properties holding on it, e.g., whether the state is a safe/goal state.
Definition 1: A labeled Markov decision process (MDP) is a tuple M = (S, A, T, AP, L) where
• S is a finite set of states.
• A is a finite set of actions. • is a partial transition probability function. For any state
and any action
,
With a slight abuse of notation, let A(s) be the set of allowed actions on the state s.
• AP is a finite set of labels.
• is a labeling function.
Definition 2: A policy decides the action to take from the sequence of states visited so far. Given a policy
and an initial state
, the MDP M becomes purely probabilistic, denoted by
. The system
is not necessarily Markovian.
B. Probabilistic Computation Tree Logic
The probabilistic computation tree logic (PCTL) is defined inductively from atomic propositions, temporal operators and probability operators. It reasons about the probabilities of time-dependent properties.
Definition 3 (Syntax): Let AP be a set of atomic propositions. A PCTL state formula is defined by
where is a (possibly infinite) time horizon, and
is a threshold.1 The operators
and
are called probability operators, and the “next”, “until” and “release” operators
are called temporal operators.
More temporal operators can be derived by composition: for example, “or” is ; “true” is
; “finally” is
; and “always” is
. For simplicity, we write
and
as U, R, F and G, respectively.
Definition 4 (Semantics): For an MDP M = (S, A, T, , the satisfaction relation |= is defined by for a state s or path
by
where . And
means the path
is drawn from the MDP M under the policy
, starting from the state s from.
The PCTL formulas (or
) mean that the maximal (or minimal) satisfaction probability of “next”
is
. The PCTL formulas
(or
) mean that the maximal (or mini- mal) satisfaction probability that
holds “until”
holds is
.
In this section, we consider the statistical model check- ing of non-nested PCTL specifications using an upper-confidence-bound based Q-learning. For simplicity, we focus on and
where
and
are atomic propositions. Other cases can be handled in the same way. We discuss the case of T = 1 in Section III-A, the case of T > 1 in Section III-B, and the case of
in Section III-C. Similar to other works on statistical model checking [3], [4], we make the following assumption.
Assumption 1: For and
with
and
, we assume that
and
, respectively.
When it holds, as the number of samples increases, the samples will be increasingly concentrated on one side of the threshold p by the Central Limit Theorem. Therefore, a statistical analysis based on the majority of the samples has increasing accuracy. When it is violated, the samples would be evenly distributed between the two sides of the boundary p, regardless of the sample size. Thus, no matter how the sample size increases, the accuracy of any statistical test would not increase. Compared to statistical model checking algorithms based on sequential probability ratio tests (SPRT) [25], [26], no assumption on the indifference region is required here. Finally, by Assumption 1, we have the additional semantic equivalence between the PCTL speci-fications: and
; thus, we will not distinguish between them below.
For further discussion, we first identify a few trivial cases. For , let
Then for any policy if
; and
if
. The same holds for
by defining
to be the union of end components of the MDP M labeled by
(this only requires knowing the topology of M) [16]. In the rest of this section, we focus on handling the nontrivial case
.
A. Single Time Horizon
When T = 1, for any , the PCTL specification
(or
) holds on a random path
starting from the state s if and only if
, where
and
are from (1). Thus, it suffices to learn from samples whether
where
and means
is drawn from the transition probability
for state s and action a. This is an |A(s)|-arm bandit problem; we solve this problem by upper-confidence-bound strategies [27], [28].
Specifically, for the iteration k, let be the number samples for the one-step path
, and with a slight abuse of notation, let
The unknown transition probability function is estimated by the empirical transition probability function
And the estimation of from the existing k samples is
Since the value of the Q-function is bounded, we can construct a confidence interval for the estimate
with statistical error at most
using Hoeffding’s inequality by
where we set the value of the division to be for
.
Remark 1: We use Hoeffding’s bounds to yield hard guarantees on the statistical error of the model checking algorithms. Tighter bounds like Bernstein’s bounds [29] can also be used, but they only yield asymptotic guarantees on the statistical error.
The sample efficiency for learning for the bandit problem (2) depends on the choice of sampling policy, decided from the existing samples. A provably best solution is to use the Q-learning from [27], [28]. Specifically, an upper confidence bound (UCB) is constructed for each state-action pair using the number of samples and the observed reward, and the best action is chosen with the highest possible reward, namely the UCB. The sampling policy is chosen by maximizing the possible reward greedily:
The action is chosen arbitrarily when there are multiple candidates. The choice of in (7) ensures that the policy giving the upper bound of the value function gets most frequently sampled in the long run.
To initialize the iteration, the Q-function is set to
to ensure that every state-action is sampled at least once. The
where p is the probability threshold in the non-nested PCTL formula. Remark 2: For or
, it suffices to change the termination condition (9) by returning true if
, and returning false if
. The same statements hold for general PCTL specifications, as discussed in Sections III-B and III-C Now, we summarize the above discussion by Algorithm 1 and Theorem 1 below. Theorem 1: The return value of Algorithm 1 is correct with probability at least
. Proof: We provide the proof of a more general state- ment in Theorem 2.
Require: MDP M, parameter .
4: Sample from M, and update the transition probability function by (3)(4).
5: Update the bounds on the Q-function and the policies by (6)(7).
Remark 3: The Hoeffding bounds in (6) are conservative. Consequently, as shown in the simulations in Section IV, the actual statistical error of the our algorithms can be smaller than the given value. However, as the MDP is unknown, finding tighter bounds is challenging. One possible solution is to use asymptotic bounds, such as Bernstein’s bounds [29]. Accordingly, the algorithm will only give asymptotic probabilistic guarantees.
B. Finite Time Horizon
When , for any
, let
i.e., and
are the maximal satisfaction probability of
for a random path starting from s for any policy and any policy with first action being a, respectively. By definition,
and
satisfy the Bellman equation
The second equality of the second equation is derived from
by the semantics of PCTL.
From (11), we check by induction on the time horizon T . For
, the lower and upper bounds for
can be derived using the bounds on the value function for the previous step — for h = 1 from (6) and for
h > 0 by the following lemma.
and
where is a parameter such that
with probability at least
. The bounds in (12) are derived from (11) by applying Hoeffding’s inequality, using the fact that
and the Q-functions are bounded within [0, 1].
From the boundedness of , we note that this confidence interval encompasses the statistical error in both the estimated transition probability function
and the bounds
and
of the value function. Accordingly, the policy
chosen by the OFU principle at the h step is
with an optimal action chosen arbitrarily when there are multiple candidates, to ensure that the policy giving the upper bound of the value function is sampled the most in the long run. To initialize the iteration, the Q-function is set to
for all , to ensure that every state-action is sampled at least once.
Sampling by the updated policy can be performed in either episodic or non-episodic ways [24]. The only requirement is that the state-action pair
should be performed frequently for each
and for each state s satisfying
. In addition, batch samples may be drawn, namely sampling over the state-action pairs multiple times before updating the policy. In this work, for simplicity, we use a non-episodic, non-batch sampling method, by drawing
for all and state s such that
. The Q-function and the value function are set and initialized
Require: MDP M, parameters for
.
1: Initialize the Q-function and the policy by (15)(14). 2: Obtain and
by (1).
4: Sample by (16), and update the transition probability function by (3)(4).
5: Update the bounds by (12)(13) and the policy by (14).
by (13) and (15). The termination condition is give by
where p is the probability threshold in the non-nested PCTL formula. The above discussion is summarized by Algorithm 2 and Theorem 2. Theorem 2: Algorithm 2 terminates with probability 1 and its return value is correct with probability at least , where
. Proof: By construction, as the number of iterations
. Thus, by Assumption 1, the termination condition (17) will be satisfied with probability 1. Now, let E be the event that the return value of Algorithm 2 is correct, and let
be the event that Algorithm 2 terminates at the iteration k, then we have
. For any k, the event E happens given that
holds, if the Hoeffding confidence intervals given by (12) hold for any actions
, and state s with
. Thus, we have
, where N =
, implying that the return value of Algorithm 2 is correct with probability
. By Theorem 2, the desired overall statistical error splits into the statistical errors for each state-action pair through the time horizon. For implementation, we can split it equally by
. The specification
can be handled by replacing argmax with argmin in (14), and max with min in (13). The termination condition is the same as (17). Remark 4: Due to the semantics in Definition 4, running Algorithm 2 proving
or disproving
is easier than disproving
or proving
; and the difference increases with the number of actions |A| and the time horizon T . This is because proving
or disproving
requires only finding and evaluating some policy
with
, while disproving it requires evaluating all possible policies with sufficient accuracy. This is illustrated by the simulation results presented in Section IV.
C. Infinite Time Horizon
Infinite-step satisfaction probability can be estimated from finite-step satisfaction probabilities, using the monotone convergence of the value function in the time step H,
where p is the probability threshold in the non-nested PCTL formula.
The general idea in using the monotonicity to check infinite horizon satisfaction probability in finite time is that if we check both and its negation
at the same time, one of them should terminate in finite time. Here
and
are treated as atomic propositions. We can use Algorithm 2 to check their satisfaction probabilities for any time horizon T simultaneously. The termination in finite time is guaranteed, if the time horizon for both computations increase with the iterations. The simplest choice is to increase H by 1 for every K iterations; however, this brings the problem of tuning K. Here, we use the convergence of the best policy as the criterion for increasing H for each satisfaction computation. Specifically, for all the steps h in each iteration, in addition to finding the optimal policy
with respect to the upper confidence bounds of the Q-functions
by (14), we also consider the the optimal policy with respect to the lower confidence bounds of the Q-functions
. Obviously, when
argmax
, we know that the policy
is optimal for all possible Q-functions within
. This implies that these bounds are fine enough for estimating
; thus, if the algorithm does not terminate by the condition (19), we let
stops and the largest time horizon is H, then the return value is correct with probability at least . Thus, the theorem holds.
Remark 5: By Theorem 3, given the desired overall con-fidence level , we can split it geometrically by
, where
.
Remark 6: Similar to Section III-B, checking for
is derived by replacing argmax with argmin in (14), and max with min in (13). The termination condition is the same as (19).
Remark 7: Finally, we note that the exact savings of sample costs for Algorithms 2 and 3 depend on the structure of the MDP. Specifically, the proposed method is more efficient than [9], [10], [30], when the satisfaction probabilities differ significantly among actions, as it can quickly detect suboptimal actions without over-sampling on them. On the other hand, if all the state-action pairs yield the same Q-value, then an equal number of samples will be spent on each of them — in this case, the sample cost of Algorithms 2 and 3 is the same as [9], [10], [30].
To evaluate the performance of the proposed algorithms, we ran them on two different sets of examples. In all the simulations, the transition probabilities are unknown to the algorithm (this is different from [9]).
The first set contains 10 randomly generated MDPs with different sizes. For these MDPs, we considered the formula for the finite horizon, and
for the infinite horizon. In both cases,
, and H are chosen arbitrarily. The second set contains 9 versions of the Sum of Two Dice program. The standard version [31] models the sum of two fair dice, each with 6 different possibilities numbered 1, . . . , 6. To consider MDPs with different sizes, we consider 9 cases where each dice is still fair, but has n possibilities numbered 1, . . . , n, with n = 3 in the smallest example, and n = 17 in the largest example. For these MDPs, we considered the formula
for the finite horizon, and
for the infinite horizon. In both cases
encodes the atomic predicate that is true iff values of both dice are chosen and their sum is less than an arbitrarily
CHECKING PROPOSITIONS
ARE CHOSEN ARBITRARILY. COLUMN
chosen constant. Also, in the finite case, H = 5 in the smallest example and 10 everywhere else.
For each MDP, we first numerically estimate the values of and
, for the randomly generated MDPs, and
, and
, for the variants of the two-dice examples, using the known models on PRISM [32]. Then, we use Algorithms 2 and 3 on the example models with only knowledge of the topology of the MDPs and without knowing the exact transition probabilities. For every MDP, we tested each algorithm with two different thresholds p, one smaller and the other larger than the estimated probability, to test the proposed algorithms, with
set to 5%. We ran each randomly generated test 100 times and each two-dice variant test 10 times. Here we only report average running time and average number of iterations. All tests returned the correct answers — this suggests that the Hoeffding’s bounds used in the proposed algorithms are conservative (see Remark 3). The algorithms are implemented in Scala and ran on Ubuntu 18.04 with i7-8700 CPU 3.2GHz and 16GB memory.
Tables I and II show the results for finite horizon reachability. An interesting observation in these tables is that in all examples, disproving the formula is 3 to 100 times faster. We believe this is mainly because, to disprove , all we need is one policy
for which
holds. However, to prove
, one needs to show that every policy
satisfies
(see Remark 4).
Tables III and IV show the results for infinite horizon reachability. Note that Algorithm 3 considers both the formula and its negation, and contrary to the finite horizon reachability, disproving a formula is not always faster for the infinite case. In most of the larger examples that are randomly generated, and
are very small on average. This shows that in these examples, the algorithm was smart enough to learn there is no need to increase H in order to
CHECKING ON VARIANTS OF SUM-OF-TWO-DICE MDPS. ATOMIC PROPOSITION
IS TRUE IFF BOTH DICE HAVE CHOSEN THEIR
COLUMN IS THE NUMBER OF ALTERNATIVES ON EACH DICE. EACH MDP HAS TWO ACTIONS (i.e.
CHECKING ARE VALUES OF THE CORRESPONDING VARIABLES IN ALGORITHM 3 AT
solve the problem. However, this is not the case for two-dice examples. We believe this is because in the current implementation, the decision to increase H does not consider the underlying graph of the MDP. For example, during the execution, if the policy forces the state to enter a self-loop with only one enabled action, which is the case in two-dice examples, then after every iteration the value of H will be increased by 1.
We proposed a statistical model checking method for Probabilistic Computation Tree Logic on Markov decision processes using reinforcement learning. We first checked PCTL formulas with bounded time horizon, using upper-
CHECKING AND
ARE VALUES OF THE CORRESPONDING VARIABLES IN ALGORITHM 3 AT TERMINATION.
confidence-bounds based Q-learning, and then extended the technique to unbounded-time specifications by finding a proper truncation time by checking the specification of interest and its negation at the same time. Finally, we demonstrated the efficiency of our method on several case studies.
[1] C. Baier, B. Haverkort, H. Hermanns, and J. Katoen, “Model-checking algorithms for continuous-time Markov chains,” IEEE Transactions on Software Engineering, vol. 29, no. 6, pp. 524–541, 2003.
[2] Handbook of Model Checking, 2018.
[3] K. G. Larsen and A. Legay, “Statistical Model Checking: Past, Present, and Future,” in Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques, 2016, pp. 3–15.
[4] G. Agha and K. Palmskog, “A Survey of Statistical Model Checking,” ACM Trans. Model. Comput. Simul., vol. 28, no. 1, pp. 6:1–6:39, 2018.
[5] G. E. Fainekos, A. Girard, H. Kress-Gazit, and G. J. Pappas, “Temporal logic motion planning for dynamic robots,” Automatica, vol. 45, no. 2, pp. 343–352, 2009.
[6] H. Kress-Gazit, M. Lahijanian, and V. Raman, “Synthesis for Robots: Guarantees and Feedback for Robot Behavior,” Annual Review of Control, Robotics, and Autonomous Systems, vol. 1, no. 1, pp. 211– 236, 2018.
[7] A. K. Bozkurt, Y. Wang, M. Zavlanos, and M. Pajic, “Control synthesis from linear temporal logic specifications using model-free reinforcement learning,” in IEEE International Conference on Robotics and Automation (ICRA) (Submitted), 2020.
[8] D. Henriques, J. G. Martins, P. Zuliani, A. Platzer, and E. M. Clarke, “Statistical Model Checking for Markov Decision Processes,” in 2012 Ninth International Conference on Quantitative Evaluation of Systems, 2012, pp. 84–93.
[9] T. Br´azdil, K. Chatterjee, M. Chmel´ık, V. Forejt, J. Kˇret´ınsk´y, M. Kwiatkowska, D. Parker, and M. Ujma, “Verification of Markov Decision Processes Using Learning Algorithms,” in Automated Technology for Verification and Analysis, 2014, pp. 98–114.
[10] J. Fu and U. Topcu, “Probably Approximately Correct MDP Learning and Control With Temporal Logic Constraints,” arXiv:1404.7073 [cs], 2014.
[11] P. Ashok, J. Kˇret´ınsk´y, and M. Weininger, “PAC Statistical Model Checking for Markov Decision Processes and Stochastic Games,” arXiv:1905.04403 [cs], 2019.
[12] R. S. Sutton and A. G. Barto, “Reinforcement Learning: An Introduction,” p. 352, 2018.
[13] X. Li, C.-I. Vasile, and C. Belta, “Reinforcement Learning With Temporal Logic Rewards,” arXiv:1612.03471 [cs], 2016.
[14] A. Jones, D. Aksaray, Z. Kong, M. Schwager, and C. Belta, “Robust Satisfaction of Temporal Logic Specifications via Reinforcement Learning,” arXiv:1510.06460 [cs], 2015.
[15] M. L. Littman, U. Topcu, J. Fu, C. Isbell, M. Wen, and J. MacGlashan, “Environment-Independent Task Specifications via GLTL,” arXiv:1704.04341 [cs], 2017.
[16] C. Baier and J.-P. Katoen, Principles of Model Checking, 2008.
[17] E. M. Hahn, M. Perez, S. Schewe, F. Somenzi, A. Trivedi, and D. Wojtczak, “Omega-Regular Objectives in Model-Free Reinforcement Learning,” in Tools and Algorithms for the Construction and Analysis of Systems, 2019, vol. 11427, pp. 395–412.
[18] M. Hasanbeig, Y. Kantaros, A. Abate, D. Kroening, G. J. Pappas, and I. Lee, “Reinforcement learning for temporal logic control synthesis with probabilistic satisfaction guarantees,” in Proceedings of the 58th Conference on Decision and Control. IEEE, 2019, pp. 5338–5343.
[19] E. M. Hahn, G. Li, S. Schewe, A. Turrini, and L. Zhang, “Lazy Probabilistic Model Checking without Determinisation,” arXiv:1311.2928 [cs], 2013.
[20] D. Kini and M. Viswanathan, “Complexity of model checking mdps against LTL specifications,” in 37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2017, December 11-15, 2017, Kanpur, India, ser. LIPIcs, S. V. Lokam and R. Ramanujam, Eds., vol. 93. Schloss Dagstuhl - Leibniz-Zentrum f¨ur Informatik, 2017, pp. 35:1–35:13.
[21] ——, “Limit deterministic and probabilistic automata for ltlInternational Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, 2015, pp. 628–642.
[22] K. Sen, M. Viswanathan, and G. Agha, “Statistical Model Checking of Black-Box Probabilistic Systems,” in Computer Aided Verification, 2004, pp. 202–215.
[23] ——, “On Statistical Model Checking of Stochastic Systems,” in Computer Aided Verification, 2005, vol. 3576, pp. 266–280.
[24] C. Szepesv´ari, “Algorithms for Reinforcement Learning,” Synthesis Lectures on Artificial Intelligence and Machine Learning, vol. 4, no. 1, pp. 1–103, 2010.
[25] P. Zuliani, “Statistical model checking for biological applications,” International Journal on Software Tools for Technology Transfer, vol. 17, no. 4, pp. 527–536, 2015.
[26] Y. Wang, N. Roohi, M. West, M. Viswanathan, and G. E. Dullerud, “Statistical verification of PCTL using stratified samples,” in 6th IFAC Conference on Analysis and Design of Hybrid Systems (ADHS), IFACPapersOnLine, vol. 51, 2018, pp. 85–90.
[27] V. Kuleshov and D. Precup, “Algorithms for multi-armed bandit problems,” arXiv:1402.6028 [cs], 2014.
[28] S. Bubeck, “Regret Analysis of Stochastic and Nonstochastic Multiarmed Bandit Problems,” Foundations and Trends Rin Machine Learning, vol. 5, no. 1, pp. 1–122, 2012.
[29] V. Mnih, C. Szepesv´ari, and J.-Y. Audibert, “Empirical Bernstein stopping,” in Proceedings of the 25th International Conference on Machine Learning - ICML ’08, 2008, pp. 672–679.
[30] B. Balle and M. Mohri, “Learning Weighted Automata,” in Algebraic Informatics, 2015, vol. 9270, pp. 1–21.
[31] D. Knuth and A. Yao, Algorithms and Complexity: New Directions and Recent Results. Academic Press, 1976, ch. The complexity of nonuniform random number generation.
[32] M. Kwiatkowska, G. Norman, and D. Parker, “PRISM 4.0: Verification of Probabilistic Real-Time Systems,” in Computer Aided Verification, 2011, vol. 6806, pp. 585–591.