Efficient Simplification of Bisimulation Formulas

Uffe H. Engberg

BRICS ∗Department of Computer Science, University of Aarhus, Denmark

Kim S. Larsen^{†}

Department of Mathematics and Computer Science, Odense University, Denmark

Abstract

The problem of checking or optimally simplifying bisimulation formulas is likely to be computationally very hard. We take a different view at the problem: we set out to define a very fast algorithm, and then see what we can obtain. Sometimes our algorithm can simplify a formula perfectly, sometimes it cannot. However, the algorithm is extremely fast and can, therefore, be added to formula-based bisimulation model checkers at practically no cost. When the formula can be simplified by our algorithm, this can have a dramatic positive effect on the better, but also more time consuming, theorem provers which will finish the job.

1 Introduction

The need for validity checking or optimal simplification of first order bisimulation formulas has arisen from recent work on symbolic bisimulation checking of value-passing calculi [4, 9, 15]. The NP-completeness of checking satisfiability of propositional formulas [3] implies that validity checking of that class of formulas is co-NP complete. Additionally, checking of quantified formulas is P-space hard [7], so there is not much hope for a fast algorithm for deciding exactly when a bisimulation formula is valid.

Instead, we set out to solve the problem of what you can get for free, i.e., to what extent is it possible to decide validity simply while reading the formula? As it turns out, there is almost nothing that can be done in linear time. The most simple tasks of storing and retrieving information about variables will cost O(n log n). So, we allowed ourselves this extra log-factor and changed the question to what you can get almost for free. As we shall demonstrate in this paper, the algorithm we have designed is very fast. Not alone does it run in O(n log n); the constant is also very small. On average, we read through the formulas at a rate of about 75 Kbytes per second. Of course, this is only interesting if the algorithm outputs useful answers reasonably frequently, i.e., in the absence of an obvious notion of optimal simplification (to a minimal equivalent formula), if the algorithm can reasonably frequently guarantee that the formula is valid, rule out that the formula could be valid, or maybe simplify a huge formula to a much smaller equivalent one. It is not easy to measure how often the algorithm produces a useful answer, but through examples, we show that there are families of process expressions which give rise to formulas, where our algorithm is successful.

∗ Basic Research in Computer Science, a Centre of the Danish National Research Foundation.

† The initial part of this work was done while this author was at Aarhus University.

The algorithm make a single pass over the formula making no assumptions about the variable names. Notice that this also implies that if formulas are passed on to our algorithm from another program, they do not have to be saved at any point, but can be passed on to our program via pipelining.

As already mentioned, in addition to validity checking, we can also simplify formulas. This greatly increases the usefulness of this work. Even if our algorithm fails to prove the validity of a formula, it will quite often simplify the formula so drastically that the validity of the formula (or the opposite) can easily be asserted by the user. Another possibility is to check the simplified formula for validity using other tools. Tools that would succeed more often, but the complexity of which would make it impossible to work on the original formula. The main advantage of simplifying formulas is that the algorithm can be built into the program generating the bisimulation formulas and simplify the formula on the fly. Also, intermediate simplifications can be used to prune the generation of other subformulas. This can be of vital importance since the formulas can become exponentially large.

Our algorithms work just as well on formulas with free variables as on closed formulas. This means that by simplifying a formula with free variables, we actually characterize the conditions, in terms of the free variables, under which two processes are bisimilar.

2 Bisimulation Formulas

In this section, we introduce bisimulation formulas and some general notions from formal logic. Due to lack of space we shall only briefly sketch how bisimulation formulas are obtained.

In [4, 9], bisimulation formulas are used in a three stage process of verifying bisimilarity of value-passing programs ([15] obtain similar formulas, albeit with a different approach).

In the first stage, symbolic transition graphs (a generalization of the standard notion of labeled transition graphs) are generated from terms of some value-passing language, say the full CCS calculus [14]. The two graphs are symbolic bisimilar [4, 9, 10] iff the two terms are bisimilar in traditional sense.

Below, two processes are shown together with their associated graphs. Following [14], 0 is the process having no actions, whereas the prefixed process τ.p can make an internal action and then act as p. Similarly, there are input (output) prefixes α?x. (α!x.) for receiving (sending) values on channel α. The expression if E then p can do the actions of p, provided the condition E evaluates to true, T. The process p + p′ acts as either p or p′.

A_{1}(x, y) =^{def} τ.0 + τ.if x ≡ y then τ.0

[figure: g_{1}; T, τ; T, τ; x ≡ y, τ]

A_{3}(x, y) =^{def} τ.(if x ≡ y then τ.0) + if x ≡ y then τ.0

[figure: g_{3}; x ≡ y, τ; T, τ; x ≡ y, τ]

To shorten the presentation, all nodes except for root nodes, have been omitted from the graphs. Each edge is labeled with a guarding condition and a (symbolic) action. The initial conditions of the graph g_{1} associated with A_{1} are T, whereas the last condition is x ≡ y, i.e., x and y should have equivalent values.

In the next stage, an algorithm is used for finding a first order boolean expression mgb, called the most general boolean, characterizing the conditions for which two finite symbolic transition graphs are (symbolic) bisimilar.

Intuitively, two processes are bisimilar if, whenever one process can do an action, the other has a matching action such that the resulting two processes again are bisimilar. This is reflected in the bisimulation formula. For example, the fact that g_{3} must match an action corresponding to the left edge of g_{1}, is captured in the mgb_{g_{1},g_{3}} subformula

T → \begin{matrix}T ∧ [T ∧ (x ≡ y → F)] \\ ∨ \\ x ≡ y ∧ [T ∧ T] \end{matrix}

If an instantiation of variables satisfies the guarding condition T of g_{1}, then it must satisfy a guarding condition, T or x ≡ y, of g_{3} as well as the corresponding mgb, [T∧(a ≡ y → F)] or [T ∧ T].

When matching output actions, the values sent must be equal. An equality predicate captures this. By input, universal quantification is used to express that for all values received, the processes are bisimilar.

In the final stage, validity of the bisimulation formula is checked. If it is valid, the original programs are bisimilar under all instantiations. Otherwise, the formula expresses the weakest conditions on the instantiations for which they are bisimilar. Later, in section 7, we shall see that mgb_{g_{1},g_{3}} is in fact valid.

Formally, the class of formulas, which we will work with in the rest of this paper, is defined by the syntax

E ::= P | E ∧ E | E ∨ E | P → E | ∀x: E and P ::= T | F | x ≡ y,

where x and y range over a set, V, of variables. As usual, formulas are closed if they have no free variables. Notice that bisimulation formulas only have universal quantification. The binary predicate symbol ≡ is assumed be interpreted as an equivalence relation ≡_{D} over a nonempty domain D. It is then standard how to define when an environment, i.e., a function from V to D, satisfies a formula. An environment satisfies a set of formulas Γ, if it satisfies each formula of Γ. Γ semantically entails E, written Γ ⊧ E, if E is satisfied by any environment satisfying Γ. E is valid, ⊧ E, if ∅ ⊧ E.

The class of bisimulation formulas is a subset of the class of all quantified formulas and checking validity of bisimulation formulas is not P-space hard. An easy reduction shows that checking satisfiability with respect to an environment is NP complete, so presumably checking validity of bisimulation formulas is co-NP complete.

We now state some general properties of entailment relevant for the development of the algorithm. For simplicity, we write Γ as E_{1}, …, E_{n} when Γ = {E_{1}, …, E_{n}}. Similarly, we write Γ, Δ for Γ ∪ Δ.

Theorem 1 (Entailment)

a) If Γ ⊧ E then Γ, Δ ⊧ E  (Ext)
b) If E ∈ Γ then Γ ⊧ E  (Rep)
c) If Γ ⊧ E and Γ, E ⊧ E′ then Γ ⊧ E′ (Cut)
d) If Γ ⊧ E and E ⊧ E′ then Γ ⊧ E′  (Trans)
e) Γ ⊧ E and Γ ⊧ E′ iff Γ ⊧ E ∧ E′  (Conj)
f) Γ, E ⊧ E′ iff Γ ⊧ E → E′  (Imp)

Proof Standard, see e.g. [16]. □

In general, there is not any similar disjunction theorem allowing both introduction and elimination to the right. However, from the entailment theorems and a few tautologies, we get proposition 2. As a consequence of ≡_{D} being an equivalence relation we also have proposition 3.

Proposition 2 If Γ ⊧ E or Γ ⊧ E′, then Γ ⊧ E ∨ E′.

Proposition 3 a) ⊧ x ≡ x b) x ≡ y ⊧ y ≡ x c) x ≡ y, y ≡ z ⊧ x ≡ z

3 The Abstract Algorithm

We now set out to design an algorithm for checking validity of formulas with an equivalence predicate. We keep it as abstract as possible to allow for a large degree of freedom in the choice of data structures in the actual implementation.

Intuitively, the idea of the algorithm is to collect in a relation R (over variables) information about variables known to be equivalent when checking subformulas. For instance, checking the validity of a formula like x ≡ y → E is reduced to checking E under the assumption that x and y are equivalent, i.e. (x, y) is added to R and E then checked. To exploit that ≡ is an equivalence relation, the symmetric and transitive closure, is taken before proceeding to E. However, when checking E of the formula ∀x: E the situation is quite the opposite. Since a new scope is entered, all previous collected information in R concerning x, must be removed before E is checked.

Formally, for R denote the symmetric and transitive closure by R^{⊕}, the reflexive closure, R ∪ {(x, x) | x ∈ V }, by R^{0} and the removal of x, {(y, z) ∈ R | y ≠ x, z ≠ x}, by R \ x. Notice, R \ x ⊆ R, and if R is symmetrically and transitively closed, then so is R \ x.

In order to connect with the logic, we associate with R the set of formulas R_{≡} =^{def} {x ≡ y | (x, y) ∈ R}. The notions of closures and removal extend to R_{≡} in the natural way: R_{≡} \ x is (R \ x)_{≡} etc.

The algorithm is conveniently described using Kleene’s three-valued logic [11], the three truth-values being t for “true”, f for “false” and u for “undefined”/ “unknown”. The Kleene truth tables for conjunction, ∧_{K}, disjunction, ∨_{K}, and implication, →_{K}, are:

∧^{K} t f u
t t f u
f f f f
u u f u

∨_{K} t f u
t t t t
f t f u
u t u u

→^{K} t f u
t t f u
f t t t
u t u u

The abstract algorithm is expressed in terms of a function, |⊧, which given a bisimulation formula E and a symmetrically and transitively closed relation R, returns t only if R_{≡} ⊧ E, and f only if R_{≡} |̸= E. From now on, R is assumed to be symmetrically and transitively closed. Writing |⊧ infix, the definition is:

R |⊧ E is case E of T : t F : f x ≡ y : if x R^{0} y then t else u E′ ∧ E′′ : R |⊧ E′ ∧_{K} R |⊧ E′′ E′ ∨ E′′ : R |⊧ E′ ∨_{K} R |⊧ E′′ E′ → E′′ : R |⊧ E′ →_{K} R′ |⊧ E′′, where R′ = \{ \begin{matrix}(R ∪ \{(x, y)\})^{⊕}, & if E′ is x ≡ y \\ R, & if E′ is T or F \end{matrix} ∀x: E′ : R \ x |⊧ E′

Notice that |⊧ is well-defined because we take the symmetric and transitive closure of (R ∪ {(x, y)}).

Given a formula E, the initial call to this function will be ∅ |⊧ E, where ∅ is the empty relation.

Proving correctness is a matter of proving soundness of |⊧ relative to ⊧. First, we need a small result linking R_{≡} to universal quantification.

Lemma 4 If R_{≡} \ x ⊧ E, then R_{≡} ⊧ ∀x: E.

Proof Assume that R_{≡} \x ⊧ E and let an environment ρ satisfying R_{≡} be given. Because R_{≡} \ x ⊆ R_{≡}, ρ must satisfy R_{≡} \ x as well. Now x does not occur in any formula of R_{≡} \ x so all environments differing from ρ only on the value of x, will then also satisfy R_{≡} \x. By the assumption each such environment also satisfies E wherefore the original environment ρ satisfies ∀x: E. □

Writing |⊧ E for ∅ |⊧ E, we can now state the correctness of the algorithm.

Theorem 5 (Correctness) a) If |⊧ E = t, then ⊧ E. b) If |⊧ E = f, then |̸= E.

Proof Part a) of the theorem follows from the stronger statement

if R |⊧ E = t then, R_{≡} ⊧ E

which we prove by induction on the structure of E. Assume R |⊧ E = t. We consider the forms of E:

T, F: In general, Γ ⊧ T, so also R_{≡} ⊧ T. The case of F is trivial, since R |⊧ F ≠ t. x ≡ y: By definition of ^{0}, it follows that R |⊧ x ≡ y = t iff either x R y or x = y.

Now, x R y is equivalent to x ≡ y ∈ R_{≡}. By (Rep), we get R_{≡} ⊧ x ≡ y. In the case x = y, the situation is really that E is x ≡ x. By (Ext) and a) of proposition 3, we directly obtain R_{≡} ⊧ x ≡ x.

E′ ∧ E′′: By definition, R |⊧ E′ ∧ E′′ = t implies R |⊧ E′ = t and R |⊧ E′′ = t. By induction, we obtain that R_{≡} ⊧ E′ and R_{≡} ⊧ E′′. Using (Conj), we obtain that R_{≡} ⊧ E′ ∧ E′′.

E′ ∨ E′′: Similar, using proposition 2 instead of (Conj).

E′ → E′′: By the definition of →_{K}, we must have R |⊧ E′ = f or R′ |⊧ E′′ = t. The forms of E′:

T: Then R′ = R and because R |⊧ T = t, it follows that R |⊧ E′′ = t. As above we deduce R_{≡} ⊧ E′′. Using (Ext), we get R_{≡}, T ⊧ E′′ and therefore R_{≡} ⊧ T → E′′ follows by (Imp).

F: In general Γ, F ⊧ E, so in particular R_{≡}, F ⊧ E′′. By (Impl), R_{≡} ⊧ F → E′′. x ≡ y: We have R |⊧ x ≡ y = t or R |⊧ x ≡ y = u. In either case, we must have R′ |⊧ E′′ = t, where R′ = (R ∪ {(x, y)})^{⊕}. By induction, we get R′_{≡} ⊧ E′′, which is the same as (R_{≡}, x ≡ y)^{⊕} ⊧ E′′. Now any z ≡ w in (R_{≡}, x ≡ y)^{⊕} can be deduced from R_{≡}, x ≡ y so by repeated use of (Cut), each of these z ≡ w can be removed from the hypothesis and we finally get R_{≡}, x ≡ y ⊧ E′′. Thus, by (Impl), R_{≡} ⊧ x ≡ y → E′′.

∀x: E′: By the induction hypothesis we get that R_{≡} \ x ⊧ E′. The result follows from lemma 4.

Part b) follows similarly from the stronger statement that if R |⊧ E = f, then R_{≡} ⊧ ¬E.

□

4 The Concrete Algorithm

In this section, we discuss the implementation of the abstract algorithm outlined in section 3. The function |⊧, which is defined there, closely follows the structure of a formula E. The concrete implementation in this section will follow this structure in exactly the same way. So, the primary task is to find a representation of the relation R such that operations on this relation (union, closure, checking for equivalence, etc.) can be performed efficiently.

The primary operations are to make two variables equivalent and to test whether two variables are already equivalent. This is an instance of the so-called disjoint set problem, which is usually solved using rooted trees [6]. To obtain the best possible performance, path compression (McIllroy and Morris) and union by rank [17] (or similar schemes) are normally used to obtain an amortized complexity of O(A^{−1}(n)) per find operation [17, 19], where A^{−1} is the inverse of the (unary) Ackermann function [1].

However, when processing formulas like (x ≡ y → E) ∧ E′, we need to first form the union of the equivalence classes of x and y, then process the expression E, and then deunion (undo) the last union before processing E′. Path compressions are impossible to undo without ruining the complexity, so we only use union by rank, and obtain a complexity of O(log n) per find [18]. In order to undo the unions, each union operation is registered on a stack. In this way, deunions can be done in constant time (unions are still constant time). These three operations, find, union, and deunion, can also be implemented such that the amortized complexity for the find operation becomes O(log n/(log log n)). That proposal is from [12]. See [20] for the analysis. However, the size of the overhead is so large that for formulas that we consider (up to approximately 5Mbytes), this method is slower. For further details on disjoint set implementations, see [13]. We call the structure we use a union-find-deunion (UFD) structure.

For formulas without universal quantification, this would be all we would need. However, formulas like (∀x: E) ∧ E′ require that the variable x is freed from previous unions while processing E. Afterwards, for the processing of E′, all the old information on x must be restored. Having to keep track of several versions of variables means that the variables cannot be used directly in the UFD structure. Instead, we do the following: at any point during the processing of a formula, each variable, x, has an associated stack of pointers corresponding to the number of active versions of x. In greater detail, when a quantifier construction ∀x: is encountered, a pointer is pushed onto x’s stack. The pointer points to a new item in the UFD structure not related to anything, which was previously there. In this way, the old environment can be restored by simply popping the stack.

In order to access the stacks associated with variable names as fast as possible, variable names (along with the pointer to the stacks) are organized in a red-black tree [2, 8], which is one of the efficient implementations of dictionaries with a complexity of O(log n) per operation, where n is the number of elements in the tree.

To summarize, we use a red-black tree that has variable names as keys and stacks of pointers as values. All these pointers point into a common UFD structure. In addition, the UFD structure has its own stack of undo information. We refer to the structure consisting of all these other data structures as the combined structure.

In the following, we list the operations that the three data structures are assumed to be equipped with. The description is brief as all this is quite well known. However, it seems useful to introduce the names of the operations on the different structures.

A stack is a collection of values, which can be removed from the structure only in the reverse order of which they were inserted. Assume that S is a stack and v is a value. The following operations are supported: Push(S, v), Pop(S), Top(S), Empty(S), and InitStack().

A dictionary implements a set of pairs (k, v), where k is a key value from a totally ordered domain and v is any value. We assume that each key value appears at most once in the dictionary. If T is a dictionary, then the following operations are supported: Insert(T, k, v), Delete(T, k), Member(T, k), LookUp(T, k), and InitTree().

A UFD structure is a collection of elements some of which may be equivalent with other elements. The following operations are supported: Union(U, p, q), Find(U, p), Deunion(U), and InitUFD(). Obviously, the implementation is basically the well-known union-find structure using a stack to save information about the unions.

A Kleene boolean is an implementation of Kleenes three-valued logic. The three Kleene truth-values TRUE, FALSE, and UNKNOWN correspond to t, f, and u, respectively. The operations Kand, Kor, and Kimp implement the operations ∧_{K}, ∨_{K}, and →_{K} as described in the tables of section 3. Furthermore, Ktu turns an ordinary boolean into the Kleene boolean TRUE if it is true and otherwise into UNKNOWN.

The Algorithm

In this section, we present the concrete algorithm, which implements the abstract algorithm from section 3. Basically, this is all about representing the relation R using advanced data structures. We assume that the formula E has a representation in the form of a syntax tree. There are well-developed standard techniques to define and manipulate syntax trees. For clarity, we leave out these details.

Also, to present the crucial parts of the algorithm as clearly as possible, we treat E_{1} ∧ E_{2} and E_{1} ∨ E_{2} independently. In reality, as we want to process the formula using pipelining, we should process E_{1} first and not until after that has been done can we decide whether a conjunction or a disjunction is been processed. Another reasonable assumption would be to require that the program generating the formula does this using a prefix notation like ∧(E_{1}, E_{2}) and ∨(E_{1}, E_{2}).

For simplicity, we assume that the formulas are closed, i.e., they do not have any free variables. This is no serious simplification since free variables can be treated as if they were bound at the outermost level.

The concrete implementation follows the structure of the formula in the same way as |⊧, except that the call for the left-hand operand of implication is unfolded and incorporated directly into the case analysis.

function check(E: formula) → Kleene boolean;

var r: Kleene boolean; p,q: pointers; (* into the UFD structure *)

case E of T: r := TRUE; F: r := FALSE; x ≡ y: r := Ktu(Find(U,Top(LookUp(T,x))) = Find(U,Top(LookUp(T,y)))); E_{1} ∧ E_{2}: r := Kand(check(E_{1}),check(E_{2})); E_{1} ∨ E_{2}: r := Kor(check(E_{1}), check(E_{2})); T → E_{1}: r := check(E_{1}); F → E_{1}: r := TRUE; (x ≡ y) → E_{1}: p := Find(U,Top(LookUp(T,x))); q := Find(U,Top(LookUp(T,y)));

if p ≠ q then Union(U,p,q);

r := Kimp(Ktu(p ≠ q),check(E_{1}));

if p ≠ q then Deunion(U); ∀x: E_{1}: if ¬Member(T,x) then Insert(T,x,InitStack()); new(p); Push(LookUp(T,x),p); r := check(E_{1}); Pop(LookUp(T,x)); free(p); if Empty(LookUp(T,x)) then Delete(T,x);

end;

return r; end;

Before use, T is declared as a red-black tree and properly initialized using InitTree().

Similarly, U is declared as a UFD structure and initialized by a call to InitUFD().

Correctness

Proposition 6 The combined structure immediately after a call to the function check is exactly as it were immediately before the call to check.

Proof By induction in the number of calls to the function check. The base case is when this number is one, which means that check is not called recursively. Thus, we must be in one of the cases T, F, or x ≡ y. The result follows since the combined structure is not altered in any of these cases.

For the induction step, the result follows trivially from the induction hypothesis in the case where E is E′ ∧ E′′, E′ ∨ E′′, T → E′, or F → E′, since the combined structure is not changed.

Assume that E is (x ≡ y) → E′. By the induction hypothesis, the call check(E′) leaves the structure unchanged. The claim follows as Deunion(U) will undo the last union not yet undone. This must be Union(U,p,q), as the combined structure after the call to check(E′) is exactly as it were before the call.

Assume that E is ∀x : E′. By the induction hypothesis, the call check(E′) leaves the structure unchanged. Since LookUp(T,x) is a stack, the statement Pop(LookUp(T,x)) will undo the effect of the statement Push(LookUp(T,x),p). Furthermore, if the stack LookUp(T,x) is empty, then this stack must have been inserted into T by this current invocation of check, so the empty stack should be deleted. □

Proposition 7 Let F be a bisimulation formula, and let E be a subexpression of F with x and y bound in the context of E. Immediately before the call check(E), the combined structure is an exact representation of R in the corresponding call R |⊧ E, i.e.,

x R^{0} y ⇔ Find(U,Top(LookUp(T,x))) = Find(U,Top(LookUp(T,y)))

Proof By induction in the structure of E. The base case is when E = F, in which case both R (and thus also R^{0}) and the combined structure are empty. For the induction step, we consider all possible forms that E could have.

If E is T, F, x ≡ y, E′ ∧ E′′, E′ ∨ E′′, T → E′, or F → E′, then the combined structure remains unchanged and the same R is used in the recursive application of |⊧.

Assume that E is (x ≡ y) → E′. Then |⊧ is called with the relation formed by adding (x, y) to R and taking the symmetric and transitive closure. In the combined structure, if x and y do not already belong to the same equivalence class, then the equivalence classes of x and y are joined. Notice that given the representation of the combined structure and the way it is used, it is automatically closed reflexively, symmetrically, and transitively.

Assume that E is ∀x: E′. Then |⊧ is called with the relation formed from R by deleting all pairs that include x. In the combined structure, a new pointer into the UFD structure is created and placed on the top of x’s variable stack, thus effectively hiding any pairs involving x; except that the pair (x, x) will belong to the structure ensuring reflexitivity.

□

Lemma 8 The function, check, correctly implements |⊧.

Proof From proposition 6, it follows that a function semantically equivalent to the function check can be written by letting the combined structure be a value-passing parameter to check. As the two algorithms are structurally equivalent modulo unfolding, it is sufficient to consider the use of the combined structure and R. From proposition 7, it follows that the combined structure is an exact representation of R^{0}. □

Theorem 9 Let E be a bisimulation formula, and let n be the size of E. Then the time-complexity of check(E) is O(n log n).

Proof The algorithm is recursive in the structure of E, and clearly, there are a constant number of statements per symbol in E. These statements either perform constant-time operations, or they operate on one of the data structures. As these are initially empty, and as they share the property that n operations are carried out in time O(n log n), the result follows. □

5 Extensions of the Algorithm

In this section, we consider various extensions of the algorithm. For each extension, we sketch the modifications of the abstract algorithm from section 3, and we discuss the correctness issues briefly.

Many more extension than the ones presented here are possible. However, we have decided only to present extensions according to the criteria:

a) the asymptotic complexity should not change.

b) the increase in the actual complexity should be very low (less than a factor of 10).

c) it should still be a one pass algorithm.

It is not hard to deal with constants and through the obvious transformation suggested by the equivalence

(E ∧ E′) → E′′ =|⊧ E → (E′ → E′′),

the algorithm can easily cover implication subformulas with conjunctions of predicates to the left. It is straight forward to cope with multiple equivalence relations by letting the function |⊧ work with multiple relations over variables.

The function |⊧ is only able to return t (f) if the formula is valid (unsatisfiable). However, the algorithm, |⊧_{c}, obtained from |⊧ by returning the result of (R ∪ {(x, y)})^{⊕} |⊧_{c} E′ in case of formulas of the form (x ≡ y) → E′, is able to deal with contingent formulas as well.

Theorem 10 a) If |⊧_{c} E = t then ⊧ E. b) If |⊧_{c} E = f then |̸= E.

Proof The proof of a) is almost exactly as the corresponding proof of theorem 5. Part b) is proved by showing that if R |⊧_{c} E = f then E it is not satisfied by environments identifying all variables. □

|⊧_{c} is clearly as good as |⊧. It is also strictly better because |⊧ x ≡ y → F = u and |⊧_{c} x ≡ y → F = f.

6 Simplifications

In this section, we discuss changes to the algorithm with the purpose of outputting a simplified formula equivalent to the original formula. The algorithm should contain the validity checking algorithm as a special case, i.e., if the validity checking algorithm deems a formula valid, then this new algorithm should simplify the formula to T. Also, we would like the algorithm to fulfill the criteria of the previous section.

Like the |⊧ function, the new function, |⊧_{r}, takes as arguments a relation, R, over variables and a first order formula, but now it returns a first order formula instead of a truth-value of three-valued logic. We use the same case analysis, but turn the Kleene truth tables into simplification tables, essentially by replacing u by the argument formula. Compare with the Kleene truth tables in section 3. However, this is not quite sufficient. In the ∀x: E′ case of |⊧, ∀x is eliminated completely. This cannot be done here when E′ does not simplify to T or F, so a simplification table for ∀ is also needed.

∧^{r} T F E′
T T F E′
F F F F
E E F E ∧ E′

∨_{r} T F E′
T T T T
F T F E′
E T E E ∨ E′

→^{r} T  F  E′
T T  F  E′
F T T  T
E T E → F E → E′

∀_{r} x:_{T  T}_{F  F}_{E′ ∀x: E′}

We are now ready to define |⊧_{r}.

R |⊧_{r} E is case E of x ≡ y : if x R^{0} y then T else x ≡ y E′ ∧ E′′ : R |⊧_{r} E′ ∧_{r} R |⊧_{r} E′′ E′ ∨ E′′ : R |⊧_{r} E′ ∨_{r} R |⊧_{r} E′′ E′ → E′′ : R |⊧_{r} E′ →_{r} Upd(R, E′) |⊧_{r} E′′ ∀x: E′ : ∀_{r} x: R \ x |⊧_{r} E′ E : E

The final case deals with T and F and for convenience, we have introduced an explicit update function:

Upd(R, E) = \{ \begin{matrix}(R ∪ \{(x, y)\})^{⊕}, & if E is x ≡ y \\ R, & otherwise \end{matrix}

The simplified formula is logically equivalent with the original as stated in the following correctness theorem.

Theorem 11 E if and only if |⊧_{r} E.

Proof This follows from the statement below which is proved by induction. We omit the details.

R_{≡} → E iff R_{≡} → (R |⊧_{r} E) □

The next proposition expresses that |⊧_{r} is at least as good as |⊧.

Proposition 12 If |⊧ E = t (f), then |⊧_{r} E = T (F).

The next section contains examples of simplifications using this algorithm.

A straightforward improvement of the simplification algorithm can be obtained from the semantic equivalence

E′ ∧ E′′ =|⊧ E′ ∧ (E′ → E′′).  (1)

Exploiting the simplification of E′, the conjunction case is changed to:

let E′_{r} = R |⊧_{r} E′ in E′_{r} ∧_{r} Upd(R, E′_{r}) |⊧_{r} E′′.

In this way, the algorithm can simplify (F ∨ x ≡ y) ∧ (x ≡ y → F), for example, to F.

Along the same lines, the algorithm can be improved further by using:

E ∨ E′ =|⊧ (¬E) → E′.

Writing x ≢ y for the common occurring formula x ≡ y → F, we get as a special case:

x ≢ y ∨ E =|⊧ x ≡ y → E.  (2)

As the algorithm is formulated now, there is a priori nothing that prevents the algorithm from working with more predicates such as x ≢ y and x ≤ y. In fact, the simplification algorithm is still sound since the new predicates are not simplified and do not give rise to updates of R through Upd( , ). However, we can use R to simplify the new predicates in some cases, e.g., for x ≢ y, we can add the case

if x R^{0} y then F else x ≢ y.

Now, we turn our attention to another type of simplification. The idea is that universal quantifications can be pushed inwards over conjunctions and that quantified predicates in some cases then can be simplified.

We use this observation to maintain a set, X, of variables corresponding to universal quantified variables met solely by simplification of conjunctions, and define a function |⊧_{re}, which, compared to |⊧_{r}, takes X as an extra argument.

R |⊧_{re}^{X} E is case E of x ≡ y : if  x R^{0} y  then T elseif x ∈ X or y ∈ X then F else  x ≡ y E′ ∧ E′′ : R |⊧_{re}^{X} E′ ∧_{r} R |⊧_{re}^{X} E′′ E′ ∨ E′′ : R |⊧_{re}^{∅} E′ ∨_{r} R |⊧_{re}^{∅} E′′ E′ → E′′ : R |⊧_{re}^{∅} E′ →_{r} Upd(R, E′) |⊧_{re}^{∅} E′′ ∀x: E′ : ∀_{r} x: R \ x |⊧_{re}^{X∪{x}} E′ E : E

The soundness of |⊧_{re} follows from

∀x: E ∧ E′ =|⊧ (∀x: E) ∧ (∀x: E′)
∀x: x ≡ y =|⊧ F.

Actually, the soundness of the latter requires the quotient set of the domain by the equivalence, D/≡_{D}, to have a size of at least two. However, for empty or singleton quotient sets,

do not seem very useful, so the restriction should not be significant in practice.

Notice that with the exception of the extension concerning contingent formulas, all extensions can all be combined.

7 Examples

In the first half of this section, we focus on qualitative aspects of the simplification algorithm by means of five examples used to illustrate different simplification ideas. In the second half, we deal with some quantitative aspects of the simplification algorithm and the Kleene algorithm through time measures of concrete implementations applied to increasingly larger input.

Consider the following symbolic transition graphs:

[figure: x ≡ y; x ≡ y; x ≡ y; x ≡ y; x ≡ y; x ≡ y; x ≡ y; x ≡ y; g_{1}; g_{2}; g_{3}; g_{4}; g_{5}]

All actions are internal, so τ has been omitted from the graphs together with the trivial guarding conditions T. Before proceeding, we invite the reader to try to see which graphs are bisimilar. Now, applying |⊧_{r} to the bisimulation formula mgb_{g_{i},g_{j}} (↔ mgb_{g_{j},g_{i}}), we get the table of simplified formulas

i ^{j}  1  2  3  4
2  T
3 x ≢ y ∨ x ≡ y x ≢ y ∨ x ≡ y
4 x ≡ y ∧ E  x ≡ y ∧ E  E
5 x ≡ y ∧ x ≢ y \begin{matrix}( & x ≡ y ∨ x ≡ y) \\ ∧ x ≢ y \end{matrix} x ≡ y ∧ x ≢ y \begin{matrix}x ≡ y ∧ E \\ ∧ x ≢ y \end{matrix}

where E = ((x ≡ y ∧ x ≢ y) ∨ (x ≡ y ∧ x ≡ y)), and for sake of readability, x ≡ y → F is written x ≢ y. If, in stead, we apply |⊧_{r} with the modifications corresponding to (1), many of the formulas are simplified considerably, some even completely as shown in table below to the left.

\begin{matrix}i j & 1 & 2 & 3 & 4 \\ 2 & T \\ 3 & x ≢ y ∨ x ≡ y & x ≢ y ∨ x ≡ y \\ 4 & x ≡ y & x ≡ y & x ≡ y \\ 5 & F & \begin{matrix}( & x ≡ y ∨ x ≡ y) \\ ∧ x ≢ y \end{matrix} & F & F \end{matrix}  \begin{matrix}i j & 1 & 2 & 3 & 4 \\ 2 & T \\ 3 & x ≢ y ∨ x ≡ y & x ≢ y ∨ x ≡ y \\ 4 & F & F & F \\ 5 & F & \begin{matrix}( & x ≡ y ∨ x ≡ y) \\ ∧ x ≢ y \end{matrix} & F & F \end{matrix}

If we are interested in knowing whether the graphs are bisimilar under all instantiations of x and y, we can check validity of the universal closure of the formulas, i.e. simplify the universally closed formulas to T or F if possible. The result of applying |⊧_{re} (with the modifications mentioned above) yields the table above to the right. We have omitted the quantifiers in the formulas different from T and F.

Adding to |⊧_{re} an extra case for ≢, the formula in entry (i, j) = (5, 2) would also simplify to F, and if the modification suggested from (2), i.e., transforming x ≢ y∨E to x ≡ y → E, is incorporated into the algorithms as well, then the last two entries would also simplify completely, but this time to T.

Turning to the quantitative aspects of the concrete algorithms, we consider processes defined for i ≥ 0 by

p_{i+2} ⟶^{T,α?x_{0}} q_{i+1},  q_{i+1} ⟶^{T,α?x_{1}} r_{1}^{i},  r_{k}^{i+1} ⟶^{c_{k},α?x_{k+1}} r_{k+1}^{i} and r_{k}^{0} ⟶^{c_{k},β!x_{k}} 0,

where c_{k} is the equality x_{k−1} = x_{k}. Initially two values are unconditionally received on α and then, iteratively, values are received on α provided the two most resently received values are equal. Finally, after i iterations and under the same proviso, the last value is send on β. Similarly, we define primed versions which only differ in that c′_{k} is the equality x′_{0} = x′_{k}. That is, the last value received on α is compared with very first.

In order to give the reader examples of how concrete bisimulation formulas look like, we now describe the most general boolean, mgb_{r_{k}^{i},r_{k}^{′i}}, characterizing those instantiations (environments) of r_{k}^{i} and r_{k}^{′i} for which they are late bisimilar.

\begin{aligned}mgb_{r_{k}^{i+1},r_{k}^{′i+1}} & = \begin{matrix}c_{k} → (c′_{k} ∧ ∀x_{k+1} : ∀x′_{k+1} : x_{k+1} = x′_{k+1} → mgb_{r_{k+1}^{i},r_{k+1}^{′i}}) \\ ∧ \\ c′_{k} → (c_{k} ∧ ∀x′_{k+1} : ∀x_{k+1} : x′_{k+1} = x_{k+1} → mgb_{r_{k+1}^{i},r_{k+1}^{′i}}) \end{matrix} \\ mgb_{r_{k}^{0},r_{k}^{′0}} & = \begin{matrix}c_{k} → (c′_{k} ∧ x_{k} = x′_{k} ∧ T) \\ ∧ \\ c′_{k} → (c_{k} ∧ x′_{k} = x_{k} ∧ T) \end{matrix} \end{aligned}

The most general booleans for the p’s and q’s are similar to the first formula above, except that the conditions here are T.

For 2 ≤ i ≤ 13, we have measured the average time of five runs of a C implementation of |⊧_{c} (|⊧_{r}) processing mgb_{p_{i+2},p′_{i+2}} on a SPARC station ELC. To give a few examples, mgb_{p_{13+2},p′_{13+2}} of size 5.754 Mb was simplified to t (T) in 77284 (78912) milliseconds. Similarly, mgb_{p_{13+2},p′_{13+3}}, which is 4.477 Mb large, was simplified to f in 62958 milliseconds. On average, |⊧_{c} and |⊧_{r} process input at a rate of about 75 Kbytes per second.

References

[1] W. Ackermann. Zum Hilbertschen Aufbau der reellen Zahlen. Math. Annalen, 99:118– 133, 1928.

[2] R. Bayer. Symmetric Binary B-Trees. Acta Inform., 1:290–306, 1972.

[3] S.A. Cook. The Complexity of Theorem-Proving Procedures. In ACM STOC, pages 151–158, 1971.

[4] U.H. Engberg. Simple Symbolic Bisimulations. In preparation.

[5] U.H. Engberg and K.S. Larsen. Efficient Reduction of Bisimulation Formulas. Preprint 47, Dept. of Math. and Computer Science, Odense University, 1993.

[6] B.A. Galler and M.J. Fischer. An improved equivalence algorithm. Comm. ACM, 7:301–303, 1964.

[7] M.R. Garey and D.S. Johnson. Computers and Intractability. W. H. Freeman, 1979.

[8] L.J.Guibas and R.Sedgewick. A Dichromatic Framework for Balanced Trees. IEEE FOCS, 8–21, 1978.

[9] M. Hennessy and H. Lin. Symbolic Bismulations. Tech. Rep. 1/92, University of Sussex, 1992. To appear in Theoretical Computer Science, 1995.

[10] M. Hennessy and H. Lin. Proof systems for message-passing process algebras. CON-CUR ’93, pages 202–216, August 1993.

[11] G.J. Klir and T.A. Folger. Fuzzy Sets, Uncertainty, and Information. Prentice-Hall, 1988.

[12] H. Mannila and E. Ukkonen. The set union problem with backtracking. LNCS 226, 236–243, 1986.

[13] K. Mehlhorn and A. Tsakalidis. Data Structures. In Jan van Leeuwen, editor, Handbook of Theoretical Computer Science, chapter 6, pages 301–341. Elsevier Science Publishers, 1990.

[14] R. Milner. Communication and Concurrency. Prentice-Hall, 1989.

[15] Z. Schreiber. Verification of Value-Passing Systems. In First North American Process Algebra Workshop, pages 9.1–9.20. Tech. Rep. 92-15, Johns Hopkins University, 1992.

[16] D. Scott. Notes on the formalization of logic. Technical report, Sub-faculty of Phil., Oxford, 1981.

[17] R.E. Tarjan. Efficiency of a good but not linear set union algorithm. JACM, 22:215– 225, 1975.

[18] R.E. Tarjan. Data Structures and Network Algorithms. Soc. for Industrial and Applied Math., 1983.

[19] R.E.Tarjan and J.v.Leeuwen. Worst-Case Analysis of Set Union Algorithms. JACM, 31:245–281, 1984.

[20] J. Westbrook and R.E. Tarjan. Amortized analysis of algorithms for set union with backtracking. SIAM J. Comput., 18(1):1–11, 1989.