Formal Analysis of Dialogues on Infinite Argumentation Frameworks

1 Introduction

The dialectical and dynamic dimensions of argumentation have been object of scrutiny since the inception of Dung's abstract argumentation theory (cf. [Dung, 1994; 1995]). However, while the definition and analysis of 'static' justifiability criteria (i.e., argumentation semantics [Baroni et al., 2011]) has come to form the bulk of abstract argumentation theory, comparatively little work within Dung's framework has been dedicated to a systematic study of forms of dynamic and multi-agent interaction. Some research has focused on operationalizations of argumentation semantics via two-player games (see [Modgil and Caminada, 2009] for an overview), while some other has attempted an analysis of strategic behavior in abstract forms of argumentation games (in particular [Procaccia and Rosenschein, 2005; Riveret et al., 2010; Thimm and Garcia, 2010]). This paper pursues further the understanding of multi-agent argumentation over abstract argumentation frameworks (AF) capitalizing on techniques from logic and multi-agent verification.

Contribution of the paper. The paper focuses on the formal analysis of multi-agent strategic interactions on possibly infinite argumentation frameworks. Agents are assumed to exchange arguments from possibly infinite AF. They hold private argumentation frameworks representing their 'views' on how arguments attack one another. They interact by taking turns and attacking relevant arguments expanding the framework underlying the interaction. This set up, which we call dynamic argumentation systems (DAS), is general enough to

Nicolas Maudet

Sorbonne Universit´es UPMC Univ Paris 06 CNRS, UMR 7606, LIP6 F-75005, Paris, France nicolas.maudet@lip6.fr

model a wide range of dialogue protocols and games on abstract AF. We analyse this setting formally by introducing FOA-ATL, a novel first-order extension of the (turn-based) game logic ATL [Alur et al., 2002]. This logic allows us to specify dynamic properties of strategic interactions in argumentation. The objectives of the paper consist in: (i) the development of techniques to tackle the model-checking problem of FOA-ATL; (ii) the development of techniques to analyse how static properties of argumentation frameworks influence their dynamic behavior. In other words, we are interested in isolating a class of AF for which their structure allows us to predict their dynamic behaviours. We provide preliminary positive results to both questions.

Technically, the paper models DAS as a special type of infinite-state data-aware systems [Deutsch et al., 2009; Hariri et al., 2013]. This allows us to capitalize on recent results on the formal verification of artifact-centric systems [Belardinelli et al., 2014], thus obtaining truth-preserving bisimulations for FOA-ATL.

Related work. The paper contributes to several current strands of research in abstract argumentation.

Dynamics of argumentation. How argumentation framework may change by performing operations on their structure has been object of several recent works (e.g., [Baumann, 2012; Bisquert et al., 2013; Booth et al., 2013; Doutre et al., 2014]). However, all mentioned papers assume finite AF, as they rely on the possibility of encoding them into propositional formulas [Besnard and Doutre, 2004]. Neither do they incorporate agency, as they analyse argumentation dynamics from a belief revision paradigm. Our contribution relaxes the finiteness assumption and models agents explicitly as 'protocols' dinamically modifying the structure of AF.

Infinite argumentation frameworks. The bulk of known results in abstract argumentation typically pertain to finite AF. However, infinite AF are gaining attention and have been object of several recent contributions [Baroni et al., 2012; 2013; Baumann and Spanring, 2015], which essentially focus on how known results for the finite case generalize to the infinite. Allowing an infinity of arguments is critical in applications where upper bounds on the number of available arguments cannot be established a priori. Our paper contributes to the understanding of infinite AF.

Logics for abstract argumentation. Recently, several formalizations of argumentation theory have been put forward

(e.g., [Caminada and Gabbay, 2009; Grossi, 2010] for early contributions). These works typically focus on finding logical languages (frommodal to many-valued logics) that are sufficiently expressive to represent argumentation semantics. Our focus here is rather to specify the strategic abilities of agents engaging in a dialogue/dispute, such as: 'the proponent is able to respond to all attacks by maintaining a conflict-free set of arguments' or 'the opponent has a strategy to force proponent to run out of arguments'. In this respect the paper is a first contribution to the specification of multi-agent argumentation frameworks by means of temporal logics, as well as to their formal verification (cf. [Lomuscio et al., 2009]).

Outline of the paper. Section 2 introduces the dynamics of (multi-agent) argumentation frameworks and the specification language FOA-ATL; then we state the corresponding model checking problem. Section 3 contains the main technical result, namely, bisimilar dynamic argumentation systems (DAS) satisfy the same formulas in FOA-ATL. We also investigate the impact of static features of DAS on their dynamics. We conclude in Section 4 and point to future work. For reason of space all proofs are omitted.

2 The Dynamics of AF

In this section we introduce dynamic argumentation systems (DAS). Then, we present FOA-ATL, a first-order version of the alternating-time temporal logic ATL [Alur et al., 2002], and state the corresponding model checking problem. We first present the basic terminology to be used in the paper.

2.1 Abstract Argumentation

The theoretical setting is built on abstract argumentation, as introduced in [Dung, 1994; 1995]. In what follows we assume a finite set Ag = {a0, . . . , an} of names for agents.

Definition 1 (Argumentation Framework) Given a set Ag of agent names, a (multi-agent) argumentation framework is a tuple A = 〈A, {←a}a∈Ag〉 s.t. (i) A is a (possibly infinite) set of arguments, and (ii) for every a ∈ Ag, ←a⊆ A2 is an attack relation between arguments.

Notice that Def. 1 allows argumentation frameworks, or AF, that include infinitely many arguments. This choice, while providing greater modelling flexibility, also reflects the fact that upper bounds on the number of arguments available to each agent cannot be easily established in general.

We define F(A,Ag) as the set of all AF built on sets A of arguments and Ag of agent names. Hereafter, we simply write F(Ag) whenever A is clear. Also, given set Ag = {p, o} containing the proponent p and opponent o, F(p) (resp. F(o)) are shorthands for F({p}) (resp. F({o})), i.e., the set of AF for proponent p (resp. opponent o). Finally, we define the (unindexed) attack relation ←= ⋃a∈Ag ←a.

To express relevant properties of AF, we introduce FOA, a first-order language geared towards expressing properties of attack relations. Let Aa, for a ∈ Ag, be binary predicate symbols, P0, P1, . . . unary predicate symbols, and Var a countable set of individual variables. We define first-order formulas ϕ and the set fr(ϕ) of free variables by mutual recursion.

Definition 2 (FOA) The formulas ϕ and the set of free variables fr(ϕ) are defined as follows:

• if P is a predicate symbol and x ∈ Var a variable, then P(x) is a formula with fr(P(x)) = {x};
• if ϕ is a formula, then also ¬ϕ is, and fr(¬ϕ) = fr(ϕ);
• if ϕ and ϕ′ are formulas with fr(ϕ) = fr(ϕ′ ), then also ϕ→ϕ′ is, and fr(ϕ→ϕ′ ) = fr(ϕ) = fr(ϕ′ );
• if ϕ is a formula with fr(ϕ) = {y}, then also ∀y(Aa(y, x) → ϕ) and ∀yϕ are, with fr(∀y(Aa(y, x) → ϕ)) = {x} and fr(∀yϕ) = ∅.

In the following we use the standard abbreviations ∧, ∨, and ∃. Specifically, ∃y(Aa(y, x) ∧ ϕ) (resp. ∃yϕ) is a shorthand for ¬∀y(Aa(y, x) → ¬ϕ) (resp. ¬∀y¬ϕ). Notice that every FOA formula ϕ has at most one free variable.

Finally, we extend argumentation frameworks with interpretations π that assign a subset of A to each predicate symbol P, i.e., π(P) ⊆ A. An interpreted argumentation framework is defined as a couple (A, π). We can now introduce the semantics of our first-order language.

Definition 3 (Semantics of FOA) We define whether an argument u ∈ A satisfies an FOA-formula ϕ in an interpreted AF (A, π), or (A, π, u) |= ϕ, as follows (clauses for propositional connectives are straightforward, thus omitted):

An FOA-formula ϕ is true in an interpreted AF (A, π), or (A, π) |= ϕ, iff (A, π, u) |= ϕ for every argument u ∈ A; ϕ is valid in A, or A |= ϕ, iff (A, π) |= ϕ for every interpretation π.

From a technical point of view, the language FOA is the dyadic fragment of first-order logic with one free variable. 1 Table 1 shows how this simple logic suffices to formalize several of the key notions from [Dung, 1995] (see also [Grossi, 2010]).

2.2 Dynamic Argumentation Frameworks

In this paper we are interested in analysing dialogues modeled as multi-agent processes over argumentation frameworks. As dialogues progress agents build a 'shared' (or 'public') argumentation framework which is used to evaluate the available arguments.

Agents and global states

To introduce the dynamics of argumentation frameworks we start with the notion of agent.

Definition 4 (Agent) Given sets Ag of agent names and A of arguments, an agent is a tuple a = 〈A, Act, Pr〉 where

• A ∈ F(a) is the agent's argumentation framework;
• the set Act of actions contains action attack(x, x′ ) to attack argument x′ with argument x, and action skip;

1 As such, it is equivalent to the multi-modal logic K with the universal modality [Blackburn et al., 2001].

π(P) is a stable in A iff (A, π) |= ∀x(P(x) ↔¬(∃y(A(y, x) ∧P(y)))

Table 1: Some key notions of abstract argumentation theory and their formalization in FOA (A is interpreted over ←).

• Pr : ⋃A′⊆A F(A′ ,Ag) ↦→ 2Act(A) is the local protocol function, where Act(A) is the set of ground actions α(⃗u), and for every A′ ∈ F(A′ ,Ag), attack(u, u′ ) ∈ Pr(A′ ) only if u′ ∈ A′ and u′ ←a u holds in A; while the skip action is always enabled.

By Def. 4 agent a's local state is modelled as an argumentation framework A, and she is assumed to perform the actions in Act according to protocol Pr. In particular, by definition of Pr, attacks must be relevant, i.e., the attacked argument u′ has to appear in the current argumentation framework A′ , and they must reflect actual attacks available in the agent's AF A ∈ F(a). These assumptions on protocols model the basic requirements of relevance and truthfulness in dialogues.

To model agent interaction we need to define their composition, beginning with the notion of global state.

Definition 5 (Global State) Given a set Ag of agents ai = 〈Ai, Acti, Pri〉 defined on the same (possibly infinite) set A of arguments, a global state is a couple (s, a) where (i) s ∈ F(A′ , Ag) is an argumentation framework for some A′ ⊆ A; and (ii) a ∈ Ag.

In Def. 5 all agents are defined on the same set of arguments. However, some literature on agents and argumentation suppose that each agent is endowed with a distinct set of arguments (e.g., [Rahwan and Larson, 2011]). We remark that our requirement is not a limitation because, firstly we can always consider the union of the sets of arguments for each agent, and secondly the characterising feature of AF is really the attack relation. Moreover, this assumption simplifies the presentation hereafter. Also, in a state (s, a), a is the active agent, i.e., the agent to act next; it will be omitted whenever clear from the context. We write G to denote the set of all global states. Finally, any set A′ ⊆ A can be seen as a global state where, for every a ∈ Ag, ←a is empty.

Argument Dynamics

We now introduce the dynamics of argumentation frameworks. In the rest of the paper we suppose that the only two agents are proponent p and opponent o. This assumption can be lifted but it crucially simplifies the presentation of the key (conceptual and technical) contributions of the paper.

Definition 6 (DAS) Given set Ag = {p, o} of agents defined on the same (possibly infinite) set A of arguments, a dynamic argumentation system is a tuple P = 〈Ag, I, τ, π〉 where

• I ⊆ A×{o} is the set of initial global states (s0, o);
• τ : G × (Actp(A) ∪ Acto(A)) ↦→ G is the transition function, where τ((s, a), attacka′ (⃗u)) is defined iff a = a′ and attacka′ (⃗u) ∈ Pra′ (s). Moreover, (s′ , a′ ) = τ((s, a), attack(u, u′ )) iff a′ ̸= a and s′ = 〈A′ ,←′ 〉

• π is an interpretation of predicate symbols P as above.

A DAS evolves from an initial state (s0, o) ∈ I as specified by the transition function τ, which returns a successor state for the current state and selected action. DAS are turnbased, with each agent taking one action at a time. Hereafter we assume that the opponent always moves first, that is, I is intuitively the set of arguments supported by the proponent. One key feature of DAS is that, since the set A of arguments is infinite in general, they are infinite-state systems normally. Indeed, as the dialogue unfolds, agents can introduce an infinite number of arguments from A, thus going through infinitely many states during the system's execution.

We now fix some notation. The transition relation →a is defined so that s →a s′ iff for some action αa(⃗u) ∈ Acta(A), for a ∈ {o, p}, we have that s αa(⃗u) ----→ s′ , i.e., τ ((s, a), αa(⃗u)) = (s′ , a′ ) with a′ ̸= a. A run λ from a state (s, a), or (s, a)-run, is an infinite sequence s0 →a s1 →a′ . . ., s.t. s0 = s. Notice that, since agents o and p take turns in performing actions, the sequence of agents in an (s, a)- run is uniquely determined by a, so we omit agents whenever these are clear by the context. Hence, we will often denote a state (s, a) simply as s, whenever agent a is understood. For n,m ∈ N, with n ≤ m, we define λ(n) = sn and λ[n,m] = sn , sn+1 , . . . , sm. A state s′ is reachable from s iff for some s-run λ and i ≥ 0, s′ = λ(i). Let S be the set of states reachable from any initial state s0 ∈ I. Notice also that the transition relation is serial, as each agent has a skip action enabled at each local state.

DAS, dialogues and games

It is worth comparing DAS briefly with known structures in the literature on dialogue games for abstract argumentation. In the terminology of [Thimm and Garcia, 2010] DAS can be viewed as defining a dialectical game protocol, where at each step an active agent attacks some of the available arguments. DAS can be seen as extensive game forms with infinite horizon (though they are not games, as they do not specify payoffs). They also generalize the structures underpinning the extensive-form argument games of [Procaccia and Rosenschein, 2005] by allowing agents to hold an infinite argumentation framework and to attack any of the available arguments, not only the last one uttered by some other agent. We finally show how standard dialogue games (e.g., for the grounded extension [Dung, 1994] or for credulous admissibility [Vreeswijk and Prakken, 2000]) can be modeled as DAS.

Example 1 In the game for the grounded extension two agents o and p hold the same private argumentation framework, i.e., Ao = Ap. These games are two-player zero-sum perfect information games with possibly infinite horizon. We can view them as DAS. Consider for instance the AF in Figure 1. The DAS corresponding to the game for grounded played on this AF, starting at argument t1 can be defined as follows. Fix I = {t1}. For both agents we can define the following protocol: if the current framework contains ti then attack ti with ui or ti+1, otherwise skip. This protocol encodes the 'legal' moves of o and p according to the game for the grounded extension. The possible runs of this DAS contain all possible sub-graphs of the above AF generated from t1, e.g.: ({t1}, ∅), ({t1, u1}, {(u1, t1)}), skip, . . .; or ({t1}, ∅), ({t1, t2}, {(t2, t1)}), . . . , ({t1, . . . , ti}, {(ti, ti-1)}), . . .. These runs correspond to possible dialogues in the game for the grounded extension. ■

Given a DAS P on a (possibly infinite) set A of arguments, we define the corresponding (joint) argumentation framework AP = 〈A, {←a}a∈Ag〉 so that u ←a u′ holds in AP iff u ←a u′ holds in the AF Aa for agent a ∈ Ag. By the definition of protocols (Def. 4) it is apparent that every reachable state in P is a subgraph of AP, that is,

if u ←a v holds in some s ∈ S, for some a ∈ Ag, then u ←a v holds in AP. (∗)

Thus, states in P are truthful, yet partial, representations of AP. However, the converse of (∗) does not hold in general, i.e., P needs not to include all subgraphs of AP as states. To appreciate this consider the following:

Example 2 [Example 1 continued] Now endow o with a more restrictive protocol: if the current framework contains ti then attack ti with ui, otherwise skip. This protocol makes o play more rationally, selecting arguments to which p cannot reply. The only possible run of this DAS is: ({t1}, ∅), ({t1, u1}, {(u1, t1)}), skip, . . .. ■

This asymmetry motivates the next definition. An agent is naive if its protocol allows it to move any available attack (cp. this to the more restrictive protocol of o in Example 1).

Definition 7 (Naive Agent) An agent a is naive iff for every A′ ∈ F(A′ ,Ag), attack(u, u′ ) ∈ Pr(A′ ) iff u′ ∈ A′ and u′ ←a u holds in Aa.

Intuitively, naive agents perform every possible attack available to them, irrespectively of the strategic behaviour of other agents. A DAS P is naive iff every agent in Ag is naive. Then, we remark that for naive DAS the converse of (∗) actually holds.

2.3 The Specification Language FOA-ATL

We now introduce a formal language to specify properties of interest of DAS. Arguments in DAS call for the use of firstorder logic, whereas strategy operators are needed to account for agents' behaviour. To the best of our knowledge, no logic combining these two features has ever been studied.

Definition 8 (FOA-ATL) The FOA-ATL formulas ϕ, with free variables fr(ϕ), are defined as follows:

• if ψ is an FOA-formula, then it is an FOA-ATL formula;
• if ϕ is a formula and N ⊆ Ag, then ¬ϕ, 〈〈N〉〉Xϕ, and 〈〈N〉〉Gϕ are formulas with fr(¬ϕ) = fr(〈〈N〉〉Xϕ) = fr(〈〈N〉〉Gϕ) = fr(ϕ);
• if ϕ and ϕ′ are formulas with fr(ϕ) = fr(ϕ′ ) and N ⊆ Ag, then ϕ → ϕ′ and 〈〈N〉〉ϕUϕ′ are formulas with fr(ϕ → ϕ′ ) = fr(〈〈N〉〉ϕUϕ′ ) = fr(ϕ) = fr(ϕ′ );
• if ϕ is a formula with fr(ϕ) = {y}, then ∀y(Aa(y, x) → ϕ) and ∀yϕ are formulas with fr(∀y(Aa(y, x) → ϕ)) = {x} and fr(∀yϕ) = ∅.

The language FOA-ATL is a first-order extension of the alternating-time temporal logic ATL [Alur et al., 2002]. The FOA-ATL formulas (i) 〈〈N〉〉Xϕ, (ii) 〈〈N〉〉Gϕ and (iii) 〈〈N〉〉ϕUϕ′ are read as "the agents in N have a strategy to..." (i) "...enforce ϕ at the next state", (ii) "...always enforce ϕ", and (iii) "...enforce ϕ until ϕ′ ".

To intepret FOA-ATL formulas on DAS we need to introduce the notion of a strategy for a set N of agents. An Nstrategy is a mapping fN : S + ↦→ ⋃a∈N Acta(A) s.t. fN(κ · (s, a)) ∈ Pra(s) for every κ ∈ S ∗ . Intuitively, a strategy returns an enabled action in Acta(A) for every non-empty, finite sequence of states in S +. We remark that, according to standard terminology in concurrent game models [Bulling et al., 2010], the agents in DAS have perfect information and perfect recall, that is, their strategies are determined by all information available at each global state, for all states visited up to the current state. Further, the outcome of strategy fN at state (s, a), or out((s, a), fN), is the set of all (s, a)-runs λ s.t. for every b ∈ N, (λ(i+1), b′ ) = τ((λ(i), b), fN(λ[0, i])) for all i ≥ 0. As above, we assume that strategies respect agents' turns and simply write out(s, fN), thus omitting agents whenever the latter are clear by the context.

Definition 9 (Semantics of FOA-ATL) We define whether an argument u satisfies a formula ϕ at state s in a DAS P, or (P, s, u) |= ϕ, as follows (clauses for propositional connectives are straightforward and thus omitted):

(P, s, u) |= ψ iff (s, π, u) |= ψ, if ψ is an FOA-formula (P, s, u) |= 〈〈N〉〉Xϕ iff for some N-strategy fN, for all λ ∈ out(s, fN), (P, λ(1), u) |= ϕ (P, s, u) |= 〈〈N〉〉Gϕ iff for some N-strategy fN, for all λ ∈ out(s, fN), i ≥ 0, (P, λ(i), u) |= ϕ (P, s, u) |= 〈〈N〉〉ϕUϕ′ iff for some N-strategy fN, for all λ ∈ out(s, fN), for some k ≥ 0, (P, λ(k), u) |= ϕ′ , and for all j, 0 ≤ j < k implies (P, λ(j), u) |= ϕ (P, s, u) |= ∀y(Aa(y, x) →ϕ) iff for every v ∈ s, u ←a v implies (P, s, v) |= ϕ (P, s, u) |= ∀yϕ iff for every v ∈ s, (P, s, v) |= ϕ

A formula ϕ is true at s, or (P, s) |= ϕ, if (P, s, u) |= ϕ for every arguments u ∈ s; ϕ is true in P, or P |= ϕ, if (P, s0) |= ϕ for all s0 ∈ I.

We illustrate now the expressiveness of FOA-ATL through some example properties that involve strategic and argumentation-theoretic features.

Example 3 The following formula states that opponent o can force proponent p to run out of moves in the next state:

This formula is for instance true at argument t1 in the DAS of Example 1. ■

Example 4 The following formula states that proponent p has a strategy enforcing the set of arguments in P, which includes the current argument, to be conflict-free (respectively, acceptable, admissible, complete, stable):

where χ ∈ {Cfr,Acc,Adm,Cmp, Stb}. 2 Let us focus for instance on P(x) ∧ 〈〈p〉〉G Adm(P). This is a desirable requirement for proponent's strategies in dialogue games for the grounded extension (recall Example 1) or credulous admissibility [Vreeswijk and Prakken, 2000]. This statement is false of the DAS of Example 1 (at argument t1), where o, by moving attack(u1, t1), forces p to run out of moves, no matter what interpretation π of P is selected. In fact p has no strategy to force any set of arguments containing t1 (the initial argument) to be admissible. That is: P(x) → 〈〈o〉〉G ¬Adm(P) or, equivalently, P(x) →¬〈〈p〉〉GAdm(P) for any P. 3 ■

3 Verifying Dynamic Argumentation Systems

In Section 2 we introduced DAS as a general model for (abstract) argument-based multi-agent interaction. We tailored an influential game logic in order to provide DAS with the specification language FOA-ATL. We are then able to define a model checking problem whereby strategic and argumentation-theoretic properties, such as those expressed in (1) and (2) above, can be checked against a given DAS.

Definition 10 (Model Checking Problem) Given a DAS P and an FOA-ATL-formula ϕ, determine whether for every s0 ∈ I, (P, s0, u0) |= ϕ for some argument u0.

In case that ϕ is a sentence with no free variable, the model checking problem reduces to verify whether P |= ϕ.

Model checking general data-aware systems is known to be undecidable [Deutsch et al., 2007]. In [Belardinelli et al., 2012; 2014] the same problem is proved decidable for bounded and uniform systems. Without going into details, we remark that DAS do not normally satisfy these requirements. Therefore new techniques need to be developed.

In this section we introduce a notion of bisimulation to explore under which circumstances two DAS satisfy the same formulas. In particular, we show that bisimilar DAS satisfy the same FOA-ATL formulas. Then, we investigate how the static properties of AF impact on the dynamics of DAS. This kind of results is key to tackle the model checking problem, as they allow to verify a DAS P by model checking a bisimilar DAS P ′ .

2 Recall the properties in Table 1.

3 It is a known validity of turn-based asynchronous ATL that 〈〈N〉〉Gφ ↔ 〈〈Ag\N〉〉¬φ [Alur et al., 2002].

3.1 Bisimulations for Argument Frameworks

A notion of bisimulation can naturally be defined on AF (cf. [Grossi, 2010]).

Definition 11 (Static Bisimulation) Let (A, π) = 〈A, {←a }a∈Ag, π〉 and (A′ , π′ ) = 〈A′ , {←′a }a∈Ag, π′ 〉 be interpreted AF defined on a set Ag of agents. A static bisimulation is a relation S ⊆ A×A′ s.t. for u ∈ A, u′ ∈ A′ , S(u, u′ ) implies

• (i) for every predicate symbol P, u ∈ π(P) iff u′ ∈ π′ (P);
• (ii) for every v ∈ A, if u ←a v then for some v′ ∈ A′ , u′ ←′a v′ and S(v, v′ );
• (iii) for every v′ ∈ A′ , if u′ ←′a v′ then for some v ∈ A, u ←a v and S(v, v′ ).

Two arguments u ∈ A, u′ ∈ A′ are bisimilar, or u ≃ u′ , iff S(u, u′ ) for some static bisimulation S. Finally, two AF A and A′ are statically bisimilar (or simply bisimilar) iff (i) for every u ∈ A, u ≃ u′ for some u′ ∈ A′ ; and (ii) for every u′ ∈ A′ , u′ ≃ u for some u ∈ A. We denote this as A ≃ A′ .

We can now show that bisimilar states satisfy exactly the same FOA-formulas.

Lemma 1 Given bisimilar interpreted AF (A, π) and (A′ , π′ ), and bisimilar arguments u ∈ A and u′ ∈ A′ , then for every FOA-formula ϕ,

As a result, bisimilar AF cannot be distinguished by FOAformulas. In the following we explore the conditions under which this applies to DAS as well. In particular, we say that DAS P and P ′ are statically bisimilar iff AP ≃ AP ′ for some static bisimilation that maps initial states into initial states.

3.2 Bisimulations for DAS

We first introduce a notion of dynamic bisimulation, and then explore its properties in the context of DAS. In the rest of the section we let P = 〈Ag, I, τ, π〉 and P ′ = 〈Ag, I ′ , τ ′ , π′ 〉 be two DAS defined on the same set Ag of agent names. Notice that, albeit agents may have the same name, they might differ as to their argumentation frameworks, actions, or protocols.

Definition 12 (Dynamic Simulation) Given DAS P and P ′ , a dynamic simulation is a relation R ⊆ S ×S ′ s.t. for s ∈ S, s′ ∈ S ′ , R(s, s′ ) implies:

1. s ≃ s′ for some static bisimulation S;

1. for every t ∈ S, if s -→a t then for some t′ ∈ S ′ , s′ -→′a t′ , t ≃ t′ for some bisimulation S′ ⊇ S, and R(t, t′ ).

In Def. 12 we implicitly assume that the simulation relation relates states with turns for the same active agent in Ag. Simulations can then be naturally extended to bisimulations.

Definition 13 (Dynamic Bisimulation) A relation D ⊆ S × S ′ is a dynamic bisimulation iff both D and D-1 = {〈s′ , s〉 | D(s, s′ )} are dynamic simulations.

Two states s ∈ S and s′ ∈ S ′ are dynamically bisimilar, or s ≈ s′ , iff D(s, s′ ) for some bisimulation relation D. It can be shown that ≈ is the largest dynamic bisimulation, and an equivalence relation, on S ∪ S ′ . DAS P and P ′ are dynamically bisimilar, or P ≈ P ′ , iff (i) for every s0 ∈ I, s0 ≈ s′0

o

for some s′0 ∈ I ′ , and (ii) for every s′0 ∈ I ′ , s0 ≈ s′0 for some s0 ∈ I. Notice that arguments u and u′ are or are not bisimilar always w.r.t. some states s ∈ S and s ∈ S ′ . We state this explicitly by saying that u ≃ u′ w.r.t. s and s′ . In particular, by Def. 13, if s ≈ s′ and u ≃ u′ w.r.t. s and s′ , then u and u′ are still bisimilar in all subsequent bisimilar states. This is a key feature for proving preservation of satisfaction for FOA-ATL formulas.

The first result we prove on bisimulations shows that being statically bisimilar does not imply dynamic bisimilarity, not even in the case of naive agents.

Lemma 2 Static bisimilarity does not imply dynamic bisimilarity, that is, there exist naive, statically bisimilar DAS P and P ′ such that P ̸≈ P ′ .

In Fig. 2 we report DAS P and P ′ , whose underlying AF are statically bisimilar, but that are not dynamically bisimilar.

We now show that dynamically bisimilar states satisfy the same FOA-ATLformulas.

Theorem 3 Suppose that s ≈ s′ , and u ≃ u′ w.r.t. s and s′ . Then for every FOA-ATL formula ϕ,

As a result, dynamic bisimulations preserve the satisfaction of FOA-ATL formulas. In particular, we can tackle the problem of model checking a DAS P by verifying a bisimilar DAS P ′ , and then transfering the result by Theorem 3. In particular, DAS P ′ may exhibit nice structural properties (such as being finite) that can make the verification task feasible.

3.3 From Static Properties to Dynamics

In this section we make use of bisimulations to explore how the static properties of DAS determine their dynamic features. In Lemma 2 we showed that this relationship is not straightforward, not even in the case of naive DAS. However, in some specific cases there is indeed a correspondence. The first result reduces dynamic bisimulations to static bisimulations, together with some constraints on temporal transitions. As usual, we assume that turns are respected.

Theorem 4 Let P and P ′ be DAS. Suppose that P ′ is naive and for every u ∈ s ∈ S, u′ ∈ s′ ∈ S ′ , if s ≃ s′ , u ≃ u′ w.r.t. s and s′ , and u ←a v in AP for some v ∈ A, then u′ ←′a v′ in AP ′ for some v′ ∈ A′ and either

1. v ∈ s and either (i) v′ ∈ s′ and v ≃ v′ w.r.t. s and s′ , or (ii) v′ /∈ s′ and for no w ∈ s, v ←a w in s,
2. or v /∈ s and either (i) v′ /∈ s′ , or (ii) v′ ∈ s′ and for no w′ ∈ s′ , v′ ←′a w′ in s′ .

Then, D = {(s, s′ ) | s ≃ s′} is a dynamic simulation between P and P ′ .

Notice that the assumptions in Theorem 4 imply that DAS P and P ′ are statically bisimilar. However, they have also to satisfy extra conditions (1) and (2).

The main contribution of Theorem 4 is to show that the notion of dynamic bisimulation can be reduced to static bisimulation, together with some assumptions on the structural properties of AF AP and AP ′ , in case that we consider naive DAS. Hence, in order to verify DAS we can simply model check statically bisimilar systems, and then transfer the result by using Theorem 4.

It is of interest to analyse DAS that actually satisfy the conditions above. For example, it is easy to check that whenever the underlying AF AP and AP ′ of naive DAS P and P ′ are directed acyclic graphs (DAG), where every argument is attacked by some other argument, then the conditions in Theorem 4 do indeed hold. So, for this class of naive DAS structural, static features do determine their dynamic properties.

Corollary 5 Suppose that DAS P and P ′ are naive and statically bisimilar, and that AP and AP ′ are DAG where every argument is attacked by some other argument. Then, P and P ′ are dynamically bisimilar and therefore satisfy the same FOA-ATL formulas.

4 Conclusions and FurtherWork

In many dialectical situations it is difficult to assume beforehand a bound on the number of arguments that agents have at their disposal. While some properties of such infinite argumentation frameworks have recently been investigated, their implication on debates amongst agents had not been analysed before. In this paper we set up and explored the framework of dynamic argumentation systems through a logic lens. We showed that in general static bisimilarity is not strong enough to capture equivalence of DAS (in terms of FOA-ATL formulas they satisfy), and introduced a novel notion of dynamic bisimilarity. For some specific structures (in particular acyclic ones), the static notion remains powerful enough, at least for the naive agents studied here. While in this paper we have focused on such agents (unconstrained in their argumentative moves as long as they are relevant and truthful), an interesting direction of research is to investigate how more restricted protocols would also impact the dynamics of DAS. Another noteworthy feature of our framework is that formulas in FOA-ATL can express the ability for a group of agents to ensure, for instance, that some arguments gets accepted-thus paving the way for a logical analysis of multiparty protocols, see e.g. [Bonzon and Maudet, 2011].

Acknowledgements.

The third author benefited from the support of the project AMANDE ANR-13-BS02-0004 of the French National Research Agency (ANR).