Symbolic Model Checking of Logics with Actions
- Title
- Symbolic Model Checking of Logics with Actions
- Authors
- Charles Pecheur, Franco Raimondi
FM2018 Δ | 0Kb | 28 May 2020 |
Fmics2013 Δ | 0Kb | 28 May 2020 |
GandALF2017 Δ | 0Kb | 28 May 2020 |
HMI2011 Δ | 0Kb | 28 May 2020 |
LVLPrivate Δ | 0Kb | 28 May 2020 |
LVLPrivateNews Δ | 0Kb | 28 May 2020 |
Main Δ | 0Kb | 28 May 2020 |
Members Δ | 0Kb | 28 May 2020 |
Publications Δ | 4Kb | 28 May 2020 |
Site Δ | 0Kb | 28 May 2020 |
Talks Δ | 4Kb | 28 May 2020 |
Tools Δ | 0Kb | 28 May 2020 |
- Type
- In Proceedings
- Book title
- Workshop on Model Checking and Artificial Intelligence (MOCHART), Riva del Garda, Italy, 29 Aug 2006
- Series
- LNAI
- Volume
- 4428
- Editor
- Springer
- Year
- 2007
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 ex- press 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.
Tags: Symbolic Model Checking, CTL, Actions, SMV, Epistemic Logic, Project NASA
- BibTeX Record
@INPROCEEDINGS{lvl-2007-3, TITLE = {Symbolic Model Checking of Logics with Actions}, AUTHOR = {Charles Pecheur and Franco Raimondi}, YEAR = {2007}, VOLUME = {4428}, EDITOR = {Springer}, SERIES = {LNAI}, URL = {https://lvl.info.ucl.ac.be/Publications/SymbolicModelCheckingOfLogicsWithActions}, }