Budapest University of Technology and Economics
11email: {szekeres, marussy, majzik}@mit.bme.hu
A Lazy Abstraction Algorithm for Markov Decision Processes
Abstract
Analysis of Markov Decision Processes (MDP) is often hindered by state space explosion. Abstraction is a well-established technique in model checking to mitigate this issue. This paper presents a novel lazy abstraction method for MDP analysis based on adaptive simulation graphs. Refinement is performed only when new parts of the state space are explored, which makes partial exploration techniques like Bounded Real-Time Dynamic Programming (BRTDP) retain more merged states. Therefore, we propose a combination of lazy abstraction and BRTDP. To evaluate the performance of our algorithm, we conduct initial experiments using the Quantitative Verification Benchmark Set.
Keywords:
Lazy abstraction Markov Decision Processes Abstraction refinement Probabilistic model checkingreptheorem[1]
Theorem 0.1
1 Introduction
Ensuring the reliable operation of safety-critical systems, like railway interlocking systems and embedded controllers, is vital. Probabilistic model checking addresses this by offering an automated approach with formal mathematical guarantees for the analysis of quantitative properties, like reliability and availability [20]. We focus on a fundamental task in probabilistic model checking: computing the worst-case probability of reaching an error state.
Markov Decision Processes (MDPs) are discrete-time models able to describe both probabilistic and non-deterministic behavior, used in reliability and safety analysis for worst-case modeling of unknown factors. The analysis of other modeling formalisms, like Markov Automata or Probabilistic Timed Automata, can often be reduced to MDP analysis as well.
State space explosion presents an obstacle for MDP model checking: as the number of components or variables increases, the state space may grow exponentially. Consequently, practical implementations face problems in representing the system in memory and the numerical solution methods also become intractable.
Abstraction aims to counteract this. Several abstraction-based techniques have been adapted to probabilistic systems, like CEGAR [17, 15] and abstract interpretation [7]. Partial state space exploration, like Bounded Real-Time Dynamic Programming (BRTDP) [3, 18] is another approach for counteracting it. As most existing MDP abstraction methods rely on computing the whole abstract model to choose a refinement, they do not lend themselves well to combination with partial state space exploration techniques.
Lazy abstraction [13, 23] in contrast merges state-space exploration and refinement, making it a good candidate for this combination. However, no such method has been proposed for MDPs to our knowledge.
We adapt an existing lazy abstraction algorithm [27] to MDPs (Section 3). We combine it with BRTDP, benefiting from the synergy of lazy abstraction and partial state space exploration and enabling a trade-off between time and accuracy (Subsection 3.1). We evaluate the performance of the proposed algorithms using models from the Quantitative Verification Benchmark Set [12] (Section 4).
1.0.1 Related Work
Counterexample-Guided Abstraction Refinement (CEGAR) [6] is a successful approach for abstraction-based model checking: it starts with a coarse abstraction and refines it based on abstract counterexamples.
Lazy abstraction, introduced in [13], improved CEGAR through on-demand refinement during abstract state space exploration and varying precision from node to node in the state graph. An interpolant-based version was proposed in [23]. This was adapted to timed automata [14], introducing Adaptive Simulation Graphs (ASG) as the abstract model. This allows earlier refinement, cutting spurious paths before reaching a target, and a less expensive covering check. The ASG-based algorithm was adapted to explicit value abstraction of discrete variables in [27], which we, in turn, adapt to MDPs.
Different abstraction methods have been proposed for probabilistic systems. While some CEGAR-based methods employ MDPs as abstraction [8, 15, 5], others utilize stochastic games [24, 28, 17], which we plan to incorporate in the future. Abstract interpretation has also been used for probabilistic systems [7, 11]. Some others include magnifying lens abstraction [9], which explores the whole concrete state space but keeps only its subset in memory and assume-guarantee-style abstraction [19], specialized for composite systems. To our knowledge, no lazy abstraction method has been proposed for probabilistic models yet.
The algorithm presented in this paper uses a symmetric representation constraint, resulting in an approach similar to bisimulation reduction techniques [10, 16]. The main difference is that until the whole ASG is explored, only a limited version of “bisimilarity” holds which does not take the unexplored part of the state space into account, allowing coarser partitions on the already explored part. When combined with partial exploration, the algorithm can stop before exploring the full ASG. Finite-horizon bisimulation minimization [16] and incremental bisimulation abstraction-refinement [25] are similar in that they employ a relaxed version of bisimulation. Both of them limit the bisimilarity to a fixed path length and compute exact quotients w.r.t the relaxed relation, while we base the relaxation on the currently explored state space and do not aim for computing the coarsest relation.
2 Background and Notations
is the set of probability distributions over the set . For , denotes the probability measure of according to . means is a partial function from to , and is the set of values for which is defined. For , . is a Dirac distribution: .
2.1 Markov Decision Process (MDP)
MDPs are low-level mathematical models that describe both probabilistic and non-deterministic behavior in discrete time.
Definition 1 (MDP)
An MDP is a tuple , where is the set of states, is the set of actions, is a probabilistic transition function s.t. and is the initial state.
An action is enabled in if . In this case, denotes the next state distribution after taking in , defined as . The intuitive behavior of an MDP is as follows: starting in an action is chosen non-deterministically from those enabled in the current state in each step, and the next state is sampled from . A trace of an MDP is an alternating list of states and actions such that . Fixing a strategy for resolving the non-determinism, the set of traces can be equipped with a probability measure: intuitively, the probability of a trace is the product of the probability of landing in each state of the trace after taking the action specified by the strategy in the previous state. For a detailed formal treatment, see e.g. [20].
Given an MDP of the system behavior and a set of target (error) states , we want to compute (an upper approximation of) the probability of the set of traces involving a state in with non-determinism resolved by a maximizing strategy: . The result is the same if we make all target states absorbing, allowing us to restrict the analysis to finite traces.
2.1.1 Symbolic MDPs
Most real-life models are specified symbolically using state variables and operations on them. We assume that the MDP is given by a set of variables and a set of probabilistic guarded commands . Each has a set of values it can take, and an initial value . A valuation over is a function s.t. , and is the set of all valuations over . The initial valuation of the model is a valuation s.t. . The state space of this MDP is a subset of , and its initial state is .
Let denote the set of Boolean expressions over , the set of expressions over that result in an element of , and . An assignment is a function , such that . Let denote the set of assignments for . for and is the constant resulting from replacing each in with . for is a valuation such that . for is the distribution such that .
A command consists of a guard and a result distribution over assignments . is enabled by iff . Let denote the th assignment of command for a fixed ordering. The enabled actions in each state of the represented MDP are the commands enabled by , and taking the command results in the distribution . Widely used MDP description formats, like that of PRISM [21] or the JANI [4] format can be mapped to this low-level description.
Our running example is given by the following variables and commands:
is enabled in every state, and it increments by with probability . is enabled when , and always sets to and to . is enabled when is and is 2, and sets to . 1(a) shows this MDP.
2.2 Lazy Abstraction
Abstraction-refinement methods mitigate state-space explosion by disregarding information present in the original concrete model to create an abstract model that is iteratively refined until a conclusion is reached. Lazy abstraction performs refinement on-the-fly and only on a subset of the state space.
For checking safety properties in the qualitative case, a conservative abstraction overapproximates the reachable state set. In the probabilistic setting, the probability of reaching a target state in the abstract model overapproximates that in the concrete one, which we will prove for the proposed algorithm.
We build on the lazy abstraction method of [27] for non-probabilistic systems. It constructs an Adaptive Simulation Graph (ASG) with nodes labeled by both a concrete and an abstract state: the concrete state represents all states in the abstract state regarding possible action sequences. The abstract state labels start very coarse and are refined as needed. Covering edges indicate that action sequences starting from the coverer node encompass those starting from the covered node, eliminating the need to explore paths from the covered node.
If an action is enabled in at least one concrete state described by the abstract label of a node, but not in the concrete label, the abstract label is strengthened by removing states with the action enabled. This operation can trigger additional strengthenings. The algorithm terminates once all enabled actions in non-covered nodes have been explored. The abstract labels in the finished ASG cover all reachable concrete states, and contain a target state only if one is reachable.
2.2.1 Abstract domains
Abstract states are described using an abstract domain. For a set of concrete states , an abstract domain consists of the abstract state set , a partial ordering , an abstraction function and a concretization function satisfying . lets us treat abstract states as sets of concrete states; we write “” for when is clear from the context. denotes . has two special elements: and satisfying .
Our lazy abstraction algorithms are domain agnostic, but need an abstract domain for with the following operations.
For and , abstract post operator applies an assignment in the abstract state space: . For , denotes evaluating in the abstract state space: if evaluates to for all , if evaluates to for all , otherwise .
We also need a block operation: for an abstract state , a Boolean expression and a concrete state s.t. , is an abstract state s.t. . Its goal is to give a new abstract state by removing at least those states from which satisfy (potentially others as well) while kee** .
The abstract states must be representable as Boolean expressions: for each a must exist s.t. . Relying on this, we will freely use abstract states in place of Boolean expressions.
We will use the explicit value domain (abstract states correspond to tracking only a subset of ) as an example throughout the paper which we implemented in our prototype, along with predicate abstraction (abstract states are Boolean predicates over ). A partial function s.t. is called a partial valuation, denotes the set of all partial valuations over . Description of these domains and their operations can be seen in Table 1, assuming a concrete state set .
The lazy abstraction algorithm does not use the abstraction and concretization functions and and the abstract post operator directly, only as arguments of a block operation (see later), so they need not be efficiently computable if the corresponding block operation can be implemented efficiently.
EXPL | PRED | |
and | ||
is the empty valuation, is a non-valuation element representing contradiction | ||
Boolean representation | identity (already a Boolean expression) | |
Substituting the values in , and deciding the satisfiability of the result. | if , if , if neither. | |
Substituting known variables into the result expressions. If this results in a constant, that is the result, else unknown. | strongest postcondition |
3 Lazy Abstraction for MDPs
Now we adapt the lazy algorithm to symbolic MDPs given by a variable set and a command set . Given a target formula , the goal is to compute the maximal probability of reaching a state s.t. .
We select abstract domain . The set of commands is extended with a target command: }, where is the identity assignment. A node is a target if this command is enabled in it. This ensures that the finished ASG contains a node labeled with a target state exactly if a target state is reachable in the concrete state space [27].
3.0.1 Abstract model
We use a probabilistic extension of the ASG. A direct adaptation of the non-probabilistic lazy algorithm by switching to probabilistic actions would overapproximate the target probability with no control over the approximation. Therefore, we use a stricter, symmetric representation constraint for the relation between the concrete and abstract labels of a Probabilistic ASG node.
Definition 2 (PASG)
A Probabilistic Adaptive Simulation Graph is a tuple , where is a set of nodes, is a set of transition “edges” from nodes to node distributions labeled with commands, is a set of directed covering edges, is the concrete labeling function, is the abstract labeling function.
For an edge , is the th element of for a fixed ordering. A PASG is well-labeled, if it satisfies the constraints in Table 2. The main difference from the original ASG is that in 2, we use a distribution of results instead of a single one, and 2 requires the set of enabled actions to be exactly the same in all concrete states contained in the abstract label.
In the original lazy algorithm, refinement is performed when an action disabled in , but enabled in some element of the abstract label , and we refine by blocking the guard of the action from . Here, we also refine when an action is enabled in but disabled in some element of by blocking the negation of the guard. We also need to adapt soundness to probabilities, see LABEL:thm:bi_soundness. 2 is a technical constraint to make our proofs easier.
Constraint | Formalisation |
A1) Abstract label contains the concrete label: | |
A2) Concrete label exactly represents the whole abstract label with respect to the enabled commands | |
B1) The command of a transition edge is enabled in the concrete label of the source | |
B2) For transition edges , the th result node is consistent with the th assignment: same probability, concrete label is the result of the assignment, abstract label overapproximates the result | |
C1) Abstract label of covering node contains the concrete label of covered node | |
C2) Covering node is at least as abstract as the covered node | |
C3) Covering node is not covered | |
D1) At most one node labeled with a given concrete label can be non-covered |
Example 1
1(b) shows an example PASG with black (the orange part is a refinement example explained later). The abstract label tracks only in all nodes (this could differ from node to node in general). is contained in for all nodes as the value of is the same in and (2).
covers , covers and , satisfying 2 and 2. could cover according to the labels, but it would violate 2.
This PASG is unfinished, and are not expanded. is an example for the remaining constraints. 2 is satisfied, as tracking in is enough to disable , and both and are enabled in and everywhere in . As the outgoing edges are labeled with and , 2 is satisfied. Let be the edge from . The assignments in are , paired with and paired with , which satisfies 2. E.g. for : , and .
3.0.2 Exploration
Algorithm 1 shows PASG construction. An initial node labeled is extended to a well-labeled PASG with each node either covered or expanded. Algorithm 2 shows blocking an expression from , used during refinement.
When removing a node from the waitlist, we check whether s.t. is not covered. If so, a covering edge is created and is strengthened for 2 to hold. Else, it is expanded.
If a node is selected for expansion, we check for each whether . If so, a new node is created for each with , and a transition edge is created such that for . Because of 2, if the abstract label contains states where the transition is disabled, we remove them by blocking out the negated guard (Line 3).
3.0.3 Refinement
Refinement is interleaved with exploring the abstract state space. Whenever the changes for some , the constraints may be violated. If constraint 2 is violated, the problematic covering edge is removed from . This makes non-covered, so we expand it later (Line 10).
If constraint 2 is violated by covering edge , but constraint 2 still holds, the current must be replaced with such that , and (referring to the current ). An appropriate is (Line 10).
Assume that 2 is violated by an edge . Because of how the PASG is constructed, the concrete label and probability subconstraints of 2 must still hold, but the abstract label part is violated by some node : of no longer overapproximates applying (the assignment that led to its creation) to of its parent. The violation caused by this assignment is eliminated by changing to (Line 13).
Strengthenings may create new violations, but all of them are eliminated after finite steps (if the concrete label can be finitely represented in the abstract domain), and we continue expanding non-covered nodes. Efficient implementations of the algorithm can employ sequence interpolation to strengthen the whole path up to the root at once [27], which we do when using the predicate domain, as we observed that both simple weakest-precondition-based refinement and binary interpolation lead to predicates growing very fast.
Example 2
1(b) shows an example of refinement in orange. Expanding , we realize is enabled in some states described by abstract label , but not in the concrete label . Thus, we strengthen by blocking the guard , resulting in the abstract label .
This triggers another strengthening, as no longer overapproximates applying to . is also strengthened, removing a cover edge as is no longer contained in . Strengthening a covering node also strengthens the covered nodes if the covering remains (see and ).
3.0.4 Numerical analysis
The finished PASG can be treated as an MDP . Regarding , for a non-covered node , a command is enabled if there is an edge in the PASG, and . The only action in covered nodes is , which results in their covering node.
thm:bi_soundness The maximal/minimal probability of reaching a target node in the PASG of an MDP is the same as in .
Refer to the Appendix for proofs.
Due to the symmetry of constraint 2, this abstraction can be considered similar to bisimulation-reduction, but not aiming for the coarsest bisimulation. Constructing the PASG can be computationally cheaper than the coarsest bisimulation, but the larger state space may result in more expensive numerical computation. The advantages appear when the abstraction is combined with partial state space exploration, as most bisimulation reduction algorithms in the literature cannot be done on the fly. Comparing our method to bisimulation reduction in depth (both theoretically and empirically) is planned for future work.
3.1 Combining with BRTDP
Bounded Real-Time Dynamic Programming (BRTDP) [22, 3] approximates the value function of an MDP during state space exploration. It maintains an upper and a lower bound ( and ) by generating traces and updating the bounds for the encountered states. In each step, the optimal action is chosen according to the current . The strategy for choosing a state from the result distribution is a parameter of the algorithm, for which we implemented the RANDOM and DIFF_BASED trace generation strategies from [3].
Our lazy abstraction algorithm combines well with such methods. As refinement is performed during expansion, the abstract states in an in-progress PASG are coarser than those in a finished PASG. Thus, if BRTDP reaches the required threshold before constructing the full PASG, the abstract labels remain coarser. Existing probabilistic CEGAR schemes like [17] cannot benefit from this, as they need lower and upper value bounds for all nodes for refinement, while BRTDP works best when only the value of the initial node is needed. This combination enables a controlled trade-off between time and accuracy.
The skeleton of the algorithm is the same as the BRTDP algorithm described in [3] for general MDPs. The difference is that instead of generating traces from the final PASG, we use the steps of building the PASG for trace generation. As such, refinement is also possible during trace simulation, potentially removing covers used in previous simulations.
thm:bi_brtdp_soundness The maximal probability of reaching a target state is always between and if BRTDP is used with PASG construction steps.
This theorem is non-trivial, as the traces are not generated for the finished PASG, but for an in-progress version where transient cover edges can exist which would not be present when finished. The main idea behind its proof is that if a value is propagated through a cover edge, then the value has been updated only based on traces consistent with the cover edge (as we would have already removed it if any trace inconsistent with it had been explored).
4 Evaluation
Implementation Our prototype111https://github.com/szdan97/probabilistic-theta/tree/prob-proto with the explicit value and predicate domains is implemented in the Theta model checker [26], taking JANI models[4] as input. Only properties of the form are supported where are Boolean constraints. Action result probabilities must be constant. The locations of JANI models are always tracked in the abstract states and covering can only occur between nodes with the same locations. To fairly assess the algorithms rather than the implementations, we implemented both Bounded Value Iteration (BVI) [1] and BRTDP as MDP solution techniques in Theta both with and without lazy abstraction. We precompute almost sure reachability and avoidance to speed up the numerical solution if BVI is used.
The main metrics of interest are state space size and running time. As the numerical computations mostly scale with the non-covered PASG nodes, we are especially interested in the number of non-covered nodes. Our evaluation focuses on the following research questions:
RQ1. How does lazy abstraction affect the state space size and analysis time?
RQ2. Does the combination of lazy abstraction with BRTDP lead to reduced abstract model size when converged? How does it affect the running time?
4.0.1 Setup
We used the 104 MDP model-property pairs from the Quantitative Verification Benchmark Set [12] compatible with our current implementation. The experiments were conducted using BenchExec[2], running them on the Komondor HPC 222https://hpc.kifu.hu/en with AMD EPYCTM 7763 CPUs, each run getting 8 CPU cores, 16GB RAM, and a 1-hour timeout. Convergence threshold was (absolute) for all algorithms.
4.0.2 Results and discussion
RQ1. Figure 2 shows the BVI results. Lazy abstraction often significantly reduced the state space: for example, a 3-fold reduction was possible for beb.3-4 [N=3, prop: GaveUp] (from 4632 nodes to 1559 non-covered nodes) and csma.2-6 [prop: all_before_max] (from 67741 to 24837) with EXPL, and for beb.3-4 [N=3, prop: GaveUp] (from 4632 to 1354) with PRED. There are also inputs where the explicit domain could not reduce the state space size (e.g. blocksworld.5, cdrive.2, but that is expected because of its low granularity.
Measuring the analysis time, it turned out that the overhead of more complex operations during exploration outweighed the benefits of numerical computations on a smaller state space. The overhead is apparent for EXPL, but it is much less severe than for PRED.
Predicate abstraction was sometimes able to reduce the state space more than the explicit domain when it terminated before timeout, but the opposite was also present (related plots can be found in the appendix). The overhead of interpolating using an SMT solver was often too large, and so PRED often failed to terminate in time.
We identified several abstraction-specific optimization possibilities for the implementation. For one, the interpolants returned by Z3 were often very large and had a redundant structure, which we could mitigate through structural simplification, improving both time and memory efficiency. Investigating alternative refinement methods and other solvers could also lead to better results.
Another opportunity for optimization is that like the non-probabilistic version [27], we currently create multiple nodes with the same if a concrete state is reachable on multiple paths. As one of them always covers the others, only that is explored. However, according to our investigation, there are inputs where this led to multiple magnitudes of increase in the number of nodes during exploration. Merging such nodes instead would solve this issue, but refinement must be slightly changed as the path up to the root will no longer be unambiguous. We already had some preliminary measurements with promising results regarding this modification.
RQ2. The simulation-based nature of BRTDP makes it harder to gauge the benefits of abstract BRTDP compared to standard BRTDP: there were inputs where abstract BRTDP converged with fewer nodes and where the concrete one did. (We relegated plots related to this comparison to the appendix.)
The benefits of abstract BRTDP compared to abstract BVI are much more apparent. The plots in Figure 3 show this comparison (the results of the strategy leading to fewer nodes were used for each input-domain pair for BRTDP).
The highest relative state space size reduction was on zeroconf [N=20, k=2, !reset, prop: correct] (170-fold from 64109 to 373 non-covered nodes) for EXPL and pnueli-zuck.3 [prop: live] (from 1888 to 239 non-covered nodes) for PRED. There were inputs where no further reduction was achieved though (e.g. blocksworld.5, cdrive.2, rectangle-tireworld.5, ij.10 for both domains). When both BVI and BRTDP terminated, BRTDP was often able to do so in less time, especially with PRED (the results are much more two-sided for EXPL).
5 Conclusions
We proposed a lazy abstraction algorithm for symbolic MDPs and combined it with BRTDP. We provided numerical evaluation for different versions of the proposed algorithm using the Quantitative Verification Benchmark Set, comparing them to explicitly computing the concrete state space.
The initial experimental evaluation shows potential in the proposed algorithm, especially if reducing the state space is paramount for staying within the memory limits. As the time overhead introduced by more complex computations in the state space exploration often outweighed the gains from analyzing a smaller state space, we plan to explore possible improvements for this aspect. Further measurements using other benchmark sets and more parameterizations of the scalable models in the QVBS are also planned.
Additionally, we wish to explore fine-grained transitioning between the strict representation version (see 2) and a more direct overapproximating adaptation by incorporating ideas from game-based abstraction refinement, moving the algorithm closer to standard abstraction approaches instead of bisimulation reduction.
References
- [1] Baier, C., Klein, J., Leuschner, L., Parker, D., Wunderlich, S.: Ensuring the reliability of your model checker: Interval iteration for Markov Decision Processes. In: CAV’17 (2017). https://doi.org/10.1007/978-3-319-63387-9_8
- [2] Beyer, D., Löwe, S., Wendler, P.: Reliable benchmarking: requirements and solutions. Int. J. Softw. Tools Technol. Transf. (2019). https://doi.org/10.1007/s10009-017-0469-y
- [3] Brázdil, T., Chatterjee, K., Chmelik, M., Forejt, V., Kretínský, J., Kwiatkowska, M.Z., Parker, D., Ujma, M.: Verification of Markov Decision Processes using learning algorithms. In: ATVA’14 (2014). https://doi.org/10.1007/978-3-319-11936-6_8
- [4] Budde, C.E., Dehnert, C., Hahn, E.M., Hartmanns, A., Junges, S., Turrini, A.: JANI: quantitative model and tool interaction. In: TACAS’17 (2017). https://doi.org/10.1007/978-3-662-54580-5_9
- [5] Chadha, R., Viswanathan, M.: A counterexample-guided abstraction-refinement framework for Markov decision processes. ACM TOCL (2010). https://doi.org/10.1145/1838552.1838553
- [6] Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: CAV’00 (2000). https://doi.org/10.1007/10722167_15
- [7] Cousot, P., Monerau, M.: Probabilistic abstract interpretation. In: ESOP’12 (2012). https://doi.org/10.1007/978-3-642-28869-2_9
- [8] D’Argenio, P.R., Jeannet, B., Jensen, H.E., Larsen, K.G.: Reduction and refinement strategies for probabilistic analysis. In: PAPM-PROBMIV’02 (2002). https://doi.org/10.1007/3-540-45605-8_5
- [9] De Alfaro, L., Roy, P.: Magnifying-lens abstraction for Markov decision processes. In: CAV’07 (2007). https://doi.org/10.1007/978-3-540-73368-3_38
- [10] Dehnert, C., Katoen, J., Parker, D.: SMT-Based bisimulation minimisation of Markov models. In: VMCAI’13 (2013). https://doi.org/10.1007/978-3-642-35873-9_5
- [11] Esparza, J., Gaiser, A.: Probabilistic abstractions with arbitrary domains. In: SAS’11 (2011). https://doi.org/10.1007/978-3-642-23702-7_25
- [12] Hartmanns, A., Klauck, M., Parker, D., Quatmann, T., Ruijters, E.: The quantitative verification benchmark set. In: TACAS’19 (2019). https://doi.org/10.1007/978-3-030-17462-0_20
- [13] Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: POPL’02 (2002)
- [14] Herbreteau, F., Srivathsan, B., Walukiewicz, I.: Lazy abstractions for timed automata. In: CAV’13 (2013). https://doi.org/10.1007/978-3-642-39799-8_71
- [15] Hermanns, H., Wachter, B., Zhang, L.: Probabilistic CEGAR. In: CAV’08 (2008). https://doi.org/10.1007/978-3-540-70545-1_16
- [16] Kamaleson, N., Parker, D., Rowe, J.E.: Finite-horizon bisimulation minimisation for probabilistic systems. In: SPIN’16 (2016). https://doi.org/10.1007/978-3-319-32582-8_10
- [17] Kattenbelt, M., Kwiatkowska, M., Norman, G., Parker, D.: Abstraction refinement for probabilistic software. In: VMCAI’09 (2009)
- [18] Kelmendi, E., Krämer, J., Křetínskỳ, J., Weininger, M.: Value iteration for simple stochastic games: Stop** criterion and learning algorithm. In: CAV’18 (2018)
- [19] Komuravelli, A., Păsăreanu, C.S., Clarke, E.M.: Assume-guarantee abstraction refinement for probabilistic systems. In: CAV’12 (2012). https://doi.org/10.1007/978-3-642-31424-7_25
- [20] Kwiatkowska, M., Norman, G., Parker, D.: Stochastic model checking. In: SFM’07 (2007)
- [21] Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: Verification of probabilistic real-time systems. In: CAV’11 (2011)
- [22] McMahan, H.B., Likhachev, M., Gordon, G.J.: Bounded real-time dynamic programming: RTDP with monotone upper bounds and performance guarantees. In: ICML’05 (2005). https://doi.org/10.1145/1102351.1102423
- [23] McMillan, K.L.: Lazy abstraction with interpolants. In: CAV’06 (2006). https://doi.org/10.1007/11817963_14
- [24] Parker, D., Norman, G., Kwiatkowska, M.: Game-based abstraction for Markov decision processes. In: QEST’06 (2006). https://doi.org/10.1109/QEST.2006.19
- [25] Song, L., Zhang, L., Hermanns, H., Godskesen, J.C.: Incremental bisimulation abstraction refinement. ACM TECS (2014). https://doi.org/10.1145/2627352
- [26] Tóth, T., Hajdu, A., Vörös, A., Micskei, Z., Majzik, I.: Theta: a framework for abstraction refinement-based model checking. In: FMCAD’17 (2017). https://doi.org/10.23919/FMCAD.2017.8102257
- [27] Tóth, T., Majzik, I.: Configurable verification of timed automata with discrete variables. Acta Informatica (2022). https://doi.org/10.1007/s00236-020-00393-4
- [28] Wachter, B., Zhang, L.: Best probabilistic transformers. In: VMCAI’10 (2010). https://doi.org/10.1007/978-3-642-11319-2_26
Appendix 0.A Proofs
For a PASG trace such that , its coverless representation is constructed such that for each where , and is dropped from the trace. The original trace can always be reconstructed from the coverless representation, as
Lemma 1
For any well-labeled finished PASG for the MDP , let be a trace of . Then there must exist a trace of with coverless representation such that for all .
Proof
For any non-covered node and concrete state , if , then all commands enabled in are enabled in because of 2 and 2 (the concrete label has at least those commands enabled that are enabled in any state described by the abstract label, and the actions enabled in a non-covered node are the commands enabled in its concrete label). Because of 2, if there is a covering edge and , the is also true. Because of the abstract label subconstraint of 2, if and choosing the assignment in leads to , then .
Based on these observations, the theorem can be proven by induction on the trace length. It holds for the 0-length trace , as . Then for an trace with length , we know that the length prefix has a corresponding trace ending in . If this is not a covered node, then is enabled in it as (from the induction assumption) , then we choose any assignment of that leads to , and choose the same assignment in leading to a node . As we observed, because of the abstract label subconstraint of 2, . If is covered, we take the action to , where is enabled, as because of 2. We take and an appropriate assignment to , and is true for the same reason as in the other case. This concludes our induction proof.
A consequence of this is that if a node is covered by in a finished PASG, then for all traces from , there exists a trace from with the same commands and assignments chosen.
Lemma 2
The maximal probability of reaching a target node in a PASG for an MDP is at least as high as the maximal probability of reaching a target state in .
Proof
Fix a maximizing memoryless strategy for the MDP (we can restrict ourselves to memoryless strategies as an optimal memoryless strategy for an MDP is also an optimal general strategy if the optimization goal is a reachability probability). This induces a Discrete-Time Markov Chain , where the probability of reaching a target state from the initial state is the maximal probability of reaching a target in . We will construct a strategy for the PASG that results in at least as high probability for reaching a target node as . Note that is not a memoryless strategy.
The aim of will be to copy the traces of . The non-trivial part of this is that because of covers, multiple states of can correspond to the same node in the PASG – that is why is not a memoryless strategy but uses the whole trace to select an action.
will obviously always choose if the trace ends in a covered node, as there is no other enabled action. Let be a coverless representation of a PASG trace . Because of 2, there is a one-to-one correspondence between the assignments of and the result nodes of the transition edge. Let be the assignment corresponding to in this trace.
We have two cases:
-
1.
A concrete trace can be constructed from by starting in , choosing and applying to in the th step. This way, we can compute which concrete state we would actually be in if this assignment sequence happened in the original state space. We will call the concretization of . This is possible only if is enabled in , which need not always be true – that will be the second case. Let be the same command as .
-
2.
The trace is not concretizable. In this case, can be anything, as such traces will never be generated by if it is constructed according to the previous case for concretizable traces, so it cannot change the induced MDP .
This is a valid strategy, as 1 ensures the selected command is enabled in the PASG node. The fact that the choice for non-concretizable traces does not matter can be seen by induction:
-
•
The only possible 1-length trace is trivially concretizable, the commands enabled in are exactly those enabled in .
-
•
Let be the concretization of a concretizable trace . At the end of , chooses a command that is enabled at the end of , resulting in a trace one step longer that is still concretizable.
Although there is always a unique assignment that results in entering a node in the PASG, this is not true in general in the original MDP (e.g. in the state , the assignments and both lead to the state – if these are the assignments of the same command, we do not know which one was chosen), so there are multiple traces with the same concretization.
Assume for a moment that concretization creates a one-to-one correspondence between abstract and concrete traces, so the aforementioned problem is not present. In this case, the probability subconstraint of 2 would ensure that the probability of according to the strategy is the same as the probability of its concretization according to .
This can be generalized to the case when there are multiple abstract traces with the same concretization : in this case, .
Proof sketch for proving this by induction: if at the first command of a trace there are two assignments and in a command leading to the same concrete state when applied to , then the probability of going from to is , and the probability of the whole trace is times the probability of the suffix ; in the PASG, these two assignments result in different nodes, but the abstract traces corresponding to the suffix are available from both nodes (or there covering nodes, which only multiplies the probability of the suffix by ), so assuming the sum of the probability of these abstract traces is , then the probability of the whole trace is , which is the original probability.
Let denote the set of abstract traces that have the concretization , and is the sum of their probabilities. From the previous statement, we have Let be the concretization of . Observe that concretization is deterministic, so for any , . Let be the set of traces that lead to target nodes, and . need not be the whole , as target nodes can cover non-target nodes, let denote the ”spurious” target traces . Let denote the set of target traces of . Observe that . Now we can prove that the target probability on is at least as high as in :
As is non-negative, and is exactly the target probability in , we have proven that the target probability in is at least as high as in . is not necessarily a maximizing strategy, so the maximal probability in can be even higher. was chosen to be maximizing, so this proves the theorem.
The probability of reaching a target state in is the sum of the probabilities of all traces reaching a target state. For each of these traces, we have a “copy” in the MDP induced by for PASG, which has the same probability, as the same commands are chosen throughout the trace and the probability of choosing a given assignment in a step of the trace is the same in the PASG as in . There are other traces as well in the PASG with strategy that end in target nodes: non-concretizable traces because of covering nodes enabling commands that are not enabled in the covered node and traces that end in target nodes that cover non-target nodes.
As already results in at least as high target reachability probability as an optimal strategy on , and it might not even be optimal, this shows that the maximal probability in the PASG must be at least as high as in .
Lemma 3
The maximal probability of reaching a target node in a PASG for an MDP is at most as high as the maximal probability of reaching a target state in .
Proof
Sketch: The proof is done similarly to that of 2, just the other way around. The main difference is that strategies on have less information in the trace than strategies in the PASG, as nodes in the PASG are basically labeled with which assignment was the last. This leads to a problem when two assignments of a command can lead to the same state in , as a strategy on the PASG may choose a different action in them (e.g. they can be covered by different nodes).
Because of this, we construct a different MDP from the symbolic description of , where the states also contain the assignment that was applied last time. This MDP is bisimilar to , the bisimulation relation being based on forgetting the last assignment – neither the “targetness” nor the enabled commands and their result distribution depends on the last assignment if the current state is known, so it is easy to prove that this is a bisimulation. As such, the maximal target probability on is the same as on .
For any maximizing memoryless strategy on the PASG, we can construct a non-memoryless strategy on such that , which is now unique because of the assignment labels. The strategy is valid, which can be proven using an “inverted” 1 based on 2. This results in at least as high a probability for reaching a target state as in the PASG.
Theorem LABEL:thm:bi_soundness
Proof
Lemma 4
The maximal probability of reaching a target state is always below if BRTDP is used with PASG construction steps.
Proof
Sketch: Let be an assignment-labeled version of similarly to the proof of 3. For an element and an assignment , the state corresponds to the state with the latest assignment being . The initial state is a special element without an assignment label. For all already existing PASG nodes , , where is the real value function of , is the assignment corresponding to according to constraint 2, and is a state of . This can be proven by induction. This is of course true when the node is created, as it is initialized to unless it is a non-target absorbing node, in which case . Whenever is updated in later steps, we have two cases:
-
1.
is non-covered, so it is updated according to a transition edge. In this case, the update corresponds to an update on according to an upper approximation of the value function , which is set to if a node exists with and otherwise. Because of the induction hypothesis, this is a valid upper bound for the value function, which means that computing a Bellman update using it is a valid
-
2.
is covered by . We do not yet know whether the currently covering node will remain covering until the finished PASG, so we cannot say that all action sequences possible from are possible from . However, as the covering edge still exists, we know that those action sequences that are possible from but not from have not been explored yet: along the way of these sequences, there exists a non-covered non-expanded node. The value of this node is currently overapproximated by . So for all action sequences possible from , they are either also possible from , or there is a prefix of it that is possible from it, and ends in a node whose value approximation is set to . Because of this (and the fact that we are aiming to maximize the value), the current value approximation of must be higher than the value of , so copying it to does not violate the induction assumption.
As is bisimilar to , , so is also an upper bound for .
Lemma 5
The maximal probability of reaching a target state is always above if BRTDP is used with PASG construction steps.
Proof
Sketch: This can be proven similarly to 4. The upper approximation is replaced in all statements with the lower approximation . The non-covered case goes the same.
If is covered by in the finished PASG, we know that all action sequences starting from are also available from . When an update happens during BRTDP, we do not know this yet. However, for all action sequences available from and not available from , as the covering edge is still there, there must be a state whose current lower approximation is , as the corresponding PASG node has not been expanded yet. So the current must be lower than .
Theorem LABEL:thm:bi_brtdp_soundness
Appendix 0.B Further Experiment Results
Figure 4 compares the PRED and EXPL domains when using BVI. Although EXPL always wins in running time, PRED can sometimes reduce the number of nodes further. If the overhead of refinement in the PRED domain can be mitigated making it terminate in time on more inputs, the better reduction capability might be observed on even more inputs.
Figure 5 compares the results using BRTDP both for the baseline and abstraction-based analysis. No clear advantage of either of them can be observed.