% The Chicago Journal of Theoretical Computer Science, Volume 1998, Article 2 % Published by MIT Press, Cambridge, Massachusetts USA % Copyright 1998 by Massachusetts Institute of Technology % \newtoks\rstyle \rstyle={cjlook} % \documentclass[v1.1,published]{cjstruct} % % Local style resources for this article. % \usestyleresource{amstext} \usestyleresource{eepic} % % Local macro definitions for this article. % \catcode`\@=11 \ifx\nopagebreakbeginpar\undeftex \newcommand{\nopagebreakbeginpar}{\@beginparpenalty10000} \fi \ifx\nopagebreakendpar\undeftex \newcommand{\nopagebreakendpar}{\@endparpenalty10000} \fi \ifx\nopagebreakinteritem\undeftex \newcommand{\nopagebreakinteritem}{\@itempenalty10000} \fi \catcode`\@=12 % \newcommand{\prooffontshape}{\fontshape{n}\selectfont} % \newcommand{\setof}[2]{\left\{\,#1:#2\,\right\}} \newcommand{\goto}{\rightarrow} \newcommand{\actlsr}{\(\forall\)CTL\(^\star\) } \newcommand{\zug}[1]{\mbox {\(\langle #1 \rangle \)}} \newcommand{\stam}[1]{} \newcommand{\bft}{\mbox{\emph{\textbf{true}}}} \newcommand{\bff}{\mbox{\emph{\textbf{false}}}} \def\squarebox#1{\hbox to #1{\hfill\vbox to #1{\vfill}}} \def\registered{\({}^{\ooalign% {\hfil\raise.07ex\hbox{{\tiny\textup{R}}}% \hfil\crcr\scriptsize\mathhexbox20D\cr}}\)} % % end of local macro definitions for this article % \begin{document} % \begin{articleinfo} % \publisher{The MIT Press} % \publishercomment{% {\Large \begin{center} Volume 1998, Article 2\\ \textit{16 March 1998} \end{center} } \par\noindent ISSN 1073--0486\@. MIT Press Journals, Five Cambridge Center, Cambridge, MA 02142-1493 USA; (617)253-2889; \emph{journals-orders@mit.edu, journals-info@mit.edu}\@. Published one article at a time in \LaTeX\ source form on the Internet\@. Pagination varies from copy to copy\@. For more information and other articles see: \begin{itemize} \item \emph{http://mitpress.mit.edu/CJTCS/} \item \emph{http://www.cs.uchicago.edu/publications/cjtcs/} \item \emph{ftp://mitpress.mit.edu/pub/CJTCS} \item \emph{ftp://cs.uchicago.edu/pub/publications/cjtcs} \end{itemize} \sentence \par\noindent The \emph{Chicago Journal of Theoretical Computer Science} is abstracted or indexed in \emph{Research Alert,\registered SciSearch,\registered Current Contents\registered/Engineering Computing \& Technology}, and \emph{CompuMath Citation Index\@.\registered} } % \copyrightstmt{% \copyright 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; \emph{journals-rights@mit.edu}\@.\pagebreak[2] } % \journal{Chicago\nolinebreak[1] Journal of Theoretical Computer\nolinebreak[1] Science} \journalcomment{% The \emph{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\@. \par \begin{trivlist} \item[\emph{Editor in chief:}] Janos Simon \item[\emph{Consulting editors:}] Joseph Halpern, Stuart A.\ Kurtz, Raimund Seidel \item[\emph{Editors:}] \begin{tabular}[t]{lll} 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\'o 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 \end{tabular} \vspace{1ex} \item[\emph{Managing editor:}] Michael J.\ O'Donnell \vspace{1ex} \item[\emph{Electronic mail:}] \emph{chicago-journal@cs.uchicago.edu} \end{trivlist} \sentence } % \bannerfile{cjtcs-banner.tex} % \volume{1998} % \articleid{2} % \selfcitation{ @article{cj98-02, author={Orna Kupferman and Moshe Y. Vardi}, title={Verification of Fair Transition Systems}, journal={Chicago Journal of Theoretical Computer Science}, volume={1998}, number={2}, publisher={MIT Press}, month={March}, year={1998} } } % \begin{retrievalinfo} \end{retrievalinfo} % \title{Verification of Fair Transition Systems} \shorttitle{Verification of Systems} % \begin{authorinfo} % % Correction to error in cjstruct.sty version 1.1. % \def\fixversion{1.1} \ifx\cjversion\fixversion \renewcommand{\printname}[1]{ \global\authorstring={#1} \global\authorstrue \ifinfo\item Printed name: #1\fi } \fi % % End of correction. % \printname{Orna Kupferman} \collname{}{Kupferman, Orna} \begin{institutioninfo} \instname{University of California at Berkeley} \department{Department of EECS} \address{}{Berkeley}{CA}{94720-1770}{U.S.A} \end{institutioninfo} \email{orna@eecs.berkeley.edu} % \url{http://www-cad.eecs.berkeley.edu/\(^\sim\)orna} \end{authorinfo} \begin{authorinfo} \printname{Moshe Y. Vardi} \collname{}{Vardi, Moshe Y.} \begin{institutioninfo} \instname{Rice University} \department{Department of Computer Science} \address{}{Houston}{TX}{77005-1892}{U.S.A.} \end{institutioninfo} \email{vardi@cs.rice.edu} % \url{http://www.cs.rice.edu/\(^\sim\)vardi} \end{authorinfo} % \shortauthors{Kupferman and Vardi} % \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. } % \begin{editinfo} \submitted{11}{02}{1997}\reported{22}{08}{l997} \submitted{28}{08}{1997}\reported{28}{10}{l997} \submitted{18}{11}{1997}\reported{24}{11}{l997} \submitted{26}{11}{1997}\reported{26}{11}{l997}\published{16}{03}{1998} \end{editinfo} % \end{articleinfo} % \begin{articletext} \tolerance=9000 \begin{abstract} \apar{Abstract-1} In program verification, we check that an implementation meets 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\@. % \apar{Abstract-2} In this work, we examine the trace-based and the tree-based approaches 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 PSPACE-complete, 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\@. \end{abstract} \asection{1}{Introduction} % \apar{1-1} In \emph{program verification\/}, we check that an {\em implementation\/} meets its \emph{specification\/}\@. 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 \cite{cj98-02-01}\@. 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 \emph{hierarchical refinement\/} for this methodology \cite{cj98-02-28,cj98-02-29,cj98-02-25}\@. % \apar{1-2} We distinguish between two approaches to implementation of specifications\@. The first approach is \emph{trace-based implementation}, where we require every computation of the implementation to correlate to some computation of the specification\@. The second approach is \emph{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 \cite{cj98-02-20,cj98-02-32,cj98-02-01}\@. 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)\@. % \apar{1-3} The tree-based approach is stronger in the following sense\@. If \({\cal I}\) is a correct tree-based implementation of the specification \({\cal S}\), then \({\cal I}\) is also a correct trace-based implementation of \({\cal S}\)\@. As shown by Milner \cite{cj98-02-31}, 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 \cite{cj98-02-37}\@. The temporal-logic analogy to the strength of the tree-based approach is the expressiveness superiority of \(\forall\)CTL\(^\star\), the universal fragment of CTL\(^\star\), over LTL \cite{cj98-02-08}\@. Indeed, while a correct trace-based implementation is guaranteed to satisfy all the LTL formulas satisfied in the specification, a correct tree-based implementation is guaranteed to satisfy all the \(\forall\)CTL\(^\star\) formulas satisfied in the specification \cite{cj98-02-17}\@. % \apar{1-4} In this work, we examine the traced-based and tree-based approaches from a complexity-theoretic point of view\@. More precisely, we consider and compare the complexity of the problem of determining whether \({\cal I}\) is a correct trace-based implementation of \({\cal S}\), and the problem of determining whether \({\cal I}\) is a correct tree-based implementation of \({\cal 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 \emph{implementation complexity} of these problems; i.e., their complexity in terms of \({\cal I}\), assuming \({\cal S}\) is fixed\@.\footnote{ The 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\@.} % \apar{1-5} We model specifications and implementations by \emph{transition systems} \cite{cj98-02-23}\@. The systems are defined over the sets \(AP_{\cal I}\) and \(AP_{\cal S}\) of \emph{atomic propositions\/} used in the implementation and specification, respectively\@. Thus, the alphabets of the systems are \(2^{AP_{\cal I}}\) and \(2^{AP_{\cal S}}\)\@. Recall that usually the implementation has more variables than the specification; hence, \(AP_{\cal I} \supseteq AP_{\cal S}\)\@. We therefore interpret correlation as equivalence with respect to \(AP_{\cal S}\)\@. In other words, associating behaviors of the implementation with those of the specification, we first project the behaviors onto \(AP_{\cal S}\)\@. Within this framework, correct trace-based implementation corresponds to \emph{containment}, and correct tree-based implementation corresponds to \emph{simulation} \cite{cj98-02-30}\@. % \apar{1-6} We start by reviewing and examining transition systems with no fairness conditions\@. It is well known that simulation can be checked in polynomial time \cite{cj98-02-31,cj98-02-06,cj98-02-03,cj98-02-19}, whereas the containment problem is in PSPACE \cite{cj98-02-42}\@. We show that the latter problem is PSPACE-hard; 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 NLOGSPACE-complete bound for the implementation complexity of containment\@. For 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 \cite{cj98-02-26,cj98-02-10,cj98-02-44,cj98-02-07}\@. % \apar{1-7} Often, we want our implementations and specifications to describe behaviors that satisfy both liveness and safety properties\@. Then, transition systems with no fairness condition are too weak, and we need the framework of \emph{fair transition systems}\@. We consider unconditional, weak, and strong fairness (also known as impartiality, justice, and compassion, respectively) \cite{cj98-02-27,cj98-02-14,cj98-02-34}\@. Within this framework, correct trace-based implementation corresponds to \emph{fair containment}, and correct tree-based implementation corresponds to \emph{fair simulation} \cite{cj98-02-04,cj98-02-02,cj98-02-17}\@. Hence, it is the complexity of these problems that should be examined when we compare the trace-based and the tree-based approaches\@. % \apar{1-8} We present a uniform method and a simple algorithm for solving the fair-containment problem for all three types of fairness conditions\@. Unlike \cite{cj98-02-09}, 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 \cite{cj98-02-45} 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\@. % \apar{1-9} We also present a uniform method and a simple algorithm for solving 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 \cite{cj98-02-33}, our algorithm can be implemented 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 PTIME-complete 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\@. % \apar{1-10} Our results (summarized in Table~1) show that when we model the specification 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\@. \asection{2}{Preliminaries} \asubsection{2.1}{Fair Transition Systems} % \apar{2.1-1} A fair transition system (transition system, for short) \(S=\zug{\Sigma,W,R,W_0,L,\alpha}\) consists of an alphabet \(\Sigma\), a finite set \(W\) of states, a total transition relation \(R \subseteq W \times W\) (i.e., for every \(w \in W\) there exists \(w' \in W\) such that \(R(w,w')\)), a set \(W_0\) of initial states, a labeling function \(L:W \rightarrow \Sigma\), and a fairness condition \(\alpha\)\@. We will define three types of fairness conditions shortly\@. A computation of \(S\) is a sequence \(\pi=w_0,w_1,w_2,\dots\) of states such that for every \(i \geq 0\), we have \(R(w_i,w_{i+1})\)\@. For an alphabet \(\Sigma\), we use \(\Sigma^*\) and \(\Sigma^\omega\) to denote the sets of all finite and infinite words over \(\Sigma\), respectively\@. For two words \(\rho_1 \in \Sigma^*\) and \(\rho_2 \in \Sigma^* \cup \Sigma^\omega\), we use \(\rho_1 \cdot \rho_2\) to denote the concatenation of \(\rho_1\) and \(\rho_2\)\@. Each computation \(\pi=w_0,w_1,w_2,\dots\) induces the word \(L(\pi)=L(w_0) \cdot L(w_1) \cdot L(w_2)\dots \in \Sigma^\omega\)\@. % \apar{2.1-2} To determine whether a computation is fair, we refer to the set \(\mbox{\emph{Inf\/}}(\pi)\) of states that \(\pi\) visits infinitely often\@. Formally, \[\mbox{\emph{Inf\/}}(\pi) = \{ w \in W \: :\mbox{ for infinitely many }i \geq 0, \mbox{ we have } w_i=w \}\] The way we refer to \(\emph{Inf\/}(\pi)\) depends upon the fairness condition of \(S\)\@. Several types of fairness conditions are studied in the literature\@. Here we consider three: \begin{itemize} \item Unconditional fairness (or impartiality), where \(\alpha \subseteq W\), and \(\pi\) is fair if and only if \(\mbox{\emph{Inf\/}}(\pi) \cap \alpha \neq \emptyset\)\@. \item Weak fairness (or justice), where \(\alpha \subseteq 2^W \times 2^W\), and \(\pi\) is fair if and only if for every pair \(\zug{B,G} \in \alpha\), we have that \(\mbox{\emph{Inf\/}}(\pi) \cap (W \setminus B) = \emptyset\) implies \(\mbox{\emph{Inf\/}}(\pi) \cap G \neq \emptyset\)\@. \item Strong fairness (or fairness), where \(\alpha \subseteq 2^W \times 2^W\), and \(\pi\) is fair if and only if for every pair \(\zug{B,G} \in \alpha\), we have that \(\mbox{\emph{Inf\/}}(\pi) \cap B \neq \emptyset\) implies \(\mbox{\emph{Inf\/}}(r) \cap G \neq \emptyset\)\@. \end{itemize} % \apar{2.1-3} In addition, we consider \emph{nonfair transition systems}; i.e., transition systems in which all the computations are fair\@. % \apar{2.1-4} It is easy to see that fair transition systems are essentially notational variants of automata on infinite words \cite{cj98-02-43}\@. In particular, the unconditional and the strong fairness conditions correspond to the B\"uchi 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\"uchi and Streett automata in the context of fair transition systems\@. % \apar{2.1-5} Defining the unconditional fairness condition as a conjunction of constraints (that is, having \(\alpha \subseteq 2^W\)) corresponds to the generalized B\"uchi 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 \(\zug{B,G}\) in a weak fairness condition is equivalent to a set \((W \setminus B) \cup G\) in a generalized unconditional fairness condition\@. % \apar{2.1-6} For a state \(w\), a \(w\)-computation is a computation \(w_0,w_1,w_2,\dots\) with \(w_0=w\)\@. We use \({\cal T}(S^w)\) to denote the set of all traces \(\sigma_0 \cdot \sigma_1 \dots \in \Sigma^\omega\) for which there exists a fair \(w\)-computation \(w_0,w_1,\dots\) in \(S\) with \(L(w_i)=\sigma_i\) for all \(i \geq 0\)\@. The \emph{trace set} \({\cal T}(S)\) of \(S\) is then defined as \(\bigcup_{w \in W_0}{\cal T}(S^w)\)\@. Thus, each transition system defines a subset of \(\Sigma^{\omega}\)\@. We say that a transition system \(S\) is \emph{empty\/} if and only if \({\cal T}(S)=\emptyset\); i.e., \(S\) has no fair computation\@. We sometimes say that \(S\) accepts a trace \(\rho\), meaning that \(\rho \in {\cal T}(S)\)\@. Note that for a nonfair transition system \(S\), the set \({\cal T}(S)\) contains all traces \(\rho \in \Sigma^\omega\) for which there exists a computation \(\pi\) with \(L(\pi)=\rho\)\@. % \apar{2.1-7} The size of a transition system and its fairness condition determine the complexity of solving questions about it\@. We define classes of transition systems according to these two characteristics\@. We use \({\cal U}, {\cal W}\), and \({\cal 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 \({\cal 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{{\cal S}(n,m)}\)\@. By \cite{cj98-02-38,cj98-02-39}, every fair transition system indeed has a complementary transition system\@. We use \(\goto\) to denote a possible translation (that preserves the trace sets of the systems) between various types of transition systems\@. For example, \({\cal W}(n,m) \goto {\cal 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 \({\cal T}(S)={\cal T}(S')\)\@. % \stam{ Finally, we sometimes speak about the \emph{union} and \emph{product} of two fair transition systems\@. Given \(S\) and \(S'\), the union of \(S\) and \(S'\) is a transition system \(S\) with \({\cal T}(S)={\cal T}(S_1) \cup {\cal T}(S_2)\)\@. Their product is a transition system \(S''\) with \({\cal T}(S'')={\cal T}(S_1) \cap {\cal T}(S_2)\)\@. By \cite{cj98-02-11}, every two fair transition systems indeed have a union and a product transition systems\@.} \asubsection{2.2}{Trace-Based and Tree-Based Implementations} % \apar{2.2-1} In this section, we formalize what it means for an implementation \(S\) to correctly implement a specification \(S'\), in both the trace-based and the tree-based approaches\@. Recall that \(S\) and \(S'\) are given as fair transition systems over the alphabets \(2^{AP}\) and \(2^{AP'}\), respectively, with \(AP \supseteq 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 \(\sigma \in 2^{AP}\), the letter \(\sigma \cap AP'\) instead of the letter \(\sigma\), all of our algorithms and results are also valid for the case \(AP \supset AP'\)\@. % \apar{2.2-2} Recall that nonfair transition systems are of special interest\@. The problems 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=\zug{\Sigma,W,R,W_0,L,\alpha}\), and \(S'=\zug{\Sigma,W',R',W'_0,L',\alpha'}\)\@. \asubsubsection{2.2.1}{Containment and Fair Containment} % \apar{2.2.1-1} The fair-containment problem of \(S\) and \(S'\) is to determine whether \({\cal T}(S) \subseteq {\cal 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\@. % \apar{2.2.1-2} While containment and fair containment refer only to the set of computations of \(S\) and \(S'\), simulation and fair simulation also refer to the branching structure of the transition systems\@. \asubsubsection{2.2.2}{Simulation} % \apar{2.2.2-1} Let \(w\) and \(w'\) be states in \(W\) and \(W'\), respectively\@. A relation \(H \subseteq W \times W'\) is a simulation relation from \(\zug{S,w}\) to \(\zug{S',w'}\) if and only if the following conditions hold \cite{cj98-02-30}: \begin{enumerate} \item \(H(w,w')\)\@. \item For all \(t\) and \(t'\) with \(H(t,t')\), we have \(L(t)= L(t')\)\@. \item For all \(t\) and \(t'\) with \(H(t,t')\) and for all \(s \in W\) such that \(R(t,s)\), there exists \(s' \in W'\) such that \(R'(t',s')\) and \(H(s,s')\)\@. \end{enumerate} % \apar{2.2.2-2} A simulation relation \(H\) is a simulation from \(S\) to \(S'\) if and only if for every \(w \in W_0\) there exists \(w' \in 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 \leq S'\)\@. Intuitively, this means that the transition system \(S'\) has more behaviors than the transition system \(S\)\@. In fact, every \actlsr formula that is satisfied in \(S'\) is satisfied also in \(S\) \cite{cj98-02-05}\@. Given \(S\) and \(S'\), the simulation problem is to determine whether \(S \leq S'\)\@. % \apar{2.2.2-3} We also mention here the \emph{bisimulation problem} \cite{cj98-02-30}\@. Two transition systems are bisimilar if and only if they have exactly the same behavior\@. Formally, a relation \(H \subseteq W \times W'\) from \(\zug{S,w}\) to \(\zug{S',w'}\) is a bisimulation if, in addition to conditions 1--3 above, the following condition also holds: \begin{enumerate} \item[4.] For all \(t\) and \(t'\) with \(H(t,t')\) and for all \(s' \in W'\) such that \(R'(t',s')\), there exists \(s \in W\) such that \(R(t,s)\) and \(H(s,s')\)\@. \end{enumerate} \asubsubsection{2.2.3}{Fair Simulation} % \apar{2.2.3-1} Let \(H \subseteq W \times W'\) be a relation over the states of \(S\) and \(S'\)\@. It is convenient to extend \(H\) to also relate infinite computations of \(S\) and \(S'\)\@. For two computations \(\pi=w_0,w_1,\dots\) in \(S\), and \(\pi'=w'_0,w'_1,\dots\) in \(S'\), we say that \(H(\pi,\pi')\) holds if and only if \(H(w_i,w'_i)\) holds for all \(i \geq 0\)\@. For a pair \(\zug{w,w'} \in W \times W'\), we say that \(\zug{w,w'}\) is \emph{good in} \(H\) if and only if for every fair \(w\)-computation \(\pi\) in \(S\), there exists a fair \(w'\)-computation \(\pi'\) in \(S'\), such that \(H(\pi,\pi')\)\@. % \apar{2.2.3-2} Let \(w\) and \(w'\) be states in \(W\) and \(W'\), respectively\@. A relation \(H \subseteq W \times W'\) is a fair-simulation relation from \(\zug{S,w}\) to \(\zug{S',w'}\) if and only if the following conditions hold \cite{cj98-02-17}: \begin{enumerate} \item \(H(w,w')\)\@. \item For all \(t\) and \(t'\) with \(H(t,t')\), we have \(L(t)= L(t')\)\@. \item For all \(t\) and \(t'\) with \(H(t,t')\), the pair \(\zug{t,t'}\) is good in \(H\)\@. \end{enumerate} % \apar{2.2.3-3} A fair-simulation relation \(H\) is a fair simulation from \(S\) to \(S'\) if and only if for every \(w \in W_0\) there exists \(w' \in W'_0\) such that \(H(w,w')\)\@. If there exists a fair simulation from \(S\) to \(S'\), we say that \(S\) \emph{fair simulates} \(S'\), and we write \(S \leq S'\)\@. Intuitively, this means that the transition system \(S'\) has more fair behaviors than the transition system \(S\)\@. In fact, every fair-\actlsr formula (that is, every \actlsr formula with path quantification ranging only over fair computations \cite{cj98-02-13}) that is satisfied in \(S'\) is also satisfied in \(S\) \cite{cj98-02-17}\@. The fair-simulation problem is, given \(S\) and \(S'\), to determine whether \(S \leq S'\)\@. Note that when they relate nonfair transition systems, fair simulation and simulation coincide\@. % \apar{2.2.3-4} We also mention here the \emph{fair-bisimulation problem} \cite{cj98-02-17}\@. Two transition systems are bisimilar if and only if they have exactly the same fair behavior\@. Formally, a relation \(H \subseteq W \times W'\) from \(\zug{S,w}\) to \(\zug{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 \(\zug{w,w'} \in W \times W'\) is good in \(H\) if and only if for every fair \(w\)-computation \(\pi\) in \(S\), there exists a fair \(w'\)-computation \(\pi'\) in \(S'\) such that \(H(\pi,\pi')\), and for every fair \(w'\)-computation \(\pi'\) in \(S'\), there exists a fair \(w\)-computation \(\pi\) in \(S\) such that \(H(\pi,\pi')\)\@. % \apar{2.2.3-5} It is easy to see that simulation implies containment, and that fair simulation implies fair containment; that is, if \(S \leq S'\), then \({\cal T}(S) \subseteq {\cal 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)^\omega\)\@. As such, \({\cal T}(S) \subseteq {\cal 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\)\@. % \begin{figure}[htb] \begin{center} \setlength{\unitlength}{0.00625000in} \begingroup\makeatletter\ifx\SetFigFont\undefined \def\x#1#2#3#4#5#6#7\relax{\def\x{#1#2#3#4#5#6}}% \expandafter\x\fmtname xxxxxx\relax \def\y{splain}% \ifx\x\y % LaTeX or SliTeX? \gdef\SetFigFont#1#2#3{% \ifnum #1<17\tiny\else \ifnum #1<20\small\else \ifnum #1<24\normalsize\else \ifnum #1<29\large\else \ifnum #1<34\Large\else \ifnum #1<41\LARGE\else \huge\fi\fi\fi\fi\fi\fi \csname #3\endcsname}% \else \gdef\SetFigFont#1#2#3{\begingroup \count@#1\relax \ifnum 25<\count@\count@25\fi \def\x{\endgroup\@setsize\SetFigFont{#2pt}}% \expandafter\x \csname \romannumeral\the\count@ pt\expandafter\endcsname \csname @\romannumeral\the\count@ pt\endcsname \csname #3\endcsname}% \fi \fi\endgroup \begin{picture}(457,139)(0,-10) \path(70,77) (63.359,68.891) (58.125,63.875) (50.000,62.000) % \path(50,62) (45.500,69.797) (44.375,75.799) (44.000,82.375) (44.375,88.904) (45.500,94.766) (50.000,102.000) % \path(50,102) (58.125,100.500) (63.359,95.531) (70.000,87.000) % \path(63.723,92.347)(70.000,87.000)(66.978,94.672) \path(190,87) (196.641,95.531) (201.875,100.500) (210.000,102.000) % \path(210,102) (214.500,94.766) (215.625,88.904) (216.000,82.375) (215.625,75.799) (214.500,69.797) (210.000,62.000) % \path(210,62) (201.875,63.875) (196.641,68.891) (190.000,77.000) % \path(196.463,71.878)(190.000,77.000)(193.292,69.440) \path(116.062,100.509)(111.000,94.000)(118.530,97.361) \path(111,94) (117.756,98.938) (123.029,102.000) (131.000,104.000) % \path(131,104) (138.971,102.000) (144.244,98.938) (151.000,94.000) % \path(110,72) (116.756,67.484) (122.029,64.375) (130.000,62.000) % \path(130,62) (137.971,64.375) (143.244,67.484) (150.000,72.000) % \path(144.534,65.826)(150.000,72.000)(142.271,69.124) \path(310,17) (303.359,8.891) (298.125,3.875) (290.000,2.000) % \path(290,2) (285.500,9.797) (284.375,15.799) (284.000,22.375) (284.375,28.904) (285.500,34.766) (290.000,42.000) % \path(290,42) (298.125,40.500) (303.359,35.531) (310.000,27.000) % \path(303.723,32.347)(310.000,27.000)(306.978,34.672) \path(430,27) (436.641,35.531) (441.875,40.500) (450.000,42.000) % \path(450,42) (454.500,34.766) (455.625,28.904) (456.000,22.375) (455.625,15.799) (454.500,9.797) (450.000,2.000) % \path(450,2) (441.875,3.875) (436.641,8.891) (430.000,17.000) % \path(436.463,11.878)(430.000,17.000)(433.292,9.440) \put(90,77){\makebox(0,0)[b]{\smash{{{\SetFigFont{8}{9.6}{rm}\(a\)}}}}} \put(260,102){\makebox(0,0)[b]{\smash{{{\SetFigFont{8}{9.6}{rm}\(S':\)}}}}} \put(15,102){\makebox(0,0)[b]{\smash{{{\SetFigFont{8}{9.6}{rm}\(S:\)}}}}} \put(410,17){\makebox(0,0)[b]{\smash{{{\SetFigFont{8}{9.6}{rm}\(b\)}}}}} \put(330,17){\makebox(0,0)[b]{\smash{{{\SetFigFont{8}{9.6}{rm}\(a\)}}}}} \put(410,77){\makebox(0,0)[b]{\smash{{{\SetFigFont{8}{9.6}{rm}\(a\)}}}}} \put(330,77){\makebox(0,0)[b]{\smash{{{\SetFigFont{8}{9.6}{rm}\(a\)}}}}} \put(170,77){\makebox(0,0)[b]{\smash{{{\SetFigFont{8}{9.6}{rm}\(b\)}}}}} \path(356.062,40.509)(351.000,34.000)(358.530,37.361) \path(351,34) (357.756,38.938) (363.029,42.000) (371.000,44.000) % \path(371,44) (378.971,42.000) (384.244,38.938) (391.000,34.000) % \put(90,82){\ellipse{42}{42}} \put(170,82){\ellipse{42}{42}} \put(330,82){\ellipse{42}{42}} \put(410,82){\ellipse{42}{42}} \put(330,22){\ellipse{42}{42}} \put(410,22){\ellipse{42}{42}} \path(330,62)(330,42) \path(328.000,50.000)(330.000,42.000)(332.000,50.000) \path(350,12) (356.756,7.484) (362.029,4.375) (370.000,2.000) % \path(370,2) (377.971,4.375) (383.244,7.484) (390.000,12.000) % \path(384.534,5.826)(390.000,12.000)(382.271,9.124) \path(170,122)(170,102) \path(168.000,110.000)(170.000,102.000)(172.000,110.000) \path(90,122)(90,102) \path(88.000,110.000)(90.000,102.000)(92.000,110.000) \path(430,52)(425,37) \path(425.632,45.222)(425.000,37.000)(429.427,43.957) \path(410,122)(410,102) \path(408.000,110.000)(410.000,102.000)(412.000,110.000) \path(330,122)(330,102) \path(328.000,110.000)(330.000,102.000)(332.000,110.000) \path(410,62)(410,42) \path(408.000,50.000)(410.000,42.000)(412.000,50.000) \end{picture} % \afigcap{1}{\({\cal T}(S) \subseteq {\cal T}(S')\) but \(S \not \leq S'\)} \label{nosim} \end{center} \end{figure} \asubsection{2.3}{Complexity Measures} % \apar{2.3-1} In the rest of this paper, we examine the traced-based and the tree-based 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 \({\cal T}(S) \subseteq {\cal T}(S')\) and \(S \leq S'\), in terms of the size of \(S\), assuming \(S'\) is fixed\@. % \apar{2.3-2} We refer to three complexity classes: PSPACE, PTIME, and NLOGSPACE, briefly described as follows (for a full definition, see \cite{cj98-02-16})\@. We say that a problem is \emph{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 \({\cal P}\) is complete for a complexity class \(C\) if and only if \({\cal P}\) is in \(C\) and is also \(C\)-hard\@. % \apar{2.3-3} Some of the results we study, mainly those that we consider nonfair transition systems, are known; therefore we only review them\@. \asection{3}{Verification of Nonfair Transition Systems} % \apar{3-1} In this section, we study the complexity of the containment and simulation problems\@. We show that while the containment problem is harder, its implementation complexity is lower than that of the simulation problem\@. \asubsection{3.1}{The Containment Problem} % \begin{alabsubtext}{Theorem}{1}{} \label{tc c} The containment problem is PSPACE-complete\@. \end{alabsubtext} % \begin{alabsubtext}{Proof of Theorem}{1}{} \prooffontshape \apar{Proof of Theorem 1-1} The upper bound follows from known PSPACE bound to the fair-containment problem for unconditionally fair transition systems (\cite{cj98-02-42}, see also Theorem~5)\@. % \apar{Proof of Theorem 1-2} We can regard an unconditionally fair system \(S=\zug{\Sigma,W,R,W_0,L,\alpha}\), with \(\alpha \subseteq W\), as a \emph{finite-acceptance} transition system\@. The traces of a finite-acceptance transition system are finite words over the alphabet \(\Sigma\)\@. A finite computation \(\pi=w_0,\dots,w_k\) is ``fair'' in \(S\) (that is, \(L(\pi)\) is accepted) if and only if \(w_k \in \alpha\)\@. We call the states in \(\alpha\) \emph{final} states\@. A finite-acceptance transition system \(S\) is universal if and only if \({\cal T}(S)=\Sigma^*\)\@. In \cite{cj98-02-35}, 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 \cite{cj98-02-35} is of regular expressions, yet regular expressions can be linearly translated to finite-acceptance transition systems)\@. % \apar{Proof of Theorem 1-3} We reduce the universality problem for finite-acceptance transition systems to the containment problem\@. Consider a finite-acceptance transition system \(S=\zug{\Sigma,W,R,W_0,L,\alpha}\)\@. Let \[S'=\zug{\Sigma \cup \{\#\},W \cup \{w_{\#}\}, R \cup R_{\#}, W_0, L', W \cup \{w_{\#}\}}\] be a nonfair transition system, where: \begin{itemize} \item For every \(w \in (\alpha \cup \{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\@. \item For every state \(w \in W\), we have \(L'(w)=L(w)\)\@. In addition, \(L'(w_{\#})=\{\#\}\)\@. \end{itemize} % \apar{Proof of Theorem 1-4} We prove that \(\Sigma^* \subseteq {\cal T}(S)\) if and only if \(\Sigma^\omega \cup (\Sigma^* \cdot \{\#\}^\omega) \subseteq {\cal T}(S')\)\@. Assume first that \(\Sigma^\omega \cup (\Sigma^* \cdot \{\#\}^\omega) \subseteq {\cal T}(S')\), and assume, by way of contradiction, that there exists \(\rho \in \Sigma^*\) such that \(\rho \not \in {\cal T}(S)\)\@. Let \(\pi=w_0,w_1,\dots\) be an accepting computation of \(S'\) on \(\rho \cdot \#^\omega\)\@. By the definition of \(L'\), we have that \(\pi \in W^* \cdot w_{\#}^\omega\)\@. Let \(k\) be such that \(w_k \neq w_{\#}\) and \(w_{k+1} = w_{\#}\)\@. As \(R_{\#}(w_k, w_{k+1})\), it must be that \(w_k \in \alpha\)\@. In addition, for all \(0 \leq i < k-1\), we have \(R(w_i,w_{i+1})\)\@. Hence \(w_0,\dots,w_{k}\) is an accepting computation of \(S\) on \(\rho\), and we reach a contradiction\@. % \apar{Proof of Theorem 1-5} Assume now that \(\Sigma^* \subseteq {\cal T}(S)\)\@. Consider a trace \(\rho \in \Sigma^*\)\@. Let \(w_0,w_1,\dots,w_k\) be an accepting computation of \(S\) on \(\rho\)\@. Clearly, \(w_0,w_1,\dots,w_k,w_{\#}^\omega\) is an accepting computation of \(S'\) on \(\rho \cdot \{\#\}^\omega \)\@. Hence, \(\Sigma^* \cdot \{\#\}^\omega \subseteq {\cal T}(S')\)\@. Next, consider a trace \(\rho= \sigma_0,\sigma_1,\dots \in \Sigma^\omega\)\@. We define a tree that embodies all the possible runs of \(S\) on finite prefixes of \(\rho\)\@. The tree has a root labeled \(\epsilon\)\@. 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)=\sigma_0\)\@. For \(l \geq 0\), a node \(w\) of level \(i\) has as successors nodes \(w'\) for which \(R(w,w')\) and \(L(w')=\sigma_{l+1}\)\@. Because \(\Sigma^* \subseteq {\cal T}(S)\), the tree embodies accepting runs for all the (infinitely many) finite prefixes of \(\rho\), and is therefore infinite\@. Hence, by K\"onig's lemma, we can pick a sequence \(\pi=\epsilon,w_0,w_1,\dots\)\ such that \(w_0 \in W_0\), and for all \(j \geq 0\), we have that \(L(w_j)=\sigma_j\) and \(R(w_j,w_{j+1})\)\@. As such, \(\pi\) is an accepting run of \(S'\) on \(\rho\)\@. As we can easily construct a nonfair transition system for \(\Sigma^\omega \cup (\Sigma^* \cdot \{\#\}^\omega)\), we are done\@. {\nopagebreakbeginpar\markendlst{Proof of Theorem 1}} \end{alabsubtext} % \begin{alabsubtext}{Theorem}{2}{} \label{tc ic} The implementation complexity of the containment problem is NLOGSPACE-complete\@. \end{alabsubtext} % \begin{alabsubtext}{Proof of Theorem}{2}{} \prooffontshape In Theorem~6, we prove an NLOGSPACE upper bound for the implementation complexity of the more general fair-containment 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 \cite{cj98-02-22}\@.\footnote{The proof in \cite{cj98-02-22} 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 \cite{cj98-02-21,cj98-02-41} for NLOGSPACE = co-NLOGSPACE; the argument for the completeness is easy)\@.} Given a directed graph \(G\) with two designated nodes \(s\) and \(t\), we can view \(G\) as a nonfair transition system \(S_G\) over \(\Sigma=\{\sigma,s,t\}\) in which all states are initial states, all states except \(s\) and \(t\) are labeled \(\sigma\), 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 \({\cal T}(G) \subseteq \{\sigma,t\}^* \cdot \{\sigma,s\}^\omega \cup \{\sigma,t\}^\omega\)\@. Since we can specify the expression in the right with a fixed nonfair transition system, we are done\@. {\nopagebreakbeginpar\markendlst{Proof of Theorem 2}} \end{alabsubtext} \asubsection{3.2}{The Simulation Problem} % \begin{alabsubtext}{Theorem}{3}{} \label{simulation c} The simulation problem is PTIME-complete\@. \end{alabsubtext} % \begin{alabsubtext}{Proof of Theorem}{3}{} \prooffontshape The upper bound is given in \cite{cj98-02-31}\@. The lower bound follows from the reduction in \cite{cj98-02-06} (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\@. {\nopagebreakbeginpar\markendlst{Proof of Theorem 3}} \end{alabsubtext} % \begin{alabsubtext}{Theorem}{4}{} \label{simulation ic} The implementation complexity of the simulation problem is PTIME-complete\@. \end{alabsubtext} % \begin{alabsubtext}{Proof of Theorem}{4}{} \prooffontshape \apar{Proof of Theorem 4-1} Membership in PTIME follows from Theorem~3\@. % \apar{Proof of Theorem 4-2} We prove hardness in PTIME by reducing the NAND circuit value problem (NANDCV), proved to be PTIME-complete in \cite{cj98-02-18,cj98-02-15}, 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 \(\beta\) constructed solely of NAND gates of fanout \(2\), and a vector \(\zug{x_1,\dots,x_n}\) of Boolean input values\@. The problem is to determine whether the output of \(\beta\) on \(\zug{x_1,\dots,x_n}\) is~\(1\)\@. Formally, we denote a Boolean circuit of NAND gates by a tuple \(\beta=\zug{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,\dots,g_n\)), \(g_{out} \in G \cup G_{in}\) is the output gate, \(T_l: G \rightarrow G \cup G_{in}\) maps each internal gate to its left input, and \(T_r: G \rightarrow G \cup G_{in}\) maps each internal gate to its right input\@. Note that since there are no circular dependencies in \(\beta\), the graph induced by \(T_l\) and \(T_r\) is acyclic\@. % \apar{Proof of Theorem 4-3} The idea of the reduction is as follows\@. We define a fixed transition system \(S'\) that embodies all the NAND circuits \(\beta\) and input vectors \(\vec{x}\) for which the value of \(\beta\) on \(\vec{x}\) is~\(1\)\@. Then, given a circuit \(\beta\) and an input vector \(\vec{x}\), we translate them to a transition system \(S\) such that \(S \leq S'\) if and only if the value of \(\beta\) on \(\vec{x}\) is~\(1\)\@. % \begin{figure}[htb] \begin{center} \setlength{\unitlength}{0.00875000in} \begingroup\makeatletter\ifx\SetFigFont\undefined \def\x#1#2#3#4#5#6#7\relax{\def\x{#1#2#3#4#5#6}}% \expandafter\x\fmtname xxxxxx\relax \def\y{splain}% \ifx\x\y % LaTeX or SliTeX? \gdef\SetFigFont#1#2#3{% \ifnum #1<17\tiny\else \ifnum #1<20\small\else \ifnum #1<24\normalsize\else \ifnum #1<29\large\else \ifnum #1<34\Large\else \ifnum #1<41\LARGE\else \huge\fi\fi\fi\fi\fi\fi \csname #3\endcsname}% \else \gdef\SetFigFont#1#2#3{\begingroup \count@#1\relax \ifnum 25<\count@\count@25\fi \def\x{\endgroup\@setsize\SetFigFont{#2pt}}% \expandafter\x \csname \romannumeral\the\count@ pt\expandafter\endcsname \csname @\romannumeral\the\count@ pt\endcsname \csname #3\endcsname}% \fi \fi\endgroup \begin{picture}(532,339)(0,-10) \path(169,189)(301,2)(486,52) \path(478.799,47.982)(486.000,52.000)(477.755,51.843) \path(364,189)(236,2)(47,52) \path(55.245,51.887)(47.000,52.000)(54.222,48.020) \path(171,212)(301,252) \path(293.942,247.736)(301.000,252.000)(292.766,251.559) \path(231.216,240.613)(226.000,247.000)(227.597,238.910) \path(226,247)(306,77) \path(300.784,83.387)(306.000,77.000)(304.403,85.090) \path(326,77)(371,187) \path(369.822,178.838)(371.000,187.000)(366.120,180.353) \path(209,247)(164,137) \path(165.178,145.162)(164.000,137.000)(168.880,143.647) \path(221,47) (225.295,44.141) (228.810,41.651) (233.680,37.602) (236.000,32.000) % \path(236,32) (233.488,29.448) (228.844,27.625) (222.777,26.531) (216.000,26.166) (209.223,26.531) (203.156,27.625) (198.512,29.448) (196.000,32.000) % \path(196,32) (198.320,37.602) (203.190,41.651) (206.705,44.141) (211.000,47.000) % \path(205.386,40.960)(211.000,47.000)(203.204,44.312) \path(170,135)(296,322)(487,272) \path(478.754,272.091)(487.000,272.000)(479.767,275.961) \path(336,62)(481,62) \path(473.000,60.000)(481.000,62.000)(473.000,64.000) \path(336,267)(376,287)(486,72) \path(480.576,78.211)(486.000,72.000)(484.137,80.033) \path(391,212)(481,257) \path(474.739,251.633)(481.000,257.000)(472.950,255.211) \path(336,262)(481,262) \path(473.000,260.000)(481.000,262.000)(473.000,264.000) \path(363,135)(236,322)(46,272) \path(53.228,275.970)(46.000,272.000)(54.246,272.102) \path(196,67)(156,107) \path(163.071,102.757)(156.000,107.000)(160.243,99.929) \path(336,257)(376,217) \path(368.929,221.243)(376.000,217.000)(371.757,224.071) \path(336,57)(376,37)(486,252) \path(484.137,243.967)(486.000,252.000)(480.576,245.789) \path(321,277) (325.295,279.859) (328.810,282.349) (333.679,286.398) (336.000,292.000) % \path(336,292) (333.488,294.552) (328.844,296.375) (322.777,297.469) (316.000,297.834) (309.223,297.469) (303.156,296.375) (298.512,294.552) (296.000,292.000) % \path(296,292) (298.321,286.398) (303.190,282.349) (306.705,279.859) (311.000,277.000) % \path(303.204,279.688)(311.000,277.000)(305.386,283.040) \put(316,257){\makebox(0,0)[b]{\smash{{{\SetFigFont{8}{9.6}{rm}101\(\swarrow\)}}}}} \put(376,197){\makebox(0,0)[b]{\smash{{{\SetFigFont{8}{9.6}{rm}001\(\swarrow\)}}}}} \put(156,197){\makebox(0,0)[b]{\smash{{{\SetFigFont{8}{9.6}{rm}110\(\swarrow\)}}}}} \put(156,117){\makebox(0,0)[b]{\smash{{{\SetFigFont{8}{9.6}{rm}001\(\searrow\)}}}}} \put(216,57){\makebox(0,0)[b]{\smash{{{\SetFigFont{8}{9.6}{rm}011\(\searrow\)}}}}} \put(316,57){\makebox(0,0)[b]{\smash{{{\SetFigFont{8}{9.6}{rm}101\(\searrow\)}}}}} \put(376,117){\makebox(0,0)[b]{\smash{{{\SetFigFont{8}{9.6}{rm}110\(\searrow\)}}}}} \put(216,257){\makebox(0,0)[b]{\smash{{{\SetFigFont{8}{9.6}{rm}011\(\swarrow\)}}}}} \path(21,57) (18.223,52.869) (15.844,49.453) (12.000,44.625) (6.000,42.000) % \path(6,42) (3.703,44.703) (2.062,49.375) (1.078,55.359) (0.750,62.000) (1.078,68.641) (2.062,74.625) (3.703,79.297) (6.000,82.000) % \path(6,82) (12.000,79.375) (15.844,74.547) (18.223,71.131) (21.000,67.000) % \path(14.898,72.547)(21.000,67.000)(18.226,74.766) \path(21,257) (18.223,252.869) (15.844,249.453) (12.000,244.625) (6.000,242.000) % \path(6,242) (3.703,244.703) (2.062,249.375) (1.078,255.359) (0.750,262.000) (1.078,268.641) (2.062,274.625) (3.703,279.297) (6.000,282.000) % \path(6,282) (12.000,279.375) (15.844,274.547) (18.223,271.131) (21.000,267.000) % \path(14.898,272.547)(21.000,267.000)(18.226,274.766) \path(511,267) (513.777,271.131) (516.156,274.547) (520.000,279.375) (526.000,282.000) % \path(526,282) (528.297,279.297) (529.937,274.625) (530.922,268.641) (531.250,262.000) (530.922,255.359) (529.937,249.375) (528.297,244.703) (526.000,242.000) % \path(526,242) (520.000,244.625) (516.156,249.453) (513.777,252.869) (511.000,257.000) % \path(517.102,251.453)(511.000,257.000)(513.774,249.234) \path(511,67) (513.777,71.131) (516.156,74.547) (520.000,79.375) (526.000,82.000) % \path(526,82) (528.297,79.297) (529.937,74.625) (530.922,68.641) (531.250,62.000) (530.922,55.359) (529.937,49.375) (528.297,44.703) (526.000,42.000) % \path(526,42) (520.000,44.625) (516.156,49.453) (513.777,52.869) (511.000,57.000) % \path(517.102,51.453)(511.000,57.000)(513.774,49.234) \put(496,57){\makebox(0,0)[b]{\smash{{{\SetFigFont{8}{9.6}{rm}1\(\swarrow\)}}}}} \put(496,257){\makebox(0,0)[b]{\smash{{{\SetFigFont{8}{9.6}{rm}0\(\searrow\)}}}}} \put(36,257){\makebox(0,0)[b]{\smash{{{\SetFigFont{8}{9.6}{rm}1\(\searrow\)}}}}} \put(36,57){\makebox(0,0)[b]{\smash{{{\SetFigFont{8}{9.6}{rm}0\(\swarrow\)}}}}} \path(391,112)(481,67) \path(472.950,68.789)(481.000,67.000)(474.739,72.367) \put(156,202){\ellipse{40}{30}} \put(36,62){\ellipse{28}{28}} \put(36,262){\ellipse{28}{28}} \path(296,262)(236,262) \path(244.000,264.000)(236.000,262.000)(244.000,260.000) \path(236,62)(296,62) \path(288.000,60.000)(296.000,62.000)(288.000,64.000) \path(361,112)(231,72) \path(238.058,76.264)(231.000,72.000)(239.234,72.441) \path(316,77)(316,247) \path(318.000,239.000)(316.000,247.000)(314.000,239.000) \put(376,202){\ellipse{40}{30}} \put(496,62){\ellipse{28}{28}} \put(496,262){\ellipse{28}{28}} \put(216,62){\ellipse{40}{30}} \put(316,62){\ellipse{40}{30}} \put(316,262){\ellipse{40}{30}} \put(216,262){\ellipse{40}{30}} \put(156,122){\ellipse{40}{30}} \put(376,122){\ellipse{40}{30}} \path(216,247)(216,77) \path(214.000,85.000)(216.000,77.000)(218.000,85.000) \path(168.614,179.165)(164.000,186.000)(164.854,177.798) \path(164,186)(204,76) \path(199.386,82.835)(204.000,76.000)(203.146,84.202) \path(196,62)(51,62) \path(59.000,64.000)(51.000,62.000)(59.000,60.000) \path(141,112)(51,67) \path(57.261,72.367)(51.000,67.000)(59.050,68.789) \path(196,267)(156,287)(46,72) \path(47.863,80.033)(46.000,72.000)(51.424,78.211) \path(141,212)(51,257) \path(59.050,255.211)(51.000,257.000)(57.261,251.633) \path(196,262)(51,262) \path(59.000,264.000)(51.000,262.000)(59.000,260.000) \path(196,57)(156,37)(46,252) \path(51.424,245.789)(46.000,252.000)(47.863,243.967) \path(330.614,240.165)(326.000,247.000)(326.854,238.798) \path(326,247)(366,137) \path(361.386,143.835)(366.000,137.000)(365.146,145.202) \path(171,192)(301,72) \path(293.765,75.957)(301.000,72.000)(296.478,78.896) \path(237.235,247.043)(230.000,251.000)(234.522,244.104) \path(230,251)(360,131) \path(378.000,179.000)(376.000,187.000)(374.000,179.000) \path(376,187)(376,137) \path(374.000,145.000)(376.000,137.000)(378.000,145.000) \path(191.757,249.929)(196.000,257.000)(188.929,252.757) \path(196,257)(156,217) \path(160.243,224.071)(156.000,217.000)(163.071,221.243) \path(348.000,200.000)(356.000,202.000)(348.000,204.000) \path(356,202)(176,202) \path(184.000,204.000)(176.000,202.000)(184.000,200.000) \path(184.000,124.000)(176.000,122.000)(184.000,120.000) \path(176,122)(356,122) \path(348.000,120.000)(356.000,122.000)(348.000,124.000) \path(158.000,179.000)(156.000,187.000)(154.000,179.000) \path(156,187)(156,137) \path(154.000,145.000)(156.000,137.000)(158.000,145.000) \path(340.243,74.071)(336.000,67.000)(343.071,71.243) \path(336,67)(376,107) \path(371.757,99.929)(376.000,107.000)(368.929,102.757) \end{picture} % \afigcap{2}{A fixed transition system that embodies all NAND circuits} \label{nand} \end{center} \end{figure} % \apar{Proof of Theorem 4-4} The transition system \(S'\) (see Figure~2) has 12 states\@. Eight states correspond to internal gates\@. Each of these states is an entry in the truth table of the operator NAND, attributed with a direction, either \(\swarrow\) or \(\searrow\)\@. Thus, the ``internal states'' of \(S'\) are \(\zug{001\swarrow}\), \(\zug{011\swarrow}\), \(\zug{101\swarrow}\), \(\zug{110\swarrow}\), \(\zug{001\searrow}\), \(\zug{011\searrow}\), \(\zug{101\searrow}\), and \(\zug{110\searrow}\)\@. Four more states correspond to the input gates of the circuit\@. Each of these states is a Boolean value, attributed with a direction; thus the ``input states'' are \(\zug{0\swarrow}\), \(\zug{1\swarrow}\), \(\zug{0\searrow}\), and \(\zug{1\searrow}\)\@. The intuition is that an internal state \(\zug{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 \(\zug{val,d}\) corresponds to an input gate with output \(val\) that can only be a \(d\) input of other gates\@. % \apar{Proof of Theorem 4-5} Accordingly, the transitions from an internal state \(\zug{l,r,val,d}\) correspond 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=\swarrow\) or \(val=r\) and \(d=\searrow\)\@. For example, the internal state \(\zug{101\swarrow}\) has transitions to the states \(\zug{001\swarrow}, \zug{011\swarrow}, \zug{101\swarrow}, \zug{110\searrow}, \zug{1\swarrow}\), and \(\zug{0\searrow}\)\@. It has transitions from all states \(\zug{l,r,val,d}\) with \(l=0\)\@. In addition, the input states have self loops\@. % \apar{Proof of Theorem 4-6} We label an internal state by either \(\swarrow\) or \(\searrow\), according to its directional element\@. For example, the node \(\zug{101\swarrow}\) is labeled \(\{\swarrow\}\)\@. We label an input state by both its value and direction\@. For example, the node \(\zug{1\searrow}\) is labeled \(\{1, \searrow\}\)\@. 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\@. % \apar{Proof of Theorem 4-7} Given a circuit \(\beta=\zug{G,G_{in},g_{out},T_l,T_r}\) and an input vector \(\vec{x}\), the transition system \(S\) is simply \(\beta\), with attributions of directions, and labeling of input gates according to \(\vec{x}\)\@. More precisely, we duplicate all gates and inputs of \(\beta\) so that the output of each gate is either always a left input of other gates, in which case we label it with \(\swarrow\), or always a right input of other gates, in which case we label it with \(\searrow\)\@. 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, {\footnotesize \(S=\zug{\{\swarrow,\searrow\} \cup \{0,1\} \times \{\swarrow,\searrow\},(G \cup G_{in}) \times \{\swarrow,\searrow\}, T, \{g_{out}\} \times \{\swarrow, \searrow\}, L}\)}, where: \begin{itemize} \item \(T(\zug{g,d},\zug{g',d'})\) if and only if one of the following holds: \begin{enumerate} \item \(g \in G\), \(d'=l\), and \(T_l(g)=g'\), \item \(g \in G\), \(d'=r\), and \(T_r(g)=g'\), or \item \(g \in G_{in}\), \(g=g'\), and \(d=d'\)\@. \end{enumerate} \item For \(g \in G\), we have \(L(\zug{g,d})=d\)\@. For \(g_i \in G_{in}\), we have \(L(\zug{g_i,d})=\zug{x_i,d}\)\@. \end{itemize} % \apar{Proof of Theorem 4-8} We define the \emph{depth} of a gate as the length of the longest path from it to an 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 \in G_{in}\), we have \(depth(g)=0\), and for \(g \in G\), we have \(depth(g)=1+ \max \{depth(T_l(g)),depth(T_r(g))\}\)\@. % \apar{Proof of Theorem 4-9} We first prove that for a simulation relation \(H\) from \(S\) to \(S'\) and for every pair \(\zug{\zug{g,d},\zug{val,d'}}\) or \(\zug{\zug{g,d},\zug{l,r,val,d'}}\) in \(H\), the output of the gate \(g\) on the vector \(\vec{x}\) is \(val\)\@. The proof proceeds by induction on \(depth(g)\)\@. If \(depth(g)=0\), then \(g \in G_{in}\)\@. Let \(g=g_i\)\@. By the definition of \(L'\), the state \(\zug{g_i,d}\) is labeled with \(x_i\) and can therefore be related by \(H\) only to states \(\zug{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 \in G\), and \(\zug{g,d}\) is mapped to some internal state \(t=\zug{l,r,v,d'}\)\@. By the definition of simulation, for every successor \(\zug{g',d'}\) of \(\zug{g,d}\) there exists a successor \(t'\) of \(t\) such that \(H(g',t')\)\@. We know that \(\zug{g,d}\) has two successors, \(\zug{T_l(g),\swarrow}\) and \(\zug{T_r(g),\searrow}\)\@. By the definition of \(S'\), all the successors of \(t\) that are labeled with \(\swarrow\) 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 \(\mbox{NAND}(l,r)\)\@. By the definition of \(S'\), we also have \(v=\mbox{NAND}(l,r)\), and we are done\@. % \apar{Proof of Theorem 4-10} We now prove that the output of \(\beta\) on \(\vec{x}\) is \(1\) if and only if \(S\) simulates \(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 \(\zug{g_{out},\swarrow}\) and \(\zug{g_{out},\searrow}\) of \(S\) are related by \(H\) to states with \(val=1\)\@. Hence, by the above claim, the output of \(\beta\) on \(\vec{x}\) is \(1\)\@. % \apar{Proof of Theorem 4-10} Assume that the output of \(\beta\) on \(\vec{x}\) is \(1\)\@. Consider a relation \(H\) from the states of \(S\) to the states of \(S'\) in which \(H({\zug{g,d},\zug{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 \(\vec{x}\), and \(d=d'\); and \(H(\zug{g,d},\zug{val,d'})\) for an input gate \(g\) if and only if \(val\) is the output of \(g\) on \(\vec{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=\zug{g,d}\) for \(g \in 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=\zug{val,d}\), where \(val\) is the output of \(g\) on \(\vec{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=\zug{g,d}\) for \(g \in G\)\@. Let \(w'_1\) be such that \(H(w_1,w'_1)\)\@. By the definition of \(H\), we have \(w'_1=\zug{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 \(\vec{x}\)\@. By the definition of \(S\), the state \(w_1\) has as successors the two states \(\zug{T_l(g),\swarrow}\) and \(\zug{T_r(g),\searrow}\)\@. Consider the state \(w_2=\zug{T_l(g),\swarrow}\)\@. Let \(w'_2=\zug{l_2,r_2,val_2,\swarrow}\) 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 \(\vec{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 \(\zug{T_r(g),\searrow}\) is similar\@. {\nopagebreakbeginpar\markendlst{Proof of Theorem 4}} \end{alabsubtext} \asection{4}{Verification of Fair Transition Systems} % \apar{4-1} In this section, we study the complexity of the fair-containment and the fair-simulation problems\@. We show that both problems are PSPACE-complete, and that the implementation complexity of both problems is significantly lower\@. \asubsection{4.1}{The Fair-Containment Problem} % \apar{4.1-1} We have seen that the containment problem is PSPACE-complete, and that 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\@. % \begin{alabsubtext}{Lemma}{1}{} \label{w to u} \({\cal W}(n,m) \goto {\cal U}(nm)\)\@. \end{alabsubtext} % \begin{alabsubtext}{Proof of Lemma}{1}{} \prooffontshape Consider a weakly fair transition system \(S=\zug{\Sigma, W, R, W_0, L, \alpha}\), with fairness condition \(\alpha=\{\zug{B_1,G_1},\dots,\zug{B_m,G_m}\}\)\@. For every \(W' \subseteq W\) and pair \(\zug{B_i,G_i}\), we have that \(W'\ \cap\ (W \setminus B_i) = \emptyset\) implies that \(W'\ \cap\ G_i \neq \emptyset\), if and only if \(W'\ \cap\ ((W \setminus B_i) \cup G_i) \neq \emptyset\)\@. Hence, a computation \(\pi\) is fair in \(S\) if and only if it is fair in all the unconditionally fair transition systems \(S_i=\zug{\Sigma,W,R,L,W_0,(W \setminus B_i) \cup G_i}\)\@. The result then follows from the known bound on the size of the product of unconditionally fair transition systems \cite{cj98-02-11}\@. {\nopagebreakbeginpar\markendlst{Proof of Lemma 1}} \end{alabsubtext} % \begin{alabsubtext}{Lemma}{2}{} \label{fo} Given a transition system \(S \in {\cal U}(n)\) with a state space \(W\) and a set \(B \subseteq W\), we can construct a transition system \(S' \in {\cal U}(2n)\) such that a trace \(\rho\) is accepted by \(S'\) if and only if there exists a fair computation \(\pi\) in \(S\) such that \(\mbox{{\em Inf\/}}(\pi) \cap B = \emptyset\) and \(L(\pi)=\rho\)\@. \end{alabsubtext} % \begin{alabsubtext}{Proof of Lemma}{2}{} \prooffontshape \apar{Proof of Lemma 2-1} The idea, as suggested in \cite{cj98-02-24}, is that the transition 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=\zug{\Sigma,W,R,L,W_0,\alpha}\), we define \(S'=\zug{\Sigma,W \times \{1,2\},R',L',W_0 \times \{1\},\alpha \times \{2\}}\), where: \begin{itemize} \item For every \(w\) and \(w'\) in \(W\) and \(i\) and \(i'\) in \(\{1,2\}\), we have that \\ \(R'(\zug{w,i},\zug{w',i'})\) if and only if \(R(w,w')\) and either: \begin{itemize} \item \(w' \not \in B\) and \(i \leq i'\), or \item \(w' \in B\) and \(i = i' = 1\)\@. \end{itemize} \item For every \(w \in W\) and \(i \in \{1,2\}\), we have \(L'(\zug{w,i})= L(w)\)\@. \end{itemize} % \apar{Proof of Lemma 2-2} We prove the correctness of our construction\@. Consider a trace \(\rho \in \Sigma^\omega\), and assume there exists a fair computation \(\pi=w_0,w_1,\dots\ \) in \(S\) such that \(\mbox{{\em Inf\/}}(\pi) \cap B = \emptyset\) and \(L(\pi)=\rho\)\@. Let \(w_i\) be such that for all \(j > i\), we have \(w_j \not \in B\)\@. The computation \(\pi' = \zug{w_0,1}, \zug{w_1,1}, \dots, \zug{w_i,1}, \zug{w_{i+1},2}, \zug{w_{i+2},2},\dots\ \) is then fair in \(S'\), and \(\rho\) is accepted by \(S'\)\@. Assume now that \(\rho\) is accepted by \(S'\); thus, there exists a computation \(\pi' = \zug{w_0,i_0}, \zug{w_1,i_1}, \dots\ \) in \(S'\) such that \(L(\pi')=\rho\) and \(\mbox{\emph{Inf\/}}(\pi') \cap (\alpha \times \{2\}) \neq \emptyset\)\@. As no transitions from states in \(W \times \{2\}\) to states in \(W \times \{1\}\) are possible, the computation \(\pi'\) eventually gets trapped in states in \(W \times \{2\}\)\@. Therefore, as no transitions to states in \(B \times \{2\}\) are possible, the computation \(\pi'\) visits states in \(B\) only finitely often\@. Finally, as \(R'(\zug{w,i},\zug{w',i'})\) only if \(R(w,w')\), the computation \(\pi=w_0, w_1,\dots\) 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'\)\@. {\nopagebreakbeginpar\markendlst{Proof of Lemma 2}} \end{alabsubtext} % \begin{alabsubtext}{Lemma}{3}{} \label{s to u} \({\cal S}(n,m) \goto {\cal U}(n 2^{O(m)})\)\@. \end{alabsubtext} % \begin{alabsubtext}{Proof of Lemma}{3}{} \prooffontshape \apar{Proof of Lemma 3-1} Consider a strongly fair transition system \(S=\zug{\Sigma,W,R,L,W_0,\alpha}\) with fairness condition \(\alpha=\{\zug{B_1,G_1},\dots,\zug{B_m,G_m}\}\)\@. With every \(I \subseteq \{1,\dots,m\}\), we associate an unconditionally fair transition system \(S_I\) that accepts the traces \(L(\pi)\) of \(S\) for which \(\mbox{\emph{Inf\/}}(\pi) \cap B_i \neq \emptyset\) and \(\mbox{\emph{Inf\/}}(\pi) \cap G_i \neq \emptyset\) for all \(i \in I\), and \(\mbox{\emph{Inf\/}}(\pi) \cap B_i = \emptyset\) for all \(i \not \in I\)\@. For that, we first define a weakly fair transition system \(S'_I=\zug{\Sigma,W,R,W_0,L,\alpha_I}\) that accepts the traces \(L(\pi)\) of \(S\) for which \(\mbox{\emph{Inf\/}}(\pi) \cap B_i \neq \emptyset\) and \(\mbox{\emph{Inf\/}}(\pi) \cap G_i \neq \emptyset\) for all \(i \in I\)\@. This is done by defining \(\alpha_I = \bigcup_{i \in I} \{\zug{W, B_i}, \zug{W,G_i}\}\)\@. If \(S \in {\cal S}(n,m)\), then \(S'_I \in {\cal W}(n,2m)\) and hence, by Lemma~1, we can translate it to \(S''_I \in {\cal U}(2nm)\)\@. Let \(B=\bigcup_{i \not \in I} B_i\)\@. Clearly, for every computation \(\pi\) of \(S''_I\), we have that \(\mbox{\emph{Inf\/}}(\pi) \cap B_i = \emptyset\) for all \(i \not \in I\) if and only if \(\mbox{\emph{Inf\/}}(\pi) \cap B = \emptyset\)\@. Hence, according to Lemma~2, we can construct the transition system \(S_I\) with \(4nm\) states\@. % \apar{Proof of Lemma 3-2} We prove that \({\cal T}(S)= \bigcup_{I \subseteq \{1,2,\dots,m\}} {\cal T}(S_I)\)\@. A computation \(\pi\) is fair in \(S\) if for every pair \(\zug{B_i,G_i}\), either \(\mbox{\emph{Inf\/}}(\pi) \cap B_i = \emptyset\), or both \(\mbox{\emph{Inf\/}}(\pi) \cap B_i \neq \emptyset\) and \(\mbox{\emph{Inf\/}}(\pi) \cap G_i \neq \emptyset\)\@. Let \(f(\pi) \subseteq \{1,\dots,m\}\) be such that \(\mbox{\emph{Inf\/}}(\pi) \cap B_i \neq \emptyset\) if and only if \(i \in f(\pi)\)\@. It is easy to see that \(\pi\) is fair in \(S\) if and only if \(\pi\) is fair in \(S_{f(\pi)}\)\@. The lemma now follows from the fact that union is easy for transition systems (e.g., by defining the initial set as union of the initial sets of the underlying systems)\@. {\nopagebreakbeginpar\markendlst{Proof of Lemma 3}} \end{alabsubtext} % \begin{alabsubtext}{Theorem}{5}{} \label{cont comp} The fair-containment problem \({\cal T}(S) \subseteq {\cal T}(S')\) for \(S \in \bigcup\{{\cal U,W,S}\}\) and \(S' \in \bigcup\{{\cal U,W,S}\}\) is PSPACE-complete\@. \end{alabsubtext} % \begin{alabsubtext}{Proof of Theorem}{5}{} \prooffontshape \apar{Proof of Theorem 5-1} As there are three possible types for the transition 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: \begin{enumerate} \item Translate the transition system \(S\) to an unconditionally fair transition system \(S_U\)\@. \item Construct an unconditionally fair transition system \(\overline{S'_U}\) that complements the transition system \(S'\)\@. \item Check \({\cal T}(S_U) \cap {\cal T}(\overline{S'_U})\) for emptiness\@. \end{enumerate} % \apar{Proof of Theorem 5-2} This is how we perform step 1 for the three possible types of \(S\): \begin{enumerate} \item \({\cal U}(n) \goto {\cal U}(n)\)\@. \item \({\cal W}(n,m) \goto {\cal U}(nm)\) [Lemma~1]\@. \item \({\cal S}(n,m) \goto {\cal U}(n 2^{O(m)})\) [Lemma~3]\@. \end{enumerate} % \apar{Proof of Theorem 5-3} This is how we perform step 2 for the three possible types of \(S'\): \begin{enumerate} \item \(\overline{{\cal U}(n)} \goto {\cal U}(2^{O(n \log n)})\) \cite{cj98-02-38}\@. \item \(\overline{{\cal W}(n,m)} \goto \overline{{\cal U}(nm)} \goto {\cal U}(2^{O(nm \log (nm))})\) \cite{cj98-02-38}\@. \item \(\overline{{\cal S}(n,m)} \goto {\cal S}(2^{O(nm \log(nm))},nm) \goto {\cal U}(2^{O(nm \log(nm))})\) \cite{cj98-02-39}\@. \end{enumerate} % \apar{Proof of Theorem 5-4} For all three types of \(S\), going to \(S_U\) involves an at-most exponential 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'\) \cite{cj98-02-11}\@. By \cite{cj98-02-45}, the nonemptiness problem for unconditionally fair transition systems is in NLOGSPACE\@. Hence, as NLOGSPACE = co-NLOGSPACE, checking the product of \(S_U\) and \(\overline{S'_U}\) for emptiness can be done in space polynomial in their sizes\@. % \apar{Proof of Theorem 5-5} Hardness in PSPACE follows from the PSPACE lower bound for trace containment (Theorem~1)\@. Indeed, we can easily define a fairness condition for which all the computations are fair (\(\alpha=W\) for unconditional fairness and \(\alpha = \emptyset\) for weak and strong fairness)\@. {\nopagebreakbeginpar\markendlst{Proof of Theorem 5}} \end{alabsubtext} \asubsubsection{4.1.1}{Implementation Complexity} % \apar{4.1.1-1} Recall that our main concern is the complexity in terms of the (much larger) implementation\@. We now turn to consider the implementation complexity of fair containment\@. % \begin{alabsubtext}{Theorem}{6}{} \label{cont imp comp} The implementation complexity of checking \({\cal T}(S) \subseteq {\cal T}(S')\) for \(S \in \bigcup\{{\cal U,W}\}\) and \(S' \in \bigcup\{{\cal U,W,S}\}\) is NLOGSPACE-complete\@. \end{alabsubtext} % \begin{alabsubtext}{Proof of Theorem}{6}{} \prooffontshape In the case where \(S \in \bigcup\{{\cal 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)\@. {\nopagebreakbeginpar\markendlst{Proof of Theorem 6}} \end{alabsubtext} % \apar{4.1.1-2} So, for the case where the implementation does not use the strong fairness 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\@. % \begin{alabsubtext}{Lemma}{4}{} \label{sw intersection} For \(S_1 \in {\cal S}(n_1,m)\) and \(S_2 \in {\cal U}(n_2)\), there exists \(S \in {\cal S}(n_1 n_2,m+1)\) such that \({\cal T}(S)={\cal T}(S_1) \cap {\cal T}(S_2)\)\@. \end{alabsubtext} % \begin{alabsubtext}{Proof of Lemma}{4}{} \prooffontshape Given a strongly fair transition system \(S_1=\zug{\Sigma,W_1,R_1,W_1^0,L_1,\alpha}\) and an unconditionally fair transition system \(S_2=\zug{\Sigma,W_2,R_2,W_2^0,L_2,\beta}\), consider the strongly fair transition system \(S=\zug{\Sigma,W,R,W_0,L,\gamma}\), where: \begin{itemize} \item \(W=\{\zug{w_1,w_2}\): \(w_1 \in W_1, w_2 \in W_2\), and \(L_1(w_1)=L_2(w_2)\}\), \item \(R(\zug{w_1,w_2}, \zug{w'_1,w'_2})\) if and only if \(R_1(w_1,w'_1)\) and \(R_2(w_2,w'_2)\), \item \(W_0=(W_1^0 \times W_2^0) \cap W\), \item for every \(\zug{w_1,w_2} \in W\), we have \(L(\zug{w_1,w_2})= L_1(w_1)\), and \item \(\gamma \subseteq 2^W \times 2^W\) is such that \(\zug{G,B} \in \gamma\) if and only if either there exists \(\zug{G',B'} \in \alpha\) for which \(G=(G' \times W_2) \cap W\) and \(B=(B' \times W_2) \cap W\), or \(G=W\) and \(B=(W_1 \times \beta) \cap W\)\@. \end{itemize} 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\@. {\nopagebreakbeginpar\markendlst{Proof of Lemma 4}} \end{alabsubtext} % \begin{alabsubtext}{Theorem}{7}{} \label{Streett imp ub} The implementation complexity of checking \({\cal T}(S) \subseteq {\cal T}(S')\) for \(S \in {\cal S}\) and \(S' \in \bigcup\{{\cal U,W,S}\}\) is in PTIME\@. \end{alabsubtext} % \begin{alabsubtext}{Proof of Theorem}{7}{} \prooffontshape 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 \({\cal T}(S) \cap {\cal T}(\overline{S'_U})\)\@. The nonemptiness problem for strongly fair transition systems can be solved in polynomial time \cite{cj98-02-12}\@. Hence, by Lemma~4, we can check the nonemptiness of the intersection in time polynomial in the size of \(S\)\@. {\nopagebreakbeginpar\markendlst{Proof of Theorem 7}} \end{alabsubtext} % \apar{4.1.1-3} Note that the algorithm presented in the proof of Theorem~7 uses time 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 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\@. % \begin{alabsubtext}{Theorem}{8}{} \label{Streett nonemptiness lb} The nonemptiness problem for strongly fair transition systems is PTIME-hard\@. \end{alabsubtext} % \begin{alabsubtext}{Proof of Theorem}{8}{} \prooffontshape \apar{Proof of Theorem 8-1} We do a reduction from propositional anti-Horn satisfiability (PAHS)\@. Propositional anti-Horn clauses are obtained from propositional Horn clauses by replacing each proposition \(p\) with \(\neg p\)\@. Thus, a propositional anti-Horn clause is either of the form \(p \rightarrow q_1 \vee \dots \vee q_n\) (an empty disjunction is equivalent to false) or of the form \(q_1 \vee \dots \vee q_n\)\@. As propositional Horn satisfiability is PTIME-complete \cite{cj98-02-36}, then clearly, so is PAHS\@. % \apar{Proof of Theorem 8-2} Given an instance \(I\) of PAHS, we construct the transition system: \[S_I=\zug{\{a\},W ,W \times W,W,L,\alpha}\] where: \begin{itemize} \item \(W=Q \times \{s\}\), where \(Q\) is the set of all the propositions in \(I\), and \(s \not \in Q\), \item \(L\) maps all states to \(a\), and \item \(\alpha\) is the strongly fair condition defined as follows: \begin{itemize} \item for a clause \(p \rightarrow q_1 \vee \dots \vee q_n\) in \(I\), we have \(\zug{\{p\}, \{q_1,\dots,q_n\}}\) in \(\alpha\), and \item for a clause \(q_1 \vee \dots \vee q_n\) in \(I\), we have \(\zug{W, \{q_1, \dots, q_n\}}\) in \(\alpha\)\@. \end{itemize} \end{itemize} % \apar{Proof of Theorem 8-3} Each computation of \(S_I\) induces an assignment to the propositions in \(I\)\@. A proposition is assigned \emph{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 \emph{false})\@. The definition of \(\alpha\) thus guarantees that \(I\) is satisfiable if and only if \(S_I\) is nonempty\@. {\nopagebreakbeginpar\markendlst{Proof of Theorem 8}} \end{alabsubtext} % \apar{4.1.1-4} We note that the nonemptiness problem for strongly fair transition systems is already PTIME-hard for systems with pairs of a constant size\@. In 3-PAHS, all the clauses are of the form \(p \rightarrow q_1 \vee 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 \(\zug{\{q\},\{p\}}\), one for each \(q \in W \setminus \{p\}\)\@. % \apar{4.1.1-5} Therefore, unlike unconditionally or weakly fair transition systems, for 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\@. % \begin{alabsubtext}{Theorem}{9}{} \label{Streett imp tb} The implementation complexity of checking \({\cal T}(S) \subseteq {\cal T}(S')\) for \(S \in {\cal S}\) and \(S' \in \bigcup\{{\cal U,W,S}\}\) is PTIME-complete\@. \end{alabsubtext} \asubsection{4.2}{The Fair-Simulation Problem} \asubsubsection{4.2.1}{The Upper Bound} % \begin{alabsubtext}{Theorem}{10}{} \label{fs ub} The fair-simulation problem \(S \leq S'\) for \(S \in \bigcup\{{\cal U,W,S}\}\) and \(S' \in \bigcup\{{\cal U,W,S}\}\) is in PSPACE\@. \end{alabsubtext} % \begin{alabsubtext}{Proof of Theorem}{10}{} \prooffontshape \apar{Proof of Theorem 10-1} Given \(S=\zug{\Sigma,W,R,W_0,L,\alpha}\) and \(S'=\zug{\Sigma,W',R',W'_0,L',\alpha'}\), 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 \in W_0\) there exists \(w' \in W'_0\) such that \(H(w,w')\)\@. We then check (also easily) that for all \(\zug{w,w'} \in H\), we have \(L(w) = L(w')\)\@. It is left to check that for all \(\zug{w,w'} \in H\), the pair \(\zug{w,w'}\) is good in \(H\)\@. To do this, we define, for every \(\zug{w,w'} \in 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 \(\pi\) in \(W^\omega\) for which there exists a fair \(w'\)-computation \(\pi'\) in \(S'\) such that \(H(\pi,\pi')\)\@. Clearly, the pair \(\zug{w,w'}\) is good in \(H\) if and only if \({\cal T}(A_w) \subseteq {\cal T}(U_{w'})\)\@. % \apar{Proof of Theorem 10-2} We define \(A_w\) and \(U_{w'}\) as follows\@. The transition system \(A_w\) does nothing but trace the \(w\)-computations of \(S\), accepting those that satisfy \(S\)'s acceptance condition\@. Formally, \(A_w=\zug{W,W,R,\{w\},L'',\alpha}\), where for all \(u \in W\), we have \(L''(u)=u\)\@. % \apar{Proof of Theorem 10-3} The transition system \(U_{w'}\) has members of \(H\) as its set of states\@. Thus, 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 \(\pi'' \in H^\omega\), whose \(W'\) elements form the computation \(\pi' \in (W')^{\omega}\) and whose states are labeled with \(\pi \in W^\omega\), satisfies \(H(\pi,\pi')\)\@. Formally, \(U_{w'}=\zug{W,H,R'',W''_0,L''',\alpha''}\), where: \begin{itemize} \item \(R''\) is adjusted to the new state space; i.e., \(R''(\zug{t,t'},\zug{q,q'})\) if and only if \(R'(t',q')\), \item \(W''_0=(W \times \{w'\}) \cap H\), \item for every \(\zug{t,t'} \in H\), we have \(L'''(\zug{t,t'})=t\), and \item \(\alpha''\) is also adjusted to the new state space; i.e., each set \(B \subseteq W'\) in \(\alpha'\) is replaced by the set \((W \times B) \cap H\) in \(\alpha''\)\@. \end{itemize} 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'}\)\@. % \apar{Proof of Theorem 10-4} According to Theorem~5, checking that \({\cal T}(A_w) \subseteq {\cal T}(U_{w'})\) can be done in space polynomial in the sizes of \(A_w\) and \(U_{w'}\), thus polynomial in the sizes of \(S\) and \(S'\)\@. {\nopagebreakbeginpar\markendlst{Proof of Theorem 10}} \end{alabsubtext} % \apar{Proof of Theorem 10-5} We note that our algorithm can be easily adjusted to check \(S\) and \(S'\) for fair bisimulation\@. \asubsubsection{4.2.2}{The Lower Bound} % \apar{4.2.2-1} For a transition system \(S=\zug{\Sigma,W,R,W_0,L,\alpha}\), we say that \(S\) is \emph{universal\/} if and only if \({\cal T}(S)=\Sigma^\omega\)\@. The {\em 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 \(S\) is universal \cite{cj98-02-35}\@. 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\@. % \begin{alabsubtext}{Theorem}{11}{} The universality problem, \(L(S)=\Sigma^\omega\) for \(S \in \bigcup\{{\cal U,W,S}\}\), is PSPACE-hard\@. \end{alabsubtext} % \begin{alabsubtext}{Proof of Theorem}{11}{} \prooffontshape \apar{Proof of Theorem 11-1} We do a reduction from polynomial-space Turing 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\@. % \apar{Proof of Theorem 11-2} We now give the details of the construction of \(S_T\)\@. Let \(T=\zug{\Gamma,Q,\rightarrow,q_0,F}\), where \(\Gamma\) is the alphabet, \(Q\) is the set of states, \(\rightarrow \subseteq Q \times \Gamma \times Q \times \Gamma \times \{L,R\}\) is the transition relation (we use \((q,a) \rightarrow (q',b,\Delta)\) 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 \(\Delta\)), \(q_0\) is the initial state, and \(F \subseteq Q\) is the set of accepting states\@. We encode a configuration of \(T\) by a string \(\# \gamma_1 \gamma_2 \dots (q,\gamma_i) \dots \gamma_{s(n)}\)\@. That is, a configuration starts with \(\#\), and all its other letters are in \(\Gamma\), except for one letter in \(Q \times \Gamma\)\@. The meaning of such a configuration is that the \(j^\mathrm{th}\) cell in \(T\), for \(1 \leq j \leq s(n)\), is labeled \(\gamma_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 \dots b\) (with \(s(n)-1\) occurrences of \(b\)s) where \(b\) stands for an empty cell\@. We can then encode a computation of \(T\) by a sequence of configurations\@. % \apar{Proof of Theorem 11-3} Let \(\Sigma=\{\#\} \cup \Gamma \cup (Q \times \Gamma)\) and let \(\# \sigma_1 \dots \sigma_{s(n)} \# \sigma'_1 \dots \sigma'_{s(n)}\) be two successive configurations of \(T\)\@. We also set \(\sigma_0\), \(\sigma'_0\), and \(\sigma_{s(n)+1}\) to \(\#\)\@. For each triple \(\zug{\sigma_{i-1},\sigma_i,\sigma_{i+1}}\) with \(1 \leq i \leq s(n)\), we know by the transition relation of \(T\) what \(\sigma'_i\) should be\@. In addition, the letter \(\#\) should repeat exactly every \(s(n)+1\) letters\@. Let \(next(\zug{\sigma_{i-1},\sigma_i,\sigma_{i+1}})\) denote our expectation for \(\sigma'_i\)\@. That is: \begin{itemize} \item \(\mathit{Next}(\zug{\gamma_{i-1},\gamma_i,\gamma_{i+1}})= \mathit{next}(\zug{\#,\gamma_i,\gamma_{i+1}})= \mathit{next}(\zug{\gamma_{i-1},\gamma_i,\#})= \gamma_i\)\@. \item \(\mathit{Next}(\zug{(q,\gamma_{i-1}),\gamma_i,\gamma_{i+1}})= \mathit{next}(\zug{(q,\gamma_{i-1}),\gamma_i,\#})=\) \begin{center} \(\left\{ \begin{array}{ll} \gamma_i & \mbox{if \((q,\gamma_{i-1}) \rightarrow (q',\gamma'_{i-1},L)\)}\\ (q',\gamma_i) & \mbox{if \((q,\gamma_{i-1}) \rightarrow (q',\gamma'_{i-1},R)\)} \end{array} \right.\) \end{center} \item \(\mathit{Next}(\zug{\gamma_{i-1},(q,\gamma_{i}),\gamma_{i+1}})= \mathit{next}(\zug{\#,(q,\gamma_{i}),\gamma_{i+1}})=\)\\ \(\mathit{next}(\zug{\gamma_{i-1},(q,\gamma_{i}),\#})= \gamma'_i\) where \((q,\gamma_{i}) \rightarrow (q',\gamma'_{i},\Delta)\)\@.\footnote{ We 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,\gamma_{i}) \rightarrow (q',\gamma'_{i},L)\) and the dual case where \((i=2^n)\) and \((q,\gamma_{i}) \rightarrow (q',\gamma'_{i},R)\) are not possible\@.} \item \(\mathit{Next}(\zug{\gamma_{i-1},\gamma_i,(q,\gamma_{i+1})})= \mathit{next}(\zug{\#,\gamma_i,(q,\gamma_{i+1})})=\) \begin{center} \(\left\{ \begin{array}{ll} \gamma_i & \mbox{if \((q,\gamma_{i+1}) \rightarrow (q',\gamma'_{i+1},R)\)}\\ (q',\gamma_i) & \mbox{if \((q,\gamma_{i+1}) \rightarrow (q',\gamma'_{i},L)\)} \end{array} \right.\) \end{center} \item \(\mathit{Next}(\zug{\sigma_{s(n)},\#,\sigma'_1})=\#\)\@. \end{itemize} % Consistency with \(\mathit{next}\) gives us a necessary condition for a trace to encode a legal computation\@. In addition, the computation should start with the initial configuration\@. % \apar{Proof of Theorem 11-4} To check consistency with \(next\), \(S_T\) can use its nondeterminism and guess when there is a violation of \(next\)\@. Thus, \(S_T\) guesses \(\zug{\sigma_{i-1},\sigma_i,\sigma_{i+1}} \in \Sigma^3\), guesses a position in the trace, checks whether the three letters to be read starting this position are \(\sigma_{i-1},\sigma_i\), and \(\sigma_{i+1}\), and checks whether \(next(\zug{\sigma_{i-1},\sigma_i,\sigma_{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 \dots b\)\@. Finally, checking whether a legal computation is rejecting is also easy; the final configuration has to be rejecting (one with \(q \not \in F\))\@. {\nopagebreakbeginpar\markendlst{Proof of Theorem 11}} \end{alabsubtext} % \apar{4.2.2-2} We would like to do a similar reduction to prove that the fair-simulation problem is PSPACE-hard\@. For every alphabet \(\Sigma\), let \(S_\Sigma\) be the transition system \(\zug{\Sigma,\Sigma,\Sigma \times \Sigma,\Sigma,L_\Sigma,\alpha}\), where \(L_\Sigma(\sigma)=\sigma\) and \(\alpha\) is such that all the computations of \(S_\Sigma\) are fair\@. That is, \(S_\Sigma\) is a universal transition system in which each state is associated with a letter \(\sigma \in \Sigma\) and \({\cal T}(S_\Sigma^\sigma)=\sigma \cdot \Sigma^\omega\)\@. For example, \(S_{\{a,b\}}\) is the transition system \(S\) in Figure~1\@. It is easy to see that a transition system \(S\) over \(\Sigma\) is universal if and only if \({\cal T}(S_\Sigma) \subseteq {\cal T}(S)\)\@. It is not true, however, that \(S\) is universal if and only if \(S_\Sigma \leq S\)\@. For example, the transition system \(S'\) in Figure~1 is universal, yet \(S_{\{a,b\}} \not \leq 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 \({\cal T}(S_T^w)=L(w) \cdot \Sigma^\omega\)\@. For such \(S_T\), we do have that \(S_T\) is universal if and only if \(S_\Sigma \leq S_T\)\@. Indeed, a relation that maps a state \(\sigma\) of \(S_\Sigma\) to all the states of \(S_T\) that are labeled with \(\sigma\) is a fair simulation\@. % \begin{alabsubtext}{Theorem}{12}{} \label{fs lb} The fair-simulation problem \(S \leq S'\) for \(S \in \bigcup\{{\cal U,W,S}\}\) and \(S' \in \bigcup\{{\cal U,W,S}\}\) is PSPACE-hard\@. \end{alabsubtext} % \begin{alabsubtext}{Proof of Theorem}{12}{} \prooffontshape \apar{Proof of Theorem 12-1} We prove hardness for the case where \(S'\) is a strongly fair transition system with three pairs\@. The other cases then follow from the linear translation of \(S'\) to any \(S' \in \bigcup\{{\cal 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\@. % \apar{Proof of Theorem 12-2} We now define a strongly fair transition system \(S_T\) as the union of two strongly fair transition systems, \(S_T^1\) and \(S_T^2\), with the following behaviors\@. Reading a trace \(\rho\), the fair transition system \(S_T^1\) checks for a violation of the transition relation of \(T'\) in \(\rho\) (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 \(\zug{W_1,G}\), where \(W_1\) is the set of states in \(S_T^1\) and \(G\) is a clique of \(|\Sigma|\) states, each labeled with a different letter, which \(S_T^1\) enters once it sees a violation of \(\mathit{next}\)\@. Reading a trace \(\rho\), the fair transition system \(S_T^2\) checks for the occurrence of the initial configuration in \(\rho\)\@. 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 \(\zug{B,\emptyset}\), where \(B\) is a clique of \(|\Sigma|\) 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 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 \(\zug{W_1,G}\) and \(\zug{B,\emptyset}\)\@. % \apar{Proof of Theorem 12-3} It follows that the fair transition system \(S_T\) accepts a trace \(\rho\) if \(\rho\) violates \(next\) or never visits the initial configuration\@. Thus, \(S_T\) does not accept a trace \(\rho\) if and only if \(\rho\) 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\@. % \apar{Proof of Theorem 12-4} We want, however, more than a universality test\@. We want to define \(S_T\) in such a way that if it is indeed universal, then for each of its states \(w\), we have \({\cal T}(S_T^w)=L(w) \cdot \Sigma^\omega\)\@. Let \(S_T=\zug{\Sigma,W,R,W_0,L,\alpha}\)\@. We assume that \(R \cap (W \times W_0)=\emptyset\)\@. 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=\zug{\Sigma,W,R \cup (W \times W_0),W_0,L,\alpha \cup \zug{W_0,\emptyset}}\)\@. We claim the following: \begin{alabsubtext}{Claim}{1}{} \(S'_T\) is universal if and only if for each \(\sigma \in \Sigma\) we have \(w_0 \in W_0\) with \(L(w_0)=\sigma\), and for each \(w \in W\), we have \({\cal T}(S_T^w)=L(w) \cdot \Sigma^\omega\)\@. \end{alabsubtext} % \begin{alabsubtext}{Claim}{2}{} \(S_T\) is universal if and only if \(S'_T\) is universal\@. \end{alabsubtext} % \apar{Proof of Theorem 12-5} Claim~1 is immediate, and we prove here Claim~2\@. Clearly, every computation \(\pi\) of \(S_T\) is a computation in \(S'_T\)\@. Since no computation in \(S_T\) visits \(W_0\) more than once, adding the pair \(\zug{W_0,\emptyset}\) to the acceptance condition \(\alpha\), we still have that if \(\pi\) is fair in \(S_T\), then it is also fair in \(S'_T\)\@. Hence \({\cal T}(S_T) \subseteq {\cal T}(S'_T)\); thus, if \(S_T\) is universal, so is \(S'_T\)\@. Assume now that \(S_T\) is not universal\@. Consider a trace \(\rho\) not accepted by \(S_T\)\@. Recall that \(\rho\) does not violate \(\mathit{next}\), and it visits the initial configuration of \(T\)\@. In other words, \(\rho\) 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 \(\rho\) are of that special form! Hence, if \(\rho\) is not accepted by \(S_T\), all its suffixes are also not accepted by \(S_T\)\@. We show that this implies that \(\rho\) is not accepted by \(S'_T\) too\@. Assume, by way of contradiction, that \(\rho\) is accepted by \(S'_T\)\@. Let \(\pi=w_0,w_1,\dots\ \) by a fair computation in \(S'_T\), with \(L(\pi)=\rho\)\@. By the acceptance condition of \(S'_T\), there exists \(i \geq 0\) such that \(w_i \in W_0\), and for all \(j > i\), we have \(W_j \not \in W_0\)\@. Hence, for all \(j \geq i\), we have \(R(w_j,w_{j+1})\)\@. Therefore, the computation \(\pi^i=w_i,w_{i+1},\dots\) is a fair computation in \(S_T\), and the trace \(L(\pi^i)\) is accepted by \(S_T\), contradicting the fact it is a suffix of a trace not accepted by \(S_T\)\@. % \apar{Proof of Theorem 12-6} As discussed above, Claims~1 and~2 now imply that \(S_\Sigma \leq S'_T\) if and only if \(S_T\) is universal; thus \(S_\Sigma \leq S'_T\) if and only if \(T\) does not accept the empty tape\@. Because the fairness condition of \(S_\Sigma\) can be specified in terms of either unconditional, weak, or strong fairness, we are done\@. {\nopagebreakbeginpar\markendlst{Proof of Theorem 12}} \end{alabsubtext} % \apar{4.2.2-3} Theorems~10 and~12 together imply the following\@. % \begin{alabsubtext}{Theorem}{13}{} \label{fs c} The fair-simulation problem \(S \leq S'\) for \(S \in \bigcup\{{\cal U,W,S}\}\) and \(S' \in \bigcup\{{\cal U,W,S}\}\) is PSPACE-complete\@. \end{alabsubtext} \asubsubsection{4.2.3}{Implementation Complexity} % \apar{4.2.3-1} As our discussions thus far show, fair simulation and fair containment have 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\@. % \begin{alabsubtext}{Theorem}{14}{} \label{imp fs tb} The implementation complexity of checking \(S \leq S'\) for \(S \in \bigcup\{{\cal U,W,S}\}\) and \(S' \in \bigcup\{{\cal U,W,S}\}\) is PTIME-complete\@. \end{alabsubtext} % \begin{alabsubtext}{Proof of Theorem}{14}{} \prooffontshape \apar{Proof of Theorem 14-1} We start with the upper bound\@. Consider the algorithm 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 \in \bigcup\{{\cal U,W}\}\), and is PTIME for \(S \in {\cal 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 \cite{cj98-02-33}\@. Let \[H_0=\{\zug{w,w'}: w \in W, w' \in W', \mbox{ and } L(w) =L(w')\}\] Thus, \(H_0\) is the maximal relation that satisfies condition 1 of fair simulation\@. Consider the monotonic function \(f: 2^{W \times W'} \rightarrow 2^{W \times W'}\), where \[f(H)=H \cap \{\zug{w,w'}: \zug{w,w'} \mbox{ is good in }H\}\] Thus, \(f(H)\) contains all the pairs in \(H\) that are good with respect to the relation \(H\)\@. Let \(H^\star\) be the greatest fixed point of \(f\) when restricted to pairs in \(H_0\)\@. That is, \(H^\star= \nu z. H_0 \cap f(z)\)\@. % \apar{Proof of Theorem 14-2} We now prove that \(S \leq S'\) if and only if for every \(w \in W_0\), we have \((\{w\} \times W'_0)\ \cap\ H^\star \neq \emptyset\)\@. First, as \(H^\star\) is a fair-simulation relation, the direction from right to left is immediate from the definition of fair simulation\@. Assume that \(S \leq S'\)\@. Then, there exists a fair-simulation relation \(H'\) such that for every \(w \in W_0\), we have \((\{w\} \times W'_0) \cap H' \neq \emptyset\)\@. Let \(H_i=f^i(H_0)\)\@. We show that for every \(i \geq 0\) we have \(H' \subseteq H_i\)\@. Thus, in particular, \(H' \subseteq H^\star\), and we are done\@. The proof proceeds by induction on \(i\)\@. First, since \(H'\) satisfies condition 2 of fair-simulation relations, then clearly \(H' \subseteq H_0\)\@. Assume that \(H' \subseteq H_i\), and assume by way of contradiction that \(H' \not \subseteq H_{i+1}\)\@. Then there exists \(\zug{w,w'} \in H' \setminus H_{i+1}\)\@. Since \(H' \subseteq H_i\), it follows that the pair \(\zug{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\@. % \apar{Proof of Theorem 14-3} We now consider the complexity of calculating \(H^\star\)\@. Since \(W \times W'\) is 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 \times W'|}\) candidate relations for simulation, we actually check at most \(|W \times 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\@. % \apar{Proof of Theorem 14-4} Hardness in PTIME follows from the lower bound in Theorem~4\@. {\nopagebreakbeginpar\markendlst{Proof of Theorem 14}} \end{alabsubtext} \asection{5}{Discussion} % \apar{5-1} We have examined the trace-based and the tree-based approaches to implementation from a complexity-theoretic point of view\@. Our results show that when we model the specification and the implementation by fair transition 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\@. % \apar{5-2} It is interesting to compare our results with the known complexities of LTL and \actlsr 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 \actlsr model checking\@. All four problems are PSPACE-complete \cite{cj98-02-40,cj98-02-12}\@. The model-checking algorithm of \actlsr uses as a subroutine the model-checking algorithm of LTL \cite{cj98-02-12}\@. In a similar manner, our fair-simulation 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 \actlsr is NLOGSPACE-complete \cite{cj98-02-44,cj98-02-07}\@. In contrast, we see here that implementation is easier in the trace-based approach\@. % \apar{5-3} Our results are summarized in Table~1\@. All the complexities in the table denote tight bounds\@. % \begin{table}[htb] \small \begin{center} \begin{tabular}{l||l|l|l|l|} & & Implementation & & Implementation \\ & & Complexity & & Complexity \\ & Fair & of Fair & Fair & of Fair \\ & Containment & Containment & Simulation & Simulation \\ \hline \hline \(S\) and \(S'\) with & PSPACE & NLOGSPACE & PTIME & PTIME \\ No Fairness & [Theorem 1] & [Theorem 2] & [Theorem 3] & [Theorem 4] \\ \hline \(S \in \bigcup\{{\cal U,W}\}\) and & PSPACE & NLOGSPACE & PSPACE & PTIME \\ \(S' \in \bigcup\{{\cal U,W,S}\}\) & [Theorem 5] & [Theorem 6] & [Theorem 13] & [Theorem 14] \\ \hline \(S \in {\cal S}\) and & PSPACE & PTIME & PSPACE & PTIME \\ \(S' \in \bigcup\{{\cal U,W,S}\}\) & [Theorem 5] & [Theorem 9] & [Theorem 13] & [Theorem 14] \\ \hline \end{tabular} \end{center} \normalsize \caption{Is \(S\) a correct implementation of \(S'\)?} \label{table} \end{table} % \end{articletext} % \bibliographystyle{alpha} \bibliography{cj98-02} % \end{document}