Lifted model checking for relational MDPs
2022 (English)In: Machine Learning, ISSN 0885-6125, E-ISSN 1573-0565, no 111, p. 3797-3838Article in journal (Refereed) Published
Abstract [en]
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.
Place, publisher, year, edition, pages
Springer, 2022. no 111, p. 3797-3838
Keywords [en]
Model checking, Probabilistic computation tree logic (pCTL), First-order logic, Lifted inference, Relational MDPs
National Category
Computer Sciences
Identifiers
URN: urn:nbn:se:oru:diva-100471DOI: 10.1007/s10994-021-06102-7ISI: 000814940000001Scopus ID: 2-s2.0-85132573747OAI: oai:DiVA.org:oru-100471DiVA, id: diva2:1688358
Funder
Knut and Alice Wallenberg Foundation
Note
Funding agencies:
FNRS-FWO joint programme under EOS 30992574
Flemish Government under the "Onderzoeksprogramma Artificiele Intelligentie (AI) Vlaanderen" programme
EU H2020 ICT48 project "TAILOR" 952215
Wallenberg AI, Autonomous Systems and Software Program (WASP)
KU Leuven
2022-08-182022-08-182023-12-08Bibliographically approved