To Örebro University

oru.seÖrebro University Publications
Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Lifted model checking for relational MDPs
Department of Computer Science, KU Leuven, Leuven, Belgium.
Université libre de Bruxelles, Campus de la Plaine, Bruxelles, Belgium.
Örebro University, School of Science and Technology. (Centre for Applied Autonomous Sensor Systems)ORCID iD: 0000-0002-6860-6303
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

Available from: 2022-08-18 Created: 2022-08-18 Last updated: 2023-12-08Bibliographically approved

Open Access in DiVA

No full text in DiVA

Other links

Publisher's full textScopus

Authority records

De Raedt, Luc

Search in DiVA

By author/editor
De Raedt, Luc
By organisation
School of Science and Technology
In the same journal
Machine Learning
Computer Sciences

Search outside of DiVA

GoogleGoogle Scholar

doi
urn-nbn

Altmetric score

doi
urn-nbn
Total: 60 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf