Pecheur, C.; Raimondi, F.; (2006) Symbolic model checking of logics with actions. In: Edelkamp, S. and Lomuscio, A., (eds.) Model Checking and Artifical Intelligence: 4th Workshop, MoChArt IV, Riva del garda, Italy, August 29, 2006, Revised Selected and Invited Papers. (pp. pp. 113-128). Springer Verlag: Berlin/ Heidelberg, Germany.

Preview

PDF 5625.pdf Download (222kB)

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.

Download activity - last month

Export as JSONCSVXML

Download activity - last 12 months

Export as XMLCSVJSON

Downloads by country - last 12 months

Export as XMLCSVJSON

Archive Staff Only

View Item