Name
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, eauand 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. |
Year | DOI | Venue |
|---|---|---|
2006 | 10.1007/978-3-540-74128-2_8 | MoChArt |
Keywords | Field | DocType |
action-restricted ctl,native implementation,model checking,action-state model,classical result,symbolic model checking,different implementation,nusmv package,different relation,classical ctl symbolic model-checking,general action-state structure | Epistemic modal logic,Computation tree logic,Kripke structure,Model checking,Theoretical computer science,Operator (computer programming),CTL*,Mathematics,EAX mode,Symbolic trajectory evaluation | Conference |
Volume | ISSN | Citations |
4428 | 0302-9743 | 28 |
PageRank | References | Authors |
1.11 | 12 | 2 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Charles Pecheur | 1 | 284 | 28.50 |
| Franco Raimondi | 2 | 832 | 48.18 |