The Timed Concurrent Language for Argumentation (tcla) is a framework to model concurrent interactions between communicating agents that reason and take decisions through argumentation processes, also taking into account the temporal duration of the performed actions. Time is, indeed, a crucial factor when dealing with dynamic environments in real-world applications, where agents need to act in a coordinated fashion to reach their own goals. In this paper, we discuss the syntax and the operational semantics of tcla, providing insights on how its constructs can be used to realise complex interactions between agents.
Argumentation Theory aims to understand and model the human natural fashion of reasoning, allowing one to deal with uncertainty in non-monotonic (defeasible) reasoning. In his seminal paper [1], Dung defines the building blocks of abstract argumentation.
Definition 1 (AFs). Let be the set of all available arguments1, that we call “universe”. An Abstract Argumentation Framework is a pair ⟨, ⟩ where ⊆ is a set of adopted arguments and is a binary relation on .
For two arguments , ∈ , the notation (, ) ∈ represents an attack directed from against . Acceptability of arguments is then computed through methodologies like the reinstatement labelling presented in [7], starting from attack relations in the framework. Definition 2 (Reinstatement labelling). Let F = ⟨, ⟩ be an AF and consider the set of labels L = {in, out, undec}. A labelling of F is a total function : → L. We define () = { ∈ | () = in}, () = { ∈ | () = out} and () = { ∈ | () = undec}. We say that is a reinstatement labelling if and only if it satisfies the following: • ∀ ∈ : ∈ () ⇐⇒ ∀ ∈ | (, ) ∈ : ∈ () • ∀ ∈ : ∈ () ⇐⇒ ∃ ∈ | (, ) ∈ ∧ ∈ ()
A labelling-based semantics [8] associates with an AF a subset of all the possible labellings. In Figure 1 we show an example of reinstatement labelling on an AF in which arguments and highlighted in green are in, red ones ( and ) are out, and the yellow argument (that attacks itself) is undec.
Given a labelling , it is possible to identify a correspondence with the extension-based semantics [8]. In particular, the set of in arguments coincides with a complete extension, while other semantics can be obtained through restrictions (as shown in Table 1 of [7]). In the following, we use ∈ ( ) to denote a labelling corresponding to an extension of the semantics . Besides computing a labelling for a certain semantics , one of the most common tasks performed on AFs is to verify whether an argument has a certain label in some labelling (credulous test) or in all labellings (sceptical test).
1The set is not present in the original definition by Dung and we introduce it for our convenience.
The syntax of tcla is presented in Table 1, where , , and denote a generic process, a sequence of procedure declarations (or clauses)2, a generic agent and a generic guarded agent, respectively. In Table 2, then, we give the definitions for the transition rules. ::= ., ::= . ::= | | (, ) → | (, ) → | | ‖ ::= ℎ(, ) → | -(, , ) → | -(, , ) → | + | + | ‖
Communication between tcla agents is implemented via shared memory, similarly to cla [5] and CC [9]. In the following, we denote by ℰ the class of guarded agents and by ℰ0 the class of guarded agents such that all outermost guards have = 0. Suppose we have an agent whose knowledge base is represented by a framework = ⟨, ⟩. An (′, ′) action performed by the agent results in the addition of a set of arguments ′ ⊆ (where is the universe) and a set of relations ′ to . When performing an addition, (possibly) new arguments are taken from ∖ . Intuitively, (, ) allows to specify arguments and/or attacks to be removed from the knowledge base. The removal of an argument from an AF also involves removing all attack relations outgoing from and incoming to that argument, thus making preserve the structure of an AF.
The -(, , ) → , -(, , ) → and ℎ(, ) → constructs are
explicit timing primitives that allow for the specification of timeouts. The operator ℎ(′, ′)
(rules Ch (
The operator + (If (
2Note that infinite sequences of procedure declarations are also allowed.
⟨(′, ′) → , ⟨, ⟩⟩ →− ⟨ , ⟨ ∪ ′, ∪ ′′⟩⟩
with ′′ = {(, ) ∈ ′ | , ∈ ∪ ′} ⟨(′, ′) → , ⟨, ⟩⟩ →− ⟨ , ⟨ ∖ ′, ∖ {′ ∪ ′′}⟩⟩ with ′′ = {(, ) ∈ | ∈ ′ ∨ ∈ ′}
′ ⊆ ∧ ′ ⊆ > 0 ⟨ℎ(′, ′) → , ⟨, ⟩⟩ →− ⟨ , ⟨, ⟩⟩
′ ̸⊆ ∨ ′ ̸⊆ > 0 ⟨ℎ(′, ′) → , ⟨, ⟩⟩ →− ⟨ ℎ− 1(′, ′) → , ⟨, ⟩⟩ ⟨ℎ0(′, ′) → , ⟩ →− ⟨ , ⟩
∃ ∈ () | = () > 0 ⟨-(, , ) → , ⟩ →− ⟨ , ⟩
∀ ∈ (). ̸= () > 0 ⟨-(, , ) → , ⟩ →− ⟨ -− 1(, , ) → , ⟩ ⟨-0(, , ) → , ⟩ →− ⟨ , ⟩
∀ ∈ (). = () > 0 ⟨-(, , ) → , ⟩ →− ⟨ , ⟩
∃ ∈ () | ̸= () > 0 ⟨-(, , ) → , ⟩ →− ⟨ -− 1(, , ) → , ⟩ ⟨-0(, , ) →− , ⟩ →− ⟨ , ⟩ ⟨1, ⟩ →− ⟨ 1, ⟩, 1 ̸∈ ℰ0, 1 ̸∈ ℰ
⟨1 + 2, ⟩ →− ⟨ 1, ⟩ ⟨1, ⟩ →− ⟨ 1′, ⟩, 1 ̸∈ ℰ0, 1′ ∈ ℰ ⟨1 + 2, ⟩ →− ⟨ 1′ + 2, ⟩ 1 ∈ ℰ0, ⟨2, ⟩ →− ⟨ 2, ⟩
⟨1 + 2, ⟩ →− ⟨ 2, ⟩ ⟨1, ⟩ →− ⟨ 1, ⟩, ⟨2, ⟩ →− ⟨ 2, ⟩, 1, 2 ̸∈ ℰ0, 1 ̸∈ ℰ
⟨1‖2, ⟩ →− ⟨ 1‖2, ⟩ ⟨1, ⟩ →− ⟨ 1′, ⟩, ⟨2, ⟩ →− ⟨ 2′, ⟩, 1, 2 ̸∈ ℰ0, 1′, 2′ ∈ ℰ ⟨1‖2, ⟩ →− ⟨ 1′‖2′, ⟩ 1 ∈ ℰ0, ⟨2, ⟩ →− ⟨ 2, ⟩
⟨1‖2, ⟩ →− ⟨ 2, ⟩ ⟨1, ⟩ →− ⟨ ′1, ′⟩, ⟨2, ⟩ →− ⟨ ′2, ′′⟩
⟨1‖2, ⟩ →− ⟨ ′1‖′2, * (, ′, ′′)⟩
⟨1, ⟩ →− ⟨ 1, ⟩, 1 ̸∈ ℰ0, 1 ̸∈ ℰ
⟨1 + 2, ⟩ →− ⟨ 1, ⟩
1 ∈ ℰ0, ⟨2, ⟩ →− ⟨ 2, ⟩ ND (
⟨1 + 2, ⟩ →− ⟨ 2, ⟩ ⟨1, ⟩ →− ⟨ 1′, ⟩, ⟨2, ⟩ →− ⟨ 2′, ⟩, 1, 2 ̸∈ ℰ0, 1′, 2′ ∈ ℰ ⟨1 + 2, ⟩ →− ⟨ 1′ + 2′, ⟩ Ad
Re
Ch (
If (
Pa
ND (
The guarded parallelism GP (
In this paper, we introduced tcla, a concurrent argumentation language for modelling interacting agents in which also time is taken into account. We presented both the syntax and the operational semantics. Maximal parallelism has been used to realise simultaneous execution of actions carried forward by diferent agents. As a future work, we want to adopt an interleaving approach for handling this kind of processes: we plan to have a diferent transition system in which time elapsing and computational steps are realised by two distinct types of actions.