First-order logic for safety verification of hedge rewriting systems
Electronic Communications of the EASST
Volume 72 (2015)
Proceedings of the
15th International Workshop on
Automated Verification of Critical Systems (AVoCS 2015)
First-order logic for safety verification of hedge rewriting systems
Alexei Lisitsa
14 pages
Guest Editors: Gudmund Grov, Andrew Ireland
ECEASST Home Page: http://www.easst.org/eceasst/ ISSN 1863-2122
http://www.easst.org/eceasst/
ECEASST
First-order logic for safety verification of hedge rewriting systems
Alexei Lisitsa1
Department of Computer Science, The University of Liverpool
Abstract: In this paper we deal with verification of safety properties of hedge
rewriting systems and their generalizations. The verification problem is translated
to a purely logical problem of finding a finite countermodel for a first-order formula,
which is further tackled by a generic finite model finding procedure. We show that
the proposed approach is at least as powerful as the methods using regular invariants.
At the same time the finite countermodel method is shown to be efficient and appli-
cable to the wide range of systems, including the protocols operating on unranked
trees.
Keywords: hedge rewriting, safety verification, first-order logic
1 Introduction
Hedges, or arbitrary width trees over unranked alphabets, also known as unranked trees or forests
provide with the abstractions useful in several verification contexts. Hedges and hedge transfor-
mations (rewritings) have been used for specification and verification of at least the following:
• Protocols working in tree-shaped networks of unbounded degree [27];
• XML transformations [30, 23, 27];
• Multithreaded recursive programs [8, 29].
The most challenging task of infinite state or parameterized verification appears when one
would like to establish the correctness of a system in a widest possible context - either for all
possible sizes of the system or for unbounded computations. In general such a problem is unde-
cidable and the only way to address it is to focus on restricted classes of systems and properties.
In this paper we consider the problem of safety verification for hedge rewriting systems and
explore the applicability of the very general method based on disproving the first-order formulae
by finding a countermodel. The basic intuition behind the method is that if the evolution of
the system of interest can be faithfully modelled by the derivations within first-order logic then
the safety (non-reachability of bad states) can be naturally reduced to disproving the formulae
(non-provability).
Such an approach to the safety verification has been proposed in the early work on the verifi-
cation of cryptographic protocols [28, 25, 12] and later has been extended to various classes of
parameterized and infinite state verification tasks [16, 18, 19, 20, 21].
Two attractive properties of the approach have emerged. On the one side it has turned out to
be practically efficient in many applications. On the other side it has proved to be relatively com-
plete with respect to the methods using regular invariants, in particular regular model checking,
regular tree model checking and tree completion.
1 / 14 Volume 72 (2015)
First-order logic for safety verification
Safety verification for hedge rewriting systems has been already addressed e.g. in [14, 11, 27]
with the regular invariants playing the major role.
We show in this paper the Finite CounterModel method (FCM) provides a viable alternative
to the methods using regular invariants for the verification of hedge rewriting systems. We show
that theoretically the proposed approach is at least as powerful as the methods using regular
invariants. At the same time the finite countermodel method is shown to be very flexible and
applicable to the wide range of systems. The practical efficiency of the method is illustrated
on a set of examples on verification of (1) parameterized protocols operating on arbitrary width
tree topology – for most of them an automated verification is reported for the first time; and (2)
dynamic multithreaded recursive programs.
The paper is organized as follows. The next section provides with necessary preliminaries.
In Section 3 we formulate basic verifcation problem and its translation into a logical problem
of first-order formulae disproving. In Section 4 the verification method is discussed and its
relative completeness is demonstrated. Section 5 presents the experimental results and Section 6
concludes the paper.
2 Preliminaries
2.1 First-order Logic
A first-order vocabulary is defined as a finite set Σ = F ∪P where F and P are the sets of
functional and predicate symbols, respectively. Each symbol in Σ has an associated arity, and
we have F = ∪i≥0Fi and P = ∪i≥1Pi, where Fi and Pi consist of symbols of arity i. The
elements of F0 are also called constants.
A first-order model over vocabulary Σ, or just a model is a pair M = 〈D,[[Σ]]D〉 where D is
a non-empty set called domain of M and [[Σ]]D denotes the interpretations of all symbols from
Σ in D. For a domain D and a function symbol f of arity n ≥ 1 an interpretation of f in D is a
function [[ f ]]D : Dn → D. For a constant c its interpretation [[c]]D is an element of D. For a domain
D and a predicate symbol P of arity n an interpretation of P in D is a relation of arity n on D, that
is [[P]]D ⊆ Dn. The model M = 〈D,[[Σ]]D〉 is called finite if D is a finite set.
We assume that the reader is familiar with the standard definitions of first-order formula, first-
order sentence, satisfaction M |= ϕ of a formula ϕ in a model M , deducibility (derivability)
Φ ` ϕ of a formula ϕ from a set of formulae Φ, first-order theory and equational theory.
2.2 Hedge Rewriting
We borrow the definitions from [14] with minor modifications. Let Σ be a finite alphabet and X
be a countable set of variables. Then the set of terms T (Σ,X ) and the set of hedges H (Σ,X ),
both over Σ and X , are defined inductively as the least sets satisfying
• T (Σ,X ) = X ∪{ f (h) | f ∈ Σ,h ∈ H (Σ,X )}
• H (Σ,X ) =
⋃
n>0{t1,...,tn | t j ∈ T (Σ,X ), j = 1,...,n}∪{Λ}
Thus, a hedge is a finite (possibly empty) sequence of terms, whereas a term is obtained by
applying an unranked functional symbol to a hedge. We denote by Λ the empty sequence of
Proc. AVoCS 2015 2 / 14
ECEASST
terms. We do not make a difference between a term and a hedge of length one, i.e. consider that
T (Σ,X )⊂H (Σ,X ). We will also do not distinguish the hedges of the form fi1(Λ),..., fik (Λ)
and words fi1,..., fik ∈ Σ
∗.
The sets of ground terms and ground hedges ( i.e., terms and hedges without variables) are
denoted T (Σ) and H (Σ). A variable x ∈ X is called linear in a hedge h ∈ H (Σ,X ) if it has
exactly one occurrence in h.
The set of variables occurring in a term t ∈ T (Σ,X ) is denoted var(t). A substitution σ is a
mapping from X to H (Σ,X ). The application of a substitution σ to a hedge h, denoted hσ , is
defined inductively as follows. For t1,...,tn ∈ T (Σ,X ) we have (t1,...,tn)σ = t1σ ...tnσ and
f (h)σ = f (hσ).
A context is a hedge h ∈ H (Σ,X ) with a distinguished variable x linear in h. We write C[x]
to denote a context with a distinguished variable x. The application of a context C[x] to a hedge
h is defined by C[h] = C{x 7→ h}.
A hedge rewriting system (HRS) is a set of rewriting rules of the form l → r, where l,r ∈
H (Σ,X ). The rewrite relation →R (resp. outer rewrite relation R ) of an HRS R is defined
as follows: h →R h′ iff there is a context C[x] (resp. a trivial context C[x] = x), a rule l → r ∈ R
and a substitution σ such that h = C[lσ] and h′ = C[rσ]. The reflexive and transitive closure of
→R (resp. R ) is denoted by →∗R (resp.
∗
R ).
Given a set of ground hedges L ⊆ H (Σ) and an HRS R we denote by post∗R(L) the set of all
hedges reachable from L, that is {h ∈ H (Σ) | ∃g ∈ L,g →∗R h}. Similarly post
∗
R, (L) denotes
{h ∈ H (Σ) | ∃g ∈ L,g ∗R h}.
2.3 Forest Automata and Regular Hedge Languages
The following definition is taken from [5].
Definition 1 A forest automaton over an unranked alphabet Σ is a tuple A = ((Q,e,∗),Σ,δ :
(Σ×Q → Q),F ⊆ Q) where (Q,e,∗) is a finite monoid, δ is a transition function and F is a set
of accepting states.
For every ground hedge h the automaton assigns a value hA ∈Q which is defined by induction:
• ΛA = e;
• f (h)A = δ ( f ,hA )
• (t1,...tn)A = tA1 ∗ ...∗t
A
n
A hedge h is accepted by the forest automaton A iff hA ∈ F . The hedge language LA of the
forest automaton A = ((Q,e,∗),Σ,δ : (Σ×Q → Q),F ⊆ Q) is defined as LA ={h | hA ∈ F}.
A hedge language L is called regular iff it is a hedge language LA of some forest automaton
A . Alternative but equivalent definitions of regular hedge languages using hedge automata and
unranked tree automata have been considered e.g. in [14, 27, 26, 15].
3 / 14 Volume 72 (2015)
First-order logic for safety verification
2.4 Finitely based sets of hedges
For a finite set of hedges B ⊆ H (Σ,X ) the set of ground instances of all hedges from B is
denoted by GI(B), that is GI(B) ={h | ∃h′ ∈ B∧h = h′θ ; h′θ is ground}.
Example 1 For Σ ={a,b, f} and B ={ f (x,b,b,y)} the language GI(B) is the set of all ground
hedges with the outer symbol f and containing two consecutive symbols b at leaves.
Notice that finitely based sets of hedges are not necessarily regular; on the other hand, it is
easy to see that if every hedge in a set B is linear then GI(B) is regular.
3 Safety Verification: from hedge rewriting to FO logic
In this section we define the basic verification problem and its translation into a purely logical
problem of disproving the first-order formula.
3.1 Basic verification problem
The general form of safety verification problems we address in this paper is as follows.
Given: An unranked vocabulary Σ, a hedge rewriting system R over Σ, a language I ⊆ H (Σ)
of initial ground hedges, a language U ⊆ H (Σ) of unsafe ground hedges.
Question: Is it true that ∀h ∈ I∀h′ ∈U h 6→∗R h
′?
We will also consider a variant of the basic verification problem for outer rewriting, where →∗
above is replaced by ∗.
Notice that in the definition of the basic verification problem the sets I and U , in general, may
be infinite. In that case we assume that the sets are defined by some finitary and constructive
means, for example as regular languages given by forest automata, or as finitely based sets of
hedges.
3.2 From hedge rewriting to first-order logic
For an unranked alphabet Σ we denote by Σ f o a ranked vocabulary Σr ∪{e,∗}∪{R(2)} where
Σ
r = { f̃ | f ∈ Σ}, with all f̃ being unary functional symbols, e is a constant (0-ary functional)
symbol, ∗ is a binary functional symbol, which we will use in infix notation and R is a binary
predicate symbol. The constant e will denote the empty hedge, i.e. the hedge of length 0, ∗ will
denote the concatenation of hedges and the semantics of R is going to capture reachability for
hedge rewriting.
Then we define the translation τ : H (Σ,X ) → T (Σ f o,X ) from hedges to terms over the
extended alphabet inductively as follows:
• τ(x) = x for x ∈ X
Proc. AVoCS 2015 4 / 14
ECEASST
• τ(Λ) = e
• τ(t1,...,tn) = Πni=1τ(ti)
• τ( f (h)) = f̃ (τ(h))
Here Πni=1τ(ti) denotes the ∗-product of τ(ti) defined as
• Π1i=1τ(ti) = τ(t1)
• Πk+1i=1 τ(ti) = (Π
k
i=1τ(ti))∗τ(tk+1)
Notice that we will specify associativity of ∗, so exact association of brackets in the product
will be immaterial.
For a hedge rewriting system R over alphabet Σ and a set of variables X we define its trans-
lation ΦR as the set of the following universally closed first-order formulae:
1. (x∗y)∗z = x∗(y∗z)
2. e∗x = x
3. x∗e = x
4. R(τ(h1),τ(h2)) for all (h1 → h2)∈ R
5. R(x,y)→ R((z∗x)∗v,(z∗y)∗v)
6. R(x,y)→ R( f̃ (x), f̃ (y)) for all unary f̃ ∈ Σ f o
7. R(x,x)
8. R(x,y)∧R(y,z)→ R(x,z).
Proposition 1 (Adequacy of the first-order translation) h1 →∗R h2 ⇔ ΦR ` R(τ(h1),τ(h2)) for
all ground h1 and h2.
Proof.
⇒ Due to transitivity of R specified in ΦR it is sufficient to show that if h1 →R h2 then
ΦR ` R(τ(h1),τ(h2)). Assume h1 →R h2 then h1 = C[lσ] and h2 = C[rσ] for some context
C[x], some substitution σ and a rewriting rule (l → r) ∈ R. Now the argument proceeds by a
simple induction on the context construction. Indeed, for the base case of the simplest context
C[x] ≡ x we have h1 ≡ lσ and h2 ≡ rσ and R(τ(h1),τ(h2)) is a ground instance of the formula
R(τ(l),τ(r)) ∈ ΦR (item 4 in the translation). It follows ΦR ` R(τ(h1),τ(h2)). There are two
step cases. Assume C[x] ≡ g1C′[x]g2 where g1 and g2 are ground hedges and C′[x] is a context.
Then we have h1 ≡ g1C′[lσ]g2, h2 ≡ g1C′[rσ]g2 and C′[lσ]→R C′[rσ]. By induction hypothesis
ΦR ` R(τ(C′[lσ]),τ(C′[rσ])). That together with the congruence axiom (5) being in ΦR implies
ΦR ` R(τ(g1)∗τ(C′[lσ])∗τ(g2),τ(g1)∗τ(C′[rσ])∗τ(g2)), and therefore, by definition of τ ,
ΦR ` R(τ(h1),τ(h2)). The second step case with C[x] ≡ f̃ (C′[x]) is dealt with in a similar way
using the congruence axiom (6).
5 / 14 Volume 72 (2015)
First-order logic for safety verification
⇐ Consider the following first-order model M in the vocabulary Σ f o. The domain of the
model is a set H (Σ) of all ground hedges over Σ. The interpretations of functional symbols and
constants are defined inductively as
• [[e]] = Λ;
• [[x∗y]] = [[x]][[y]];
• [[ f (x)]] = f ([[x]]) for all f ∈ Σ.
The interpretation of R is given by [[R]] = {(h,h′) | h,h′ ∈ H (Σ)∧h →∗R h
′}. By simple
structural induction we have [[τ(h)]] = h. That concludes the construction of M.
A straightforward check shows now that for such defined M we have M |= ΦR . Assume now
ΦR ` R(τ(h1),τ(h2)). It follows that M |= R(τ(h1),τ(h2)), that is ([[τ(h1)]],[[τ(h2)]])∈ [[R]], and
therefore (h1,h2)∈ [[R]], which in turn means h →∗R h
′ by definition of [[R]]. �
Taking a contraposition of Proposition 1 we get
ΦR 6` R(τ(h1),τ(h2))⇒ h1 6→∗R h2
which expresses the essence of the proposed verification method: in order to prove non-reachability(≈
safety) it is sufficient to disprove a first-order formula. In order to apply this observation to the
solution of basic verification problems we need to provide also the first-order representations for
the sets of initial and unsafe terms. We start with very general
Definition 2 Given an unranked alphabet Σ and a set of ground hedges H ⊆H (Σ) a first-order
formula ϕH(x) with one free variable and in vocabulary Σ f o, possibly extended by relational and
fucntional symbols, is called first-order representation of H if h ∈ H implies ` ϕH(τ(h)).
3.2.1 First-order representations of regular hedge languages
Let LA be a regular hedge language given by a forest automaton A = ((Q,e,∗),A,δ : (A×Q →
Q),F ⊆ Q).
The vocabulary of the first-order representation of A consists of unary predicates Pq for each
q ∈ Q and unary functional symbols ã for each a ∈ A.
Define ΦA as the set of the following universally closed formulae:
1. (x∗y)∗z = x∗(y∗z);
2. (x∗e) = x;
3. (e∗x) = x;
4. Pδ (a,e)(ã(e)) for every a ∈ A;
5. Pq(x)→ Pδ (a,q)(ã(x)) for every a ∈ A and q ∈ Q.
6. Pq1(x)∧Pq2(y)→ Pq3(x∗y) for all q1,q2,q3 ∈ Q such that q1 ∗q2 = q3 in Q.
Now for the forest automaton A we denote by ΦLA the formula ΦA →
∨
q∈F Pq(x)
Proc. AVoCS 2015 6 / 14
ECEASST
Proposition 2 ΦLA is a first-order representation of LA
Proof (Sketch) Straightforward induction on the hedge construction shows that ΦA `PhA (τ(h)).
The proposition statement follows immediately. �
3.2.2 Finitely based sets of hedges
For a finite set of hedges B ⊆ H (Σ,X ) the formula
∨
h∈B(∃ȳ(x = τ(h))) is a first-order repre-
sentation of GI(B). Here ȳ denotes all variables in τ(h) and x is different from all variables in
ȳ.
3.3 Outer rewriting and unary reachability encoding
In many specification and verification scenarii outer rewriting is sufficient to model all essential
aspects of the evolution of the system of interest. In that case the first-order translations can be
simplified as there is no need in the congruence axioms and the unary reachability predicate does
suffice.
Let R be a hedge rewriting system over alphabet Σ. We define its unary translation ΦUR as the
set of the following universally closed first-order formulae:
1. (x∗y)∗z = x∗(y∗z);
2. (x∗e) = x;
3. (e∗x) = x;
4. R(τ(h1))→ R(τ(h2)) for all (h1 → h2)∈ R .
Such a simplified translation captures reachability by the outer rewrite relation R as the
following proposition states.
Proposition 3 (Adequacy of the unary first-order translation) h1 ∗R h2 ⇔ Φ
U
R ∧R(τ(h1)) `
R(τ(h2)) for all ground h1 and h2.
Proof (Hint) The proof follows the arguments in the proof of Proposition 1 appropriately
modified. To prove ⇒ entailment an easy induction on the length of rewriting is used. To prove
⇐ a semantical argument taking as the interpretation of unary predicate R the set of the term
encodings of all reachable from h1 hedges, is applied. �
4 Back to safety verification
Now we have defined all necessary concepts and the basic verification problem defined in
Sect. 3.1 gets its full specification.
7 / 14 Volume 72 (2015)
First-order logic for safety verification
Given: An unranked vocabulary Σ, a hedge rewriting system R over Σ, a first-order representa-
tion ϕI of the language I ⊆ H (Σ) of initial ground hedges, a first-order representation ϕU
of the language U ⊆ H (Σ) of unsafe ground hedges.
Question: Is it true that ∀h ∈ I∀h′ ∈U h 6→∗R h
′?
Proposition 4 If the verification problem above has a negative answer, that is ∃t1 ∈ I∃t2 ∈
Ut1 →∗R t2 then ΦR `∃x ∃y (ϕI(x)∧ϕU (y)∧R(x,y)).
Proof. The proposition statement follows immediately from Proposition 1 and Definition 2.
�
4.1 Verification method
Taking contraposition of Proposition 4 we have ΦR 6` ∃x ∃y (ϕI(x)∧ϕU (y)∧R(x,y)) implies
∀h ∈ I∀h′∈U h 6→∗R h
′, that is a positive answer to an instance of the basic verification problem.
Thus, the essence of the finite countermodels (FCM) verification method we advocate in this
paper is:
To demonstrate a positive answer to an instance of a basic verification problem ap-
ply an automated generic finite model procedure to find a countermodel to ΦR →
∃x∃yϕI(x)∧ϕU (y)∧R(x,y), or equivalently a model for ΦR∧¬∃x∃yϕI(x)∧ϕU (y)∧
R(x,y).
The next theorem, which is a generalization of similar theorems in [17, 21] (the case of word
languages) and [19] (the case of tree languages), shows the applicability of FCM method and its
relative completeness with respect to the methods based on regular invariants [14, 27].
Theorem 1 Let R be a hedge rewriting system over unranked alphabet Σ, ϕI and ϕU be
first-order formulae representing the regular sets I and U of initial and unsafe hedges, re-
spectively. Let Inv be a regular set of hedges such that post∗R(I) ⊆ Inv and Inv ∩U = /0,
that is a regular invariant separating I and U . Then there is a finite model M such that
M |= ΦR ∧¬∃x,y(R(x,y)∧ϕI(x)∧ϕU (y)).
Proof. (Sketch) Assume the condition of the theorem holds. Let AI = ((QI,eI,∗I),A,δI,FI ⊆
QI), AInv = ((QInv,eI,∗Inv),A,δInv,FInv ⊆ QInv) and AU = ((QU ,eI,∗U ),A,δU ,FU ⊆ QU ) be for-
est automata recognizing regular hedge languages I,Inv and U , respectively. Then the required fi-
nite model M is constructed as follows. The domain D of the model is QI×QInv×QU . The inter-
prettaion of e is [[e]] = (eI,eInv,eU ). The interpretation of ∗ is given by (q1,q2,q3)[[∗]](q′1,q
′
2,q
′
3) =
(q1 ∗I q′1,q2 ∗Inv q
′
2,q3 ∗U q
′
3). For all a ∈ A the interpretations are given by [[a]](q1,q2,q3) =
(δI(a,q1),δInv(a,q2),δU (a,q3)). Once we defined the interpretations of all functional symbols
(including constants) any ground term t gets its interpretation [[t]] ∈ D in a standard way. De-
fine the interpretation of R as [[R]] = {([[τ(h)]],[[τ(h′)]]|h →∗R h
′}. For all predicates Pq with
q ∈ QI used in ϕI the interpretations are defined as [[Pq]] ={(q,x,y)|x ∈ QInv,y ∈ QU}. Similarly,
[[Pq]] = {(x,q,y)|x ∈ QI,y ∈ QU} for q ∈ QInv and [[Pq]] = {(x,y,q)|x ∈ QI,y ∈ QInv}. Now it is
straightforward exercise to show that the such defined model is indeed as required. �.
Proc. AVoCS 2015 8 / 14
ECEASST
5 Experiments
In this section we present the experimental results of applications of the FCM method for safety
verification of hedge rewriting systems. In the experiments we used the finite model finder
Mace4 [24] within the package Prover9-Mace4, version 05, December 20071.
5.1 Tree arbiter protocol and other protocols on unranked trees
We consider here as a case study the verification of parameterized Tree-arbiter Protocol working
on the trees of unbounded branching degree. We take the description of the protocol from [4]
where its automated verification has been demonstrated for the case of binary trees.
The protocol supervises the access to a shared resource of a set of processes arranged in a tree
topology. The processes competing for the resource are located in the leaves of the trees. The
safety property to be verified is that of mutual exclusion - at no point, two or more processes at
leaves of the tree can get an access to the resource (obtain a token). A process in the protocol can
be in state idle (i), requesting (r), token (t) or below (b). All the processes are initially in state
i. A node is in state b whenever there is a node below (descendant) in state t. When a leaf is in
state r, the request is propagated upwards until it encounters a node in state t of b (aware of the
presence of the token). A node state t can choose to pass it upwards or pass it downwards to a
requesting node in state r.
We model the tree arbiter protocol as a hedge rewriting system Rta consisting of the rules:
1. i(x r(y) z)→ r(xr(y)z) (request propagated upwards)
2. t(x r(y) z)→ b(xt(y)z) (token passed downwards)
3. b(x t(y) z)→ t(xi(y)z) (token passed upwards)
4. i(Λ)→ r(Λ) (idle leaf node becomes requesting)
The set of initial configurations is a hedge language consisting of all hedges in which all leaves
are either r(Λ) or i(Λ), all intermediate nodes (neither leaves, nor the top) are i(...) and the top
node is t(...).
The hedge language of unsafe configurations consists of all hedges with two or more leaves
with t(Λ) (tokens). Now we represent the verification problem in the format required by FCM
method.
The automata AI and AU reconginizing the sets of initial, respectively unsafe states and
the first-order translation Φ of the hedge rewriting system and the automata can be found in the
Appendix A of the extended version [22] of this paper.
After translation of the protocol specification and forest automata recognizing the initial and
unsafe configurations into a first order formula Φ and (un)safety condition into a formula Ψ the
safety is established automatically by Mace4 finding a countermodel for Φ → Ψ of size 3 in
0.03s.
1 the system configuration used in experiments: Intel(R) Core (TM)2 Duo CPU, T7100 1.8Ghz 1.79 Ghz, 1.00 GB of
RAM.
9 / 14 Volume 72 (2015)
First-order logic for safety verification
We have applied FCM to the verification of other protocols operating on the unranked trees.
The specification of the protocols are taken from [4, 6] where their automated verification has
been demonstrated for the binary trees case. In [19] we have considered the application of FCM
for the verification of binary tree case protocols. The table below lists the parameterized tree
protocols and shows the time it took Mace4 to find a countermodel and verify a safety property
for the case of unranked trees (first column). For comparison the times it took to verify the
binary tree versions of the same protocols by FCM [19] and by regular tree model checking [6]
are given in the second and third columns, respectively.
Protocol Time Time from [19] Time from[6]∗
Token 0.04 0.02s 0.06s
Two-way Token 0.04 0.03s 0.09s
Percolate 0.06 0.09s 2.4s
Tree arbiter 0.03 0.03s 0.31s
∗ the system configuration used in [6] was Intel Centrino 1.6GHZ with 768MB of RAM
Further details of the experiments can be found in [16].
As far as we are aware the automated verification of the above parameterized protocols over
trees of unbounded degree is reported here for the first time, with an exception being Two-way
Token protocol verified in [27].
5.2 Verification of Synchronised PAD Systems
The verification techniques based on disproving in first-order logic are very flexible and can
accommodate various constraints on the properties of the systems of interest. To illustrate this
point we consider an automated verification of a program which involves dynamic creation of
processes. We take as an example a program from [29] specified in terms of Synchronised PAD
Systems [29]. Such systems can be seen as an extension of hedge rewriting systems to the case
of two different associative constructors, one of which being commutative. Furthermore the
rewriting is constrained to capture the effects of modelled synchronisation.
Let Sync = {a,b,c,...} be a set of actions such that every action a ∈ Sync corresponds to a
co-action ā ∈ Sync s.t. ¯̄a = a. Let Act = Sync∪{τ} be the set of all the actions, where τ is a
special action.
Let Var = {X,Y,...} be a set of process variables and T be the set of process terms t over
Var defined by:
t ::= 0 | X | t ·t | t||t
Definition 3 A Synchronised PAD (SPAD) is a finite set of rules of the form X ↪→a t or X ·Y ↪→a
t, where X,Y ∈Var,t ∈ T and a ∈ Act
The process terms are considered modulo the following equational theory SE of structural
equivalence:
A1: t ·0 = 0·t = t||0 = 0||t = t
Proc. AVoCS 2015 10 / 14
ECEASST
Figure 1: An example from [29]
A2: (t ·t′)·t′′ = t ·(t′ ·t′′)
A3: t||t′ = t′||t
A4: (t||t′)||t′′ = t||(t′||t′′)
A SPAD R induces a transition relation �a over T by the following inference rules:
θ1 :
t1↪→at2∈R
t1�at2
; θ2 :
t1�at′1
t1·t2�at′1·t2
; θ3 :
t1=0,t2�at′2
t1·t2�at1·t′2
θ4 :
t1�at′1
t1||t2�at′1||t2;t2||t1�at2||t
′
1
θ5 :
t1�at2;t2�āt′2;a,ā∈Sync
t1||t2�τ t′1||t
′
2
The equational theory SE induces a transition relation �aSE over T defined by ∀t,t
′∈T ,t �aSE
t′ iff ∃u,u′ s.t. t =SE u,u �a u′ and u′ =SE t′. For w ∈ Act∗ the transition relations �w and →wSE
are defined in a standard way.
5.2.1 Example
Consider the program represented in Fig 1 which involves dynamic creation of processes. The
figure represents the flow graph of a program having two procedures π1 and π2 such that:
• π1 calls itself in parallel with another procedure π2.
• π2 calls itself recursively,
• π1 and π2 communicate via the synchronizing actions a,b, and their corresponding co-
actions ā and b̄, and the program starts at point n0
The safety property to be verified is “starting from n0, the program never reaches a configura-
tion where the control point m1 is active.”
The program is modelled by the Syncronized PAD R [29] which includes the following rules:
11 / 14 Volume 72 (2015)
First-order logic for safety verification
R1 : n0 ↪→a n1
R2 : n1 ↪→b̄ n2
R3 : n0 ↪→τ (n0 ‖ m0)·n2
R4 : m0 ↪→b m1
R5 : m1 ↪→ā m2
R6 : m0 ↪→τ m0 ·m4
R7 : m3 ·m4 ↪→τ m2
R8 : m2 ·m4 ↪→τ m3
The above verification task is formulated in terms of R as follows. Show that there are no w ∈ τ∗
and t ∈ T such that m0 is a subterm of t and n0 �wSE t.
Notice that the transition relation �wSE with w ∈ τ
∗ encodes the reachability by a rewriting
process, where the rules with ↪→τ can be applied without any restrictions, whereas the rules with
↪→a with a ∈ Sync can be applied only if a some rule ↪→ā with a co-action superscript is applied
simultaneously ”in parallel” subterm (cf. the rule θ5).
We claim now that one can specify the first-order formulae:
• ΦR describing the reachability by �wSE , the initial configuration and the set of unsafe
configurations, and
• Ψ specifying unsafety condition
such that if ΦR ` Ψ then the program is unsafe. See the details in Appendix B of the extended
version [22] of this paper. We apply Mace4 and a countermodel of the size 3 for ΦR → Ψ is
found in 2s.
6 Conclusion
We have shown in this paper that the simple encoding of hedge rewriting systems by first-order
logic and using available finite model finders provides with an interesting and viable alternative
to the existing methods for the verification of systems working on the trees of unbounded degree.
On the one side it is relatively complete w.r.t. the methods using regular invariants. On the other
side it is either practically efficient, as our automated verification of parameterized protocols
working on the trees of unbounded degree illustrates well, or at least looks promising to explore
the boundaries of its practical applicability, as our SPAD example shows. The advantages of the
FCM method are (1) it is simple, (2) it is flexible, (3) it is modular and (4) it reuses existing tools.
The FCM method has a natural limitation that it can be used only to establish the safety. If safety
actually does not hold looking for the countermodels does not help. One can use then automated
theorem provers to confirm that indeed the safety is violated by searching for the proofs of
formulas of the form Φ → Ψ. One direction for the future work here is the development of the
systematic procedures which would extract the unsafe traces from first-order proofs.
Bibliography
[1] Parosh Aziz Abdulla, Jonsson B. Verifying programs with unreliable channels. Information and
Computation, 127(2):91-101, June 15, 1996.
Proc. AVoCS 2015 12 / 14
ECEASST
[2] Abdulla, Parosh Aziz and Jonsson, Bengt and Mahata, Pritha and d’Orso, Julien, Regular Tree
Model Checking, in Proceedings of the 14th International Conference on Computer Aided Verifica-
tion, CAV ’02, 2002, 555–568
[3] Abdulla, P.A., Jonsson,B., Nilsson, M., & Saksena, M., (2004) A Survey of Regular Model Check-
ing, In Proc. of CONCUR’04, volume 3170 of LNCS, pp 35–58, 2004.
[4] Parosh Aziz Abdulla, Noomene Ben Henda, Giorgio Delzanno, Frdric Haziza and Ahmed Rezine,
Parameterized Tree Systems, in Formal Techniques for Networked and Distributed Systems, FORTE
2008, Lecture Notes in Computer Science, 2008, Volume 5048/2008, 69-83.
[5] Mikolaj Bojanczyk, Igor Walukiewicz, Forest Algebras, in Logic and Automata, History and Per-
spectives (J.Flum, E.Gradel, T. Wilke eds.), Amsterdam University Press, 2007, 107–132.
[6] A. Bouajjani, P. Habermehl,A. Rogalewicz, T. Vojnar, Abstract Regular Tree Model Checking, Elec-
tronic Notes in Theoretical Computer Science, 149, (2006), 37–48.
[7] Parosh Aziz Abdulla, Giorgio Delzanno, Noomene Ben Henda, Ahmed Rezine. Monotonic Ab-
straction: on Efficient Verification of Parameterized Systems. Int. J. Found. Comput. Sci. 20(5):
779-801 (2009)
[8] A. Bouajjani and T. Touili. On computing reachability sets of process rewrite systems, in Proc. 16th
Int. Confenerence on Rewriting Techniques And Applications (RTA’05), LNCS 3467, 2005
[9] R. Caferra, A. Leitsch, N. Peltier, Automated Model Building, Applied Logic Series, 31, Kluwer,
2004.
[10] G. Delzanno. Constraint-based Verification of Parametrized Cache Coherence Protocols. Formal
Methods in System Design, 23(3):257–301, 2003.
[11] Julien d’Orso and Tayssir Touili. Regular Hedge Model Checking, Proc. of the 4th IFIP International
Conference on Theoretical Computer Science (TCS’06), 2006.
[12] Goubault-Larrecq, J., (2010), Finite Models for Formal Security Proofs, Journal of Computer Secu-
rity, 6: 1247–1299, 2010.
[13] Guttman, J., (2009) Security Theorems via Model Theory, Proceedings 16th International Workshop
on Expressiveness in Concurrency, EXPRESS, EPTCS, vol. 8 (2009)
[14] F. Jacquemard and M. Rusinowitch, Closure of Hedge-Automata Languages by Hedge Rewriting,
in A. Voronkov (Ed.): RTA 2008, LNCS 5117, pp 157–171, 2008.
[15] L. Libkin, Logics for unrankeed trees: an overview. Logical Methods in Computer Science,2:1-
31,2006.
[16] A. Lisitsa Verification via countermodel finding
http://www.csc.liv.ac.uk/˜alexei/countermodel/
[17] Lisitsa, A., (2010c), Finite model finding for parameterized verification, CoRR abs/1011.0447:
(2010)
[18] Lisitsa, A., (2010b), Reachability as deducibility, finite countermodels and verification. In Proceed-
ings of ATVA 2010, LNCS 6252, 233–244
13 / 14 Volume 72 (2015)
First-order logic for safety verification
[19] Lisitsa, A., (2011), Finite countermodels for safety verification of parameterized tree systems,
CORR abs/1107.5142 (2011)
[20] Lisitsa, A, (2012) Finite Models vs Tree Automata in Safety Verification, In Proc. RTA’12, pp
225–239
[21] Lisitsa, A., (2013) Finite Reasons for Safety. Parameterized Verification by Finite Model Finding,
Journal of Automated Reasoning, 51(4): 431-451 (2013)
[22] Lisitsa, A., (2015) First-order logic for safety verification of hedge
rewriting systems, extended version of this paper, available at
www.csc.liv.ac.uk/˜alexei/countermodel/avocs15.pdf
[23] S. Maneth, A. Berlea, T. Perst, and H. Seidl, Xml type checking with macro tree transducers, PODS,
2005
[24] W. McCune Prover9 and Mace4 http://www.cs.unm.edu/˜mccune/mace4/
[25] Selinger, P., (2001), Models for an adversary-centric protocol logic. Electr. Notes Theor. Comput.
Sci. 55(1) (2001)
[26] J.W. Tatcher, Characterizing derivation trees of context-free grammars through a generalization of
finite automata theory. J. Comput. Syst. Sci., 1:317-322, 1967.
[27] Tayssir Touili, Computing transitive closures of hedge transformations, IJCCBS, volume 3, 1/2,
2012, 132–150
[28] Weidenbach, C., (1999), Towards an Automatic Analysis of Security Protocols in First-Order Logic,
in H. Ganzinger (Ed.): CADE-16, LNAI 1632, pp. 314–328, 1999.
[29] Tayssir Touili. Dealing with communication for dynamic multithreaded recursive programs. Invited
Paper In Proc. of VISSAS’05.
[30] Silvano Dal Zilio and Denis Lugiez, XML schema, tree logic and sheaves automata, RTA’03, 2003.
Proc. AVoCS 2015 14 / 14
Introduction
Preliminaries
First-order Logic
Hedge Rewriting
Forest Automata and Regular Hedge Languages
Finitely based sets of hedges
Safety Verification: from hedge rewriting to FO logic
Basic verification problem
From hedge rewriting to first-order logic
First-order representations of regular hedge languages
Finitely based sets of hedges
Outer rewriting and unary reachability encoding
Back to safety verification
Verification method
Experiments
Tree arbiter protocol and other protocols on unranked trees
Verification of Synchronised PAD Systems
Example
Conclusion