Source-linked AI summary
Path Abstraction for Markov Reward Models
Arnd Hartmanns, Robert Modderman
TL;DR
Path abstraction was established for refining counterexamples and computing reachability probabilities on DTMCs, but its extension to expected rewards required corresponding MRM guarantees. This paper develops that extension in a free-monoid framework, proves preservation and monotonic absorption, and provides a linear-equation recipe with a PARI/GP implementation. The computation is justified through the relationship between expected rewards and expected visiting times of transitions.
Problem
Path abstraction had been developed for reachability probabilities on DTMCs, leaving its extension to expected rewards on MRMs to be established.
Method
The paper formulates MRMs using free monoids, defines path abstraction over arbitrary state sets, and computes it through linear equation systems linked to expected visiting times.
Results
Path abstraction preserves MRM structure and monotonic absorption, and the proposed numerical computation matches the abstract formulation.
Takeaways & Limitations
Expected rewards can be handled by moving normalized expected rewards onto abstract transitions while preserving total expected accumulated rewards.
Takeaways & Limitations
An efficient implementation and heuristics for choosing abstraction sets remain future work.
Abstract
from arXiv · showhide
Path abstraction originated as a technique for counterexample refinement in probabilistic model checking. Given a discrete-time Markov chain, it summarises the probabilities passing through a subset of the states onto new transitions of a smaller chain. In earlier work, we proved its correctness and that it is monotonically absorbing. In this paper, we extend path abstraction from reachability probabilities on discrete-time Markov chains to expected rewards on Markov reward models. Working in a novel free monoid view of Markov chains throughout, we prove that path abstraction preserves the Markov reward model structure when abstracting over arbitrary sets of states, and that it remains monotonically absorbing. Finally, we give a numerical recipe, accompanied by a reference implementation in PARI/GP, that computes path abstraction by solving linear equation systems. Its correctness rests on the relationship between expected rewards and expected visiting times of transitions.
1 Introduction
This section motivates extending path abstraction from reachability probabilities on DTMCs to expected rewards on MRMs. It presents proofs for structural preservation and monotonic absorption, plus a linear-equation computation recipe.
- Motivation: Path abstraction reroutes probability mass through a chosen state set onto transitions of a smaller chain.It can also solve a DTMC locally, avoiding the transition blow-up possible with state elimination, although the smallest subproblems remain linear equation systems.
- Prior work: Earlier work proved that path abstraction preserves the DTMC structure and is monotonically absorbing for arbitrary abstraction sets.Monotonic absorption means abstracting first over a subset and then over a superset gives the same result as abstracting directly over the superset.
- Contributions: This paper extends path abstraction from reachability probabilities to expected accumulated rewards for reaching a goal in MRMs.The authors work in a free monoid view and prove preservation of MRM structure and monotonic absorption over arbitrary abstraction sets.
- Computation: The paper gives a numerical recipe and PARI/GP reference implementation that compute MRM path abstractions by solving linear equation systems.The concrete computation is justified using the relationship between expected rewards and expected visiting times of transitions.
2 Background
The background develops a free-monoid representation of paths, probabilities, and rewards. It then defines Markov chains and MRMs in that representation and situates them within probabilistic model checking.
- Free monoids and languages: The free monoid Σ* represents finite sequences over a state-space alphabet, with words, letters, concatenation, prefixes, factors, and languages as basic objects.The presentation introduces path concatenation and related language operations for reasoning about paths.
- Reduction: The reduction operator red(A, x) replaces maximal factors from A* by their first letters and prevents consecutive symbols from A in the reduced word.Examples include red({a,b})(a+bc) = ac and red({p,i,n,g}, mapping) = map.
- Probabilistic model checking: Probabilistic model checking asks for reachability probabilities and expected rewards before reaching absorbing goal states, using substochastic Markov chains when row sums need not equal one.The paper uses “Markov chain” for substochastic DTMCs, whose transition probabilities satisfy row sums at most one.
- Markov chains: A free-monoid Markov chain assigns transition probabilities directly to nonempty state sequences while satisfying normalization and the factorization P(xsy) = P(xs)P(sy).Singleton states have probability 1, and the sequence-based definition agrees with products of transition probabilities for paths.
- Markov reward models: A Markov reward model extends a Markov chain with a reward function that is additive across compatible path concatenations and zero on singleton or zero-probability sequences.Because path abstraction operates on transitions, the paper associates rewards with transitions in its free-monoid formulation.
3 Path Abstraction
Path abstraction removes internal states and replaces their behavior with transitions that preserve probabilities and expected rewards. For MRMs, the construction yields intermediate MRMs, supports monotonic absorption, and enables model checking through successive abstractions.
- Path abstraction construction: Path abstraction removes transitions involving non-input abstraction states and adds transitions connecting input states to output states.The new transitions summarize behavior inside the abstraction set.
- Path abstraction construction: For MRMs, each abstract transition receives the expected reward of paths through the abstraction set, normalized by their internal probability.The normalization of expected rewards is central to preserving monotonic absorption.
- Example: Successive abstractions can model-check an example locally, where the path s1s2s3s7 has probability 4/9 and reward 29.Its expected reward contribution is at least 4/9 · 29 > 10, establishing the original model’s expected reward exceeds 10.
- Path abstraction as model checking: Path abstraction over all nonabsorbing states stores each reachable goal’s probability and conditional expected reward on a direct transition from the initial state.For an absorbing goal t, the stored probability is Ps0(♢t), and the stored reward is Es0(♢t)/Ps0(♢t).
- Correctness: The construction produces another MRM and preserves reachability probabilities and expected rewards through monotonic absorption.These properties justify using intermediate MRMs for counterexample refinement.
4 Correctness Properties
Path abstraction is well-defined for Markov reward models and remains monotonically absorbing over nested abstraction sets. These properties support preserving the model structure while refining or fully model checking an MRM.
- 4.1 Well-definedness: Path abstraction over any subset of an MRM’s state space yields another MRM.The proof establishes both the Markov-chain structure and the reward-function axioms for the abstracted model.
- 4.1 Well-definedness: The abstracted reward function satisfies the required zero-value and additive decomposition properties for valid state sequences.The proof handles boundary cases and uses the free-monoid structure together with transition-probability factorisation.
- 4.2 Monotonic Absorption: For nested sets A ⊆ B, abstracting first over A and then over B produces the same MRM as abstracting directly over B.The transition probabilities follow from Markov-chain monotonic absorption; the reward functions are shown equal using normalised local expected rewards.
- 4.2 Monotonic Absorption: Monotonic absorption also means adding or removing isolated states does not affect the abstraction.Consequently, abstracting over a suitable superset can yield the result of fully abstracting over all eventually selected states.
5 Numerical Recipe
The numerical recipe computes abstract MRM rewards by reducing path sums to linear algebra. It uses transition expected visiting times and matrix powers to connect the concrete computation with the abstract formulation.
- Recipe setup: The recipe computes the abstract reward function on all two-state sequences, which determines rewards on every non-empty state sequence.It handles the nontrivial case through a linear equation system whose unknowns are the states in U.
- Matrix construction: The transient-state matrix T records transition probabilities within U, and Q = (1 −T)−1 sums all finite internal traversals.The construction relies on T having spectral radius less than 1.
- Main result: Theorem 5 expresses each abstract transition reward as a matrix-based sum of concrete transition rewards weighted by expected visiting information.The proof matches the contributions in the linear-algebra formula with the three cases of the expected-visiting-time expression.
- Expected visiting times: Expected visiting times count transition visits in the relevant sub-MRM, enabling path rewards to be rewritten as sums of transition rewards.For a transition ij, |y|ij counts its occurrences in path y, and evtij is its expected number of visits.
- Proof correspondence: The matrix products T^aTijT^b encode paths whose designated internal transition is ij, linking language probabilities to linear algebra.Tij retains only the probability of transition ij, forcing that transition at the corresponding position in the product.
6 Reference Implementation
The reference implementation extends path abstraction for reachability probabilities to expected rewards in PARI/GP. It computes state sets and matrices before handling abstract transition rewards through the linear-algebra formulation.
- Representation: The PARI/GP implementation represents an MRM with a probability matrix and a transition-reward matrix, using state 1 as the initial state.Rows and columns for states no longer relevant are set to zero.
- Computation: The implementation computes the sets I, O, U, and U1, constructs T and Q, and handles easy and hard cases for abstract rewards.The hard case corresponding to Theorem 5 is implemented in Listing 1 lines 22–33.
7 Conclusion and Future Work
The paper extends path abstraction to expected rewards in Markov reward models, proving structural preservation and monotonic absorption for arbitrary abstraction sets. It also provides a correct numerical recipe and reference implementation, while identifying efficient implementation and broader formalisation as future work.
- Path abstraction for MRMs preserves the MRM structure and remains monotonically absorbing over arbitrary sets of states.
- Each abstraction can be computed by solving one linear equation system, with a reference implementation provided in PARI/GP.
- The implementation reduces abstract path abstraction to concrete matrix problems and is proven correct using the connection between expected rewards and expected visiting times.
- Future work includes an efficient standalone or model-checking implementation and heuristics for choosing abstraction sets beyond SCC-based decomposition.
- Further directions include continuous-time Markov chains with time-bounded properties and machine-checked proofs with a correct-by-construction implementation.
A Additional Proofs
The additional proofs establish how abstraction preserves transition probabilities and rewards for paths involving abstract and interface states. They derive abstract rewards from probability-weighted rewards of concrete paths through the abstraction set.
- For paths outside the abstracted set and its interface, abstraction leaves probabilities unchanged and preserves rewards, including zero-probability paths.
- For positive-probability paths entering the abstraction set from an interface state and exiting to an outside state, the abstract reward averages concrete rewards over paths through the set.
- All remaining cases have zero abstract reward according to the proof.