Automatic Verification of Knowledge and Time with NuSMV

1 Introduction

Epistemic logic [Fagin et al., 1995; Meyer and Hoek, 1995] has traditionally played an important role in Artificial Intelligence (AI). Not only does epistemic logic provide a formal basis for reasoning about states of knowledge in automatic reasoners but it can also be seen as a formal specification language to reason about artificial agents. Indeed, epistemic concepts are particularly appropriate in multi-agent systems (MAS) as knowledge constitutes the basis for rational action. In this line of work typically one considers the epistemic modal logic S5n combined with a temporal logic for branching time or linear time interpreted on computationally grounded semantics [Wooldridge, 2000] such as the one of interpreted systems [Fagin et al., 1995], or a suitable variation of it [Wooldridge and Lomuscio, 2000].

While much attention in the 80s and 90s focused on proving meta-logical results (notably completeness and computational complexity) for various temporal and epistemic combinations [Halpern and Moses, 1992; Meyden, 1994; Meyden and Wong, 2003], considerable attention has been given in the past few years to the problem of devising model checking techniques for these formalisms [Hoek and Wooldridge,

∗The author acknowledges support from EPSRC grant GR/S49353.

†With RIACS at NASA Ames while performing this work.

‡With MCT at NASA Ames while performing this work. The author acknowledges support from EPSRC grant CNA/04/04.

2002; Gammie and van der Meyden, 2004; Raimondi and Lomuscio, 2005; Penczek and Lomuscio, 2003]. These efforts are strictly related to the recent shift of attention from theorem proving to model checking as suggested, among others, in [Halpern and Vardi, 1991].

This article intends to make a contribution in this line by proposing an efficient model checking technique for verifying CTLK (an epistemic logic on branching time [Penczek and Lomuscio, 2003]) based on NuSMV [Cimatti et al., 2002], a mainstream model checker for temporal logic. Specifically the present article makes the following points. First, it is shown that the model checking of CTLK can be (automatically) rephrased as the one of model checking the actionbased temporal logic ARCTL [Pecheur and Raimondi, 2006]. Second, we present an automatic translator from an SMV-like language for a semantics of MAS for the extension above. The main benefits of this proposal against the current stateof-the-art lies in the efficiency of the approach which we try to demonstrate by discussing experimental results.

2 Preliminaries

We summarise the formalism of interpreted systems in Section 2.1, a formalism to reason about time and knowledge in a system of agents. In Section 2.2 we discuss the problem of model checking using NuSMV.

2.1 Interpreted systems and CTLK

The formalism of interpreted systems, introduced in [Fagin et al., 1995], provides a formal framework to reason about time and knowledge in a system of agents. Let Σ be a set of n agents: Σ = {1, . . . , n}. A set of local states Li and a set of actions Acti is associated to each agent i, together with a protocol Pi : Li → 2Acti assigning a list of enabled actions to each local state. The local states of an agent change according to a local evolution function ti : Li × LE × Act → Li, where LE is the set of local states of a special agent in Σ (the environment), and Act = Act1 × . . . × Actn. The set S = L1 × . . . × Ln is called the set of global states. Given a set of initial global states I ⊆ S, the set G ⊆ S representing the set of reachable states is generated by the evolution of I and in accordance with the protocol and the agents' local evolution functions 1 . Given a set of atomic propositions AP

1 The system evolves synchronously, i.e, at each time step all the agents perform a move.

and an interpretation V ⊆ S × AP, an interpreted system is a tuple

The logic CTLK combines the traditional AI epistemic logic S5n with the temporal logic CTL. Specifically, the syntax of CTLK is defined as follows:

where Kiϕ is read as "agent i knows ϕ" and the CTL operators have the standard meaning - for example, EGϕ is read as "there exists a path where ϕ holds forever". Other derived operators are defined in a standard way (see e.g. [Clarke et al., 1999; Fagin et al., 1995]). To evaluate CTLK formulae, a Kripke model MIS = (W, I, Rt, ∼1, . . . , ∼n, V ) is associated to a given interpreted system IS, as follows: W is the set G of reachable states, I ⊆ W is the set of initial states, the temporal relation Rt ⊆ W × W is obtained using the protocols Pi and the evolutions functions ti, the epistemic relations ∼i ⊆ W × W, for i ∈ Σ, are defined by checking the equality of the i-th local component of two global states (i.e., (l1, . . . , ln) ∼i (l′1 , . . . , l′n) iff li = l′i ), and V is the evaluation relation appearing in IS2 .

The formulae defined by (1) are interpreted in MIS in a standard way: we refer to [Clarke et al., 1999; Fagin et al., 1995; Penczek and Lomuscio, 2003] for the formal definition of M |= ϕ, where |= is the standard satisfaction relation.

2.2 Model checking using NuSMV

Given a Kripke model M and a formula ϕ, model checking is defined as the problem of establishing whether or not M |= ϕ. In this approach M represents the system to be checked and ϕ the specification of the system. In the last fifteen years techniques and tools have been developed to perform the verification task in an automatic way, mainly for temporal models and temporal specifications. NuSMV [Cimatti et al., 2002] is a mature model checker for temporal logics and it has been employed in the verification of a number of examples. Other very successful model checkers exist, notably Spin [Holzmann, 1997], Verics [Nabialek et al., 2004], etc.

NuSMV has a dedicated modelling language (the SMV language), which permits the definition of the temporal model in an expressive, compact and modular way. NuSMV avoids building or exploring the state space corresponding to its models explicitly; instead, NuSMV applies symbolic techniques based on ordered binary decision diagrams (OBDDs) or propositional satisfiability (SAT) solvers to efficiently perform verification over large state spaces.

NuSMV is a command line tool available for most operating systems, and its source code is available under the terms of the GNU General Public License (GPL).

3 Model checking MAS: state of the art

Recently, different approaches have been proposed to extend model checking techniques from temporal logics to richer logics, with the aim of verifying knowledge-based and agentbased systems. Two main streams can be identified in the recent literature:

2 Note that W is, by definition, the reachable state space, i.e. it only contains states that are reachable from I through Rt. This condition is crucial for the proper interpretation of ∼i and Kiϕ.

1. Dedicated tools. Works along this line include the model checker MCK (Model Checking Knowledge, [Gammie and van der Meyden, 2004]), implementing the verification of certain classes of interpreted systems. Verics [Nabialek et al., 2004] is a model checker for MAS described using networks of timed automata. MCMAS [Raimondi and Lomuscio, 2005] is an OBDD-based model checker for MAS described in interpreted systems.
2. Extensions (and translations) to existing tools. [Hoek and Wooldridge, 2002] propose the use of local propositions to reduce the problem of model checking knowledge and time to the verification of a temporalonly model. [Wooldridge et al., 2002] define the MABLE language, and they show how the verification of this language can be reduced to the verification of PROMELA code (the input language of the model checker SPIN [Holzmann, 1997]). Similarly, [Bordini et al., 2003] introduce the language AgentSpeak(F), and they present a translation into PROMELA code.

Experimental results from the papers cited above show that, on average, purpose-built tools can handle larger examples, and that trying to use existing tools often requires manual intervention. We show below this is not necessarily the case. In the remainder of this paper our aim is to introduce a fully automated methodology that builds upon an existing tool (NuSMV) and show that it performs comparably or better than similar approaches.

4 Model checking CTLK in NuSMV

This section introduces the logic ARCTL (Action-Restricted CTL) and a proposed extension to NuSMV thereby enabling the verification of ARCTL operators. In Section 4.2 we show how the problem of model checking for CTLK can be reduced to the problem of model checking for ARCTL, thereby permitting the verification of CTLK by using NuSMV. In addition, in Section 4.3 we present an SMV-like language for interpreted systems and its translation into SMV code.

4.1 The logic ARCTL

The logic ARCTL [Pecheur and Raimondi, 2006] extends the logic CTL by allowing quantification over action labelled paths. More in detail, given a set of atomic propositions AP and a set of atomic actions AA, the syntax of ARCTL is defined as:ϕ

where ϕ and α are state and action formulae and p ∈ AP, b ∈ AA are atomic propositions over states and actions, respectively. Similarly to CTL, other temporal operators can be derived in a standard way.

A model for ARCTL is a tuple of the form M = (S, S0, A, T, VP , VA), where S is a set of states, S0 ⊆ S is a set of initial states, A is a set of actions, T ⊆ S × A × S is a transition relation (notice the dependence on actions), VP : S → 2AP is an interpretation for atomic propositions, and VA : A → 2AA is an interpretation for atomic actions. Given a model M = (S, S0, T, VP , VA), the α-restriction of M, denoted by Mα, is a model Mα = (S, S0, Tα, VP , VA), where Tα is a transition relation such that (s, a, s′ ) ∈ Tα iff (s, a, s′ ) ∈ T and a |= α (where |= is the natural extension of VA to propositional formulae α). We refer to [Pecheur and Raimondi, 2006] for further details.

For model checking purposes, we have extended NuSMV to support the verification of ARCTL formulae. We used NuSMV existing "input" variables to model ARCTL actions. In particular, we have modified the syntax of the formulae accepted by NuSMV as follows:

ctlexpr ::= . . . (existing CTL forms) EAX(simpleexpr)ctlexpr EAG(simpleexpr)ctlexpr EA(simpleexpr)[ctlexpr U ctlexpr]

where simpleexpr is a conditional expression, further restricted to contain only input variables. For example, EA(a)[p U q] is the concrete syntax for Ea[pUq]. Additionally, we have implemented extensions to the NuSMV code base to enable the verification of these operators (the details of these modifications are beyond the scope of this paper, we refer to [Pecheur and Raimondi, 2006] for further details).

4.2 Reducing CTLK to ARCTL

The problem of model checking CTLK (see Section 2.1) can be reduced to the problem of model checking ARCTL. Specifically, given a CTLK model MK and a CTLK formula ϕK, we can define an ARCTL model M = F (MK ) and an ARCTL formula F(ϕK) such that MK |= ϕK iff F(MK) |= F(ϕK). Let Σ = {1, . . . , n} be a set of agents, and let MK = (W, I,Rt, {∼i}i∈Σ, V ) be a model associated to some interpreted system IS = 〈(Li,Acti, Pi, ti)i∈Σ , I, V 〉. The model F(MK) is an ARCTL model M = (S, S0, A, T, VP , VA) such that

• S = W and S0 = I;
• the set AA = {Run,Agt1, . . . ,Agtn} contains a proposition Run to label temporal transitions (defined by Rt) and n propositions Agti (one for each agent) to label epistemic equivalence steps (defined by ∼i), and the action set A is 2AA;
• the transition relation T combines the temporal transition Rt and the epistemic relations {∼i}i∈Σ in the following way: for states s, s′ ∈ W, (i) (s, {Run}, s′) ∈ T iff sRts′ ; (ii) (s, {Agti}, s′) ∈ T iff s ∼i s′ ; (iii) (s, {a1, . . . , ak}, s′ ) ∈ T iff (s, {ai}, s′) for all 1 ≤ i ≤ k. 3

3 Case (iii) is necessary for interpreting distributed knowledge operators, but this discussion is beyond the scope of this paper.

The translation of a temporal-epistemic formula into an ARCTL formula is inductively defined as follows:

• F (p) = p, if p is a propositional formula.
• F(EXϕ) = ERunXϕ; F(E[ϕUψ]) = ERun[ϕUψ]; F (EGϕ) = ERunGϕ; F(Kiϕ) = AAgti Xϕ.

In other words we use the labels Run (Agti, respectively) to denote a temporal relation (the epistemic relation for agent i, respectively). This translation allows us to model check CTLK formulas by model checking their translations in ARCTL. Clearly a similar approach can be used for more complexmodal logics.

The translation from an interpreted system IS to the ARCTL model F(MIS) is performed automatically by a translator we have implemented (see next section).

4.3 An SMV-like language for interpreted systems

We have designed extensions of the SMV language for the description of interpreted systems and CTLK formulae. These extensions can be translated to into a standard SMV model and ARCTL formulae. Concretely, the extensions are defined as a library of M4 macros 4 . The work flow needed to perform verification of an interpreted system is summarised in Figure 1. Notice that the only manual intervention is the provision of the input file describing the problem to be verified.

In this language, an agent <name> is associated with the SMV variables <v1>,..,<vn> that define its local state, through a declaration AGENT(<name>,<v1>,..,<vn>). The actions of each agent are represented as input variables (IVAR). The protocol of each agent is described as a relation between its local state and action variables (within an SMV TRANS statement). The transition function is encoded using a new TTRANS statement, and initial conditions using a new TINIT statement. Figure 2 shows the structure of a typical definition of a class of agents as an SMV module (note that "--" starts comments in SMV, see [Cimatti et al., 2002] for details).

4 M4 [Kernighan and Ritchie, 1977] is a general-purpose macro processor available on most UNIX platforms.

MODULE anAgent(args,ENV) -- an agent module VAR local : {...}; -- the local state AGENT(me,local) -- declare the local state IVAR action : {...}; -- actions of the agent TINIT( ... ); -- initial conditions TRANS( action = case ... ) -- the agent's protocol TTRANS( NEXT(local) = case ... ) -- the agent's evolution function MODULE main -- main module VAR_ENV -- declare ENV variables VAR alice : anAgent(args1,ENV) ; -- an agent bob : anAgent(args2,ENV) ; -- another agent

Internally, the translation generates additional Boolean variables IVARS corresponding to the Run and Agti propositions of the ARCTL model (e.g. RUN, bob.me and alice.me in the model of Fig. 2), and TTRANS statements expand to standard TRANS statements conditioned on RUN.

Note that the state space of the NuSMVmodel is not a priori restricted to the (temporally) reachable states; this has to be imposed by the translation scheme. A state is reachable iff it can be reached from the initial states through a series of temporal steps (or, equivalently, iff there exists a reverse path from that state back to the initial set). Assuming we have access to reverse temporal transitions through some action condition Back in our ARCTL model, and a state condition Init for initial states, the set of the (temporally) reachable states is captured by the following ARCTL formula:

Since this is a temporal formula, it has to be folded into NuSMV properties; it cannot be used in the NuSMV model itself. For example, the CTLK formula Kiϕ expands to the ARCTL formula AAgti X(Reachable → ϕ).

Our library implements this scheme. In particular, the TTRANS construct implements an encoding scheme allowing temporal transitions to be traversed both forwards and backwards. On the specification side, new operators TAX, TAG, etc. provide the equivalent of SMV's built-in AX, AG, etc., restricted to temporal transitions, and a new operator KK implements Kiϕ. For instance, the CTLK formula AG(Ka(p∨q)) expressing that agent a always knows either p or q, is written as TAG(KK(a,p|q)).

5 Example application

In this section we model the protocol of the dining cryptographers using the formalism presented in Section 2.1, in order to enable its verification using the methodology presented in Section 4.2. The protocol was introduced by Chaum in [Chaum, 1988], and was modelled using agents by various authors [van der Meyden and Su, 2004; Raimondi and Lomuscio, 2005; Kacprzak et al., 2006]. The aim of this protocol is to allow the anonymous broadcasting of messages, and it is usually introduced using the following scenario (wording from [Chaum, 1988]):

"Three cryptographers are sitting down to dinner at their favorite three-star restaurant. Their waiter informs them that arrangements have been made with the maitre d'hotel for the bill to be paid anonymously. One of the cryptographers might be paying for dinner, or it might have been NSA (U.S. National Security Agency). The three cryptographers respect each other's right to make an anonymous payment, but they wonder if NSA is paying. They resolve their uncertainty fairly by carrying out the following protocol:

Each cryptographer flips an unbiased coin behind his menu, between him and the cryptographer on his right, so that only the two of them can see the outcome. Each cryptographer then states aloud whether the two coins he can see-the one he flipped and the one his left-hand neighbour flipped-fell on the same side or on different sides. If one of the cryptographers is the payer, he states the opposite of what he sees. An odd number of differences uttered at the table indicates that a cryptographer is paying; an even number indicates that NSA is paying (assuming that dinner was paid for only once). Yet if a cryptographer is paying, neither of the other two learns anything from the utterances about which cryptographer it is"

This protocol can be extended to any number n of cryptographers greater than three. We encode the scenario by using an interpreted system by introducing n agents C1, . . . ,Cn, and one agent E to represent the environment (which selects the payer and the result of coin tosses at the beginning of each run, non-deterministically) [Raimondi and Lomuscio, 2005].

The local state of cryptographer Ci is modelled using three variables equali, paidi, eveni, representing respectively whether the coins that Ci can see are equal or different, whether Ci is the payer, and whether the number of different utterances reported is even. 5 The list of actions for each cryptographer includes the actions do nothing, say equal, and say different, performed in compliance with the description provided above. In the initial state the variables for each cryptographer are initialised to a null value, and they are updated in the first time step, to reflect the environment's configuration. At this point, each cryptographer utters the appropriate phrase (represented by say equal or say different) and the variable storing the value of "different" utterances (either even or odd) is appropriately updated.

The key properties of this scenario [van der Meyden and Su, 2004] are easy to express using CTLK. For instance:

Formula (4) expresses the property that, if the first cryptographer did not pay for the dinner and there is an odd number of utterances, then, upon update of his local state, the first cryptographer knows that someone of the remaining cryptographers paid for the dinner, but the first cryptographer does not know who the payer is. Formula (5) expresses the property that if the number of utterances is even, the first cryptographers knows that nobody paid for the dinner.

5 We refer to [Kacprzak et al., 2006] for other possible encodings of the same protocol. Our choice here is motivated by the need of comparing our experimental results with the ones in [Raimondi and Lomuscio, 2005; Kacprzak et al., 2006].

We have encoded this scenario using the language presented in Section 4.3 and we have been able to verify the example for up to nine cryptographers 6 . Experimental results are reported in the next section.

6 Experimental results

Table 1 reports the time results obtained in the verification of the example presented in the previous section, as a function of the number of cryptographers (first column). The third column reports the time required for the verification of the formulae 4 and 5 (appropriately translated into ARCTL formulae). The second column reports the number of Boolean variables required to encode the example (see [Clarke et al., 1999] for more details on this technique), and provides an estimate for the size of the model; for instance, 137 Boolean variables are required to encode an example with 7 cryptographers, corresponding to a maximal state space of size 2137 ≈ 1041.

The fourth and fifth columns report the time results obtained in the verification of the protocol of the dining cryptographers using the model checkers MCMAS and Verics, as reported in [Raimondi and Lomuscio, 2005; Kacprzak et al., 2006], for the verification of the same formulae mentioned above, as a function of the number of cryptographers. Notice that, in the case of MCMAS, the verification time does not depend on the formula being verified and it is usually a fraction of the time spent in reading and parsing the model (the opposite is true for NuSMV, because of different implementation choices). The last column reports the time results for Verics. Differently from the previous two cases, Verics's results are based on an implementation of Bounded Model Checking for CTLK. [Penczek and Lomuscio, 2003]. Due to this, Verics's performance for this two formulae is worse than the other two model checkers, but Verics is normally capable of finding counterexamples for false formulae effectively: in [Kacprzak et al., 2006] it is shown that certain false formulae can be verified in scenarios with up to 100 cryptographers. Neither MCMAS nor the technique of this article can handle this magnitude of state spaces.

6.1 Discussion

A comparison of the results obtained with the three model checkers is reported in Figure 3. Clearly for the formulae considered here the approach presented here performs moderately better than MCMAS and VERICS. The better performance is due to the optimisation techniques implemented in NuSMV (such as on-the-fly model checking and caching). Obviously, experimental results depend on the examples tested and it is not appropriate to draw final conclusions on one example only. Additionally, we would expect VERICS to outperform the approach presented here when trying to falsify formulas on very large state spaces. Nevertheless, we think the discussion above shows that the technique presented here can significantly complement the other model checkers in many instances.

6 The source code for these examples is available from http://www.cs.ucl.ac.uk/staff/f.raimondi/dincrypt-code.zip.

We could not compare our methodology to other existing approaches based on existing model checkers (see Section 3). Indeed, such approaches often require a manual intervention in the translation from their specific programming language into the programming language of the temporal model checkers, and this is not feasible for large examples such as the one considered here.

7 Conclusion

In this paper we have presented a novel technique for model checking CTLK that relies on the translation of this logic into action-based temporal logic and model checking of this logic with NuSMV. The approach is sound and complete and our implementation shows experimental results that are in line with or better than existing specialised tools.

The use of macros for extending the NuSMV language has allowed for easy prototyping but limits the syntactic flexibility. A more natural syntax could be supported with more involved translation facilities. Further planned work includes investigating optimisation of the verification scheme, both at the level of the translation from CTLK to ARCTL and through additional extensions or optimizations of NuSMV itself. Moreover, we limited our analysis to dining cryptographers because this is the only scenario for which experimental results are available in the literature. In future work we certainly plan to use the technique and tool presented here to investigate more realistic scenarios.

Another important issue to be addressed is the handling of witness traces generated by NuSMV, which need to be formulated back in terms of the original CTLK model. We would also like to investigate using NuSMV's SAT-based bounded model checking capabilities rather than the current OBDDbased approach. Given the limitation of NuSMV, this requires shifting from branching to linear temporal logic, requiring a new and more restrictive encoding scheme for CTLK properties. The feasibility and applicability of such a scheme remains to be explored.