A Framework for Belief-based Programs and Their Verification
Authors: Daxin Liu, Gerhard Lakemeyer
JAIR 2025 | Venue PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Theoretical | In this paper, we propose a formalism for belief programs based on a modal logic of actions and beliefs which allows us to conveniently express PCTL-like temporal properties. We also investigate the decidability and undecidability of the verification problem. The verification problem is undecidable because belief programs are probabilistic variants of Golog programs with sensing, for which undecidability was shown by Zarrieß and Claßen (2016). |
| Researcher Affiliation | Academia | Daxin Liu EMAIL Nanjing University Nanjing, Jiangsu 210023 China Gerhard Lakemeyer EMAIL RWTH Aachen University Aachen, NRW 52074 Germany |
| Pseudocode | Yes | Table 1: An online belief program for the coffee robot. 1 while B(hpos = 2) < 1 do 2 east(1)|sensecoffee; 3 end While |
| Open Source Code | No | The paper does not contain any explicit statements or links indicating that the source code for the methodology described in this paper is publicly available. It mentions using existing model-checking tools but does not provide its own implementation. |
| Open Datasets | No | As an illustrative example, consider a robot searching for coffee in a one-dimensional world as in Fig 1. Initially, the horizontal position hpos of the robot is at 0 and the coffee is at 2, the space is infinite, namely hpos could be any integer. |
| Dataset Splits | No | The paper focuses on theoretical contributions and illustrative examples, not on empirical evaluations with datasets. Therefore, no dataset splits are mentioned or applicable. |
| Hardware Specification | No | The paper primarily presents a theoretical framework and does not describe any experiments that would require specific hardware specifications. |
| Software Dependencies | No | The paper mentions exploiting existing model-checking tools like Prism (Kwiatkowska et al., 2011) or Storm (Hensel et al., 2022) but does not specify the version numbers of these or any other software dependencies used for their work. |
| Experiment Setup | No | The paper is theoretical in nature and does not describe any experimental setups, hyperparameters, or training configurations. |