Publications

Symbolic Model Checking of Logics with Actions

Authors
Charles Pecheur, Franco Raimondi
Tags
, , , , ,
Title
Symbolic Model Checking of Logics with Actions
Authors
Charles Pecheur, Franco Raimondi
mochart4.pdf Δ   216Kb   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 Tags: , , , , ,

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},
  }