232
M. Bozga et al.
Interaction Logic. For a constant κ ≥ 1, fixed throughout the paper, the Interaction
Logic ILκ is built on top of a countably infinite set Var of variables, the set Pred =
N
k=1 P
k of monadic predicate symbols ranged over by pr (i.e. the logic has a predicate
symbol for each port), the binary predicate ≤, and the successor functions succ 0 , ...,
succ κ−1 , of arity one. The formulae of ILκ are generated by the syntax
t := i ∈ Var | succ 0 (t) | ... | succ κ−1 (t)
terms
φ := t 1 ≤ t 2 | pr(t) | φ 1 ∧ φ 2 | ¬φ 1 | ∃i . φ 1 formulae
Abbreviations like t 1 = t 2 , t 1 < t 2 , φ 1 ∨ φ 2 , φ 1 ↔ φ 2 , and ∀i . φ are defined as usual.
ILκ is interpreted over finite ranked trees of arity κ, which we identify with a prefixclosed language of words, also called nodes, over the alphabet {0, . . . , κ − 1}. The root of
the tree is the empty word , and the children of w are w0, w1,..., w(κ − 1). Formally,
an interpretation or structure is a pair I = (U,ι), where the universe U is a tree and
ι assigns a node to each variable and a set of nodes to each predicate in Pred. The
predicate ≤ and the functions succ 0 ,...,succ k−1 have the usual fixed interpretations: If t
and t are interpreted as w and w , then t 1 ≤ t 2 holds iff w is a prefix of w , and succ i (t) is
interpreted as the node wi, if wi ∈ U, and as the root otherwise. So, loosely speaking,
successor functions wrap around to the root.
When κ = 1, formulae are interpreted on languages {, 0, 00,..., 0 n−1 } for some number n. To simplify notation, in this case we assume that they are interpreted over the set
{0, 1,..., n − 1}, and succ 0 is the usual successor function on numbers, modulo n.
Intuitively, a universe U determines an instance of the component-based system,
with one instance of each component for each w ∈ U. So, for example, for κ = 1 and
U = {0, 1, 2,..., n − 1} in our running example we have philosophers 0, 1,...,n − 1 and
forks 0, 1,..., n − 1. Generally, with κ = 1 we can describe pipeline and token-ring architectures, whereas higher values describe tree-shaped architectures.
Interaction formulae. A formula of ILκ is an interaction formula if it is the conjunction
of the following formula:
∀i∀ j .
p,q∈Pred
type(p)=type(q)
p(i) ∧ q( j) → i j
(3)
with a finite disjunction of formulae of the form:
C(i 1 ,..., i )
def
= ϕ ∧
j=1 p j (i j ) ∧
m
j=1 ∀k . ψ j → q j (k)
(4)
where ϕ, ψ 1 , . . . , ψ m are conjunctions of atomic formulae of the form t 1 ≤ t 2 and their
negations. Intuitively, formula (3) is a generic axiom that prevents two ports of the same
instance of a component type from interacting. The formulae of form (4) are called the
clauses of the interaction formula.
Example 1. Consider a component-based system S = C
1
, C
2
,Γ, where C
1 and C
2 have
ports p 1 and p 2 , respectively, and Γ has one single clause
C(i, j, k) = (i < j ∧ k = succ( j)) ∧ (p 1 (i) ∧ p 2 ( j)) ∧ ∀i.i > k → p 1 (i)
Γ states that an interaction consists of: the i-th process of type C
1 executes transition p 1 ;
the j-th process of type C
2 executes p 2 ; and, for every i > ( j + 1) mod n, the i-th process
of type C
1 executes transition p 1 as well; all this happens simultaneously in one atomic
step.
M. Bozga et al.
Interaction Logic. For a constant κ ≥ 1, fixed throughout the paper, the Interaction
Logic ILκ is built on top of a countably infinite set Var of variables, the set Pred =
N
k=1 P
k of monadic predicate symbols ranged over by pr (i.e. the logic has a predicate
symbol for each port), the binary predicate ≤, and the successor functions succ 0 , ...,
succ κ−1 , of arity one. The formulae of ILκ are generated by the syntax
t := i ∈ Var | succ 0 (t) | ... | succ κ−1 (t)
terms
φ := t 1 ≤ t 2 | pr(t) | φ 1 ∧ φ 2 | ¬φ 1 | ∃i . φ 1 formulae
Abbreviations like t 1 = t 2 , t 1 < t 2 , φ 1 ∨ φ 2 , φ 1 ↔ φ 2 , and ∀i . φ are defined as usual.
ILκ is interpreted over finite ranked trees of arity κ, which we identify with a prefixclosed language of words, also called nodes, over the alphabet {0, . . . , κ − 1}. The root of
the tree is the empty word , and the children of w are w0, w1,..., w(κ − 1). Formally,
an interpretation or structure is a pair I = (U,ι), where the universe U is a tree and
ι assigns a node to each variable and a set of nodes to each predicate in Pred. The
predicate ≤ and the functions succ 0 ,...,succ k−1 have the usual fixed interpretations: If t
and t are interpreted as w and w , then t 1 ≤ t 2 holds iff w is a prefix of w , and succ i (t) is
interpreted as the node wi, if wi ∈ U, and as the root otherwise. So, loosely speaking,
successor functions wrap around to the root.
When κ = 1, formulae are interpreted on languages {, 0, 00,..., 0 n−1 } for some number n. To simplify notation, in this case we assume that they are interpreted over the set
{0, 1,..., n − 1}, and succ 0 is the usual successor function on numbers, modulo n.
Intuitively, a universe U determines an instance of the component-based system,
with one instance of each component for each w ∈ U. So, for example, for κ = 1 and
U = {0, 1, 2,..., n − 1} in our running example we have philosophers 0, 1,...,n − 1 and
forks 0, 1,..., n − 1. Generally, with κ = 1 we can describe pipeline and token-ring architectures, whereas higher values describe tree-shaped architectures.
Interaction formulae. A formula of ILκ is an interaction formula if it is the conjunction
of the following formula:
∀i∀ j .
p,q∈Pred
type(p)=type(q)
p(i) ∧ q( j) → i j
(3)
with a finite disjunction of formulae of the form:
C(i 1 ,..., i )
def
= ϕ ∧
j=1 p j (i j ) ∧
m
j=1 ∀k . ψ j → q j (k)
(4)
where ϕ, ψ 1 , . . . , ψ m are conjunctions of atomic formulae of the form t 1 ≤ t 2 and their
negations. Intuitively, formula (3) is a generic axiom that prevents two ports of the same
instance of a component type from interacting. The formulae of form (4) are called the
clauses of the interaction formula.
Example 1. Consider a component-based system S = C
1
, C
2
,Γ, where C
1 and C
2 have
ports p 1 and p 2 , respectively, and Γ has one single clause
C(i, j, k) = (i < j ∧ k = succ( j)) ∧ (p 1 (i) ∧ p 2 ( j)) ∧ ∀i.i > k → p 1 (i)
Γ states that an interaction consists of: the i-th process of type C
1 executes transition p 1 ;
the j-th process of type C
2 executes p 2 ; and, for every i > ( j + 1) mod n, the i-th process
of type C
1 executes transition p 1 as well; all this happens simultaneously in one atomic
step.