Chicago Journal of Theoretical Computer Science

The MIT Press

Volume 1998, Article 2 16 March 1998

ISSN 1073–0486. MIT Press Journals, Five Cambridge Center, Cambridge, MA 02142-1493 USA; (617)253-2889; journals-orders@mit.edu, journals-info@mit.edu. Published one article at a time in L^{A}TEX source form on the Internet. Pagination varies from copy to copy. For more information and other articles see:

• http://mitpress.mit.edu/CJTCS/

• http://www.cs.uchicago.edu/publications/cjtcs/

• ftp://mitpress.mit.edu/pub/CJTCS

• ftp://cs.uchicago.edu/pub/publications/cjtcs Kupferman and Vardi Verification of Systems (Info)

The Chicago Journal of Theoretical Computer Science is abstracted or indexed in Research Alert,◯^{R}SciSearch,◯^{R}Current Contents◯^{R}/Engineering Computing & Technology, and CompuMath Citation Index.◯^{R}

\begin{matrix}c \\ ◯ \end{matrix}1998 The Massachusetts Institute of Technology. Subscribers are licensed to use journal articles in a variety of ways, limited only as required to insure fair attribution to authors and the journal, and to prohibit use in a competing commercial product. See the journal’s World Wide Web site for further details. Address inquiries to the Subsidiary Rights Manager, MIT Press Journals; (617)253-2864; journals-rights@mit.edu.

The Chicago Journal of Theoretical Computer Science is a peer-reviewed scholarly journal in theoretical computer science. The journal is committed to providing a forum for significant results on theoretical aspects of all topics in computer science.

Editor in chief: Janos Simon

Consulting editors: Joseph Halpern, Stuart A. Kurtz, Raimund Seidel

Editors:

Martin Abadi  Greg Frederickson John Mitchell
Pankaj Agarwal Andrew Goldberg Ketan Mulmuley
Eric Allender Georg Gottlob Gil Neiger
Tetsuo Asano  Vassos Hadzilacos David Peleg
Laszló Babai  Juris Hartmanis Andrew Pitts
Eric Bach  Maurice Herlihy James Royer
Stephen Brookes Ted Herman  Alan Selman
Jin-Yi Cai  Stephen Homer  Nir Shavit
Anne Condon  Neil Immerman  Eva Tardos
Cynthia Dwork Howard Karloff  Sam Toueg
David Eppstein Philip Klein  Moshe Vardi
Ronald Fagin  Phokion Kolaitis Jennifer Welch
Lance Fortnow Stephen Mahaney Pierre Wolper
Steven Fortune Michael Merritt

Managing editor: Michael J. O’Donnell

Electronic mail: chicago-journal@cs.uchicago.edu

[ii]

Verification of Fair Transition Systems

Orna Kupferman  Moshe Y. Vardi

16 March, 1998

Abstract

In program verification, we check that an implementation meets

Abstract-1

its specification. Both the specification and the implementation describe the possible behaviors of the program, although at different levels of abstraction. We distinguish between two approaches to implementation of specifications. The first approach is trace-based implementation, where we require every computation of the implementation to correlate to some computation of the specification. The second approach is tree-based implementation, where we require every computation tree embodied in the implementation to correlate to some computation tree embodied in the specification. The two approaches to implementation are strongly related to the linear-time versus branching-time dichotomy in temporal logic.

In this work, we examine the trace-based and the tree-based ap-

Abstract-2

proaches from a complexity-theoretic point of view. We consider and compare the complexity of verification of fair transition systems, modeling both the implementation and the specification in the two approaches. We consider unconditional, weak, and strong fairnesses. For the trace-based approach, the corresponding problem is fair containment. For the tree-based approach, the corresponding problem is fair simulation. We show that while both problems are PSPACEcomplete, their complexities in terms of the size of the implementation do not coincide, and the trace-based approach is easier. As the implementation is normally much bigger than the specification, we see this as an advantage of the trace-based approach. Our results are at variance with the known results for the case of transition systems with no fairness, where no approach is evidently advantageous.

1

Kupferman and Vardi Verification of Systems §1

1 Introduction

In program verification, we check that an implementation meets its specifi-

1-1

cation. Both the specification and the implementation describe the possible behaviors of the program, but the implementation is more concrete than the specification, or, equivalently, the specification is more abstract than the implementation [AL91]. This basic notion of verification suggests a top-down method for design development. Starting with a highly abstract specification, we can construct a sequence of “behavior descriptions.” Each description refers to its predecessor as a specification, so it is less abstract than its predecessor. The last description contains no abstractions, and constitutes the implementation. Hence the name hierarchical refinement for this methodology [LS84, LT87, Kur94].

We distinguish between two approaches to implementation of specifica-

1-2

tions. The first approach is trace-based implementation, where we require every computation of the implementation to correlate to some computation of the specification. The second approach is tree-based implementation, where we require every computation tree embodied in the implementation to correlate to some computation tree embodied in the specification. The exact notion of correct implementation then depends on how we interpret correlation. We can, for example, interpret correlation as identity. Then, a correct trace-based implementation is one in which every computation is also a computation of the specification, and a correct tree-based implementation is one in which every embodied computation tree is also embodied in the specification. Numerous interpretations of correlation are suggested and studied in the literature [Hen85, Mil89, AL91]. Here we consider a simple definition of correlation, and interpret it as equivalence with respect to the variables joint to the implementation and the specification, as the implementation is typically defined over a wider set of variables (reflecting the fact that it is more concrete than the specification).

The tree-based approach is stronger in the following sense. If I is a cor-

1-3

rect tree-based implementation of the specification S, then I is also a correct trace-based implementation of S. As shown by Milner [Mil80], the opposite situation is not true. The two approaches to implementation are strongly related to the linear-time versus branching-time dichotomy in temporal logic [Pnu85]. The temporal-logic analogy to the strength of the tree-based approach is the expressiveness superiority of ∀CTL^{⋆}, the universal fragment of CTL^{⋆}, over LTL [CD88]. Indeed, while a correct trace-based implementation

2 is guaranteed to satisfy all the LTL formulas satisfied in the specification, a correct tree-based implementation is guaranteed to satisfy all the ∀CTL^{⋆} formulas satisfied in the specification [GL94].

In this work, we examine the traced-based and tree-based approaches

1-4

from a complexity-theoretic point of view. More precisely, we consider and compare the complexity of the problem of determining whether I is a correct trace-based implementation of S, and the problem of determining whether I is a correct tree-based implementation of S. The different levels of abstraction in the implementation and the specification are reflected in their sizes. The implementation is typically much larger than the specification, and it is the implementation’s size that is the computational bottleneck. Therefore, of particular interest to us is the implementation complexity of these problems; i.e., their complexity in terms of I, assuming S is fixed.^{1}

We model specifications and implementations by transition systems

1-5

[Kel76]. The systems are defined over the sets AP_{I} and AP_{S} of atomic propositions used in the implementation and specification, respectively. Thus, the alphabets of the systems are 2^{AP_{I}} and 2^{AP_{S}}. Recall that usually the implementation has more variables than the specification; hence, AP_{I} ⊇ AP_{S}. We therefore interpret correlation as equivalence with respect to AP_{S}. In other words, associating behaviors of the implementation with those of the specification, we first project the behaviors onto AP_{S}. Within this framework, correct trace-based implementation corresponds to containment, and correct tree-based implementation corresponds to simulation [Mil71].

We start by reviewing and examining transition systems with no fair-

1-6

ness conditions. It is well known that simulation can be checked in polynomial time [Mil80, BGS92, AV95, HHK95], whereas the containment problem is in PSPACE [SVW87]. We show that the latter problem is PSPACEhard; thus the tree-based approach is easier than the trace-based approach. Yet, once we turn to consider the implementation complexity of simulation and containment, the trace-based approach is easier than the tree-based approach. Indeed, we show that the implementation complexity of simulation is PTIME-complete, which is most likely harder than the NLOGSPACEcomplete bound for the implementation complexity of containment. For

3 these reasons, when we consider transition systems with no fairness, there is no clear advantageous approach. This is reminiscent of the computational relations of branching-time model checking and linear-time model checking: while model checking is easier for the branching paradigm, the implementation complexity of model checking in the two paradigms coincide [LP85, CES86, VW86, BVW94].

1The distinction between the relative sizes of the implementation and the specification is less significant in the context of hierarchical refinement. There, each internal behavior description is both an implementation (of some step i in the chain of successive refinements)

and a specification (of step i + 1 in the chain). Thus, the distinction is crucial only in the last refinement step, which handles the final, and hence largest, implementation.

Often, we want our implementations and specifications to describe be-

1-7

haviors that satisfy both liveness and safety properties. Then, transition systems with no fairness condition are too weak, and we need the framework of fair transition systems. We consider unconditional, weak, and strong fairness (also known as impartiality, justice, and compassion, respectively) [LPS81, Eme90, MP92]. Within this framework, correct trace-based implementation corresponds to fair containment, and correct tree-based implementation corresponds to fair simulation [BBLS92, ASB^{+}94, GL94]. Hence, it is the complexity of these problems that should be examined when we compare the trace-based and the tree-based approaches.

We present a uniform method and a simple algorithm for solving the

1-8

fair-containment problem for all three types of fairness conditions. Unlike [CDK93], we consider the case where both the specification and the implementation are nondeterministic, as is appropriate in a hierarchical refinement framework. We prove that the problem is PSPACE-complete for all three types. For the case where the implementation uses the unconditional or weak fairness conditions, our nondeterministic algorithm requires space logarithmic in the size of the implementation (regardless of the type of fairness condition used in the specification). For the case where the implementation uses the strong fairness condition, we suggest an alternative algorithm that runs in time polynomial in the size of the implementation. We show that these algorithms are optimal; the implementation complexity of fair containment is NLOGSPACE-complete for implementations that use the unconditional or weak fairness conditions [VW94] and is PTIME-complete for implementations that use the strong fairness condition. To prove the latter, we show that the nonemptiness problem for fair transition systems with a strong fairness condition is PTIME-hard.

We also present a uniform method and a simple algorithm for solving

1-9

the fair-simulation problem for the three types of fairness conditions. Our algorithm uses the fair-containment algorithm as a subroutine. We prove that the problem is PSPACE-complete for all three types. Like Milner’s algorithm for checking simulation [Mil90], our algorithm can be implemented

Kupferman and Vardi Verification of Systems §2.1

4 as a calculation of a fixed-point expression. The running time of our algorithm is polynomial in the size of the implementation. We show that this is optimal; thus, the implementation complexity of fair simulation is PTIMEcomplete for all types of fairness conditions. In fact, in proving the latter, we prove that the implementation complexity of simulation (without fairness conditions) is PTIME-hard as well.

Our results (summarized in Table 1) show that when we model the speci-

1-10

fication and the implementation by fair transition systems, or we consider the implementation complexity of verification, the computational advantage of the tree-based approach disappears. Furthermore, when we consider the implementation complexity, checking implementations that use unconditional or weak fairness conditions is easier in the trace-based approach.

2 Preliminaries

2.1 Fair Transition Systems

A fair transition system (transition system, for short) S = ⟨Σ, W, R, W_{0}, L, α⟩

2.1-1

consists of an alphabet Σ, a finite set W of states, a total transition relation R ⊆ W × W (i.e., for every w ∈ W there exists w′ ∈ W such that R(w, w′)), a set W_{0} of initial states, a labeling function L : W → Σ, and a fairness condition α. We will define three types of fairness conditions shortly. A computation of S is a sequence π = w_{0}, w_{1}, w_{2}, … of states such that for every i ≥ 0, we have R(w_{i}, w_{i+1}). For an alphabet Σ, we use Σ^{∗} and Σ^{ω} to denote the sets of all finite and infinite words over Σ, respectively. For two words ρ_{1} ∈ Σ^{∗} and ρ_{2} ∈ Σ^{∗} ∪ Σ^{ω}, we use ρ_{1} · ρ_{2} to denote the concatenation of ρ_{1} and ρ_{2}. Each computation π = w_{0}, w_{1}, w_{2}, … induces the word L(π) = L(w_{0}) · L(w_{1}) · L(w_{2}) … ∈ Σ^{ω}.

To determine whether a computation is fair, we refer to the set Inf (π) of

2.1-2

states that π visits infinitely often. Formally,

Inf (π) = {w ∈ W : for infinitely many i ≥ 0, we have w_{i} = w}

The way we refer to Inf (π) depends upon the fairness condition of S. Several types of fairness conditions are studied in the literature. Here we consider three:

• Unconditional fairness (or impartiality), where α ⊆ W, and π is fair if

and only if Inf (π) ∩ α ≠ ∅. 5 • Weak fairness (or justice), where α ⊆ 2^{W} × 2^{W}, and π is fair if and

only if for every pair ⟨B, G⟩ ∈ α, we have that Inf (π) ∩ (W \ B) = ∅ implies Inf (π) ∩ G ≠ ∅.

• Strong fairness (or fairness), where α ⊆ 2^{W} × 2^{W}, and π is fair if and only if for every pair ⟨B, G⟩ ∈ α, we have that Inf (π) ∩ B ≠ ∅ implies Inf (r) ∩ G ≠ ∅.

In addition, we consider nonfair transition systems; i.e., transition sys-

2.1-3

tems in which all the computations are fair.

It is easy to see that fair transition systems are essentially notational

2.1-4

variants of automata on infinite words [Tho90]. In particular, the unconditional and the strong fairness conditions correspond to the Büchi and Streett acceptance conditions. This correspondence motivates our noncanonical definition of fairness, where the unconditional fairness condition consists of a single constraint, whereas the weak and strong fairness conditions consist of a conjunction of constraints. In the sequel, we use results from the theory of Büchi and Streett automata in the context of fair transition systems.

Defining the unconditional fairness condition as a conjunction of con-

2.1-5

straints (that is, having α ⊆ 2^{W}) corresponds to the generalized Büchi condition from automata theory. Note that such generalized unconditional fairness conditions are very similar to weak fairness conditions; in fact, they can be viewed as a special case of weak fairness conditions, with B = W in all pairs. Moreover, as we state formally in Lemma 1, weak fairness conditions can be easily translated to generalized unconditional fairness conditions. Indeed, a pair ⟨B, G⟩ in a weak fairness condition is equivalent to a set (W \ B) ∪ G in a generalized unconditional fairness condition.

For a state w, a w-computation is a computation w_{0}, w_{1}, w_{2}, … with

2.1-6

w_{0} = w. We use T (S^{w}) to denote the set of all traces σ_{0} · σ_{1} … ∈ Σ^{ω} for which there exists a fair w-computation w_{0}, w_{1}, … in S with L(w_{i}) = σ_{i} for all i ≥ 0. The trace set T (S) of S is then defined as ⋃_{w∈W_{0}} T (S^{w}). Thus, each transition system defines a subset of Σ^{ω}. We say that a transition system S is empty if and only if T (S) = ∅; i.e., S has no fair computation. We sometimes say that S accepts a trace ρ, meaning that ρ ∈ T (S). Note that for a nonfair transition system S, the set T (S) contains all traces ρ ∈ Σ^{ω} for which there exists a computation π with L(π) = ρ.

The size of a transition system and its fairness condition determine the

2.1-7

complexity of solving questions about it. We define classes of transition

Kupferman and Vardi Verification of Systems §2.2.1

6 systems according to these two characteristics. We use U, W, and S to distinguish between the unconditional, weak, and strong fairness conditions, respectively. We measure the size of a transition system by the number of its states (the number of edges is at most quadratic in the number of states) and, in the case of weak and strong fairness, also by the number of pairs in its fairness condition. For example, the set of unconditionally fair transition systems with n states is denoted U(n). We also use a line over the transition system to denote the complementary transition system (one that accepts the complementary trace set). For example, the set of transition systems that complements strongly fair transition systems with n states and m pairs is denoted by \overline{S(n, m)}. By [Saf88, Saf92], every fair transition system indeed has a complementary transition system. We use → to denote a possible translation (that preserves the trace sets of the systems) between various types of transition systems. For example, W(n, m) → U(nm) means that each weakly fair transition system S with n states and m pairs can be translated to an unconditionally fair transition system S′ with nm states such that T (S) = T (S′).

2.2 Trace-Based and Tree-Based Implementations

In this section, we formalize what it means for an implementation S to cor-

2.2-1

rectly implement a specification S′, in both the trace-based and the treebased approaches. Recall that S and S′ are given as fair transition systems over the alphabets 2^{AP} and 2^{AP′}, respectively, with AP ⊇ AP′. For technical convenience, we assume that AP = AP′; thus, the implementation and the specification are defined over the same alphabet. By taking, for each σ ∈ 2^{AP}, the letter σ ∩ AP′ instead of the letter σ, all of our algorithms and results are also valid for the case AP ⊃ AP′.

Recall that nonfair transition systems are of special interest. The prob-

2.2-2

lems that formalize correct trace-based and tree-based implementations in this framework are containment and simulation. Once we add fairness to the systems, the corresponding problems are fair containment and fair simulation. Below we define the four problems. All problems are defined with respect to two transition systems: S = ⟨Σ, W, R, W_{0}, L, α⟩, and S′ = ⟨Σ, W′, R′, W′_{0}, L′, α′⟩.

7 2.2.1 Containment and Fair Containment

The fair-containment problem of S and S′ is to determine whether T (S) ⊆

2.2.1-1

T (S′); that is, whether every trace accepted by S is also accepted by S′. When S and S′ are nonfair, we call the problem containment.

While containment and fair containment refer only to the set of computa-

2.2.1-2

tions of S and S′, simulation and fair simulation also refer to the branching structure of the transition systems.

2.2.2 Simulation

Let w and w′ be states in W and W′, respectively. A relation H ⊆ W × W′

2.2.2-1

is a simulation relation from ⟨S, w⟩ to ⟨S′, w′⟩ if and only if the following conditions hold [Mil71]:

1. H(w, w′).

2. For all t and t′ with H(t, t′), we have L(t) = L(t′).

3. For all t and t′ with H(t, t′) and for all s ∈ W such that R(t, s), there exists s′ ∈ W′ such that R′(t′, s′) and H(s, s′).

A simulation relation H is a simulation from S to S′ if and only if for

2.2.2-2

every w ∈ W_{0} there exists w′ ∈ W′_{0} such that H(w, w′). If there exists a simulation from S to S′, we say that S simulates S′, and we write S ≤ S′. Intuitively, this means that the transition system S′ has more behaviors than the transition system S. In fact, every ∀CTL^{⋆} formula that is satisfied in S′ is satisfied also in S [BCG88]. Given S and S′, the simulation problem is to determine whether S ≤ S′.

We also mention here the bisimulation problem [Mil71]. Two transition

2.2.2-3

systems are bisimilar if and only if they have exactly the same behavior. Formally, a relation H ⊆ W × W′ from ⟨S, w⟩ to ⟨S′, w′⟩ is a bisimulation if, in addition to conditions 1–3 above, the following condition also holds:

4. For all t and t′ with H(t, t′) and for all s′ ∈ W′ such that R′(t′, s′), there exists s ∈ W such that R(t, s) and H(s, s′).

2.2.3 Fair Simulation

Let H ⊆ W × W′ be a relation over the states of S and S′. It is convenient

2.2.3-1

to extend H to also relate infinite computations of S and S′. For two computations π = w_{0}, w_{1}, … in S, and π′ = w′_{0}, w′_{1}, … in S′, we say that H(π, π′)

8 holds if and only if H(w_{i}, w′_{i}) holds for all i ≥ 0. For a pair ⟨w, w′⟩ ∈ W ×W′, we say that ⟨w, w′⟩ is good in H if and only if for every fair w-computation π in S, there exists a fair w′-computation π′ in S′, such that H(π, π′).

Let w and w′ be states in W and W′, respectively. A relation H ⊆ W ×W′

2.2.3-2

is a fair-simulation relation from ⟨S, w⟩ to ⟨S′, w′⟩ if and only if the following conditions hold [GL94]:

1. H(w, w′).

2. For all t and t′ with H(t, t′), we have L(t) = L(t′).

3. For all t and t′ with H(t, t′), the pair ⟨t, t′⟩ is good in H.

A fair-simulation relation H is a fair simulation from S to S′ if and only

2.2.3-3

if for every w ∈ W_{0} there exists w′ ∈ W′_{0} such that H(w, w′). If there exists a fair simulation from S to S′, we say that S fair simulates S′, and we write S ≤ S′. Intuitively, this means that the transition system S′ has more fair behaviors than the transition system S. In fact, every fair-∀CTL^{⋆} formula (that is, every ∀CTL^{⋆} formula with path quantification ranging only over fair computations [EL87]) that is satisfied in S′ is also satisfied in S [GL94]. The fair-simulation problem is, given S and S′, to determine whether S ≤ S′. Note that when they relate nonfair transition systems, fair simulation and simulation coincide.

We also mention here the fair-bisimulation problem [GL94]. Two tran-

2.2.3-4

sition systems are bisimilar if and only if they have exactly the same fair behavior. Formally, a relation H ⊆ W × W′ from ⟨S, w⟩ to ⟨S′, w′⟩ is a fair bisimulation if conditions 1–3 hold with the following symmetric definition of when a pair is good in H. In fair bisimulation, a pair ⟨w, w′⟩ ∈ W × W′ is good in H if and only if for every fair w-computation π in S, there exists a fair w′-computation π′ in S′ such that H(π, π′), and for every fair w′-computation π′ in S′, there exists a fair w-computation π in S such that H(π, π′).

It is easy to see that simulation implies containment, and that fair simu-

2.2.3-5

lation implies fair containment; that is, if S ≤ S′, then T (S) ⊆ T (S′). The opposite, however, is not true. Consider the two transition systems S and S′ presented in Figure 1. Note that while the system S has two initial states, one labeled by a and one labeled by b, the system S′ has three initial states, two labeled by a and one labeled by b. The trace sets of both transition systems are (a + b)^{ω}. As such, T (S) ⊆ T (S′), but still, S does not simulate S′. Indeed, no initial state of S′ can be paired, by any H, to the initial state labeled a of S.

9

a  S′ : S :  b a  a a b
Figure 1: T (S) ⊆ T (S′) but S ≰ S′

2.3 Complexity Measures

In the rest of this paper, we examine the traced-based and the tree-based

2.3-1

approaches from a complexity-theoretic point of view. We consider and compare the complexity of the four problems. The different levels of abstraction in the implementation and the specification are reflected in their sizes. The implementation is typically much larger than the specification, and it is the implementation’s size that is the computational bottleneck. Therefore, of particular interest to us is the implementation complexity of these problems; i.e., the complexity of checking whether T (S) ⊆ T (S′) and S ≤ S′, in terms of the size of S, assuming S′ is fixed.

We refer to three complexity classes: PSPACE, PTIME, and

2.3-2

NLOGSPACE, briefly described as follows (for a full definition, see [GJ79]). We say that a problem is in PSPACE (PTIME) if there exists a deterministic algorithm for solving the problem such that the working space (time, respectively) required for executing the algorithm is polynomial in the size of its input. The problem is in NLOGSPACE if there exists a nondeterministic algorithm for solving the problem such that the working space required for the algorithm is logarithmic in the size of its input. A program P is complete for a complexity class C if and only if P is in C and is also C-hard.

Some of the results we study, mainly those that we consider nonfair tran-

2.3-3

sition systems, are known; therefore we only review them.

3 Verification of Nonfair Transition Systems

In this section, we study the complexity of the containment and simulation

3-1

problems. We show that while the containment problem is harder, its implementation complexity is lower than that of the simulation problem.

10

3.1 The Containment Problem

Theorem 1 The containment problem is PSPACE-complete.

Proof of Theorem 1 The upper bound follows from known PSPACE

Proof of Theorem 1-1

bound to the fair-containment problem for unconditionally fair transition systems ([SVW87], see also Theorem 5).

We can regard an unconditionally fair system S = ⟨Σ, W, R, W_{0}, L, α⟩,

Proof of Theorem 1-2

with α ⊆ W, as a finite-acceptance transition system. The traces of a finiteacceptance transition system are finite words over the alphabet Σ. A finite computation π = w_{0}, …, w_{k} is “fair” in S (that is, L(π) is accepted) if and only if w_{k} ∈ α. We call the states in α final states. A finite-acceptance transition system S is universal if and only if T (S) = Σ^{∗}. In [MS72], Mayer and Stockmayer prove a PSPACE lower bound for the problem of determining whether a finite-acceptance transition system S is universal (the framework in [MS72] is of regular expressions, yet regular expressions can be linearly translated to finite-acceptance transition systems).

We reduce the universality problem for finite-acceptance transition sys-

Proof of Theorem 1-3

tems to the containment problem. Consider a finite-acceptance transition system S = ⟨Σ, W, R, W_{0}, L, α⟩. Let

S′ = ⟨Σ ∪ {#}, W ∪ {w_{#}}, R ∪ R_{#}, W_{0}, L′, W ∪ {w_{#}}⟩

be a nonfair transition system, where:

• For every w ∈ (α ∪ {w_{#}}), we have R_{#}(w, w_{#}). Thus S′ has the transitions of S augmented with transitions from all the final states to the state w_{#}, which has a self loop.

• For every state w ∈ W, we have L′(w) = L(w). In addition, L′(w_{#}) = {#}.

We prove that Σ^{∗} ⊆ T (S) if and only if Σ^{ω}∪(Σ^{∗}·{#}^{ω}) ⊆ T (S′). Assume

Proof of Theorem 1-4

first that Σ^{ω} ∪ (Σ^{∗} · {#}^{ω}) ⊆ T (S′), and assume, by way of contradiction, that there exists ρ ∈ Σ^{∗} such that ρ ∉ T (S). Let π = w_{0}, w_{1}, … be an accepting computation of S′ on ρ · #^{ω}. By the definition of L′, we have that π ∈ W^{∗} · w_{#}^{ω}. Let k be such that w_{k} ≠ w_{#} and w_{k+1} = w_{#}. As R_{#}(w_{k}, w_{k+1}), it must be that w_{k} ∈ α. In addition, for all 0 ≤ i < k − 1, we have R(w_{i}, w_{i+1}). Hence w_{0}, …, w_{k} is an accepting computation of S on ρ, and we reach a contradiction.

11 Assume now that Σ^{∗} ⊆ T (S). Consider a trace ρ ∈ Σ^{∗}. Let w_{0}, w_{1}, …, w_{k}

Proof of Theorem 1-5

be an accepting computation of S on ρ. Clearly, w_{0}, w_{1}, …, w_{k}, w_{#}^{ω} is an accepting computation of S′ on ρ · {#}^{ω}. Hence, Σ^{∗} · {#}^{ω} ⊆ T (S′). Next, consider a trace ρ = σ_{0}, σ_{1}, … ∈ Σ^{ω}. We define a tree that embodies all the possible runs of S on finite prefixes of ρ. The tree has a root labeled ϵ. The nodes of level 1 (that is, nodes that have a path of length 1 from the root) are states w_{0} in W_{0} for which L(w_{0}) = σ_{0}. For l ≥ 0, a node w of level i has as successors nodes w′ for which R(w, w′) and L(w′) = σ_{l+1}. Because Σ^{∗} ⊆ T (S), the tree embodies accepting runs for all the (infinitely many) finite prefixes of ρ, and is therefore infinite. Hence, by König’s lemma, we can pick a sequence π = ϵ, w_{0}, w_{1}, … such that w_{0} ∈ W_{0}, and for all j ≥ 0, we have that L(w_{j}) = σ_{j} and R(w_{j}, w_{j+1}). As such, π is an accepting run of S′ on ρ. As we can easily construct a nonfair transition system for Σ^{ω} ∪(Σ^{∗}·{#}^{ω}), we are done.

Proof of Theorem 1 □

Theorem 2 The implementation complexity of the containment problem is NLOGSPACE-complete.

Proof of Theorem 2 In Theorem 6, we prove an NLOGSPACE upper bound for the implementation complexity of the more general faircontainment problem for unconditionally fair transition systems. The lower bound follows easily by a reduction from the nonreachability problem in a directed graph, proved to be NLOGSPACE-complete in [Jon75].^{2} Given a directed graph G with two designated nodes s and t, we can view G as a nonfair transition system S_{G} over Σ = {σ, s, t} in which all states are initial states, all states except s and t are labeled σ, and the states s and t are labeled with s and t, respectively. It is easy to see that the node t is not reachable from s if and only if T (G) ⊆ {σ, t}^{∗} · {σ, s}^{ω} ∪ {σ, t}^{ω}. Since we can specify the expression in the right with a fixed nonfair transition system, we are done.

Proof of Theorem 2 □

12

2The proof in [Jon75] is for the reachability problem. Yet, for every problem P, we have that P is NLOGSPACE-complete if and only if P is co-NLOGSPACE-complete (see [Imm88, Sze88] for NLOGSPACE = co-NLOGSPACE; the argument for the completeness is easy).

3.2 The Simulation Problem

Theorem 3 The simulation problem is PTIME-complete.

Proof of Theorem 3 The upper bound is given in [Mil80]. The lower bound follows from the reduction in [BGS92] (the reduction there proves PTIME-hardness for bisimulation, but it is valid also for simulation). An additional proof of the lower bound is given in Theorem 4.

Proof of Theorem 3 □

Theorem 4 The implementation complexity of the simulation problem is PTIME-complete.

Proof of Theorem 4 Membership in PTIME follows from Theorem 3.

Proof of Theorem 4-1

We prove hardness in PTIME by reducing the NAND circuit value prob-

Proof of Theorem 4-2

lem (NANDCV), proved to be PTIME-complete in [Gol77, GHR95], to the problem of determining whether a transition system S simulates a fixed transition system S′, both with no fairness. In the NANDCV problem, we are given a Boolean circuit β constructed solely of NAND gates of fanout 2, and a vector ⟨x_{1}, …, x_{n}⟩ of Boolean input values. The problem is to determine whether the output of β on ⟨x_{1}, …, x_{n}⟩ is 1. Formally, we denote a Boolean circuit of NAND gates by a tuple β = ⟨G, G_{in}, g_{out}, T_{l}, T_{r}⟩, where G is the set of internal gates, G_{in} is the set of input gates (identified as g_{1}, …, g_{n}), g_{out} ∈ G ∪ G_{in} is the output gate, T_{l} : G → G ∪ G_{in} maps each internal gate to its left input, and T_{r} : G → G ∪ G_{in} maps each internal gate to its right input. Note that since there are no circular dependencies in β, the graph induced by T_{l} and T_{r} is acyclic.

The idea of the reduction is as follows. We define a fixed transition system

Proof of Theorem 4-3

S′ that embodies all the NAND circuits β and input vectors x⃗ for which the value of β on x⃗ is 1. Then, given a circuit β and an input vector x⃗, we translate them to a transition system S such that S ≤ S′ if and only if the value of β on x⃗ is 1.

The transition system S′ (see Figure 2) has 12 states. Eight states corre-

Proof of Theorem 4-4

spond to internal gates. Each of these states is an entry in the truth table of the operator NAND, attributed with a direction, either ↙ or ↘. Thus, the “internal states” of S′ are ⟨001 ↙⟩, ⟨011 ↙⟩, ⟨101 ↙⟩, ⟨110 ↙⟩, ⟨001 ↘⟩, ⟨011 ↘⟩, ⟨101 ↘⟩, and ⟨110 ↘⟩. Four more states correspond to the input gates of the circuit. Each of these states is a Boolean value, attributed with a

13

101↙  001↙ 110↙ 001↘  011↘  101↘  110↘ 011↙  1↙ 0↘ 1↘ 0↙

Figure 2: A fixed transition system that embodies all NAND circuits

direction; thus the “input states” are ⟨0 ↙⟩, ⟨1 ↙⟩, ⟨0 ↘⟩, and ⟨1 ↘⟩. The intuition is that an internal state ⟨l, r, val, d⟩ corresponds to a NAND gate that has the value l in its left input, has the value r in its right input, and whose output val can be only a d-input of other gates. Similarly, an input state ⟨val, d⟩ corresponds to an input gate with output val that can only be a d input of other gates.

Accordingly, the transitions from an internal state ⟨l, r, val, d⟩ corre-

Proof of Theorem 4-5

spond to the possible ways of having l and r as right and left inputs, respectively. Thus, we have transitions from this state to all (internal or input) states with either val = l and d =↙ or val = r and d =↘. For example, the internal state ⟨101 ↙⟩ has transitions to the states ⟨001 ↙⟩, ⟨011 ↙⟩, ⟨101 ↙⟩, ⟨110 ↘⟩, ⟨1 ↙⟩, and ⟨0 ↘⟩. It has transitions from all states ⟨l, r, val, d⟩ with l = 0. In addition, the input states have self loops.

We label an internal state by either ↙ or ↘, according to its directional

Proof of Theorem 4-6

element. For example, the node ⟨101 ↙⟩ is labeled {↙}. We label an input state by both its value and direction. For example, the node ⟨1 ↘⟩ is labeled {1, ↘}. We define the initial states of S′ to be those with val = 1, and we impose no fairness condition. Clearly, the size of S′ is fixed.

14 Given a circuit β = ⟨G, G_{in}, g_{out}, T_{l}, T_{r}⟩ and an input vector x⃗, the

Proof of Theorem 4-7

transition system S is simply β, with attributions of directions, and labeling of input gates according to x⃗. More precisely, we duplicate all gates and inputs of β so that the output of each gate is either always a left input of other gates, in which case we label it with ↙, or always a right input of other gates, in which case we label it with ↘. In addition, we add self loops to the input gates and label them with their values. As the set of initial states, we take both attributions of g_{out}. Formally, S = ⟨{↙, ↘} ∪ {0, 1} × {↙, ↘}, (G ∪ G_{in}) × {↙, ↘}, T, {g_{out}} × {↙, ↘}, L⟩, where:

• T (⟨g, d⟩, ⟨g′, d′⟩) if and only if one of the following holds:

1. g ∈ G, d′ = l, and T_{l}(g) = g′,

2. g ∈ G, d′ = r, and T_{r}(g) = g′, or

3. g ∈ G_{in}, g = g′, and d = d′.

• For g ∈ G, we have L(⟨g, d⟩) = d. For g_{i} ∈ G_{in}, we have L(⟨g_{i}, d⟩) = ⟨x_{i}, d⟩.

We define the depth of a gate as the length of the longest path from it to an

Proof of Theorem 4-8

input gate. Note that the only cycles in S are the self loops in the input gates, and the path cannot use them. Thus, for g ∈ G_{in}, we have depth(g) = 0, and for g ∈ G, we have depth(g) = 1 + max{depth(T_{l}(g)), depth(T_{r}(g))}.

We first prove that for a simulation relation H from S to S′ and for every

Proof of Theorem 4-9

pair ⟨⟨g, d⟩, ⟨val, d′⟩⟩ or ⟨⟨g, d⟩, ⟨l, r, val, d′⟩⟩ in H, the output of the gate g on the vector x⃗ is val. The proof proceeds by induction on depth(g). If depth(g) = 0, then g ∈ G_{in}. Let g = g_{i}. By the definition of L′, the state ⟨g_{i}, d⟩ is labeled with x_{i} and can therefore be related by H only to states ⟨val, d′⟩ for which val = x_{i}. Assume that the claim holds for all gates of depth at most i. Let g be such that depth(g) = i + 1. Then, g ∈ G, and ⟨g, d⟩ is mapped to some internal state t = ⟨l, r, v, d′⟩. By the definition of simulation, for every successor ⟨g′, d′⟩ of ⟨g, d⟩ there exists a successor t′ of t such that H(g′, t′). We know that ⟨g, d⟩ has two successors, ⟨T_{l}(g), ↙⟩ and ⟨T_{r}(g), ↘⟩. By the definition of S′, all the successors of t that are labeled with ↙ have value l. Therefore, by the induction hypothesis, the output of T_{l}(g) is l. Similarly, the output of T_{r}(g) is r. Thus, the output of g is NAND(l, r). By the definition of S′, we also have v = NAND(l, r), and we are done.

15 We now prove that the output of β on x⃗ is 1 if and only if S simulates

Proof of Theorem 4-10

S′. Assume first that S simulates S′. Let H be the simulation relation from S to S′. When we take as the initial set of S′ the states with val = 1, both states ⟨g_{out}, ↙⟩ and ⟨g_{out}, ↘⟩ of S are related by H to states with val = 1. Hence, by the above claim, the output of β on x⃗ is 1.

Assume that the output of β on x⃗ is 1. Consider a relation H from the

Proof of Theorem 4-10

states of S to the states of S′ in which H(⟨g, d⟩, ⟨l, r, val, d′⟩) for an internal gate g if and only if l is the value of the left input to g, r is the value of the right input to g, val is the output of g on x⃗, and d = d′; and H(⟨g, d⟩, ⟨val, d′⟩) for an input gate g if and only if val is the output of g on x⃗ and d = d′. We show that H is a simulation relation from S to S′. Consider a state w_{1} in S with H(w_{1}, w′_{1}). We have to show that for every successor w_{2} of w_{1} there exists a successor w′_{2} of w′_{1} such that H(w_{2}, w′_{2}). Consider first the case where w_{1} = ⟨g, d⟩ for g ∈ G_{in}. By the definition of S, the state w_{1} has a single successor w_{2} with w_{2} = w_{1}. Let w′_{1} be such that H(w_{1}, w′_{1}). By the definition of H, we have w′_{1} = ⟨val, d⟩, where val is the output of g on x⃗. By the definition of S′, the state w′_{1} has a single successor w′_{2} with w′_{2} = w′_{1}; hence H(w_{2}, w′_{2}). Consider now the case where w_{1} = ⟨g, d⟩ for g ∈ G. Let w′_{1} be such that H(w_{1}, w′_{1}). By the definition of H, we have w′_{1} = ⟨l_{1}, r_{1}, val_{1}, d⟩, where l_{1} is the value of the left input to g, r_{1} is the value of the right input to g, and val_{1} is the output of g on x⃗. By the definition of S, the state w_{1} has as successors the two states ⟨T_{l}(g), ↙⟩ and ⟨T_{r}(g), ↘⟩. Consider the state w_{2} = ⟨T_{l}(g), ↙⟩. Let w′_{2} = ⟨l_{2}, r_{2}, val_{2}, ↙⟩ be a successor of w′_{1} for which l_{2} is the value of the left input to T_{l}(g), r_{2} is the value of the right input to T_{l}(g), and val is the output of T_{l}(g) on x⃗. By the definition of S′, such a successor w′_{2} exists. Also, by the definition of H, we have H(w_{2}, w′_{2}). The proof for the state ⟨T_{r}(g), ↘⟩ is similar.

Proof of Theorem 4 □

4 Verification of Fair Transition Systems

In this section, we study the complexity of the fair-containment and the fair-

4-1

simulation problems. We show that both problems are PSPACE-complete, and that the implementation complexity of both problems is significantly lower.

16

4.1 The Fair-Containment Problem

We have seen that the containment problem is PSPACE-complete, and that

4.1-1

its implementation complexity is NLOGSPACE-complete. In this section, we check what happens to the complexity when we augment the transition systems with fairness conditions. We start with some auxiliary results.

Lemma 1 W(n, m) → U(nm).

Proof of Lemma 1 Consider a weakly fair transition system S = ⟨Σ, W, R, W_{0}, L, α⟩, with fairness condition α = {⟨B_{1}, G_{1}⟩, …, ⟨B_{m}, G_{m}⟩}. For every W′ ⊆ W and pair ⟨B_{i}, G_{i}⟩, we have that W′ ∩ (W \ B_{i}) = ∅ implies that W′ ∩ G_{i} ≠ ∅, if and only if W′ ∩ ((W \ B_{i}) ∪ G_{i}) ≠ ∅. Hence, a computation π is fair in S if and only if it is fair in all the unconditionally fair transition systems S_{i} = ⟨Σ, W, R, L, W_{0}, (W \ B_{i}) ∪ G_{i}⟩. The result then follows from the known bound on the size of the product of unconditionally fair transition systems [Cho74].

Proof of Lemma 1 □

Lemma 2 Given a transition system S ∈ U(n) with a state space W and a set B ⊆ W, we can construct a transition system S′ ∈ U(2n) such that a trace ρ is accepted by S′ if and only if there exists a fair computation π in S such that Inf(π) ∩ B = ∅ and L(π) = ρ.

Proof of Lemma 2 The idea, as suggested in [Kur87], is that the transition

Proof of Lemma 2-1

system S′ guesses a position in each of its computations from which no state of B can be visited. For that, it maintains two copies of S. The first copy allows visits in states in B. The second copy does not allow visits in states in B. Each computation starts in the first copy, and should eventually move to the second copy. Formally, for S = ⟨Σ, W, R, L, W_{0}, α⟩, we define S′ = ⟨Σ, W × {1, 2}, R′, L′, W_{0} × {1}, α × {2}⟩, where:

• For every w and w′ in W and i and i′ in {1, 2}, we have that R′(⟨w, i⟩, ⟨w′, i′⟩) if and only if R(w, w′) and either:

– w′ ∉ B and i ≤ i′, or

– w′ ∈ B and i = i′ = 1.

• For every w ∈ W and i ∈ {1, 2}, we have L′(⟨w, i⟩) = L(w). 17 We prove the correctness of our construction. Consider a trace ρ ∈ Σ^{ω},

Proof of Lemma 2-2

and assume there exists a fair computation π = w_{0}, w_{1}, … in S such that Inf (π)∩B = ∅ and L(π) = ρ. Let w_{i} be such that for all j > i, we have w_{j} ∉ B. The computation π′ = ⟨w_{0}, 1⟩, ⟨w_{1}, 1⟩, …, ⟨w_{i}, 1⟩, ⟨w_{i+1}, 2⟩, ⟨w_{i+2}, 2⟩, … is then fair in S′, and ρ is accepted by S′. Assume now that ρ is accepted by S′; thus, there exists a computation π′ = ⟨w_{0}, i_{0}⟩, ⟨w_{1}, i_{1}⟩, … in S′ such that L(π′) = ρ and Inf (π′) ∩ (α × {2}) ≠ ∅. As no transitions from states in W × {2} to states in W × {1} are possible, the computation π′ eventually gets trapped in states in W × {2}. Therefore, as no transitions to states in B ×{2} are possible, the computation π′ visits states in B only finitely often. Finally, as R′(⟨w, i⟩, ⟨w′, i′⟩) only if R(w, w′), the computation π = w_{0}, w_{1}, … exists and is fair in S, and we are done. Note that S′ is not necessarily total. For that, we restrict S′ to states that have at least one R′-successor. Clearly, this does not affect the traces of S′.

Proof of Lemma 2 □

Lemma 3 S(n, m) → U(n2^{O(m)}).

Proof of Lemma 3 Consider a strongly fair transition system S =

Proof of Lemma 3-1

⟨Σ, W, R, L, W_{0}, α⟩ with fairness condition α = {⟨B_{1}, G_{1}⟩, …, ⟨B_{m}, G_{m}⟩}. With every I ⊆ {1, …, m}, we associate an unconditionally fair transition system S_{I} that accepts the traces L(π) of S for which Inf (π) ∩ B_{i} ≠ ∅ and Inf (π) ∩ G_{i} ≠ ∅ for all i ∈ I, and Inf (π) ∩ B_{i} = ∅ for all i ∉ I. For that, we first define a weakly fair transition system S′_{I} = ⟨Σ, W, R, W_{0}, L, α_{I}⟩ that accepts the traces L(π) of S for which Inf (π) ∩ B_{i} ≠ ∅ and Inf (π) ∩ G_{i} ≠ ∅ for all i ∈ I. This is done by defining α_{I} = ⋃_{i∈I}{⟨W, B_{i}⟩, ⟨W, G_{i}⟩}. If S ∈ S(n, m), then S′_{I} ∈ W(n, 2m) and hence, by Lemma 1, we can translate it to S′′_{I} ∈ U(2nm). Let B = ⋃_{i∉I} B_{i}. Clearly, for every computation π of S′′_{I}, we have that Inf (π) ∩ B_{i} = ∅ for all i ∉ I if and only if Inf (π) ∩ B = ∅. Hence, according to Lemma 2, we can construct the transition system S_{I} with 4nm states.

Proof of Lemma 3-2 We prove that T (S) = ⋃_{I⊆{1,2,...,m}} T (S_{I}). A computation π is fair in S if for every pair ⟨B_{i}, G_{i}⟩, either Inf (π) ∩ B_{i} = ∅, or both Inf (π) ∩ B_{i} ≠ ∅ and Inf (π) ∩ G_{i} ≠ ∅. Let f(π) ⊆ {1, …, m} be such that Inf (π) ∩ B_{i} ≠ ∅ if and only if i ∈ f(π). It is easy to see that π is fair in S if and only if π is fair in S_{f(π)}. The lemma now follows from the fact that union is easy for

18 transition systems (e.g., by defining the initial set as union of the initial sets of the underlying systems).

Proof of Lemma 3 □

Theorem 5 The fair-containment problem T (S) ⊆ T (S′) for S ∈ ⋃{U, W, S} and S′ ∈ ⋃{U, W, S} is PSPACE-complete. Proof of Theorem 5 As there are three possible types for the transition

Proof of Theorem 5-1

system S and three possible types for the transition system S′, we have nine containment problems to solve to prove a PSPACE upper bound. We solve them all using the same method:

1. Translate the transition system S to an unconditionally fair transition system S_{U}.

2. Construct an unconditionally fair transition system \overline{S′_{U}} that complements the transition system S′.

3. Check T (S_{U}) ∩ T (\overline{S′_{U}}) for emptiness.

This is how we perform step 1 for the three possible types of S:

Proof of Theorem 5-2

1. U(n) → U(n).

2. W(n, m) → U(nm) [Lemma 1].

3. S(n, m) → U(n2^{O(m)}) [Lemma 3].

This is how we perform step 2 for the three possible types of S′:

Proof of Theorem 5-3

1. \overline{U(n)} → U(2^{O(n log n)}) [Saf88].

2. \overline{W(n, m)} → \overline{U(nm)} → U(2^{O(nm log(nm))}) [Saf88].

3. \overline{S(n, m)} → S(2^{O(nm log(nm))}, nm) → U(2^{O(nm log(nm))}) [Saf92].

For all three types of S, going to S_{U} involves an at-most exponential

Proof of Theorem 5-4

blowup. Similarly, for all three types of S′, going to \overline{S′_{U}} involves an at-most exponential blowup. Thus, the size of the product of S_{U} and \overline{S′_{U}} is exponential in the sizes of S and S′ [Cho74]. By [VW94], the nonemptiness problem for unconditionally fair transition systems is in NLOGSPACE. Hence, as

19

Chicago Journal of Theoretical Computer Science 1998-2 NLOGSPACE = co-NLOGSPACE, checking the product of S_{U} and \overline{S′_{U}} for emptiness can be done in space polynomial in their sizes.

Hardness in PSPACE follows from the PSPACE lower bound for trace

Proof of Theorem 5-5

containment (Theorem 1). Indeed, we can easily define a fairness condition for which all the computations are fair (α = W for unconditional fairness and α = ∅ for weak and strong fairness).

Proof of Theorem 5 □

4.1.1 Implementation Complexity

Recall that our main concern is the complexity in terms of the (much larger)

4.1.1-1

implementation. We now turn to consider the implementation complexity of fair containment.

Theorem 6 The implementation complexity of checking T (S) ⊆ T (S′) for S ∈ ⋃{U, W} and S′ ∈ ⋃{U, W, S} is NLOGSPACE-complete.

Proof of Theorem 6 In the case where S ∈ ⋃{U, W}, the translation of S to S_{U} involves only a polynomial blowup. Thus, in this case, fixing the size of S′, the nondeterministic algorithm described in the proof of Theorem 5, requires space logarithmic in the size of S. Hardness in NLOGSPACE follows from the NLOGSPACE lower bound for the implementation complexity of containment (Theorem 2).

Proof of Theorem 6 □

So, for the case where the implementation does not use the strong fairness

4.1.1-2

condition, our fair-containment algorithm requires space that is only polylogarithmic in the size of the implementation. Clearly, this is not the case when the implementation does use the strong fairness condition. Then, our algorithm requires space that is polynomial in the size of the implementation, and time that is exponential in the size of the implementation. We suggest an alternative algorithm that requires time that is only polynomial in the size of the implementation. The price is larger complexity in terms of the size of the specification. We first need the following lemma.

Lemma 4 For S_{1} ∈ S(n_{1}, m) and S_{2} ∈ U(n_{2}), there exists S ∈ S(n_{1}n_{2}, m + 1) such that T (S) = T (S_{1}) ∩ T (S_{2}).

20 Proof of Lemma 4 Given a strongly fair transition system S_{1} = ⟨Σ, W_{1}, R_{1}, W_{1}^{0}, L_{1}, α⟩ and an unconditionally fair transition system S_{2} = ⟨Σ, W_{2}, R_{2}, W_{2}^{0}, L_{2}, β⟩, consider the strongly fair transition system S = ⟨Σ, W, R, W_{0}, L, γ⟩, where:

• W = {⟨w_{1}, w_{2}⟩: w_{1} ∈ W_{1}, w_{2} ∈ W_{2}, and L_{1}(w_{1}) = L_{2}(w_{2})},

• R(⟨w_{1}, w_{2}⟩, ⟨w′_{1}, w′_{2}⟩) if and only if R_{1}(w_{1}, w′_{1}) and R_{2}(w_{2}, w′_{2}),

• W_{0} = (W_{1}^{0} × W_{2}^{0}) ∩ W,

• for every ⟨w_{1}, w_{2}⟩ ∈ W, we have L(⟨w_{1}, w_{2}⟩) = L_{1}(w_{1}), and

• γ ⊆ 2^{W} × 2^{W} is such that ⟨G, B⟩ ∈ γ if and only if either there exists ⟨G′, B′⟩ ∈ α for which G = (G′ × W_{2}) ∩ W and B = (B′ × W_{2}) ∩ W, or G = W and B = (W_{1} × β) ∩ W.

It is easy to see that S accepts an input trace if and only if both S_{1} and S_{2} accept it, and that its size is as required.

Proof of Lemma 4 □

Theorem 7 The implementation complexity of checking T (S) ⊆ T (S′) for S ∈ S and S′ ∈ ⋃{U, W, S} is in PTIME.

Proof of Theorem 7 Given S and S′, we construct, as in the proof of Theorem 5, the unconditionally fair transition system \overline{S′_{U}}. Unlike the algorithm there, we do not translate the transition system S to an unconditionally fair system. Rather, we check the nonemptiness of T (S)∩T (\overline{S′_{U}}). The nonemptiness problem for strongly fair transition systems can be solved in polynomial time [EL85]. Hence, by Lemma 4, we can check the nonemptiness of the intersection in time polynomial in the size of S.

Proof of Theorem 7 □

Note that the algorithm presented in the proof of Theorem 7 uses time

4.1.1-3

and space exponential in the size of the specification, in contrast to the algorithm in the proof of Theorem 5 that uses space polynomial in the size of the specification. Nevertheless, as S′ is usually much smaller than S, the algorithm in the proof of Theorem 7 may work better in practice. Can we do better and get the NLOGSPACE complexity we have for implementations

21 that use the unconditional or weak fairness conditions? As we now show, the answer to this question is most likely negative. To see this, we first need the following theorem.

Theorem 8 The nonemptiness problem for strongly fair transition systems is PTIME-hard.

Proof of Theorem 8 We do a reduction from propositional anti-Horn sat-

Proof of Theorem 8-1

isfiability (PAHS). Propositional anti-Horn clauses are obtained from propositional Horn clauses by replacing each proposition p with ¬p. Thus, a propositional anti-Horn clause is either of the form p → q_{1} ∨ … ∨ q_{n} (an empty disjunction is equivalent to false) or of the form q_{1} ∨…∨q_{n}. As propositional Horn satisfiability is PTIME-complete [Pla84], then clearly, so is PAHS.

Given an instance I of PAHS, we construct the transition system:

Proof of Theorem 8-2

S_{I} = ⟨{a}, W, W × W, W, L, α⟩

where:

• W = Q×{s}, where Q is the set of all the propositions in I, and s ∉ Q,

• L maps all states to a, and

• α is the strongly fair condition defined as follows:

– for a clause p → q_{1} ∨ … ∨ q_{n} in I, we have ⟨{p}, {q_{1}, …, q_{n}}⟩ in α, and

– for a clause q_{1} ∨ … ∨ q_{n} in I, we have ⟨W, {q_{1}, …, q_{n}}⟩ in α.

Each computation of S_{I} induces an assignment to the propositions in I. A

Proof of Theorem 8-3

proposition is assigned true if and only if the computation visits it infinitely often. In addition, for each assignment to the propositions in I, there exists a computation of S_{I} that induces it (the state s guarantees that the above also holds for the assignment in which all propositions are assigned false). The definition of α thus guarantees that I is satisfiable if and only if S_{I} is nonempty.

Proof of Theorem 8 □

22 We note that the nonemptiness problem for strongly fair transition sys-

4.1.1-4

tems is already PTIME-hard for systems with pairs of a constant size. In 3-PAHS, all the clauses are of the form p → q_{1} ∨ q_{2}, except possibly one clause, which has the form p. It is easy to see that by introducing polynomially many new propositions, every instance I of PAHS can be reduced to an instance I′ of 3-PAHS. Given such I, we can construct a strongly fair transition system in which every pair has at most three states in its two sets. The construction is the same as the one suggested in the proof, only that we handle the clause p by |W | − 1 pairs of the form ⟨{q}, {p}⟩, one for each q ∈ W \ {p}.

Therefore, unlike unconditionally or weakly fair transition systems, for

4.1.1-5

which the nonemptiness problem is NLOGSPACE-complete, testing strongly fair transition systems for nonemptiness is PTIME-complete. Theorems 7 and 8 imply the following theorem.

Theorem 9 The implementation complexity of checking T (S) ⊆ T (S′) for S ∈ S and S′ ∈ ⋃{U, W, S} is PTIME-complete.

4.2 The Fair-Simulation Problem

4.2.1 The Upper Bound

Theorem 10 The fair-simulation problem S ≤ S′ for S ∈ ⋃{U, W, S} and S′ ∈ ⋃{U, W, S} is in PSPACE.

Proof of Theorem 10 Given S = ⟨Σ, W, R, W_{0}, L, α⟩ and S′ =

Proof of Theorem 10-1

⟨Σ, W′, R′, W′_{0}, L′, α′⟩, we show how to check in polynomial space that a candidate relation H is a simulation from S to S′. The claim then follows, since we can enumerate all candidate relations using polynomial space. First, we check (easily) that for every w ∈ W_{0} there exists w′ ∈ W′_{0} such that H(w, w′). We then check (also easily) that for all ⟨w, w′⟩ ∈ H, we have L(w) = L(w′). It is left to check that for all ⟨w, w′⟩ ∈ H, the pair ⟨w, w′⟩ is good in H. To do this, we define, for every ⟨w, w′⟩ ∈ H, two transition systems. The alphabet of both systems is W. The first transition system, A_{w}, accepts all the fair w-computations in S. The second transition system, U_{w′}, accepts all the sequences π in W^{ω} for which there exists a fair w′-computation π′ in S′ such that H(π, π′). Clearly, the pair ⟨w, w′⟩ is good in H if and only if T (A_{w}) ⊆ T (U_{w′}).

23 We define A_{w} and U_{w′} as follows. The transition system A_{w} does nothing

Proof of Theorem 10-2

but trace the w-computations of S, accepting those that satisfy S’s acceptance condition. Formally, A_{w} = ⟨W, W, R, {w}, L′′, α⟩, where for all u ∈ W, we have L′′(u) = u.

The transition system U_{w′} has members of H as its set of states. Thus,

Proof of Theorem 10-3

each state has two elements. The second element of each state in U_{w′} is a state in W′, and according to R′, it induces the transitions. The first element in each state of U_{w′} is a state in W, and it induces the labeling. This combination guarantees that a computation π′′ ∈ H^{ω}, whose W′ elements form the computation π′ ∈ (W′)^{ω} and whose states are labeled with π ∈ W^{ω}, satisfies H(π, π′). Formally, U_{w′} = ⟨W, H, R′′, W′′_{0}, L′′′, α′′⟩, where:

• R′′ is adjusted to the new state space; i.e., R′′(⟨t, t′⟩, ⟨q, q′⟩) if and only if R′(t′, q′),

• W′′_{0} = (W × {w′}) ∩ H,

• for every ⟨t, t′⟩ ∈ H, we have L′′′(⟨t, t′⟩) = t, and

• α′′ is also adjusted to the new state space; i.e., each set B ⊆ W′ in α′ is replaced by the set (W × B) ∩ H in α′′.

Note that R′′ is not necessarily total. For that, we restrict U_{w′} to states that have at least one R′′ successor. Clearly, this does not affect the traces of U_{w′}.

According to Theorem 5, checking that T (A_{w}) ⊆ T (U_{w′}) can be done in

Proof of Theorem 10-4

space polynomial in the sizes of A_{w} and U_{w′}, thus polynomial in the sizes of S and S′.

Proof of Theorem 10 □

We note that our algorithm can be easily adjusted to check S and S′ for

Proof of Theorem 10-5

fair bisimulation.

4.2.2 The Lower Bound

For a transition system S = ⟨Σ, W, R, W_{0}, L, α⟩, we say that S is universal

4.2.2-1

if and only if T (S) = Σ^{ω}. The universality problem is to determine whether a given transition system is universal. As we have already mentioned in the proof of Theorem 1, Mayer and Stockmayer prove a PSPACE lower bound for the problem of determining whether a finite-acceptance transition system

24 S is universal [MS72]. Our PSPACE lower bound for the fair-simulation problem follows the lines of their proofs, and we first give its details, which are easily adjusted to infinite traces.

Theorem 11 The universality problem, L(S) = Σ^{ω} for S ∈ ⋃{U, W, S}, is PSPACE-hard.

Proof of Theorem 11 We do a reduction from polynomial-space Turing

Proof of Theorem 11-1

machines. Given a Turing machine T of space complexity s(n), we construct a transition system S_{T} of size linear in T, and s(n) such that S_{T} is universal if and only if T does not accept the empty tape. We assume, without loss of generality, that once T reaches a final state, it loops there forever. The system S_{T} accepts a trace w if and only if w is not an encoding of a legal computation of T over the empty tape, or if w is an encoding of a legal yet rejecting computation of T over the empty tape. Thus, S_{T} rejects a trace w if and only if it encodes a legal and accepting computation of T over the empty tape. Hence S_{T} is universal if and only if T does not accept the empty tape.

We now give the details of the construction of S_{T}. Let T =

Proof of Theorem 11-2

⟨Γ, Q, →, q_{0}, F ⟩, where Γ is the alphabet, Q is the set of states, →⊆ Q×Γ×Q×Γ×{L, R} is the transition relation (we use (q, a) → (q′, b, Δ) to indicate that when T is in state q and it reads the input a in the current tape cell, it moves to state q′, writes b in the current tape cell, and its reading head moves one cell to the left/right, according to Δ), q_{0} is the initial state, and F ⊆ Q is the set of accepting states. We encode a configuration of T by a string #γ_{1}γ_{2} … (q, γ_{i}) … γ_{s(n)}. That is, a configuration starts with #, and all its other letters are in Γ, except for one letter in Q × Γ. The meaning of such a configuration is that the j^{th} cell in T, for 1 ≤ j ≤ s(n), is labeled γ_{j}, the reading head points at cell i, and T is in state q. For example, the initial configuration of T is #(q_{0}, b)b … b (with s(n) − 1 occurrences of bs) where b stands for an empty cell. We can then encode a computation of T by a sequence of configurations.

Proof of Theorem 11-3 Let Σ = {#} ∪ Γ ∪ (Q × Γ) and let #σ_{1} … σ_{s(n)}#σ′_{1} … σ′_{s(n)} be two successive configurations of T. We also set σ_{0}, σ′_{0}, and σ_{s(n)+1} to #. For each triple ⟨σ_{i−1}, σ_{i}, σ_{i+1}⟩ with 1 ≤ i ≤ s(n), we know by the transition relation of T what σ′_{i} should be. In addition, the letter # should repeat exactly every s(n)+1 letters. Let next(⟨σ_{i−1}, σ_{i}, σ_{i+1}⟩) denote our expectation for σ′_{i}. That is:

25 • Next(⟨γ_{i−1}, γ_{i}, γ_{i+1}⟩) = next(⟨#, γ_{i}, γ_{i+1}⟩) = next(⟨γ_{i−1}, γ_{i}, #⟩) = γ_{i}.

• Next(⟨(q, γ_{i−1}), γ_{i}, γ_{i+1}⟩) = next(⟨(q, γ_{i−1}), γ_{i}, #⟩) =

\{ \begin{matrix}γ_{i} & if (q, γ_{i−1}) → (q′, γ′_{i−1}, L) \\ (q′, γ_{i}) & if (q, γ_{i−1}) → (q′, γ′_{i−1}, R) \end{matrix}

• Next(⟨γ_{i−1}, (q, γ_{i}), γ_{i+1}⟩) = next(⟨#, (q, γ_{i}), γ_{i+1}⟩) = next(⟨γ_{i−1}, (q, γ_{i}), #⟩) = γ′_{i} where (q, γ_{i}) → (q′, γ′_{i}, Δ).^{3}

• Next(⟨γ_{i−1}, γ_{i}, (q, γ_{i+1})⟩) = next(⟨#, γ_{i}, (q, γ_{i+1})⟩) =

\{ \begin{matrix}γ_{i} & if (q, γ_{i+1}) → (q′, γ′_{i+1}, R) \\ (q′, γ_{i}) & if (q, γ_{i+1}) → (q′, γ′_{i}, L) \end{matrix}

• Next(⟨σ_{s(n)}, #, σ′_{1}⟩) = #.

Consistency with next gives us a necessary condition for a trace to encode a legal computation. In addition, the computation should start with the initial configuration.

To check consistency with next, S_{T} can use its nondeterminism and

Proof of Theorem 11-4

guess when there is a violation of next. Thus, S_{T} guesses ⟨σ_{i−1}, σ_{i}, σ_{i+1}⟩ ∈ Σ^{3}, guesses a position in the trace, checks whether the three letters to be read starting this position are σ_{i−1}, σ_{i}, and σ_{i+1}, and checks whether next(⟨σ_{i−1}, σ_{i}, σ_{i+1}⟩) is not the letter to come s(n) + 1 letters later. Once S_{T} sees such a violation, it goes to an accepting sink. To check that the first configuration is not the initial configuration, S_{T} simply compares the first s(n) + 1 letters with #(q_{0}, b)b … b. Finally, checking whether a legal computation is rejecting is also easy; the final configuration has to be rejecting (one with q ∉ F).

Proof of Theorem 11 □

We would like to do a similar reduction to prove that the fair-simulation

4.2.2-2

problem is PSPACE-hard. For every alphabet Σ, let S_{Σ} be the transition system ⟨Σ, Σ, Σ × Σ, Σ, L_{Σ}, α⟩, where L_{Σ}(σ) = σ and α is such that all the

26 computations of S_{Σ} are fair. That is, S_{Σ} is a universal transition system in which each state is associated with a letter σ ∈ Σ and T (S_{Σ}^{σ}) = σ · Σ^{ω}. For example, S_{{a,b}} is the transition system S in Figure 1. It is easy to see that a transition system S over Σ is universal if and only if T (S_{Σ}) ⊆ T (S). It is not true, however, that S is universal if and only if S_{Σ} ≤ S. For example, the transition system S′ in Figure 1 is universal, yet S_{{a,b}} ≰ S′. Our reduction overcomes this difficulty by defining S_{T} in such a way that if S_{T} is universal, then for each of its states w, we have T (S_{T}^{w}) = L(w) · Σ^{ω}. For such S_{T}, we do have that S_{T} is universal if and only if S_{Σ} ≤ S_{T}. Indeed, a relation that maps a state σ of S_{Σ} to all the states of S_{T} that are labeled with σ is a fair simulation.

3We assume that the reading head of T does not “fall” from the right or the left boundaries of the tape. Thus, the case where (i = 1) and (q, γ_{i}) → (q′, γ′_{i}, L) and the dual case where (i = 2^{n}) and (q, γ_{i}) → (q′, γ′_{i}, R) are not possible.

Theorem 12 The fair-simulation problem S ≤ S′ for S ∈ ⋃{U, W, S} and S′ ∈ ⋃{U, W, S} is PSPACE-hard.

Proof of Theorem 12 We prove hardness for the case where S′ is a

Proof of Theorem 12-1

strongly fair transition system with three pairs. The other cases then follow from the linear translation of S′ to any S′ ∈ ⋃{U, W, S}. As in the previous proof, we do a reduction from polynomial space Turing machines. Given the Turing machine T, let T′ be as follows. Whenever T reaches an accepting configuration, T′ “cleans” the tape and starts from the beginning (i.e., empty tape and initial state at the left end of the tape). Thus, T accepts the empty tape if and only if T′ has an infinite computation, in which case it visits the initial configuration infinitely often.

We now define a strongly fair transition system S_{T} as the union of two

Proof of Theorem 12-2

strongly fair transition systems, S_{T}^{1} and S_{T}^{2} , with the following behaviors. Reading a trace ρ, the fair transition system S_{T}^{1} checks for a violation of the transition relation of T′ in ρ (by guessing a violation of next). If S_{T}^{1} sees a violation, it goes to an accepting sink. Therefore, the acceptance condition of S_{T}^{1} is a single pair ⟨W_{1}, G⟩, where W_{1} is the set of states in S_{T}^{1} and G is a clique of |Σ| states, each labeled with a different letter, which S_{T}^{1} enters once it sees a violation of next. Reading a trace ρ, the fair transition system S_{T}^{2} checks for the occurrence of the initial configuration in ρ. Because the initial configuration starts with # and has no other # in it, it is easy to check its occurrence. If S_{T}^{2} sees the initial configuration, it goes to a rejecting sink. The acceptance condition of S_{T}^{2} is therefore a single pair ⟨B, ∅⟩, where B is a clique of |Σ| states, each labeled with a different letter, which S_{T}^{2} enters once it sees an occurrence of the initial configuration. Assuming the state spaces

27 of S_{T}^{1} and S_{T}^{2} are disjoint, the fair transition system S_{T} simply has one copy of S_{T}^{1} , and one copy of S_{T}^{2} ; its initial set is the union of the initial sets of S_{T}^{1} and S_{T}^{2} ; and its fairness condition has the two pairs ⟨W_{1}, G⟩ and ⟨B, ∅⟩.

It follows that the fair transition system S_{T} accepts a trace ρ if ρ violates

Proof of Theorem 12-3

next or never visits the initial configuration. Thus, S_{T} does not accept a trace ρ if and only if ρ does not violate next and it visits the initial configuration of T. Therefore, S_{T} is universal if and only if T does not accept the empty tape. Indeed, in both cases there exists no accepting computation of T on the empty tape.

We want, however, more than a universality test. We want to define S_{T}

Proof of Theorem 12-4

in such a way that if it is indeed universal, then for each of its states w, we have T (S_{T}^{w}) = L(w) · Σ^{ω}. Let S_{T} = ⟨Σ, W, R, W_{0}, L, α⟩. We assume that R ∩ (W × W_{0}) = ∅. Thus, no computation of S_{T} visits states from W_{0} more than once (this can be easily achieved by duplicating states in W_{0} that are visited more than once). We define the transition system S′_{T} by adding to S_{T} the transitions from all states to all of the initial states, with the requirement that these transitions can be used only finitely often. Accordingly, S′_{T} = ⟨Σ, W, R ∪ (W × W_{0}), W_{0}, L, α ∪ ⟨W_{0}, ∅⟩⟩. We claim the following:

Claim 1 S′_{T} is universal if and only if for each σ ∈ Σ we have w_{0} ∈ W_{0} with L(w_{0}) = σ, and for each w ∈ W, we have T (S_{T}^{w}) = L(w) · Σ^{ω}.

Claim 2 S_{T} is universal if and only if S′_{T} is universal.

Claim 1 is immediate, and we prove here Claim 2. Clearly, every com-

Proof of Theorem 12-5

putation π of S_{T} is a computation in S′_{T}. Since no computation in S_{T} visits W_{0} more than once, adding the pair ⟨W_{0}, ∅⟩ to the acceptance condition α, we still have that if π is fair in S_{T}, then it is also fair in S′_{T}. Hence T (S_{T}) ⊆ T (S′_{T}); thus, if S_{T} is universal, so is S′_{T}. Assume now that S_{T} is not universal. Consider a trace ρ not accepted by S_{T}. Recall that ρ does not violate next, and it visits the initial configuration of T. In other words, ρ is of the form yx where y is a prefix not violating next and x is an infinite computation of T′ (the initial configuration of T is the first configuration in x). An infinite computation of T′ visits the initial configuration infinitely often. Therefore, all the suffixes of ρ are of that special form! Hence, if ρ is not accepted by S_{T}, all its suffixes are also not accepted by S_{T}. We show that this implies that ρ is not accepted by S′_{T} too. Assume, by way of contradiction, that ρ is accepted by S′_{T}. Let π = w_{0}, w_{1}, … by a fair computation

28 in S′_{T}, with L(π) = ρ. By the acceptance condition of S′_{T}, there exists i ≥ 0 such that w_{i} ∈ W_{0}, and for all j > i, we have W_{j} ∉ W_{0}. Hence, for all j ≥ i, we have R(w_{j}, w_{j+1}). Therefore, the computation π^{i} = w_{i}, w_{i+1}, … is a fair computation in S_{T}, and the trace L(π^{i}) is accepted by S_{T}, contradicting the fact it is a suffix of a trace not accepted by S_{T}.

As discussed above, Claims 1 and 2 now imply that S_{Σ} ≤ S′_{T} if and only

Proof of Theorem 12-6

if S_{T} is universal; thus S_{Σ} ≤ S′_{T} if and only if T does not accept the empty tape. Because the fairness condition of S_{Σ} can be specified in terms of either unconditional, weak, or strong fairness, we are done.

Proof of Theorem 12 □

Theorems 10 and 12 together imply the following.

4.2.2-3

Theorem 13 The fair-simulation problem S ≤ S′ for S ∈ ⋃{U, W, S} and S′ ∈ ⋃{U, W, S} is PSPACE-complete.

4.2.3 Implementation Complexity

As our discussions thus far show, fair simulation and fair containment have

4.2.3-1

the same complexity. In Theorem 14, we show that when we consider the implementation complexity of fair simulation, the picture is different. Here, checking implementations that use the unconditional or weak fairness conditions is not easier than checking implementations that use the strong fairness condition; hence fair simulation is most likely harder than fair containment, and the trace-based approach is more efficient.

Theorem 14 The implementation complexity of checking S ≤ S′ for S ∈ ⋃{U, W, S} and S′ ∈ ⋃{U, W, S} is PTIME-complete.

Proof of Theorem 14 We start with the upper bound. Consider the algo-

Proof of Theorem 14-1

rithm presented in the proof of Theorem 10. It checks whether a candidate relation H is a simulation. Once we fix S′, then, by Theorems 6 and 9, the complexity of checking each pair in the candidate relation is NLOGSPACE for S ∈ ⋃{U, W}, and is PTIME for S ∈ S. Once we fix S′, the number of pairs in each candidate relation is linear in the size of S. Thus, fixing S′, the problem of checking a candidate relation H is in PTIME. Instead of guessing a relation H and checking it, we do a fixed-point computation as follows [Mil90]. Let

H_{0} = {⟨w, w′⟩ : w ∈ W, w′ ∈ W′, and L(w) = L(w′)}

29 Thus, H_{0} is the maximal relation that satisfies condition 1 of fair simulation. Consider the monotonic function f : 2^{W ×W′} → 2^{W ×W′}, where

f(H) = H ∩ {⟨w, w′⟩ : ⟨w, w′⟩ is good in H}

Thus, f(H) contains all the pairs in H that are good with respect to the relation H. Let H^{⋆} be the greatest fixed point of f when restricted to pairs in H_{0}. That is, H^{⋆} = νz.H_{0} ∩ f(z).

We now prove that S ≤ S′ if and only if for every w ∈ W_{0}, we have

Proof of Theorem 14-2

({w}×W′_{0}) ∩ H^{⋆} ≠ ∅. First, as H^{⋆} is a fair-simulation relation, the direction from right to left is immediate from the definition of fair simulation. Assume that S ≤ S′. Then, there exists a fair-simulation relation H′ such that for every w ∈ W_{0}, we have ({w} × W′_{0}) ∩ H′ ≠ ∅. Let H_{i} = f^{i}(H_{0}). We show that for every i ≥ 0 we have H′ ⊆ H_{i}. Thus, in particular, H′ ⊆ H^{⋆}, and we are done. The proof proceeds by induction on i. First, since H′ satisfies condition 2 of fair-simulation relations, then clearly H′ ⊆ H_{0}. Assume that H′ ⊆ H_{i}, and assume by way of contradiction that H′ ⊈ H_{i+1}. Then there exists ⟨w, w′⟩ ∈ H′ \ H_{i+1}. Since H′ ⊆ H_{i}, it follows that the pair ⟨w, w′⟩ is not good in H_{i}, which implies, again by the containment of H′ in H_{i}, that it is also not good in H′. Then, however, H′ does not satisfy condition 3 of fair simulation, and we reach a contradiction.

We now consider the complexity of calculating H^{⋆}. Since W × W′ is

Proof of Theorem 14-3

finite, we can calculate H iteratively, starting with H_{0} until we reach a fixed point. Because f is monotonic, we must iterate it at most polynomially many times. Hence, out of the 2^{|W ×W′|} candidate relations for simulation, we actually check at most |W × W′| relations. Recall that if S′ is fixed, the problem of checking a candidate relation is in PTIME. Also, if S′ is fixed, we have only linearly many candidate relations to check. The problem is therefore in PTIME.

Hardness in PTIME follows from the lower bound in Theorem 4.

Proof of Theorem 14-4

Proof of Theorem 14 □

5 Discussion

We have examined the trace-based and the tree-based approaches to imple-

5-1

mentation from a complexity-theoretic point of view. Our results show that when we model the specification and the implementation by fair transition

30 systems, the complexity of checking the correctness of a trace-based implementation coincides with that of checking the correctness of a tree-based implementation. Furthermore, when we consider the implementation complexity, then checking implementations that use the unconditional or weak fairness condition is easier in the trace-based approach. Overall, it seems that the trace-based approach is advantageous.

It is interesting to compare our results with the known complexities of

5-2

LTL and ∀CTL^{⋆} model checking. Trace-based implementations are part of the linear-time paradigm, and correspond to LTL model checking. Tree-based implementations are part of the branching-time paradigm, and correspond to ∀CTL^{⋆} model checking. All four problems are PSPACE-complete [SC85, EL85]. The model-checking algorithm of ∀CTL^{⋆} uses as a subroutine the model-checking algorithm of LTL [EL85]. In a similar manner, our fairsimulation algorithm uses as a subroutine the fair-containment algorithm. Clearly, the implementation dichotomy and the temporal-logic dichotomy have a lot in common. When we turn to consider the program complexity of model checking, which is the analog to our implementation complexity, this is no longer true. The program complexity of model checking for both LTL and ∀CTL^{⋆} is NLOGSPACE-complete [VW86, BVW94]. In contrast, we see here that implementation is easier in the trace-based approach.

Our results are summarized in Table 1. All the complexities in the table

5-3

denote tight bounds.

Implementation  Implementation
Complexity  Complexity
Fair  of Fair  Fair  of Fair
Containment Containment  Simulation  Simulation
S and S′ with  PSPACE  NLOGSPACE PTIME  PTIME
No Fairness  [Theorem 1] [Theorem 2]  [Theorem 3] [Theorem 4]
S ∈ ⋃{U, W} and PSPACE  NLOGSPACE PSPACE  PTIME
S′ ∈ ⋃{U, W, S} [Theorem 5] [Theorem 6]  [Theorem 13] [Theorem 14]
S ∈ S and PSPACE PTIME PSPACE PTIME
S′ ∈ ⋃{U, W, S} [Theorem 5] [Theorem 9]  [Theorem 13] [Theorem 14]

Table 1: Is S a correct implementation of S′?

Kupferman and Vardi Verification of Systems

31 Acknowledgment of support: Part of this work was done in Bell Laboratories during the DIMACS Special Year on Logic and Algorithms.

Orna Kupferman’s work was supported in part by the Office of Naval Research Young Investigator Award N00014-95-1-0520, by the National Science Foundation CAREER Award CCR-9501708, by the National Science Foundation grant CCR-9504469, by the Air Force Office of Scientific Research contract F49620-93-1-0056, by the Army Research Office MURI grant DAAH-04-96-1-0341, by the Advanced Research Projects Agency grant NAG2-892, and by the Semiconductor Research Corporation contract 95-DC-324.036.

Moshe Y. Vardi’s work was supported in part by the National Science Foundation grants CCR-9628400 and CCR-9700061, and by a grant from the Intel Corporation.

References

[AL91] M. Abadi and L. Lamport. The existence of refinement mappings. Theoretical Computer Science, 82(2):253–284, 1991.

[ASB^{+}94] A. Aziz, V. Singhal, F. Balarin, R. Brayton, and A. L. Sangiovanni-Vincentelli. Equivalences for fair Kripke structures. In Proceedings of the 21st International Colloquium on Automata, Languages and Programming, Jerusalem, Israel, July 1994.

[AV95] H. R. Andersen and B. Vergauwen. Efficient checking of behavioural relations and modal assertions using fixed-point inversion. In Computer Aided Verification, Proceedings of the 7th International Conference, volume 939 of Lecture Notes in Computer Science, pages 142–154, Berlin, July 1995. Springer-Verlag.

[BBLS92] S. Bensalem, A. Bouajjani, C. Loiseaux, and J. Sifakis. Property preserving simulations. In Proceedings of the 4th Conference on Computer Aided Verification, volume 663 of Lecture Notes in Computer Science, pages 260–273, Berlin, June 1992. Springer-Verlag.

[BCG88] M. C. Browne, E. M. Clarke, and O. Grumberg. Characterizing finite Kripke structures in propositional temporal logic. Theoretical Computer Science, 59:115–131, 1988.

32 [BGS92] J. Balcazar, J. Gabarro, and M. Santha. Deciding bisimilarity is

P-complete. Formal Aspects of Computing, 4(6):638–648, 1992.

[BVW94] O. Bernholtz, M. Y. Vardi, and P. Wolper. An automata-theoretic approach to branching-time model checking. In D. L. Dill, editor, Computer Aided Verification, Proceedings of the 6th International Conference, volume 818 of Lecture Notes in Computer Science, pages 142–155, Berlin, June 1994. Springer-Verlag.

[CD88] E. M. Clarke and I. A. Draghicescu. Expressibility results for linear-time and branching-time logics. In Proceedings of the Workshop on Linear Time, Branching Time, and Partial Order in Logics and Models for Concurrency, volume 354 of Lecture Notes in Computer Science, pages 428–437, Berlin, 1988. Springer-Verlag.

[CDK93] E. M. Clarke, I. A. Draghicescu, and R. P. Kurshan. A unified approach for showing language containment and equivalence between various types of ω-automata. Information Processing Letters, 46:301–308, 1993.

[CES86] E. M. Clarke, E. A. Emerson, and A. P. Sistla. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems, 8(2):244–263, January 1986.

[Cho74] Y. Choueka. Theories of automata on ω-tapes: A simplified approach. Journal of Computer and System Sciences, 8:117–141, 1974.

[EL85] E. A. Emerson and C.-L. Lei. Temporal model checking under generalized fairness constraints. In Proceedings of the 18th Hawaii International Conference on System Sciences, North Hollywood, CA, 1985. Western Periodicals Company.

[EL87] E. A. Emerson and C.-L. Lei. Modalities for model checking: Branching time logic strikes back. Science of Computer Programming, 8:275–306, 1987.

[Eme90] E. A. Emerson. Temporal and modal logic. Handbook of Theoretical Computer Science, pages 997–1072, 1990.

33 [GHR95] R. Greenlaw, H. J. Hoover, and W. L. Ruzzo. Limits of Parallel

Computation. Oxford University Press, 1995.

[GJ79] M. Garey and D. S. Johnson. Computers and Intractability: A Guide to the Theory of NP-Completeness. W. Freeman and Co., San Francisco, 1979.

[GL94] O. Grumberg and D. E. Long. Model checking and modular verification. ACM Transactions on Programming Languages and Systems, 16(3):843–871, 1994.

[Gol77] L. M. Goldschlager. The monotone and planar circuit value problems are log space complete for P. SIGACT News, 9(2):25–29, 1977.

[Hen85] M. Hennessy. Algebraic Theory of Processes. Cambridge, MA, 1985. MIT Press.

[HHK95] M. R. Henzinger, T. A. Henzinger, and P. W. Kopke. Computing simulations on finite and infinite graphs. In Proceedings of the 36th Symposium on Foundations of Computer Science, pages 453–462, Los Alamitos, CA, 1995. IEEE Computer Society Press.

[Imm88] N. Immerman. Nondeterministic space is closed under complement. SIAM Journal on Computing, 17:935–938, 1988.

[Jon75] N. D. Jones. Space-bounded reducibility among combinatorial problems. Journal of Computer and System Sciences, 11:68–75, 1975.

[Kel76] R. M. Keller. Formal verification of parallel programs. Communications of the ACM, 19:371–384, 1976.

[Kur87] R. P. Kurshan. Complementing deterministic Büchi automata in polynomial time. Journal of Computer and System Science, 35:59–71, 1987.

[Kur94] R. P. Kurshan. Computer Aided Verification of Coordinating Processes. Princeton, NJ, 1994. Princeton University Press.

34 [LP85] O. Lichtenstein and A. Pnueli. Checking that finite state con-

current programs satisfy their linear specification. In Proceedings of the 12th ACM Symposium on Principles of Programming Languages, pages 97–107, New York, January 1985. ACM.

[LPS81] D. Lehman, A. Pnueli, and J. Stavi. Impartiality, justice, and fairness—the ethics of concurrent termination. In Proceedings of the 8th Colloquium on Automata, Programming, and Languages (ICALP), volume 115 of Lecture Notes in Computer Science, pages 264–277, Berlin, July 1981. Springer-Verlag.

[LS84] S. S. Lam and A. U. Shankar. Protocol verification via projection. IEEE Transactions on Software Engineering, 10:325–342, 1984.

[LT87] N. A. Lynch and M. R. Tuttle. Hierarchical correctness proofs for distributed algorithms. In Proceedings of the 6th ACM Symposium on Principles of Distributed Computing, pages 137–151, New York, 1987. ACM.

[Mil71] R. Milner. An algebraic definition of simulation between programs. In Proceedings of the 2nd International Joint Conference on Artificial Intelligence, pages 481–489, London, September 1971. British Computer Society.

[Mil80] R. Milner. A Calculus of Communicating Systems, volume 92 of Lecture Notes in Computer Science. Berlin, 1980. Springer-Verlag.

[Mil89] R. Milner. Communication and Concurrency. Englewood Cliffs, NJ, 1989. Prentice-Hall.

[Mil90] R. Milner. Operational and algebraic semantics of concurrent processes. Handbook of Theoretical Computer Science, pages 1201– 1242, 1990.

[MP92] Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems: Specification. Berlin, January 1992. Springer-Verlag.

[MS72] A. R. Meyer and L. J. Stockmeyer. The equivalence problem for regular expressions with squaring requires exponential time. In

35 Proceedings of the 13th IEEE Symposium on Switching and Automata Theory, pages 125–129, New York, 1972. IEEE Computer Group.

[Pla84] D. A. Plaisted. Complete problems in the first-order predicate calculus. Journal of Computer and System Sciences, 29(1):8–35, 1984.

[Pnu85] A. Pnueli. Linear and branching structures in the semantics and logics of reactive systems. In Proceedings of the 12th International Colloquium on Automata, Languages and Programming, Lecture Notes in Computer Science, pages 15–32, Berlin, 1985. Springer-Verlag.

[Saf88] S. Safra. On the complexity of ω-automata. In Proceedings of the 29th IEEE Symposium on Foundations of Computer Science, pages 319–327, Los Alamitos, CA, October 1988. IEEE Computer Society Press.

[Saf92] S. Safra. Exponential determinization for ω-automata with strongfairness acceptance condition. In Proceedings of the 24th ACM Symposium on Theory of Computing, New York, May 1992. ACM.

[SC85] A. P. Sistla and E. M. Clarke. The complexity of propositional linear temporal logic. Journal of the ACM, 32:733–749, 1985.

[SVW87] A. P. Sistla, M. Y. Vardi, and P. Wolper. The complementation problem for Büchi automata with applications to temporal logic. Theoretical Computer Science, 49:217–237, 1987.

[Sze88] R. Szelepcsinyi. The method of forced enumeration for nondeterministic automata. Acta Informatica, 26:279–284, 1988.

[Tho90] W. Thomas. Automata on infinite objects. Handbook of Theoretical Computer Science, pages 165–191, 1990.

[VW86] M. Y. Vardi and P. Wolper. An automata-theoretic approach to automatic program verification. In Proceedings of the First Symposium on Logic in Computer Science, pages 322–331, Los Alamitos, CA, June 1986. IEEE Computer Society Press.

36 [VW94] M. Y. Vardi and P. Wolper. Reasoning about infinite compu-

tations. Information and Computation, 115(1):1–37, November 1994.

37