PaperlayerView exact revision on arXiv

Source-linked AI summary

Verification of Markov Decision Processes using Learning Algorithms

Tomáš Brázdil, Krishnendu Chatterjee, Martin Chmelík, Vojtěch Forejt, Jan Křetínský, Marta Kwiatkowska, David Parker, Mateusz Ujma

arXiv:1402.2967v3cs.LO

TL;DR

The paper addresses how to verify MDP reachability without exhaustively exploring the state space. It introduces learning-based methods for complete and limited information, producing exact or PAC bounds, and reports speed-ups while extending to arbitrary MDPs and unbounded objectives.

  • Problem

    MDP verification can be limited by the time and memory required to store and exhaustively explore the full model.

  • Method

    The framework uses trajectory-generating learning algorithms to guide partial exploration, with BRTDP for complete information and DQL for limited information.

  • Results

    The methods produce exact lower and upper bounds with complete information and PAC lower and upper bounds with limited information, with experiments reporting speed-ups over PRISM.

  • Takeaways & Limitations

    The framework supports unbounded probabilistic reachability for arbitrary MDPs and extends to LTL objectives and minimum reachability probabilities.

  • Takeaways & Limitations

    The BRTDP approach requires conditions ensuring that state-action pairs used by ǫ-optimal strategies are selected often enough for almost-sure convergence.

Abstract

from arXiv · show

We present a general framework for applying machine-learning algorithms to the verification of Markov decision processes (MDPs). The primary goal of these techniques is to improve performance by avoiding an exhaustive exploration of the state space. Our framework focuses on probabilistic reachability, which is a core property for verification, and is illustrated through two distinct instantiations. The first assumes that full knowledge of the MDP is available, and 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, and yields probabilistic guarantees, again in terms of both the lower and upper bounds, which provides efficient stopping criteria for the approximation. The latter is the first extension of statistical model-checking for unbounded properties in MDPs. In contrast with other related approaches, we do not restrict our attention to time-bounded (finite-horizon) or discounted properties, nor assume any particular properties of the MDP. We also show how our techniques extend to LTL objectives. We present experimental results showing the performance of our framework on several examples.

1 Introduction

The paper frames learning-based verification as a way to reduce exhaustive MDP exploration while preserving reachability guarantees. It develops complete- and limited-information approaches that support arbitrary MDPs and unbounded properties.

  • 1 Introduction: Learning-based exploration uses trajectories and approximations of reachability probabilities to guide model exploration and reduce the explored state space.The framework targets verification efficiency by avoiding unnecessary storage and exploration of the full model.
  • 1 Introduction: The framework distinguishes complete information, where the MDP is known, from limited information, where only trajectories can be sampled.These settings produce different classes of guarantees.
  • 1 Introduction: BRTDP provides correct lower and upper bounds with complete information, whereas DQL provides PAC lower and upper bounds when only sampling is available.PAC guarantees allow a non-zero probability that the bounds are incorrect.
  • 1 Introduction: The techniques apply to arbitrary MDPs by detecting end components on the fly and extend to LTL objectives and minimum reachability probabilities.End components can otherwise cause learning or heuristic methods to converge to incorrect values.
  • 1.1 Related Work: The DQL-based method is presented as the first statistical model-checking technique for unbounded properties on MDPs.Prior approaches considered time-bounded properties or used discounting to ensure convergence.
  • Experimental Results: Experiments report considerable speed-ups over PRISM’s fastest methods, enabled by constructing an ǫ-optimal policy while exploring only part of the state space.The paper also identifies rare events as a potential source of slowdown for RTDP-based exploration.

2 Basics about MDPs and Learning Algorithms

This section defines MDPs, reachability values, strategies, and the learning framework’s approximation guarantees. Algorithms iteratively update lower and upper value bounds from simulated executions under either complete or limited information.

  • Basics about MDPs: MDPs combine nondeterministic action choices with probabilistic transitions and are used to model stochastic behaviour in verification.The model captures phenomena such as failures, lossy communication, environmental uncertainty, and explicit randomisation.
  • Objectives and values: Unbounded reachability asks whether a target set F is eventually reached, while the value of a state is the supremum reachability probability over strategies.A strategy is ǫ-optimal when its reachability probability is within ǫ of the value.
  • Learning Algorithms for MDPs: A learning algorithm simulates MDP executions and updates lower and upper approximations U and L of the state-action value function.The approximations are initialized to enclose the true values and are updated for visited states.
  • Learning Algorithms for MDPs: The algorithm terminates when the maximum upper value over enabled actions falls below the requested precision ǫ.This stopping rule uses max_a U(s, a) < ǫ as stated in the learning framework.
  • Learning Algorithms for MDPs: Learning computations may be randomized and occasionally incorrect because updates depend only on visited states and sampled executions.When almost-sure convergence cannot be guaranteed, PAC correctness requires termination with sufficiently high probability.
  • Information settings: Complete information means knowing the entire MDP, whereas limited information provides the initial state, enabled-action access, and the ability to sample executions.The limited-information setting also assumes a positive lower bound pmin on nonzero transition probabilities.

3 MDPs without End Components

The section instantiates a learning framework for unbounded reachability in MDPs without end components using BRTDP with complete information and DQL with limited information. Both algorithms maintain lower and upper approximations, with BRTDP converging almost surely and DQL achieving PAC guarantees under the EC-free assumption.

  • Framework: The framework assumes no end components except terminal states 0 and 1, then instantiates learning algorithms for unbounded reachability.The paper later extends these methods to arbitrary MDPs.
  • BRTDP: BRTDP uses complete transition information to update lower and upper state-action bounds by probability-weighted successor values.Its exploration samples actions maximizing the current upper bound, while updates proceed backward along sampled paths.
  • BRTDP: BRTDP converges almost surely under the EC-free assumption.
  • DQL: DQL estimates successor-value averages from sampled trajectories when transition probabilities are unknown, using delayed updates and an error adjustment.The delay parameter m must be large enough for the estimates to be sufficiently close to the true values.
  • DQL: DQL is probably approximately correct under the EC-free assumption, with parameters selected from the desired precision and error tolerance.The paper states that these parameters can be conservatively approximated using limited information about the MDP.
  • Extensions: The same framework can be adapted to bounded reachability by adding a step counter and making non-target states at the bound rejecting.

4 Unrestricted MDPs

The section removes the EC-free restriction by detecting end components during simulation and collapsing them on the fly. The resulting OBRTDP and ODQL algorithms provide guarantees for arbitrary MDPs.

  • Motivation: End components can prevent BRTDP and DQL from converging, because greedy upper-bound choices may preserve an overly large upper bound indefinitely.In the example, the true value is 0.5 while the upper bound remains 1, so the error does not decrease.
  • On-the-fly processing: Preprocessing all maximal end components requires the full graph, so the paper instead detects and processes end components during exploration.This supports settings with limited information or models too large for exhaustive exploration.
  • On-the-fly processing: The on-the-fly procedure identifies candidate components from repeated state-action appearances, then collapses each discovered component into a single state.Collapsed states can be made terminal with value 1 when they contain a target, or value 0 when no actions leave them and no target is present.
  • Complete information: The identification lemma gives a conditional probability bound that a frequently repeated state-action set is an end component.For i ≥ κ and sufficiently long exploration, the probability is at least 1 − 2c_i i^3 · (p_min/E_m)^−κ.
  • Complete information: OBRTDP, the on-the-fly BRTDP variant, converges almost surely for all MDPs.
  • Complete information: Every maximal end component found in the explored auxiliary MDP and contained in the explored state set is an end component of the original MDP.
  • Limited information: ODQL simulates exits from collapsed components by sampling internal actions uniformly until an exit state is reached, while controlling cumulative identification error.Its parameters are chosen so the total error from on-the-fly collapsing is at most δ/2.
  • Limited information: ODQL is probably approximately correct for all MDPs.

5 Experimental Results

The experiments compare BRTDP with three successor-selection heuristics against PRISM on four benchmark models. BRTDP outperforms PRISM by constructing an ϵ-optimal policy while exploring only part of the state space.

  • Heuristics: The three heuristics select successors randomly, by maximum bound gap, or systematically in round-robin order.The round-robin heuristic guarantees sure termination.
  • Experimental setup: Four benchmark models—zeroconf, wlan, firewire, and mer—were evaluated using BRTDP and PRISM.The first three use unbounded probabilistic reachability properties, while mer uses a time-bounded property.
  • Experimental setup: BRTDP terminates when the initial state's lower and upper bounds differ by at most ϵ, using ϵ = 10^-6 except for zeroconf, where ϵ = 10^-8.PRISM value iteration uses the same convergence tolerance criterion; its strategy is not formally guaranteed to be ϵ-optimal in all cases, although it was on these examples.
  • Results: BRTDP outperforms PRISM on all four benchmarks.The reported verification times are averaged over 20 runs.
  • Results: The algorithm constructs an ϵ-optimal policy while exploring only a portion of the state space.The number of distinct visited states is described as, on average, three orders of magnitude smaller than the total model size.
  • Results: RTDP is generally the slowest heuristic and is sensitive to model probabilities, whereas BRTDP and round-robin perform very similarly.Rare events can make crucial states unlikely to be visited, slowing RTDP considerably.

6 Conclusions

The paper presents a learning-based framework for verifying MDPs, including techniques for unbounded probabilistic reachability in arbitrary MDPs. It provides exact bounds with complete information and probabilistically correct bounds with limited information.

  • The framework applies learning algorithms to MDP verification.
  • For arbitrary MDPs, the techniques analyse unbounded probabilistic reachability properties.
  • Complete information yields exact bounds, while limited information yields probabilistically correct bounds.
  • Future work includes exploring other learning algorithms and combining learning algorithms with symbolic probabilistic-verification methods.

A Proof of Theorem 1: Correctness of BRTDP

The proof establishes correctness and almost-sure termination of BRTDP under an assumption excluding nontrivial end components. It uses converging upper and lower bounds and shows that their gap vanishes almost surely.

  • Assumption: The proof assumes that the MDP has no end components except trivial components containing terminal states 1 and 0.State 1 is the only target state, and state 0 is a sink.
  • Bound convergence: The proof tracks upper and lower action-value bounds whose limits are well defined and finite.For each state and action, the bounds satisfy an invariant ordering around the true value function.
  • Gap convergence: The limiting gap is shown to vanish almost surely by analyzing states and actions visited infinitely often during the algorithm's simulations.The argument assumes a positive limiting gap and derives a contradiction with the absence of nontrivial end components.
  • Theorem consequence: Consequently, Algorithm 1 almost surely terminates for every ϵ > 0 and returns a correct result.The correctness follows from the pointwise invariant U_i ≥ V ≥ L_i.

B Proof of Theorem 2: Analysis of the DQL algorithm

The DQL analysis establishes probabilistic guarantees for upper and lower reachability estimates under Assumption 1, using separate bound-update bookkeeping and contraction arguments. It culminates in an approximately optimal strategy and a bounded confidence interval after a stated number of steps.

  • Algorithm setup: Algorithm 6 initializes upper estimates to 1 except at target state 0, lower estimates to 0 except at target state 1, and tracks separate update statistics.The algorithm maintains accumulators, counters, timestamps, and learning flags for both bounds.
  • Algorithm operation: DQL explores by choosing uniformly among actions with maximal upper-bound estimates, sampling a successor, and updating upper and lower accumulators when their learning flags permit.Terminal states restart the simulation; otherwise exploration continues from the newly reached state.
  • Algorithm operation: Updating accumulators immediately, rather than after termination, changes iteration counts only by constant factors in the big-O analysis; stack-like propagation can accelerate convergence.The proof compares immediate, queue-like, and stack-like update orders.
  • Analytical foundations: The Bellman operator iterated |S| times is shown to be a contraction, yielding a unique solution to the associated Bellman system under the stated termination conditions.Banach's fixed-point theorem supplies uniqueness after the contraction result.
  • Probabilistic bounds: The analysis bounds update and failure events probabilistically, including at most |S||A| successful upper-value updates and probability δ/6 for violating Assumption 2.It also establishes that upper estimates remain above optimal values with the stated high probability.
  • Final guarantee: Under Assumption 1, Algorithm 6 follows an ε/2-optimal strategy on all but O(ζT δ)) steps and achieves U(s0) − L(s0) ≤ ε with probability at least 1 − δ.The same guarantee is stated in both the theorem and its extracted result passages.

C.1 Proofs of Lemma 1

The proof models exploration under a fixed memoryless strategy as a finite Markov chain, whose bottom strongly connected components correspond to end-components of the MDP. Standard recurrence bounds then show that repeated visits identify an end-component with high conditional probability.

  • Lemma 1 conclusion: If exploration does not terminate within 3i^3 iterations, the conditional probability that Appear(ω, i) is an end-component is at least 1 − 2c_i i^3 · (p_min/E_m)^−κ.The additional factor accounts for the probability of reaching a relevant bottom component.
  • Markov-chain construction: The EXPLORE phase induces a finite Markov chain whose states represent MDP state-action pairs and whose transitions incorporate successor probabilities and uniformly selected maximizing actions.This construction lets the proof apply Markov-chain recurrence arguments to MDP exploration.
  • Markov-chain construction: Every bottom strongly connected component of the induced chain determines an end-component of the MDP.Bottom components are recurrent classes visited almost surely on infinite paths.
  • Recurrence bound: With probability at least 1 − 2c_i i^3, a path reaches a bottom component and visits all its states at least i+1 times within the stated bounded exploration period.The bound combines failure to reach a bottom component with insufficient repeated visits.

C.2 Proofs of Lemma 2

The proof of Lemma 2 shows that processing an end-component preserves values outside it and assigns a uniform value throughout its states when the component is made terminal. The assigned value is 0 when it excludes the target and 1 when it contains the target.

  • Lemma 2 statement: Calling MAKETERMINAL with value i assigns VM(s) = i to every state s in the end-component.This is the first stated property of the procedure.
  • Lemma 2 statement: States outside the processed region retain their values after the procedure.The proof invokes the corresponding construction theorem for this preservation property.
  • Value assignment: If the end-component contains no target state, all its states have reachability value 0 because its actions remain closed within the component.No path from the component reaches the target under the stated construction condition.
  • Value assignment: If the end-component intersects the target set, uniformly selecting its designated actions visits all component states almost surely, giving every state reachability value 1.The proof uses almost-sure visitation of the component to establish target reachability.

C.3 Proofs of Lemma 3

The proof of Lemma 3 establishes that every MEC contained entirely in the explored-state set is also an end-component of the original MDP. This follows because the explored construction preserves the relevant states, actions, transitions, and connectivity.

  • Lemma 3 statement: Every MEC (R, B) in the constructed MDP with R ⊆ T is an end-component in the original MDP.This is the lemma's main claim.
  • Closure properties: The action set B remains enabled in the original MDP for every state in R.The construction preserves enabled actions on explored states.
  • Closure properties: Transitions under actions in B remain inside R, preserving the component's closure property.The transition functions agree between the constructed and original MDPs on these states and actions.
  • Connectivity: Every pair of states in R remains mutually reachable using actions from B, preserving strong connectivity.The required paths exist because the constructed MDP retains the same transitions on the relevant region.

D Proof of Theorem 3: Correctness of OBRTDP

The OBRTDP proof establishes that its bounds remain ordered around the true values despite end-component collapses, and that the algorithm almost surely terminates with a correct result. The argument reduces executions to a fixed collapsed MDP and uses end-component detection to show the remaining bound gaps vanish.

  • Bound invariants: OBRTDP preserves the invariant Ui(s,a) ≥ V(s,a) ≥ Li(s,a), including when end-components are collapsed.Collapsing end-components preserves the values of U, L, and V.
  • Fixing point: Each execution almost surely reaches a fixing point after which the current MDP remains unchanged.The stabilized MDP is obtained through finitely many end-component collapses.
  • Convergence argument: After the fixing point, states merged into the same collapsed state have identical limiting bound gaps.The proof denotes this common gap by δ(ξ) for each collapsed state ξ.
  • Convergence argument: A positive maximal limiting gap would imply an end-component among maximal-gap states, but on-the-fly detection would collapse it, yielding a contradiction.The contradiction shows that the maximal gap cannot remain positive.
  • Conclusion: Algorithm 1 with the stated UPDATE procedure and on-the-fly end-component detection almost surely terminates for every ε > 0 and returns a correct result.The correctness follows from the invariant Ui ≥ V ≥ Li together with convergence of the bounds.

E Proof of Theorem 4: Correctness of ODQL

The ODQL proof handles arbitrary MDPs by probabilistically controlling erroneous or unfinished end-component collapses and reducing the remaining analysis to an EC-free delayed Q-learning instance. It then transfers DQL’s error guarantee to obtain a correct approximation with controlled overall error.

  • End-component handling: The probability that a further collapse occurs can be made arbitrarily small after sufficiently many exploration phases.For any ε3, ε4 > 0, an i exists such that the probability of a later collapse is below ε4.
  • Probabilistic control: On executions where only end-components are collapsed, the collapsed MDP preserves the original values with probability at least 1 − ε3, while erroneous collapses are bounded by δ/2.The bound follows by choosing the exploration length parameters appropriately.
  • End-component handling: After sufficiently many exploration phases, each end-component is either never visited again or is visited infinitely often with value 1, with arbitrarily high probability.For any ε6, ε7 > 0, suitable j gives the stated behavior with probability at least 1 − ε7 after j + i exploration phases.
  • Transfer to DQL′: DQL′ on the almost-collapsed MDP preserves DQL’s error tolerance δ, including under conservative initializations of its upper and lower bounds.The proof uses the unique Bellman fixpoint in the relevant collapsed MDPs and notes that conservative bounds can only reduce later changes.
  • Final guarantee: With probability P(Good) − δ2, DQL′ returns correct bounds on the collapsed MDP, and the overall approximation error is controlled by running DQL with tolerance δ/4.The returned bounds are also the same on the pre-collapsed MDP on the good executions.
Loading 1402.2967v3…