# Lifted Model Checking for Relational MDPs

arXiv: https://arxiv.org/abs/2106.11735 · HTML: https://mlsanity.com/paper/2106.11735/

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- Builds on 7 of its 67 references that are in the map.
- First posted on arXiv 22 Jun 2021.

## Builds on (most cited first, 7 of 7)

- [Concrete Problems in AI Safety](https://mlsanity.com/paper/1606.06565/) (2016)
- [Safe Reinforcement Learning via Shielding](https://mlsanity.com/paper/1708.08611/) (2017)
- [Reinforcement Learning for Temporal Logic Control Synthesis with Probabilistic Satisfaction Guarantees](https://mlsanity.com/paper/1909.05304/) (2019)
- [Foundations for Restraining Bolts: Reinforcement Learning with LTLf/LDLf restraining specifications](https://mlsanity.com/paper/1807.06333/) (2018)
- [A storm is Coming: A Modern Probabilistic Model Checker](https://mlsanity.com/paper/1702.04311/) (2017)
- [Bounded Situation Calculus Action Theories](https://mlsanity.com/paper/1509.02012/) (2015)
- [Verification of Agent-Based Artifact Systems](https://mlsanity.com/paper/1301.2678/) (2013)

## Built on by (most cited first, 2 of 2)

- [Relational Action Bases: Formalization, Effective Safety Verification, and Invariants (Extended Version)](https://mlsanity.com/paper/2208.06377/) (2022)
- [Learning Probabilistic Temporal Safety Properties from Examples in Relational Domains](https://mlsanity.com/paper/2211.03461/) (2022)

## Abstract (arXiv)

Probabilistic model checking has been developed for verifying systems that have stochastic and nondeterministic behavior. Given a probabilistic system, a probabilistic model checker takes a property and checks whether or not the property holds in that system. For this reason, probabilistic model checking provide rigorous guarantees. So far, however, probabilistic model checking has focused on propositional models where a state is represented by a symbol. On the other hand, it is commonly required to make relational abstractions in planning and reinforcement learning. Various frameworks handle relational domains, for instance, STRIPS planning and relational Markov Decision Processes. Using propositional model checking in relational settings requires one to ground the model, which leads to the well known state explosion problem and intractability. We present pCTL-REBEL, a lifted model checking approach for verifying pCTL properties of relational MDPs. It extends REBEL, a relational model-based reinforcement learning technique, toward relational pCTL model checking. PCTL-REBEL is lifted, which means that rather than grounding, the model exploits symmetries to reason about a group of objects as a whole at the relational level. Theoretically, we show that pCTL model checking is decidable for relational MDPs that have a possibly infinite domain, provided that the states have a bounded size. Practically, we contribute algorithms and an implementation of lifted relational model checking, and we show that the lifted approach improves the scalability of the model checking approach.