Symbolic Model Checking of Logics with Actions
(2007) Proceedings of MOCHART 4: Model Checking and Artificial Intelligence — Location: Riva del Garda, Italy (29.August.2006)
Files
mochart4.pdf
Restricted Access - Adobe PDF
- 215.59 KB
Details
- Authors
- Abstract
- Reasoning about agents and modalities such as knowledge and belief leads to models where different relations over states co-exist, or equivalently, where information (labels, actions) is associated to state transitions. This paper discusses how to augment classical CTL symbolic model-checking to support logics with actions such as A-CTL (action-CTL), and how this can be implemented using BDDs in tools such as the SMV/NuSMV package. Considering general action-state structures, we first propose a natural extension of CTL to actions, called Action-Restricted CTL (ARCTL) and adapt classical results from CTL to express model checking based on three functions $eax$, $eau$ and $eag$. On these grounds, we present two different implementations of symbolic model checking with actions. The first approach encodes action-state models and logics into pure state-based models and logics, that can be checked with existing model-checkers. The second approach consists in a native implementation of the three extended operators. We report on our prototype implementation of both approaches based on NuSMV and give an overview of how this is used to model-check the temporal epistemic logic CTLK.
- Affiliations
University College London Department of Computer Science
Citations
Pecheur, C., & Raimondi, F. (2007). Symbolic Model Checking of Logics with Actions. In Stefan Edelkamp and Alessio Lomuscio (ed.), Model Checking and Artificial Intelligence (pp. 113-128). Springer. https://hdl.handle.net/2078.5/229814