PEDECIBA Informática Instituto de Computación – Facultad de Ingeniería Universidad de la República Montevideo, Uruguay

Reporte Técnico RT 14-13

Formalizing alternating-time temporal logic In the coq proof assistant

Carlos Luna – Luis Sierra – Dante Zanarini 2014

Formalizing alternating-time temporal Logic in the coq proof assistant Carlos Luna, Luis Sierra, Dante Zanarini ISSN 0797-6410 Reporte Técnico RT 14-13 PEDECIBA Instituto de Computación – Facultad de Ingeniería Universidad de la República Montevideo, Uruguay, 2014

Formalizing Alternating-time Temporal Logic in the Coq Proof Assistant Carlos Lunaa , Luis Sierraa , Dante Zanarinib,c a Instituto

de Computaci´ on, Facultad de Ingenier´ıa, Universidad de la Rep´ ublica, Uruguay b CIFASIS-CONICET, Argentina c Universidad Nacional de Rosario, Argentina

Abstract This work presents a complete formalization of Alternating-time Temporal Logic (ATL) and its semantic model, Concurrent Game Structures (CGS), in the Calculus of (Co)Inductive Constructions, using the logical framework Coq. Unlike standard ATL semantics, temporal operators are formalized in terms of inductive and coinductive types, employing a fixpoint characterization of these operators. The formalization is used to model a concurrent system with an unbounded number of players and states, and to verify some properties expressed as ATL formulas. Unlike automatic techniques, our formal model has no restrictions in the size of the CGS, and arbitrary state predicates can be used as atomic propositions of ATL. Keywords: Reactive Systems and Open Systems, Alternating-time Temporal Logic, Concurrent Game Structures, Calculus of (Co)Inductive Constructions, Coq Proof Assistant.

1. Introduction Linear-time and branching-time temporal logics are natural specification languages for reactive systems [1, 2]. Alternating-time Temporal Logic (ATL), introduced by Alur, Henzinger and Kupferman [3, 4], is a temporal logic suitable for open systems specifications, where an open system is a system that interacts with its environment and whose behavior depends on the state of the system as well as the behavior of the environment [4]. The logic ATL offers selective quantification over those paths that are possible outcomes of games. For instance, by preceding the temporal operator “eventually” with a selective path quantifier, it is possible to specify that in a game between a reactive system and the environment, the system has a strategy to reach a certain state. Email addresses: [email protected] (Carlos Luna), [email protected] (Luis Sierra), [email protected] (Dante Zanarini)

September 22, 2014

An ATL formula is interpreted over Concurrent Game Structures (CGS) [4]. Every state transition of a CGS results from a simultaneous choice of moves, one for each player. The players represent individual components and the environment of an open system. CGS can capture various forms of synchronous composition for open systems, and if augmented with fairness constraints, also asynchronous composition. ATL naturally describes, also, computations of multi-agent systems [5, 6, 7]. In multi-agent systems, different processes can have distinct goals and the interactions between them may be adversarial or cooperative. Interactions between processes in multi-agent systems can thus be seen as games in the classical framework of game theory, with adversarial coalitions [8, 9]. Our contributions In this work we formalize the CGS semantics of ATL in the Calculus of (Co)Inductive Constructions (CIC) [10, 11, 12], using the logical framework Coq [13, 14]. This formalization is divided in two parts: the logic ATL and the CGS semantics for a given game structure S. We show that the proof of the Coq proposition ϕ q guarantees that the CGS S satisfies the ATL formula ϕ in the state q of S (i.e. q |= ϕ). Moreover, the proposed deductive system is complete: whenever q |= ϕ we can prove ϕ q. This work uses a general approach to deal with CGS where the number of states is unbounded; this generality is scarcely obtained using standard model checking techniques [15]. There are works that formalize temporal logics in the CIC (in Coq). We can mention the formalization of LTL [16] and Computation Tree Logic (CTL) [17]. LTL assumes implicit universal quantification over all paths that are generated by system moves. CTL [18] allows explicit existential and universal quantification over all paths. ATL introduces a more general variety of temporal logic; offers selective quantification over those paths that are possible outcomes of games. As compared to previous work by the authors [17], the present formalization of ATL is more general and complex. This paper builts upon and extends the previously published paper [19]. Formal language used The choice of the CIC is dictated by its considerable expressive power as well as by the fact that it is supported by a tool of industrial strength, namely the Coq proof assistant. Coq is a free open source software that provides a (dependently typed) functional programming language and a reasoning framework based on higher order logic. Coq allows developing mathematical facts. This includes defining objects (integers, sets, lists, trees, functions, programs); making statements (using basic predicates, logical connectives and quantifiers); and finally writing proofs. The Coq environment helps with: advanced notations, proof search and automation, modular developments. As examples of its applicability, Coq has been used as a framework for formalizing programming environments and designing special platforms for software verification: the Gemalto and Trusted Logic companies obtained the level CC EAL 7 of certification for their formalization, developed in Coq, of the security properties of 2

the JavaCard platform [20, 21, 22]; Leroy and others developed in Coq a certified optimizing compiler for a large subset of the C programming language [23]; Barthe and others used Coq to develop Certicrypt, an environment of formal proofs for computational cryptography [24]. Contents of the paper The rest of the paper is organized as follows. In Section 2 we introduce CGS as well as the syntax and semantics of ATL. In Section 3 are formalized both the logic ATL and CGS including the notions of coalition and strategies. Unlike standard ATL semantics, temporal operators are formalized in terms of inductive and coinductive types, employing a fixpoint characterization of these operators. Then, Section 4 shows a complete list of axioms, theorems and inference rules for ATL according to [25] that have been proved in Coq with our proposal [26, 27]. In Section 5 we present the usual train example [4] as a simple but relevant case study for the bounded and unbounded cases. Section 6 considers related work, and finally Section 7 concludes with a summary of our contributions and directions for future work. Formalization A detailed description of the formalization is presented in Spanish in [26]. This document, along with the full formalization in Coq may be obtained from http://www.fceia.unr.edu.ar/~dante/. 2. Alternating-time Temporal Logic ATL is interpreted over CGS, a formalism to model multi-player games with silmutaneous moves. In this section we introduce CGS (Section 2.1) as well as the syntax and the semantics of ATL (Section 2.2) as found in [4]. 2.1. Concurrent Game Structures Definition 1 (CGS). A CGS is a tuple S = hΣ, Q, Π, π, d, δi with: • A set Σ = {1, . . . , k} of players or agents. • A set Q of states. • A finite set Π of atomic propositions. • For each q ∈ Q, a set π(q) ⊆ Π of propositions true at q. • For each player a ∈ Σ and each state q ∈ Q, a natural number da (q) ≥ 1 of moves available at state q to player a. We identify the moves of a at state q with the numbers 1, . . . , da (q). For q ∈ Q, a move vector at q is a tuple hj1 , . . . , jk i such that 1 ≤ ja ≤ da (q) for each player a. We define D(q) as the set of move vectors available at q; function D is called the move function.

3

• For each state q ∈ Q and each move vector hj1 , . . . , jk i ∈ D(q), a state δ(q, j1 , . . . , jk ) ∈ Q that results from state q if each player a ∈ Σ chooses move ja . The function δ is called transition function. For two states q and q ′ , we say that q ′ is a successor of q if there exists a move vector hj1 , . . . , jk i such that q ′ = δ(q, j1 , . . . , jk ). A computation of S is an infinite sequence (1) ω = q0 , q1 , q2 , . . . of states such that for all i ≥ 0, the state qi+1 is a successor of qi . We refer to a computation starting at state q as a q-computation. For a computation ω and a position i ≥ 0, we use ω[i] and ω[0, i] to denote the i-th state and the finite prefix q0 , . . . , qi , respectively. 2.2. ATL Syntax and Semantics Definition 2 (ATL). Let Π be a set of atomic propositions, and Σ a set of k players. The set of ATL formulas is inductively defined as follows: • p, for each p ∈ Π. • ¬ϕ, ϕ ∨ ψ, ϕ ∧ ψ, ϕ → ψ, where ϕ, ψ are ATL formulas. • hhAii# ϕ, hhAii2ϕ, hhAiiϕ U ψ, where ϕ, ψ are ATL formulas and A ⊆ Σ. The operator hh ii is a path quantifier; # (next), 2 (box) and U (until) are temporal operators. ATL can be viewed as a generalization of the branching-time temporal logic CTL where path quantifiers can be parametrized by sets of players. In particular, we obtain a CTL-equivalent logic restricting A to ∅ or Σ in Definition 2. Formulas in ATL are interpreted over states of a CGS with the same players and atomic propositions. The concept of strategy is introduced in [4] to formalize the semantics. Definition 3 (Strategy). Let S = hΣ, Q, Π, π, d, δi be a CGS and a ∈ Σ. A strategy for a is a function fa : Q+ → N that maps every nonempty finite state sequence α ∈ Q+ to a natural number such that if q is the last state of α, then 1 ≤ fa (α) ≤ da (q). Given a state q ∈ Q, and A ⊆ Σ, an A-strategy FA = {fa | a ∈ A}

(2)

is a set of strategies, one for each player in A. The outcomes of FA from a state q is the set of traces that players in A can enforce when they follow the strategies in FA . A computation ω = q0 , q1 , . . . belongs to out(q, FA ) if q0 = q and for all positions i, there is a move vector hj1 , . . . , jk i such that: 1. if a ∈ A, ja = fa (ω[0, i]), and 4

2. δ(qi , j1 , . . . , jk ) = qi+1 . Definition 4 (Standard ATL Semantics). Let S be a CGS and q a state of S. We write q |= ϕ to indicate that the ATL formula ϕ holds at q. The relation |= is defined inductively as follows: • q |= p , for atomic propositions p ∈ Π iff p ∈ π(q). • q |= ¬ϕ iff q 6|= ϕ. • q |= ϕ1 ∨ ϕ2 iff q |= ϕ1 or q |= ϕ2 . • q |= ϕ1 ∧ ϕ2 iff q |= ϕ1 and q |= ϕ2 . • q |= ϕ1 ⇒ ϕ2 iff q |= ϕ2 given that q |= ϕ1 . • q |= hhAii# ϕ iff there exists an A-strategy FA = {fa | a ∈ A}, such that for all ω ∈ out(q, FA ), we have ω[1] |= ϕ . • q |= hhAii2ϕ iff there exists an A-strategy FA = {fa | a ∈ A} such that for all ω ∈ out(q, FA ) and all positions i ≥ 0 we have ω[i] |= ϕ . • q |= hhAiiϕ1 U ϕ2 iff there exists an A-strategy FA = {fa | a ∈ A}, such that for all ω ∈ out(q, FA ) there exists a position i ≥ 0 such that ω[i] |= ϕ2 and for all positions 0 ≤ j < i we have ω[j] |= ϕ1 . 3. Formalizing CGS and ATL Our formalization is divided in two main parts. Section 3.2 provides a way to represent CGS, coalitions and strategies. In Section 3.3 we proceed to formalize the logic ATL. The formalization of temporal operators follows the axiomatization presented in [25], using fixpoints characterizations for hhAii2ϕ and hhAiiϕ U ψ. We believe that giving semantics to temporal operators using fixpoint definitions by means of inductive and coinductive types has some advantages over the standard semantics from Definition 4. The inductive and coinductive principles associated to our definition of temporal operators can be used to construct more elegant and concise proofs for ATL theorems (sect. 4) and for specific propierties of reactive systems (sect. 5). 3.1. The CIC and Coq The CIC is a type theory, in brief, a higher order logic in which the individuals are classified into a hierarchy of types. The types work very much as in strongly typed functional programming languages which means that there are basic elementary types, types defined by induction, like sequences and trees, and function types. An inductive type is defined by its constructors and its elements are obtained as finite combinations of these constructors. Data types are called “Sets” in the CIC (in Coq). When the requirement of finiteness is removed we 5

obtain the possibility of defining infinite structures, called coinductive types, like infinite sequences. On top of this, a higher-order logic is available which serves to predicate on the various data types. The interpretation of the propositions is constructive, i.e. a proposition is defined by specifying what a proof of it is and a proposition is true if and only if a proof of it has been constructed. The type of propositions is called Prop. We use the usual notation for logical connectives and quantifiers (¬, →, ∧, ∨, ∀, ∃). For anonymous functions and predicates, we utilize a notation similar to the Coq specification language. For instance, predicate pos : N → Prop is written as (λ n : N ⇒ n > 0). We define a (co)inductive predicate I by giving introduction rules of the form: P1 . . . Pm (introi ) I x1 . . . x n where free ocurrences of variables are implicitly universally quantified. In this work we use some inductive types defined in the Coq Standard Library [28]. We employ notation { } for the empty type, {1} for unit type, A + B for disjoint union (sum type). Type (seq A) denotes the set of finite sequences of type A. Empty sequence is noted as hi, and the infix notation s a e is used to denote the sequence resulting by appending element e to sequence s. The Stream type is used to represent infinite sequences of objects from a fixed type A. Constructor Cons adds an element e : A to an infinite sequence ω. Infix notation e ⊳ ω is used for (Cons e ω). We refer to [13, 14] for further details on the CIC and Coq. 3.2. Formalizing CGS We assume three basic types in sort Set: State, the set of states; Player , the players in the system; and Move, the set of moves (or actions). These types are specification parameters, and must be instantiated when specifyng a concrete CGS. Observe that we do not imposse any finiteness requirement to these types. 3.2.1. Move Vectors and Transitions A move vector is a function that assigns a move to each player, def

hMovei = Player → Move

(3)

The transition function is introduced as a relation δ : State → hMovei → State → Prop

(4)

We say that the move m is enabled at state q for player a if there exists a move vector mv and a state q ′ such that mv assigns m to player a and q ′ is the successor of q when players in Σ chooses the movements in mv. Formally, the relation enabled : State → Player → Move → Prop (5)

6

has one constructor: mv : hMovei

q ′ : State mv a = m enabled q a m

δ q mv q ′

(enabled intro)

(6)

A proof of type (enabled q a m) is interpreted as “player a can choose move m at state q”. Two expected properties are assumed over δ; the property δ f guarantees that the relation is indeed a function, while the property δ d guarantees that for every state q, if you choose a move vector mv such that (mv a) is enabled at q for every player a, then you will found an outgoing transition from q labeled with mv. δ f : ∀(q, q ′ , q ′′ : State)(mv : hMovei), δ q mv q ′ → δ q mv q ′′ → q ′ = q ′′ δ d : ∀(q : State)(mv : hMovei), (∀a : Player , enabled q a (mv a)) → ∃(q ′ : State), δ q mv q ′

(7)

3.2.2. Coalitions A coalition is a set of players A ⊆ Σ. The Coq Standard Library [28] defines a set over a universe U as an inhabitant of type U → Prop. We say that element x belongs to set X if we can exhibit a proof of proposition (X x). In particular, the union of sets X, Y is defined as: def

Union X Y = (λ x : U ⇒ X x ∨ Y x)

(8)

However, this formalization of sets is not satisfactory for our purposes due to its lack of computational content. This computational content is required, for instance, to prove the valid formula: hhAii# ϕ → hhBii# ψ → hhA ∪ Bii# (ϕ ∧ ψ)

(9)

when A and B are disjoint sets. The proof “joins” the strategies for A and B given in the premises to construct a new strategy for the coalition A ∪ B. For a player a ∈ A ∪ B, the new strategy chooses the strategy given by the first premise when a ∈ A, and the strategy given by the second premise when a ∈ B. As we will introduce strategies as an object with computational content, i.e. an inhabitant of sort Set, the election of a strategy cannot be made eliminating an inhabitant in Prop [13]. We conclude that proofs of set membership must live in sort Set. Therefore, we define a coalition as a term of type Player → Set. We say that player a belongs to coalition C if we can construct an element in type (C a). Coalitions Σ and ∅, and the union of two coalitions are defined as: def

Σ = λ a ⇒ {1}

def

∅ = λa ⇒ { }

def

A ⊎ B = λa ⇒ A a + B a

(10)

Other operators, like coalition complement, can be defined easily. We refer the interested reader to [27].

7

3.2.3. Strategies A strategy decides the next move taking into account the complete history of the game: def Strategy = seq State → State → Move (11) where the first argument is the past sequence of states, and the second the current state of the game. Let A be a coalition. A strategy for coalition A is a term of type (StrategySet A), where: def

StrategySet(A : Coalition) = ∀a : Player , A a → Strategy

(12)

A term FA : (StrategySet A) gives a strategy for each player a, provided that a ∈ A. We define the notion of FA -successor state for a coalition strategy FA . Let q be the current state, and qs the game history. We say that q ′ is an FA -successor of qs a q if there exists a move vector mv such that: 1. a transition from q to q ′ labelled with mv exists, and 2. strategy fa ∈ FA for player a ∈ A is such that fa (qs a q) = mv(a). Formally, relation suc is introduced by means of the following definition: suc : ∀A : Coalition, StrategySet A → seq State → State → State → Prop mv : hMovei δ q mv q ′ ∀(a : Player )(H : A a), FA a H qs q = mv a (suc intro) suc A FA qs q q ′

(13)

In the sequel, we will omit the first argument, since it can be inferred from the second. Also, we write q ′ ∈ suc(qs, q, FA ) for a proof of (suc FA qs q q ′ ). Note that if the initial state is q, and coalition A follows the strategy FA then for every possible successor state q ′ , we have q ′ ∈ suc(qs, q, FA ). Now, we define coinductively the set of traces that a coalition A can enforce by following the strategy FA . The relation isOut determines if the trace (q⊳q ′ ⊳ω) is a possible result of the game when players in A follows strategies in FA and game history is qs: isOut : ∀A : Coalition, StrategySet A → seq State → Trace → P rop isOut A FA (qs a q) (q ′ ⊳ ω) q ′ ∈ suc(qs, q, FA ) (isOut intro) isOut A FA qs (q ⊳ q ′ ⊳ ω)

(14)

def

where Trace = (Stream State). The set out(q, FA ) of traces a coalition A can enforce if follows strategies in FA is defined as: def

ω ∈ out(q, FA ) = isOut A FA hi (q ⊳ ω)

8

(15)

3.3. Formalizing ATL In this section we present a formalization of the syntax and semantics of ATL. Let S be a CGS, an ATL state formula is a term of type: def

StateForm = State → Prop

(16)

If q : State and ϕ : StateForm, a proof (term) of (ϕ q) is interpreted as q |= ϕ . 3.3.1. Constants and Boolean Connectives The ⊤ and ⊥ formulas are easily defined as ⊤

def

=

λ q : State ⇒ True

⊥

def

λ q : State ⇒ False

(17) =

We use a standard point-free use of boolean connectives. For state formulas ϕ, ψ, we define: ¬ϕ

def

=

λ q : State ⇒ ¬(ϕ q)

ϕ→ψ

def

λ q : State ⇒ ϕ q → ψ q

ϕ∧ψ

def

=

λ q : State ⇒ ϕ q ∧ ψ q

ϕ∨ψ

def

λ q : State ⇒ ϕ q ∨ ψ q

=

(18)

=

3.3.2. Temporal Operators The standard ATL semantics presented in Definition 4 for hhAii#ϕ uses the notion of execution traces. We present here an alternative (and equivalent) semantics using only the notion of successor state. Let q be the current state of a game. To guarantee that the property ϕ holds in the next state a coalition A should follow a strategy FA such that for every possible FA -successor state q ′ we have q ′ |= ϕ . Definition 5 (Next). Let A : Coalition, q : State and ϕ : StateForm. The relation Next : Coalition → StateForm → StateForm (19) is defined with one constructor as follows: F : StrategySet A

∀q ′ , q ′ ∈ suc(hi, q, F ) → ϕ q ′ (next) Next A ϕ q

(20)

The ATL axiomatization found in [25] establishes that hhAii2ϕ is the greatest fixed point of equation: X ↔ ϕ ∧ hhAii# X (21) Following this approach, we introduce a coinductive predicate to model this semantics for formulas of the form hhAii2ϕ. 9

Definition 6 (Box). Let A : Coalition, ϕ : StateForm and q : State. The coinductive predicate Box : Coalition → StateForm → StateForm

(22)

is defined as: ϕq F : StrategySet A ∀q ′ , q ′ ∈ suc(hi, q, F ) → Box A ϕ q ′ (box) Box A ϕ q

(23)

To construct a proof of q |= hhAii2ϕ , two conditions must hold: 1. ϕ must be valid at state q, and 2. we need to find an A-strategy F such that, for all F -successor state q ′ of q we have q ′ |= hhAii2ϕ . Using the fact that hhAiiϕ U ψ is the least fixed point of X ↔ ψ ∨ (ϕ ∧ hhAii# X)

(24)

we introduce the semantics of hhAiiϕ U ψ by an inductive relation. Definition 7 (Until). Let A : Coalition, ϕ, ψ : StateForm and q : State. The inductive relation Until : Coalition → StateForm → StateForm → StateForm

(25)

is defined with two constructors as follows: ψq ( U1 ) Until A ϕ ψ q

F : StrategySet A ϕq ∀q ′ , q ′ ∈ suc(hi, q, F ) → Until A ϕ ψ q ′ ( U2 ) Until A ϕ ψ q

(26)

If q |= ψ , then q |= hhAiiϕ U ψ (constructor U1 ). To prove q |= hhAiiϕ U ψ using constructor U2 , we need to prove that q |= ϕ and there exists an Astrategy F such that, if players in A follow this strategy, in all FA -successor state q ′ of q we have q ′ |= hhAiiϕ U ψ. ∞

Derived operators like hhAii3ϕ (eventually), and hhAii F ϕ (infinitely often) have been defined. For example, hhAii3ϕ ∞

hhAii F ϕ

def

=

hhAii⊤ U ϕ (27)

def

=

hhAii2hh∅ii3ϕ

For details see [27].

10

4. A Deductive System for ATL The formalization presented in Section 3 can be used to reason about properties of ATL and CGS. To prove ATL theorems we often use general properties involving coalitions and strategies. A complete set of axioms and inference rules for ATL is presented in [25]. We have proved all these results in our formalization. The proofs are merely outlined; however, all proofs have been formalized in Coq and are available as part of the full specification [27]. Theorem 1. The following formulas are valid in all states of all CGS: (⊥) ¬hhAii# ⊥. (⊤) hhAii# ⊤. (Σ) ¬hh∅ii# ¬ϕ → hhΣii# ϕ. (S) hhA1 ii# ϕ1 ∧ hhA2 ii# ϕ2 → hhA1 ∪ A2 ii# (ϕ1 ∧ ϕ2 ) , if A1 ∩ A2 = ∅. (FP2 ) hhAii2ϕ ↔ ϕ ∧ hhAii# hhAii2ϕ. (GFP2 ) hh∅ii2 (θ → (ϕ ∧ hhAii# θ)) → hh∅ii2 (θ → hhAii2ϕ). (FP U ) hhAiiϕ1 U ϕ2 ↔ ϕ2 ∨ (ϕ1 ∧ hhAii# hhAiiϕ1 U ϕ2 ). (LFP U ) hh∅ii2 ((ϕ2 ∨ (ϕ1 ∧ hhAii# θ)) → θ) → hh∅ii2 (hhAiiϕ1 U ϕ2 → θ). Also, the following inference rules preserves validity 1 : ϕ→ψ (monotonicity) hhAii# ϕ → hhAii# ψ

ϕ (necessitation) hh∅ii2ϕ

Proof The proof of (FP2 ) in our system is trivial, because we have used this formula as a definition for hhAii2. Formula (GFP2 ) is a consequence of the use of a coinductive type for this operator. A similar consideration can be done about formulas (FP U ), used to define formulas involving U ; and (LFP U ), consequence of the inductive definition. Formula (Σ) is valid only in classical logic. In constructive logic we can prove (Σ ′ ): ¬hh∅ii# ¬ϕ → ¬¬hhΣii# ϕ. To demonstrate the equivalence (Σ) ↔ (Σ′ ) from classical logic in our system, we must add the excluded middle law explicitly. Proof of (S) involves reasoning about union of coalitions and strategies, as well as relating the “join” of coalition strategies (collaborative game) and the traces in which each coalition plays regardless the other one (competitive game). These results are properties about 1 We omit the modus ponens rule from [25], since this rule is already valid in our meta-logic via the shallow embedding.

11

game structures, and we have proved them in [27] using definitions introduced in Section 2.1. Rule monotonicity is proved by showing that strategy FA given by premise hhAii# ϕ is an A strategy ensuring ψ in all states q ′ ∈ suc(hi, q, FA ). We prove necessitation by coinduction, unfolding Definition 6 and using the fact that ϕ is valid in all states. 2 To show that our formalization can be used as a suitable proof system for ATL, we have proved in [27] an extensive list of ATL theorems taken from [25]. Lemma 2 shows a list with a subset of such formulas. Lemma 2 (Derived formulas). The following judges can be proved valid in our formalization: (1) Regularity : ⊢ hhAii# ϕ → ¬hhΣ\Aii# ¬ϕ. (2) And monotonicity : ⊢ hhAii# (ϕ ∧ ψ) → hhAii# ϕ. (3) Coalition property 1 : ⊢ hhA1 ii# ϕ → hhA1 ⊎ A2 ii# ϕ. (4) Coalition property 2 : ⊢ hhA1 ii# ϕ ∧ hhA2 ii# ψ → hhA1 ⊎ A2 ii# (ϕ ∧ ψ). (5) Coalition monotonicity : ⊢ hhAii# ϕ → hhA ⊎ Bii# ϕ. (6) Monotonicity of hh ii2 : (ϕ → ψ) ⊢ hhAii2ϕ → hhAii2ψ. (7) Distributivity of hh ii2 : ⊢ hhAii2(ϕ → ψ) ∧ hhAii2ϕ → hhAii2ψ. (8) Induction for hh ii2 : (ϕ → (ψ ∧ hhAii# ϕ)) ⊢ ϕ → hhAii2ψ. (9) Monotonicity of hh ii U : (ϕ → ϕ′ ), (ψ → ψ ′ ) ⊢ hhAiiϕ U ψ → hhAiiϕ′ U ψ ′ . (10) Induction for hh ii U : (ψ ∨ (ϕ ∧ hhAii# χ) → χ) ⊢ hhAiiϕ U ψ → χ. 5. A Case Study The formalization presented in Section 3 has been used in Section 4 to prove general properties over CGS and the logic ATL. In this section, we specify and verify a simple concrete system which is a good guide to model and analyze many systems. Section 5.1 presents an example taken from [4], describing a control protocol for a train entering a railroad crossing. Section 5.2 presents a generalization of this model where an unknown number of trains compete to enter a gate, and the gate controller must ensure some safety and liveness properties. This example can not be directly analyzed using model checking techniques because it involves an unbounded space of states.

12

5.1. Controlling a Railroad Crossing We formalize a protocol for a train entering a railroad crossing with a finite CGS. All components for this CGS are instantiated using definitions presented in Section 3.2, and some properties for the system are specified using ATL formulas as described in Section 3.3. Example 1. The CGS ST = hk, Q, Π, π, d, δi has the following components: • k = 2. Player 1 represents the train, and player 2 the gate controller. • Q = {qout , qreq , qgran , qin }. • Π = {Out, Request, In gate, Grant}. •

– π(qout ) = {Out}, the train is outside the gate. – π(qreq ) = {Out, Request}, the train is still outside the gate, but has requested to enter. – π(qgran ) = {Out, Grant}, the controller has given the train permission to enter the gate. – π(qin ) = {In gate}, the train is in the gate.

•

– d1 (qout ) = 2 and d2 (qout ) = 1. At qout , the train can choose to either stay outside the gate, or request to enter the gate. – d1 (qreq ) = 1 and d2 (qreq ) = 3. At qreq , the controller can choose to either grant the train permission to enter the gate, or deny the train’s request, or delay the handling of the request. – d1 (qgran ) = 2 and d2 (qgran ) = 1. At qgran , the train can choose to either enter the gate, or relinquish its permission to enter the gate. – d1 (qin ) = 1 and d2 (qin ) = 2. At qin , the controller can choose to either keep the gate closed, or reopen the gate to new requests.

• The transition function δ is depicted in Figure 1. 5.1.1. A Model Based on CGS In order to prove properties of the protocol described in Example 1, we proceed to model all the components of ST following definitions presented in Section 3.2.

13

h2,1i

Out

Out,Request

qreq

qout

h1,1i

h1,2i

h1,2i

qin

h1,1i

In gate

h1,3i

h1,1i

qgran

h2,1i

Out,Grant

h1,1i

Figure 1: Graphical representation of Example 1.

States, Players and Moves. These sets are introduced as types with one constructor for each element in the set, excepting the sets of moves, where a unique constructor is used to represent an idle move. State Player Move

: : :

Set Set Set

def

= = def =

def

| qout | qreq | qgran | qin | Train | Controller | stayOut | request | grant | delay | deny | enter | relinquish | keepClosed | reopen | idle

We use the tuple notation hmt , mc i to denote the move vector: λ p : Player ⇒ (match p withTrain ⇒ mt | Controller ⇒ mc ) Transitions. Transitions are introduced with the following predicate 2 : def

δ : State → hMovei → State → Prop = | δ qout hstayOut, idlei qout | δ qreq hidle, granti qgran | δ qreq hidle, denyi qout | δ qgran hrelinquish, idlei qout | δ qin hidle, reopeni qout

|δ |δ |δ |δ

qout qreq qgran qin

hrequest, idlei hidle, delayi henter , idlei hidle, keepClosed i

qreq qreq qin qin

Coalitions. Singleton sets of players T = {Train} and C = {Controller } are defined as: def

T = λ p ⇒ match p withTrain ⇒ {1} | Controller ⇒ { } def C = λ p ⇒ match p withTrain ⇒ { } | Controller ⇒ {1} Atomic State Formulas. The atomic state formulas are easily introduced using case analysis over the current state. For example, a state formula representing 2 For

the sake of readability, we omit here the name of contructors.

14

the fact that the train is not in the gate is: def

OutGate = λ q ⇒ match q with qin ⇒ False | ⇒ True In a similar way, we define formulas Requested , Granted and InGate, according to Example 1: Requested Granted InGate

def

= = def =

def

λ q ⇒ match q with qreq ⇒ True | ⇒ False λ q ⇒ match q with qgran ⇒ True | ⇒ False λ q ⇒ match q with qin ⇒ True | ⇒ False

5.1.2. Proving Properties The following properties, taken from [4], are provable in our system: 1. Whenever the train is out of the gate and does not have a grant to enter the gate, the controller can prevent it from entering the gate: φ1 ≡ hh∅ii2 ((OutGate ∧ ¬Granted ) → hhCii2OutGate) 2. Whenever the train is out of the gate, the controller cannot force it to enter the gate: φ2 ≡ hh∅ii2 (OutGate → ¬hhCii3InGate) 3. Whenever the train is out of the gate, the train and the controller can cooperate so that the train will enter the gate: φ3 ≡ hh∅ii2 (OutGate → hhΣii3InGate) 4. Whenever the train is out of the gate, it can eventually request a grant for entering the gate, in which case the controller decides whether the grant is given or not: φ4 ≡ hh∅ii2(OutGate → hhT ii3 (Requested ∧ hhCii3Granted ∧ hhCii2¬Granted )) 5. Whenever the train is in the gate, the controller can force it out in the next step: φ5 ≡ hh∅ii2 (InGate → hhCii# OutGate) All the above properties have the form: hh∅ii2ϕ. To demonstrate the validity of these formulas it suffices to prove that ϕ is valid in all states. From this demonstration and rule necessitation (Theorem 1), we can prove hh∅ii2ϕ. We omit proofs here and refer the interested reader to [27]. 5.2. Controlling an Unbounded Number of Trains Suppose there is an unknown number of trains to cross a single gate. The gate controller must ensure some safety (for instance, at most one train is in the gate) and liveness (for instance, a request must be processed) properties. 15

5.2.1. Formalizing the System Using CGS We propose an extendend CGS S∞ as a model of the system described above. Players. The system components are the controller and the set of trains: def

Player : Set = Train : Id → Player | Controller : Player def

where Id = N. We abbreviate tn the term Train n, denoting the n-th train. States. In each state of the system, we should have information about the trains that have made a request to enter the gate, and which train has obtained such permission. To represent the set of trains that want to enter to the gate, we introduce the type: def Petition = Id → Bool For a function f : Petition, we say that tn wants to enter the gate if f tn = true. The set of states is defined as: State : Set

def

=

| qout : State | qreq : Petition → State | qgran : Petition → Id → State | qin : Petition → Id → State

The first argument of states qreq , qgran and qin is used to represent the set of trains that have made a request. The second argument of state qgran (qin ) is the id of the train having permission to enter (has entered) the gate. Moves and Move Vectors. The set of moves is similar to the finite case. Additional moves are used for communication between components. The set of moves is extended in the following way: Move

def

=

| stayOut : Move | delay : Move | enter : Move | reopen : Move

| request : Move | deny : Id → Move | relinquish : Move | idle : Move

| grant : Id → Move | denyAll : Move | keepClosed : Move

In the following moves appear the main difference with the finite example: (deny n) represents a move where the controller rejects a request from train tn , denyAll models a situation where controller can reject all requests, and (grant n) represents a situation where controller gives permission to tn . Let mc : Move be a move of the controller and let mt : Id → Move be a function assigning a move to each train, we use the notation hmt , mc i to represent the move vector defined as: λ p ⇒ (match p with tn ⇒ mt n | Controller ⇒ mc )

16

Transitions. To model the transition relation we use the following auxiliary functions: =b : Id → Id → Bool that decides equality in type Id , and an overwrite operator: ⊕ : Petition → Id → Bool → Petition such that (f ⊕ {n ← b}) applied to m returns b if m = n, and f m otherwise. The transition relation is defined as follows 3 : δ

def

=

| δ qout hλ n ⇒ stayOut, idlei qout | ∀f, (∃n : Id , f n = true) → δ qout hλ n ⇒ if f n then request else stayOut, idlei (qreq f ) | ∀f n, f n = true → δ (qreq f ) hλ n ⇒ idle, grant ni (qgran (f ⊕ {n ← false}) n) | ∀f, δ (qreq f ) hλ n ⇒ idle, delayi (qreq f ) | ∀f n, (∃m : Id , m 6= n ∧ f m = true) → δ (qreq f ) hλ n ⇒ idle, deny ni (qreq f ⊕ {n ← false}) | ∀f n, (∀m : Id , m 6= n → f m = false) → δ (qreq f ) hλ n ⇒ idle, deny ni qout | ∀f, δ (qreq f ) hλ n ⇒ idle, denyAll i qout | ∀f n, δ (qgran f n) henter n , idlei (qin f n) | ∀f n, (∀k : Id , k 6= n → f k = false) → δ (qgran f n) hrelinquish n , idlei qout | ∀f n, (∃k : Id , k 6= n ∧ f k = true) → δ (qgran f n) hrelinquish n , idlei (qreq f ) | ∀f n, δ (qin f n) hλ n ⇒ idle, keepClosed i (qin f n) | ∀f n, (∀m, f m = false) → δ (qin f n) hλ n ⇒ idle, reopeni qout | ∀f n, (∃m, f m = true) → δ (qin f n) hλ n ⇒ idle, reopeni (qreq f )

where enter n , relinquish n : Id → M ove are defined as: enter n relinquish n

def

= =

def

λ m ⇒ if m =b n then enter else idle λ m ⇒ if m =b n then relinquish else idle

The relation δ takes into account the existence of different train requests using the petition function. For instance, when the system is in state qout , there are two possible transitions: 1. no train make a request, then the system stays in qout , and 2. there exists a subset of trains making a request to enter the gate, represented with f ; in this case, the system make a transition to state (qreq f ). 3 We

have omitted constructors names.

17

Coalitions. Different coalitions can be defined for this system, depending on the properties to be specified. For example: {tn }

def

=

λp ⇒

match p with

| Train k ⇒ if n =b k then {1} else { } | Controller ⇒ { }

State Formulas. State formulas can be defined by pattern matching on states. For example, we define formula Out, valid if the current state is qout , and In(n), valid if train tn is in the gate: Out

def

In(n)

def

=

=

λ q ⇒ match q with | qout ⇒ True | ⇒ False λ q ⇒ match q with | qin f m ⇒ if n =b m then True else False | ⇒ False

5.2.2. Properties Consider the liveness property φ defined as follows φ ≡ hh∅ii2 (Out → hh{tn } ⊎ {Controller }ii3In(n))

(28)

where n ∈ Id . To prove that S∞ |= φ , we construct a strategy FA for coalition A = {tn , Controller }. Formally, FA = {fn } ⊎ {fc }, where def

fn : Strategy =

def

fc : Strategy =

λ (qs : seq State)(q : State) ⇒ match q with | qout ⇒ request | qreq f ⇒ idle | qgran f m ⇒ (if n =b m then enter else idle) | qin f m ⇒ idle end λ (qs : seq State)(q : State) ⇒ match q with | qout ⇒ idle | qreq f ⇒ (if f n then grant else denyAll ) | qgran f m ⇒ idle | qin f m ⇒ reopen end

Then, we proceed to show that if players in A follows strategy FA , a state where In(n) is valid will be eventually reached, regardless the behaviour of the other components. A detailed proof of this properties can be found in [27], along with the analysis of other safety and liveness properties, such as: • Cooperation is needed in order to ensure progress: Neither the set of trains nor the controller can enforce a trace where state In(n) is reached, for some n: hh∅ii2 (Out → ¬ (hh{Controller}ii3In(n) ∨ hh{t1 , t2 , . . .}ii3In(n))) 18

• If no train is in the gate and no permission to enter is granted, the controller can keep the empty gate forever: hh∅ii2 ((OutGate ∧ ¬InGranted ) → hh{Controller}ii2OutGate) where: OutGate

def

InGranted

def

=

=

λ q ⇒ match | qin f λ q ⇒ match | qgran

q with m ⇒ False | ⇒ True q with f m ⇒ True | ⇒ False

• The coalition {Train} can keep the system out of state qin indefinitely: hh∅ii2 (OutGate → hh{Train}ii2OutGate) 6. Related Work 6.1. Formalizations There exists previous work in formalizing temporal logic in systems other than Coq. We can mention the formalization of Temporal Logic of Actions (TLA) in the HOL prover, by L˚ angbacka [29]. The distribution of Isabelle [30, 31] contains the axiomatic encoding of Lamport’s TLA in HOL by Merz, and a formalization of a temporal logic por I/O automata by M¨ uller in HOLCF [32]. Also, we highlight formalizations of Linear Temporal Logic (LTL) [2] in PVS [33] and HOL [34]. Furthermore, there are works that formalize temporal logics in the CIC (in Coq). We can mention the formalization of Modal µ-Calculus [35, 36], LTL [16, 37], CTL [17], and Branching Time Temporal Logic [38]. In particular, LTL assumes implicit universal quantification over all paths that are generated by system moves. CTL allows explicit existential and universal quantification over all paths. ATL introduces a more general variety of temporal logic; offers selective quantification over those paths that are possible outcomes of games. As compared to previous work by the authors [17, 39, 40], the present formalization of ATL is more general and complex, given its game-theoretic basis. 6.2. Proof assistans Coq is a proof assistant similar to HOL systems, a family of interactive theorem provers based on Church’s higher-order logic including PVS [41], Isabelle/HOL, HOL4 [42] and HOL-light [43]. Unlike these systems, Coq is based on an intuitionistic type theory and is consequently closer to Matita [44, 45], Epigram [46], NuPrl [47] and Agda [48]. All these systems have in common that functions are programs that can be computed and not just binary relations like in mathematics. Coq is currently a tool of industrial strength. Impressive formalizations have been done using Coq, in different areas. Coq provides interactive proof methods, 19

decision and semi-decision algorithms, and a tactic language for letting the user define its own proof methods. Coq also provides support for high-level notations, implicit contents and various other useful kinds of macros. These features are very useful to formalize and reason about computations of open, multi-agent systems and multiplayer games. 7. Conclusions and Future Work ATL is a game-theoretic generalization of CTL with applications in the formal verification of multi-agent systems. In this paper we have presented a formalization of ATL and its semantic model CGS. Unlike standard ATL semantics, temporal operators have been interpreted in terms of inductive and coinductive types, using a fixpoint characterization of these operators in the CIC. The formalization presented here was used to model a concurrent system with an unbounded number of players and states, and we have verified some safety and liveness properties expressed as ATL formulas. Unlike automatic techniques, our formal model has no restriction in the size of the CGS, and arbitrary state predicates can be used as atomic propositions of ATL. We conclude that in systems with an intractable size, our formal model, based on an existent type theory (the CIC) with the proof assistant Coq can be used as a specification and verification tool for open multi-agent systems. A possible extension of our system would consist of formalizing fair-ATL [4], a logic extending ATL semantics with fairness constraints. These constraints rule out certain infinite computations that ignore enabled moves forever. The logic ATL is a fragment of a more expressive logic, ATL* [4]. In ATL*, a path quantifier hhAii is followed by an arbitrary linear time formula, allowing boolean combination and nesting, over # , 2 and U . Another interesting extension to our work is to formalize this logic in the CIC. ATL has been used to specify properties in contract signing protocols where n agents exchange signatures [49, 50]. The model checker Mocha [15] has succeeded in verifying these protocols in the case where two agents are involved [50]. However, model checking algorithms fail in case of multi-party protocols (n > 2), since these algorithms can be used only with a fixed (and, in practice, small) value for n. The formalization presented in this work can be used as basis for a formal verification of such protocols. Thus, a further extension of this work involves the verification of multi-party protocols following an approach similar to the one of Section 5. Acknowledgments The authors want to thank SBMF’2012 reviewers for helpful feedback on the paper that is the basis of this work.

20

References [1] E. Emerson, Temporal and modal logic, in: Handbook of Theoretical Computer Science, Elsevier, 1995, pp. 995–1072. [2] A. Pnueli, The temporal logic of programs, in: Proceedings of the 18th Annual Symposium on Foundations of Computer Science, IEEE Computer Society, Washington, DC, USA, 1977, pp. 46–57. URL http://dl.acm.org/citation.cfm?id=1398506.1382534 [3] R. Alur, T. Henzinger, O. Kupferman, Alternating-time temporal logic, in: Revised Lectures from the International Symposium on Compositionality: The Significant Difference, COMPOS’97, Springer-Verlag, London, UK, 1998, pp. 23–60. URL http://dl.acm.org/citation.cfm?id=646738.702089 [4] R. Alur, T. Henzinger, O. Kupferman, Alternating-time temporal logic, Journal of the ACM 49 (2002) 672–713. [5] J. Y. Halpern, Reasoning about knowledge: An overview, in: Proceedings of the 1986 Conference on Theoretical Aspects of Reasoning About Knowledge, TARK ’86, Morgan Kaufmann Publishers Inc., San Francisco, CA, USA, 1986, pp. 1–17. URL http://dl.acm.org/citation.cfm?id=1029786.1029788 [6] F. van Harmelen, F. van Harmelen, V. Lifschitz, B. Porter, Handbook of Knowledge Representation, Elsevier Science, San Diego, USA, 2007. [7] M. Wooldridge, An Introduction to MultiAgent Systems, 2nd Edition, Wiley & Sons, 2009. [8] M. Osborne, A. Rubinstein, A Course in Game Theory, MIT Press, 1994. [9] T. ˚ Agotnes, W. van der Hoek, M. Wooldridge, Reasoning about coalitional games., Artif. Intell. 173 (1) (2009) 45–79. URL http://dblp.uni-trier.de/db/journals/ai/ai173.html# AgotnesHW09 [10] T. Coquand, G. Huet, The calculus of constructions, Inf. Comput. 76 (2-3) (1988) 95–120. doi:10.1016/0890-5401(88)90005-3. URL http://dx.doi.org/10.1016/0890-5401(88)90005-3 [11] C. Paulin-Mohring, Inductive definitions in the system coq - rules and properties, in: TLCA ’93: Proceedings of the International Conference on Typed Lambda Calculi and Applications, Springer-Verlag, London, UK, 1993, pp. 328–345. [12] E. Gim´enez, A calculus of infinite constructions and its application to the verification of communicating systems, Ph.D. thesis, Ecole Normale Sup´erieure de Lyon (1996). 21

[13] The Coq development team, The Coq proof assistant reference manual, version 8.4, LogiCal Project, distributed electronically at http://coq. inria.fr (2012). URL http://coq.inria.fr/doc/main.html [14] Y. Bertot, P. Cast´eran, Interactive Theorem Proving and Program Development. Coq’Art: The Calculus of Inductive Constructions, Texts in Theoretical Computer Science, Springer Verlag, 2004. URL http://www.labri.fr/publications/l3a/2004/BC04 [15] R. Alur, T. Henzinger, F. Mang, S. Qadeer, S. Rajamani, S. Tasiran, Mocha: Modularity in model checking, in: CAV ’98: Proceedings of the 10th International Conference on Computer Aided Verification, SpringerVerlag, London, UK, 1998, pp. 521–525. [16] S. Coupet-Grimal, LTL in Coq, Contributions to the Coq system, Laboratoire d’Informatique Fondamentale de Marseille, available at http: //coq.inria.fr/contribs/LTL.tar.gz (2002). [17] C. Luna, Computation tree logic for reactive systems and timed computation tree logic for real time systems, Contributions to the Coq system, Universidad de la Rep´ ublica, Uruguay (2000). URL http://coq.inria.fr/pylons/contribs/index [18] J. van Leeuwen (Ed.), Handbook of Theoretical Computer Science, Volume B: Formal Models and Semantics, Elsevier and MIT Press, 1990. [19] D. Zanarini, C. Luna, L. Sierra, Alternating-time temporal logic in the calculus of (co)inductive constructions, in: R. Gheyi, D. A. Naumann (Eds.), SBMF, Vol. 7498 of Lecture Notes in Computer Science, Springer, 2012, pp. 210–225. [20] B. Chetali, Q.-H. Nguyen, About the world-first smart card certificate with eal7 formal assurances, Slides 9th ICCC, Jeju, Korea (Sep. 2008). [21] G. Betarte, E. Gim´enez, C. Loiseaux, B. Chetali, FORMAVIE: Formal Modeling and Verification of the Java Card 2.1.1 Security Architecture, in: Proceedings of eSmart’02, 2002, pp. 213–231. [22] J. Andronick, Mod´elisation et V´erification Formelles de Syst`emes Embarqu´es dans les Cartes ` a Microprocesseur – Plate-Forme Java Card et Syst`eme d’Exploitation, Ph.D. thesis, Universit´e Paris-Sud (2006). [23] X. Leroy, Formal verification of a realistic compiler, Communications of the ACM 52 (2009) 107–115. URL http://doi.acm.org/10.1145/1538788.1538814 [24] G. Barthe, B. Gr´egoire, S. Zanella B´eguelin, Formal certification of codebased cryptographic proofs, SIGPLAN Not. 44 (1) (2009) 90–101. URL http://doi.acm.org/10.1145/1594834.1480894 22

[25] V. Goranko, G. van Drimmelen, Complete axiomatization and decidability of alternating-time temporal logic, Theoretical Computer Science 353 (1) (2006) 93–117. [26] D. Zanarini, Formalizaci´ on de l´ ogica temporal alternante en el c´ alculo de construcciones coinductivas, Master’s thesis, FCEIA, Universidad Nacional de Rosario, Argentina, available at www.fceia.unr.edu.ar/~dante (2008). [27] D. Zanarini, Formalization of alternating time temporal logic in Coq, available at www.fceia.unr.edu.ar/~dante (2010). URL http://www.fceia.unr.edu.ar/dante [28] The Coq development team, The Coq Standard Library, LogiCal Project, available at http://coq.inria.fr/stdlib/ (2012). URL http://coq.inria.fr/stdlib [29] T. Langbacka, A hol formalisation of the temporal logic of actions, in: T. F. Melham, J. Camilleri (Eds.), Higher Order Logic Theorem Proving and Its Applications, Springer, Berlin, Heidelberg, 1994, pp. 332–345. [30] M. Wenzel, L. C. Paulson, T. Nipkow, The Isabelle framework, in: O. A. Mohamed, C. Mu˜ noz, S. Tahar (Eds.), Theorem Proving in Higher Order Logics: TPHOLs 2008, LNCS 5170, Springer, 2008, pp. 33–38. URL http://dx.doi.org/10.1007/978-3-540-71067-7_7 [31] T. Nipkow, M. Wenzel, L. C. Paulson, Isabelle/HOL: A Proof Assistant for Higher-order Logic, Springer-Verlag, Berlin, Heidelberg, 2002. [32] O. M¨ uller, T. Nipkow, D. v. Oheimb, O. Slotosch, HOLCF = HOL + LCF, Journal of Functional Programming 9 (1999) 191–223. [33] A. Pnueli, T. Arons, TLPVS: A PVS-based LTL verification system., in: N. Dershowitz (Ed.), Verification: Theory and Practice, Vol. 2772 of Lecture Notes in Computer Science, Springer, 2003, pp. 598–625. URL http://dblp.uni-trier.de/db/conf/birthday/Manna2003.html# PnueliA03 [34] K. Schneider, D. Hoffmann, A HOL conversion for translating linear time temporal logic to omega-automata, in: Theorem Proving in Higher Order Logics, Springer, 1999, pp. 255–272. [35] M. Miculan, On the formalization of the modal µ-calculus in the calculus of inductive constructions, Inf. Comput. 164 (1) (2001) 199–231. [36] C. Sprenger, A verified model checker for the modal µ-calculus in coq, in: B. Steffen (Ed.), TACAS, Vol. 1384 of Lecture Notes in Computer Science, Springer, 1998, pp. 167–183.

23

[37] S. Coupet-Grimal, An axiomatization of linear temporal logic in the calculus of inductive constructions., J. Log. Comput. 13 (6) (2003) 801–813. URL http://dblp.uni-trier.de/db/journals/logcom/logcom13. html#Coupet-Grimal03 [38] M.-H. Tsai, B.-Y. Wang, Formalization of ctl* in calculus of inductive constructions, in: M. Okada, I. Satoh (Eds.), ASIAN, Vol. 4435 of Lecture Notes in Computer Science, Springer, 2006, pp. 316–330. [39] C. Luna, Especificaci´ on y an´ alisis de sistemas de tiempo real en teor´ıa de tipos, Master’s thesis, Fac. de Ingenier´ıa, Universidad de la Rep´ ublica, Uruguay (2000). [40] C. Luna, The railroad crossing example, Contributions to the Coq system, Universidad de la Rep´ ublica, Uruguay (2000). URL http://coq.inria.fr/pylons/contribs/index [41] S. Owre, J. M. Rushby, N. Shankar, Pvs: A prototype verification system, in: Proceedings of the 11th International Conference on Automated Deduction: Automated Deduction, CADE-11, Springer-Verlag, London, UK, UK, 1992, pp. 748–752. URL http://dl.acm.org/citation.cfm?id=648230.752639 [42] K. Slind, M. Norrish, A brief overview of hol4, in: Proceedings of the 21st International Conference on Theorem Proving in Higher Order Logics, TPHOLs ’08, Springer-Verlag, Berlin, Heidelberg, 2008, pp. 28–32. URL http://dx.doi.org/10.1007/978-3-540-71067-7_6 [43] S. Berghofer, T. Nipkow, C. Urban, M. Wenzel (Eds.), Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings, Vol. 5674 of Lecture Notes in Computer Science, Springer, 2009. [44] A. Asperti, C. S. Coen, al, Matita, Available at http://matita.cs.unibo. it/. [45] A. Asperti, W. Ricciotti, C. S. Coen, E. Tassi, The matita interactive theorem prover, in: N. Bjørner, V. Sofronie-Stokkermans (Eds.), CADE, Vol. 6803 of Lecture Notes in Computer Science, Springer, 2011, pp. 64–69. [46] C. McBride, al, Epigram 2 : an experimental dependently typed functional programming language., Available at http://www.e-pig.org/ darcs/Pig09/web/. [47] R. L. Constable, J. L. Bates, C. Kreitz, R. van Renesse, al, Prl : Proof/program refinement logic, Available at http://www.cs.cornell. edu/info/projects/nuprl/. [48] C. Coquand, T. Coquand, U. Nurell, al, Agda, Available at http://wiki. portal.chalmers.se/agda. 24

[49] S. Kremer, J. Raskin, A game-based verification of non-repudiation and fair exchange protocols, Journal of Computer Security 11 (3) (2003) 399–429. [50] R. Chadha, S. Kremer, A. Scedrov, Formal analysis of multiparty contract signing, Journal of Automated Reasoning 36 (1-2) (2006) 39–83.

25