Symbolic Model Checking of Logics with Actions

摘要: Reasoning about agents and modalities such as knowledge belief leads to models where different relations over states co-exist, or equivalently, information (labels, actions) is associated state transitions. This paper discusses how augment classical CTL symbolic model-checking support logics with actions A-CTL (action-CTL), this can be implemented using BDDs in tools the SMV/NuSMV package. Considering general action-state structures, we first propose a natural extension of actions, called Action-Restricted (ARCTL) adapt results from express model checking based on three functions eax, eauand eag. On these grounds, present two implementations actions. The approach encodes into pure state-based logics, that checked existing model-checkers. second consists native implementation extended operators. We report our prototype both approaches NuSMV give an overview used model-check temporal epistemic logic CTLK.