%\documentclass[10pt]{llncs}
%\documentclass[runningheads,a4paper]{llncs}
\documentclass[]{elsarticle}

\usepackage{makeidx}
\usepackage{times,amssymb}
\usepackage{latexsym}
\usepackage{url} 

%\usepackage[dvips]{graphicx} 
%\usepackage[pdftex]{graphicx} 

%\ifx\pdftexversion\undefined 
%\usepackage[dvips]{graphicx} 
%\else
%\input supp-pdf.tex
%\usepackage[pdftex]{graphicx} 
%\DeclareGraphicsRule{*}{mps}{*}{} 
%\fi

\input supp-pdf.tex
\usepackage{graphicx} 
\DeclareGraphicsRule{*}{mps}{*}{} 

\usepackage{amsmath}
\usepackage{textcomp}
\usepackage{mathrsfs}
\usepackage{epstopdf}
\usepackage{subfig}

%\usepackage{txfonts}
%\usepackage{fullpage}
%\renewcommand{\baselinestretch}{1.5}
\input{style.tex}

% TODO: Extend the theory to grafting, non-fair EG, complete proofs of
% correctness, method of extracting a d-diagram from a computation
%
% NOTE: Need to quantify the class of properties we can detect

%\bibliographystyle{splncs}

% adjust the width and height

%\setlength{\textwidth}{6.7in}
%\setlength{\textheight}{10.15in}

%\setlength{\textheight}{8.5in}

% adjust the margins
% use the following formulae
% sidemargin: 0.5*(\paperwidth - \textwidth) - 1.0in
% topmargin: 0.5*(\paperheight - 
%                 (\textheight + \headheight + \headsep + \footheight))
%            - 1.0in
 

%\setlength{\oddsidemargin}{0.0in}
%\setlength{\evensidemargin}{\oddsidemargin}


%\setlength{\headheight}{0in}
%\setlength{\headsep}{0in}
 %\setlength{\footheight}{0in}
%\setlength{\topmargin}{0.3in}
 %\setlength{\parindent}{1pc}


% adjust the parameters

% \renewcommand{\baselinestretch}{.96}


% allow figures to occupy the whole page

\renewcommand{\topfraction}{1}
\renewcommand{\textfraction}{0}

% reduce the spacing between text and figure

% \setlength{\textfloatsep}{12pt plus 2pt minus 2pt}


% specify the path for the figures

\graphicspath{{figures/}}
\newcommand{\h}{\hspace*{0.2in}}


% useful commands and environments



\begin{document}

%\date{}
\title{Modeling, Analyzing and Slicing Periodic Distributed Computations\tnoteref{t1}}
\tnotetext[t1]{part of the work was performed at the University of Texas
at Austin supported in part by the
NSF Grants CNS-0718990, CNS-1115808, Texas Education Board Grant 781, SRC Grant 2006-TJ-1426,
    and Cullen Trust for Higher Education Endowed Professorship.
} 

%Monitoring for Violation of Liveness Properties in Distributed Systems

%make title bold and 14 pt font (Latex default is non-bold, 16pt) 
%\author{Anurag Agarwal \and Vijay K. Garg\\
%{University of Texas at Austin, Austin TX~~78712-0233}
%}
%\email{anurag@cs.utexas.edu \and garg@ece.utexas.edu}

%\begin{tabular}[t]{c@{\extracolsep{8em}}c c} 
%Anurag Agarwal  & Vijay K. Garg\thanks{part of the work was performed at the University of Texas at Austin supported in part by the NSF Grant CNS-0509024, Texas Education Board Grant 781, SRC Grant 2006-TJ-1426, and Cullen Trust for Higher Education Endowed Professorship.} & Vinit Ogale \\
       %Department of Computer Sciences & IBM India Research Lab & Department of Electrical and Computer Engg. \\
       %University of Texas at Austin & Vasant Kunj & University of Texas at Austin \\
        %Austin, TX~~78712-0233 & Delhi, India & Austin, TX~~78712-1084 \\
        %{\sf anurag@cs.utexas.edu} & {\sf vijgarg1@in.ibm.com} & {\sf ogale@ece.utexas.edu} \\
%\end{tabular}

\author{
Vijay K. Garg\corref{cor1}}
\ead{garg@ece.utexas.edu}
%\fntext[fn1]{part of the work was performed at the University of Texas
%at Austin supported in part by the
%NSF Grants CNS-0509024, CNS-0718990, Texas Education Board Grant 781, SRC Grant 2006-TJ-1426,
%    and Cullen Trust for Higher Education Endowed Professorship.
%} 
\cortext[cor1]{Corresponding author}

\author{Anurag Agarwal\fnref{fn1}}
\fntext[fn1]{currently at Google}
%{\sf anurag.agarwal@gmail.com}\\
%{\sf garg@ece.utexas.edu}\\

\author{Vinit Ogale\fnref{fn2}}
\fntext[fn2]{currently at Microsoft}
\address{
%Department of Electrical and Computer Engineering \\
The University of Texas at Austin \\
Austin, TX 78712-1084, USA \\
%{\sf ogale@ece.utexas.edu}
%{\sf garg@ece.utexas.edu}\\
%{\sf vinitog@microsoft.com}
}

%%\date{}
%\maketitle
%\thispagestyle{empty}
\begin{abstract}
  The earlier work on predicate detection has assumed that the given computation
  is finite.  Detecting violation of a liveness predicate requires that the
  predicate be evaluated on an infinite computation. In this work, we develop
 the theory and  associated algorithms for predicate detection in infinite runs. In practice,
  an infinite run can be determined in finite time 
%only 
if it consists of a recurrent
  behavior with some finite prefix. Therefore, our study is restricted to such runs.
  We introduce the concept of \emph{d-diagram}, which is a finite representation of
  infinite directed graphs. Given a d-diagram that represents an infinite distributed computation,
  we solve the problem of determining if a global predicate ever became true in the
  computation. The crucial aspect of this problem is the stopping rule that tells us
  when to conclude that the predicate can never become true in future. We also provide an
  algorithm to provide vector timestamps to events in the computation 
  for determining the dependency relationship between any two events in the infinite run.
  Finally, we give an algorithm to compute a slice of a d-diagram which concisely captures
  all the consistent global states of the computation satisfying the given predicate.
  %Vector timestamps are useful for detecting conjunctive global predicates.
\end{abstract}

\begin{keyword}
predicate detection \sep liveness violation \sep d-diagram \sep recurrent computation
\end{keyword}
% TODO : USE NODE OR SOMETHING ELSE FOR THE NODES IN THE P-DIAGRAM TO DISTINGUISH THEM FROM EVENTS IN POSET X
\maketitle


\section{Introduction}


Correctness properties of distributed programs can be classified either as 
safety properties or liveness properties. Informally, a safety 
property states that the program 
never enters a bad (or an unsafe) state, and a liveness property states
that the program eventually enters into a good state. For example, in 
the classical dining philosopher problem a safety property is that
``two neighboring philosophers
never eat concurrently'' and a liveness
property is that ``every hungry philosopher eventually eats.'' 
Assume that a programmer is interested
in monitoring for violation of a correctness property in her distributed program. 
It is clear how
a runtime monitoring system would check for violation of a safety property.
If it detects that there exists a 
consistent global state ~\cite{ChanLamp:Snap} in which two neighboring philosophers 
are eating then the safety property is violated. 
The literature in the area of global predicate detection deals with 
the complexity and algorithms for such tasks
\cite{CoopMarz:ConsDetGP,Garg:1994:DWU}.
However, the problem of detecting violation of the liveness property is harder.
At first it appears that detecting violation of a liveness property may even 
be impossible.
After all, a liveness property requires something to be true eventually and 
therefore no finite observation can detect the violation. 
We show in this paper a technique that can be used to infer 
violation of a liveness property in spite of finite observations.
Such a technique would be a basic requirement for detecting a temporal logic
formula ~\cite{Pnueli:TL} on a computation for runtime verification.

There are three important components in our technique. First, we use the
notion of a {\em recurrent} global state. Informally, a global state is recurrent in
a computation $\gamma$ if it occurs more than once in it. Existence of a recurrent
global state implies that there exists an infinite computation $\delta$ in which 
the set of events between two occurrences of can be repeated ad infinitum.
Note that $\gamma$ may not even be a prefix of $\delta$. The actual behavior 
of the program
may not follow the execution of $\delta$ due to nondeterminism.
However, we know that $\delta$ is a legal
behavior of the program and therefore violation of the liveness property in $\delta$
shows a bug in the program. We note here that in this paper we are only interested in 
algorithms that do not use randomization to ensure liveness properties. For a randomized
algorithm, existence of $\delta$ may be okay because the algorithm may guarantee liveness
only with probability one.

\begin{figure*}[htp]
\begin{center}
%\includegraphics[width=3.4in]{philosopher.fig.eps}
\includegraphics[width=3.4in]{philosopher.0}
\end{center}
\caption{A finite distributed computation $C$ of dining philosophers}
\label{fig:philosopher}
\end{figure*}

For example, in figure \ref{fig:philosopher}, a global state repeats where 
the same philosopher $P_1$ is hungry and has not eaten in between these occurrences. 
$P_1$ does get to eat after the second occurrence of the {\em recurrent} global state;
and, therefore a check that
``every hungry philosopher gets to eat''
does not reveal the bug.
%will not reveal that there exists another computation (infinite) in which $P_1$
%never gets to eat. 
It is simple to construct an infinite computation $\delta$ from the observed
finite computation $\gamma$ in which $P_1$ never eats. We simply repeat 
the execution between the first
and the second instance of the recurrent global state.
This example shows that the approach of capturing a periodic part of a computation 
can result in detection of bugs that may have gone undetected if the periodic 
behavior is not considered.

The second component of our technique is to 
develop a finite representation of the infinite behavior $\gamma$. Mathematically, we 
need a finite representation of the infinite but periodic poset $\gamma$. In this paper,
we propose the notion of d-diagram to capture infinite periodic posets. Just as 
finite directed acyclic graphs (dag's) have been used to represent
and analyze finite computations,
d-diagrams may be used for representing periodic infinite distributed computations
for monitoring or logging purposes. The logging may be useful for
replay or offline analysis of the computation.
\figref{example1} shows a d-diagram and the
corresponding infinite computation. The formal semantics of a d-diagram is given
in Section \ref{sec:infinite-graphs}. Intuitively, the infinite poset corresponds
to the infinite unrolling of the recurrent part of the d-diagram.

\begin{figure*}[tp]
\begin{center}
\includegraphics[width=5in]{shift-p-diagram.0}
\end{center}
\caption{(a) A d-diagram and (b) its corresponding infinite poset}
\label{fig:example1}
\end{figure*}

The third
component of our technique is to develop efficient algorithms for analyzing
the infinite poset given as a d-diagram. Three kinds of computation analysis
have been used in past for finite computations. The first analysis is based
on vector clocks which allows one to answer if two events are dependent 
or concurrent, for example, works by
Fidge ~\cite{Fidge:PartialOrders} and Mattern ~\cite{Mat:1989:WDAG}.
We extend the algorithm for timestamping events of a finite poset to 
that for the infinite poset. Of course, since the set of events is infinite, we do
not give explicit timestamp for all events, but only an implicit method that allows
efficient calculation of dependency information between any two events when desired.
The second analysis we use is to
detect a global predicate $B$ on the infinite poset
given as a d-diagram. 
In other words, we are interested
in determining if there exists a consistent global state which satisfies $B$. 
Since the computation is infinite, we cannot employ the traditional algorithms
\cite{CoopMarz:ConsDetGP,Garg:1994:DWU}
for predicate detection. Because the behavior is periodic it is natural
that a finite prefix of the infinite poset may be sufficient to analyze.
The crucial problem is to determine the number of times the recurrent part of
the d-diagram must be unrolled so that we can guarantee that $B$ is true
in the finite prefix {\em iff} it is true in the infinite computation. 
We show in this paper that it is sufficient to unroll the d-diagram
$N$ times where $N$ is the number of processes in the system.
%XXX: also necessary
The third analysis is based on the notion of slicing a computation introduced
in ~\cite{GarMit:2001:ICDCS,MitGar:2001:DISC}. 
Informally, a computation slice (or simply a slice) is a concise representation
of all those consistent cuts of the computation that satisfy the predicate.
%Mathematically speaking, a slice of a computation is the partially ordered set
%of all join-irreducible elements of the smallest sublattice 
Slicing is crucial in detecting nested temporal logic predicates of a distributed computation 
in the partial order model. Sen and Garg use slicing in \cite{SenGar:2003:OPODIS} to detect
a subset of CTL called Regular CTL. Ogale and Garg use it to detect another temporal logic
called BTL.
All the earlier work on computing slices was based on finite computation and we extend that
work for infinite computations in this paper.
%
%We note here that there has been earlier work in detection of temporal logic
%formulas on distributed 
%computation, such as ~\cite{G02:EDC,SenGar:2003:OPODIS,MitGar:2001:DISC,OgaleG07}.
%for example.  by using the slicing method. 
%The earlier work on detecting temporal logic predicates was restricted to 
%verifying the temporal logic formula on the finite computation with the
%interpretation of liveness predicates modified to work for finite posets.
For example, the interpretation of ``a hungry philosopher never gets to eat''
was modified by earlier work to ``a hungry philosopher does not eat by the end of the
computation.'' This interpretation, although useful in some cases, is not
accurate and may give false positives when employed by the programmer to
detect bugs. This paper is the first one to explicitly analyze the
periodic behavior to ensure that the interpretation of formulas is on the
infinite computation.

%%% VKG
%As an example, the RCTL logic can be used to represent violation of progress
%properties. These properties are of the form $\EF(p \wedge \EG(q))$.
%Intuitively, this property says that there exists a global state of the system
%on which $p$ is true and there is a path from that state on which $q$ always
%remains true. As a concrete example, in the case of dining philosophers, $p$ can
%be the predicate that ``philosopher is hungry'' and $q$ can be the predicate
%``philosopher does not get to eat''. Then the above property represents the
%violation of the progress property that ``If a philosopher is hungry, he would
%eventually get to eat''. In addition slicing can be used in conjunction with
%other general techniques to efficiently detect properties of the form $p \wedge
%q$ where $p$ is a formula in the RCTL logic and $q$ is any arbitrary
%formula. %In this case,
%we can first obtain the slice of the computation with respect to $p$ and then
%use the slice as an input to a general model checker such as
%SPIN~\cite{Holzmann97} to detect the property $q$. Since a slice is generally
%much smaller than the original computation, in most casses this technique would
%perform better than using SPIN~\cite{Holzmann97} to detect the entire formula $p
%\wedge q$.

%Although in some ways, d-diagrams are similar to other well-known representations such as
%petri-nets~\cite{petri:thesis} and message sequence charts~\cite{ITS}, there are
%some important distinctions. Discussion of these differences is deferred to
%section \ref{sec:related}. % Along with being of independent interest mathematically,
%A related question that arises in distributed debugging is that of capturing
%dependency between events. Given any two events, say $e^2$ and $g^3$, in the infinite
%poset, we would like to determine if these events are concurrent or not. 
%Therefore, we are interested in timestamping nodes in the d-diagram
%such that dependency queries can be answered efficiently. 
%Again, the traditional vector clock algorithms cannot be employed.
%In this paper, we give an algorithm to generate timestamps for
%all nodes in the d-diagram so that the vector clock values for
%any event in the infinite poset can be determined efficiently.




%TODO: Put page numbers for the book
%We also show that it is possible to compute the slice of a d-diagram with
%respect to a predicate. The class of predicates considered in this work is a
%subset of CTL~\cite{ClEm81b}, called RCTL~\cite{SenGar:2003:OPODIS}. In RCTL,
%the temporal operators are $\EF$, $\EG$, and $\AG$ and the boolean operator is
%conjunction. Moreover, atomic propositions are regular
%predicates~\cite{GarMit:2001:ICDCS}.  The class of regular predicates has the
%property that the slice with respect to a regular predicate contains
%\emph{precisely} those global states for which the predicate evaluates to true.
%Some examples of regular predicates are conjunction of local
%predicates~\cite{G02:EDC} such as ``all processes are in \emph{red} state'' and
%some relational predicates \cite{G02:EDC}.

%Since the
%temporal predicates $\EF(p)$, $\EG(p)$, and $\AG(p)$ are regular when $p$ is
%regular and class of 

%Our slicing algorithms exploit the structure of the predicate and are more
%efficient than currently used techiques in model checking programs. Recently, a
%model checking algorithm was proposed~\cite{KasGar:2005:ASE} which represents a
%distributed program as a collection of infinite posets and checks for
%reachability properties in that representation.  The results there show that
%exploiting the predicate structure can drastically improve the performance of
%the model checking algorithms. Our work opens up the avenues for representing a
%distributed program as a collection of d-diagrams and be able to check a larger
%set of properties on them.



In summary, this paper makes the following contributions:
\begin{itemize}
\item We introduce the notion of recurrent global states in a distributed computation and propose a method to detect them.
\item We introduce and study a finite representation of infinite directed computations called
  d-diagrams. 
\item We provide a method of timestamping nodes of a d-diagram so that the
happened-before relation can be efficiently determined between any two events in the given
infinite computation.
\item We define the notion of core of a d-diagram that allows us to use any predicate detection algorithm
for finite computations on infinite computations as well.
\item We present an algorithm to compute slice of the periodic computation represented using a d-diagram.
\end{itemize}

\section{A Motivating Example: A Mutual Exclusion Algorithm}
In this section we give a motivating example for the theory proposed in the paper.
Consider the distributed algorithm (shown in Fig. \ref{fig:client})
proposed by a programmer to coordinate
access to the critical section by processes $P_1 ... P_N$ in a distributed system. 
In this algorithm, a process can enter
the critical section only if it has the token. If a process is hungry and
it does not have the token, it sends a request to all processes.
Every process $P_k$ maintains an array $reqFlag$ which keeps track of all processes
that have outstanding requests for the token. When a process with the token
is done with its critical section, it sends the token to any process
that has an outstanding request. It also sends a {\em release} message to all other
processes so that they can reset the corresponding $reqFlag$.

\begin{figure}[htbp]\begin{center}
\fbox{\begin{minipage}  {\textwidth}\sf
\begin{tabbing}
x\=xxxx\=xxxx\=xxxx\=xxxx\=xxxx\= \kill
$P_k$::\\
\> {\bf var}\\
\> \> $state$: \{thinking, hungry, eating\} initially $thinking$;\\
\> \> $haveToken$: boolean initially false except for $P_1$;\\
\> \> $reqFlag$: array[$1$..$N$] of boolean initially $\forall j:reqFlag[j]=false$;\\
\> \\
\> $reqCS$: On becoming hungry (enabled if $(state=thinking)$\\
\> \> $state := hungry;$\\
\> \> if $(!haveToken)$ ;\\
\> \> \> $reqFlag[k] := true;$\\
\> \> \> send ($request$) to others;\\
\> \\
\> $recvToken$: Upon $receive(token)$ from $P_j$:\\
\> \> $haveToken := true;$\\
\> \> $reqFlag[j] := false;$\\
\> \\
\> $eat$: (enabled if $haveToken \wedge (state = hungry)$ )\\
\> \> $state := eating$;\\
\> \> $eat;$\\
\> \> $state := thinking;$\\
\> \> $reqFlag[k] := false;$\\
\\
\> $relCS$: To release critical section: (enabled if $(state = thinking)$ and $\exists i:reqFlag[i]$)\\
\> \>  send token to $P_i$;\\
\> \>  send release to all others  except $P_i$;\\
\> \> $haveToken := false;$\\
\> \\
\> $recvReq$: Upon $receive(request)$ from $P_j$:\\
\> \> \> $reqFlag[j] := true;$\\
\> \\
\> $recvRel$: Upon $receive(release)$ from $P_j$:\\
\> \> \> $reqFlag[j] := false;$\\
\end{tabbing}
\end{minipage}
} % end \fbox
\end{center}
\caption{A (faulty) distributed mutual exclusion algorithm with FIFO channels\label{fig:client}}
\end{figure}

Now suppose that the programmer is interested in testing this algorithm.
When she runs the algorithm, suppose that the following 
execution $\alpha$ takes place. All three philosophers get hungry. $P_1$ eats first and then sends token to $P_2$
who eats next. $P_1$ gets hungry again and gets the token from $P_2$. Once $P_1$
has finished eating, it sends the token to $P_3$ who eats last.
 
The distributed computation, $\alpha$ can be described in more detail by the following sequences of
events at each process.\\
%$\alpha$ takes place.
\\
$P_1$: reqCS, recvReq from $P_3$, eats, recvReq from $P_2$, 
relCS sending token to $P_2$, reqCS, recvToken from $P_2$, eats,
relCS sending token to $P_3$.\\
\\
$P_2$: recvReq from $P_3$, reqCS, recvToken from $P_1$, recvReq
from $P_1$,
relCS sending token to $P_1$, recvRel from $P_1$\\
\\
$P_3$: reqCS, recvReq from $P_2$, recvRel from $P_1$,
recvReq from $P_1$, recvRel from $P_2$, recvToken from $P_1$, eat\\

\begin{figure*}[htp]
\begin{center}
%\includegraphics[width=3.4in]{philosopher.fig.eps}
%\includegraphics[width=6.4in]{figures/mutex.dot.eps}
\includegraphics[width=6.4in]{figures/mut.pdf}
\end{center}
\caption{A finite distributed computation $\alpha$ for the mutex algorithm}
\label{fig:mutex}
\end{figure*}

The distributed computation $\alpha$ shown in Fig. \ref{fig:mutex} 
satisfies the standard safety and liveness properties: 
two processes do not eat at the same time and every hungry process eventually eats.
However, with the techniques proposed in the paper we would be able to construct
an infinite computation $\alpha'$ that is a valid execution and violates the liveness property.

Consider the following prefix $\beta$ of computation $\alpha$:\\
\\
$P_1$: reqCS, recvReq from $P_3$, eats \\
$P_2$: recvReq from $P_3$. \\
$P_3$: reqCS. \\
\\
The global state after $\beta$ is:\\
State of $P_1$: haveToken = true; reqFlag = (false, false, true); state=thinking\\
State of $P_2$: haveToken = false; reqFlag = (false, false, true); state=thinking\\
State of $P_3$: haveToken = false; reqFlag = (false, false, true); state=thinking\\

Note that the same global state occurs in $\alpha$ after $P_1$ has eaten twice in the
the following prefix: ($\beta$ followed by $\gamma$)\\
\\
$P_1$: reqCS, recvReq from $P_3$, eats, recvReq from $P_2$, 
relCS sending token to $P_2$, reqCS, recvToken from $P_2$, eats \\
\\
$P_2$: recvReq from $P_3$, reqCS, recvToken from $P_1$, recvReq
from $P_1$,
relCS sending token to $P_1$\\
\\
$P_3$: reqCS, recvReq from $P_2$, recvRel from $P_1$,
recvReq from $P_1$, recvRel from $P_2$\\
\\
Since the global state is identical after executing $\beta$ and $\beta$ followed by $\gamma$, 
there exists a valid execution $\alpha'$ in which $\beta$ is followed by
$\gamma$ an infinite number of times. The execution $\alpha'$ violates
the liveness property because $P_3$ stays hungry forever.
The infinite execution derived from $\alpha$ is shown as a p-diagram in Fig. \ref{fig:pmutex}.

\begin{figure*}[htp]
\begin{center}
%\includegraphics[width=3.4in]{philosopher.fig.eps}
\includegraphics[width=6.4in]{figures/pmut.pdf}
\end{center}
\caption{A p-diagram derived from $\alpha$ that shows violation of a liveness property}
\label{fig:pmutex}
\end{figure*}

{\bf Remark:} The algorithm can be fixed by making two changes.
First, we should maintain a {\em queue} of requests at all processes
rather than a {\em set} of requests as implemented in 
Fig. \ref{fig:client} by the boolean array $reqFlag$.
Second, a process with the token that has eaten last must release the token if the 
queue of requesting processes is nonempty.

\section{Model of a Distributed Computation}
We first describe our model of a distributed computation. 
%and a method to determine recurrent global states in that computation.
We assume a message passing asynchronous system without any shared memory or a
global clock. A distributed program consists of $N$ sequential processes denoted
by $P = \{P_1, P_2, \ldots, P_N\}$ communicating via asynchronous messages. A
\emph{local computation} of a process is a sequence of events. An event is
either an internal event, a send event or a receive event. When an event is
executed, it changes the state of the process (and possibly the state of incoming or outgoing
channels).
The predecessor and successor events of
$e$ on the process on which $e$ occurs are denoted by $pred(e)$ and $succ(e)$.

Generally a distributed computation is modeled as a partial order of a set of
events, called the \emph{happened-before relation}~\cite{Lamp:HappenBefore}. In
this paper, we instead use directed graphs to model distributed computations as
done in~\cite{MitGar:2001:DISC}. When the graph is acyclic, it represents
a distributed computation. When the distributed computation is infinite, the 
directed graph that models the computation is also infinite. An
infinite  distributed computation
is {\em periodic} if it consists of a subcomputation that is repeated
forever.
Directed graphs allow us to represent both the
computation and its slice with respect to a predicate in a uniform fashion.
However, as opposed to the earlier work, our computations can be infinite and as
a result, the directed graphs used to model the computation can be infinite.

Given a directed graph $G = \compt$, we define a \emph{consistent cut} 
%or a global state 
as a set of vertices such that if the subset contains a vertex then
it contains all its incoming neighbors. For example, the set $C = \{ a^1, b^1,
c^1,d^1, e^1, f^1, g^1 \}$ is a consistent cut for the graph shown in
figure \ref{fig:shift}(b). 
The set $\{ a^1, b^1, c^1,d^1, e^1, g^1 \}$ is not consistent because it includes
$g^1$, but does not include its incoming neighbor $f^1$.
The set of finite consistent cuts for graph $G$ is denoted
by $\C(G)$.

%Formally, $C$ is a consistent cut
%of $G$, if \[\forall x, y \in E: (x \rightarrow y) \wedge (y \in C) \Rightarrow
%(x \in C) \]. We say that a strongly connected component is \emph{non-trivial} if
%it has more than one element. We call the empty set $\emptyset$ and the set of vertices
%$E$ as \emph{trivial} consistent cuts. A distributed computation in our model
%can contain cycles. This is because whereas a computation in the happened-before
%model captures the \emph{observable} order of execution of events, a computation
%in our model captures the set of possible consistent cuts. Intuitively, each
%strongly connected component of a computation can be viewed as a
%\emph{meta-event}; a meta-event consists of one or more events.  
% The following theorem is a slight generalization of the result in
%lattice theory that the set of \emph{ideals} of a partially ordered set forms a
%finitary distributive lattice~\cite{Stan:1986:Book}. A lattice is finitary if it
%has the bottom element and is locally finite.

%\begin{theorem}\label{thm:dlattice}
%  Given a directed graph $G$, $(\C(G); \subseteq)$ forms a a finitary distributive
%  lattice.
%\end{theorem}
In this work we focus only on finite consistent cuts (or 
\emph{finite order ideals}~\cite{davey})
as they are the ones of interest for distributed
computing. 
%We use $C[i]$ to denote the subset of $C$ that contains
%events only from process $P_i$.

%For an event $x \in E$, we denote by $J(x)$, the least consistent cut which includes $x$. 
%The cut $J(x)$ can also be interpreted as principal ideal of
%the element $x$ in the directed graph $G$. 
A \emph{frontier} of a consistent cut
is the set of those events of the cut whose successors, if they exist, are not
contained in the cut. 
Formally,
\[ frontier(C) = \{ x \in C | succ(x) \textrm{ exists } \Rightarrow succ(x) \not \in C \}
\]
For the cut $C$ in figure \ref{fig:shift}(b), $frontier(C) =
\{e^1, f^1, g^1 \}$. A consistent cut is uniquely characterized by its frontier
 and in this paper we always identify a consistent cut by its frontier.
%unless a distinction is made between the cut and its frontier.

 Two events are said to be
\emph{consistent} iff they are contained in the frontier of some consistent cut,
otherwise they are inconsistent. It can be verified that events $e$ and $f$ are
consistent iff there is no path in the computation from $succ(e)$
to $f$ and from $succ(f)$ to $e$. 
%Note that in our model, an
%event can be inconsistent with itself.
%
%\begin{figure*}[tp]
%\begin{center}
%\includegraphics[width=4.5in]{computation.0}
%\end{center}
%\caption{(a) A d-diagram with process and label information (b) The computation
%  corresponding to the d-diagram}
%\label{fig:computation}
%\end{figure*}


\section{Infinite Directed Graphs}
\label{sec:infinite-graphs}
From distributed computing perspective, our intention is to provide a model for
an infinite computation of a distributed system which eventually becomes
periodic. 
Although a distributed computation in the happened-before
model~\cite{Lamp:HappenBefore} is always represented using a poset, it is useful
to have a model of infinite directed graphs for the purpose of
slicing~\cite{GarMit:2001:ICDCS,MitGar:2001:DISC}.  The directed graph does not
capture the order between events in the computation but it is used to
capture the set of possible consistent cuts or global states of the system.
To this end, we introduce the notion of \emph{d-diagram} (directed graph diagram). 
%A d-diagram is defined as follows:

\begin{definition} [d-diagram] \label{def:d-diagram}
  A d-diagram $Q$ is a tuple $(V, F, R, B)$ where $V$ is a set of vertices or
  nodes, $F$ (forward edges) is a subset of $V \times V$, $R$ (recurrent
  vertices) is a subset of $V$, and $B$ (shift edges) is a subset of $R \times
  R$. A d-diagram must satisfy the following constraint: If $u$ is a recurrent
  vertex and $(u,v) \in F$ or $(u,v) \in B$, then $v$ is also recurrent.
\end{definition}

Figure \ref{fig:example1}(a) is an example of a d-diagram. The recurrent
vertices and non-recurrent vertices in the d-diagram are represented by hollow
circles and  filled circles respectively. The forward edges are represented by
solid arrows and the shift-edges by dashed arrows. The recurrent vertices
model the computation that is periodic. Intuitively, a forward edge models
dependency between the same instance of recurrent vertices, whereas a shift-edge $(u,v)$
models dependency of instance $(i+1)$ of $v$ on instance $i$ of recurrent vertex $u$.
%We use the same convention throughout the paper for the figures. 
%In this case, the vertices $\{a,b\}$ and
%vertices $\{f, g\}$ form cycles in $F$.

Each d-diagram generates an infinite directed graph defined as follows: 
\begin{definition} [directed graph for a d-diagram] The directed graph
  $G = \compt$ for a d-diagram $Q$ is defined as follows:
  \begin{itemize}
    \item $E = \{ u^1 | u \in V \} \cup \{u^i | i \geq 2 \wedge u \in R \}$
    \item The relation $\rightarrow$ is the set of edges in $E$ given by:\\
      (1) if $(u,v) \in F$ and $u \in R$, then $\forall i: u^{i} \rightarrow v^{i}$, and
      (2) if $(u,v) \in F$ and $u \not \in R$, then $u^{1} \rightarrow v^{1}$, and (3) if
      $(v,u) \in B$, then $\forall i:v^{i} \rightarrow u^{i+1}$.
   \end{itemize}

   Furthermore, let $\mypath (G)$ be the set of pairs of vertices $(u, v)$
   such that there is a path from $u$ to $v$ in $G$.
\end{definition}

%\begin{figure*}[tp]
%\begin{center}
%\includegraphics[width=4.5in]{shift-d-diagram.0}
%\end{center}
%\caption{(a) A d-diagram and (b) its corresponding infinite directed graph}
%\label{fig:dexample}
%\end{figure*}
The set $E$ contains infinite instances of all recurrent vertices and single instances
of non-recurrent vertices. For a vertex $u^i$, we define its index as $i$.

It can be easily shown that if the relation $F$ is acyclic, then the resulting
directed graph for the d-diagram is a poset. Figure \ref{fig:example1} shows a d-diagram
along with a part of the infinite directed graph generated by it. 
Two vertices in a directed graph are said to be {\em concurrent} if there is no
path from one to other.

%
%\begin{figure}[htb]
%\begin{center}
%\scalebox{0.5}{
%\includegraphics{SimpleExamples.fig.eps}
%}
%\end{center}
%\label{fig:ExamplesOfD-Diagrams}
%\vspace{-8mm}
%\caption{Trivial examples of d-diagrams}
%\vspace{-3mm}
%\end{figure}
%
%Some other examples are as follows:
%\begin{enumerate}
%\item  %(Figure \ref{fig:ExamplesOfD-Diagrams}(i))
%The set of natural numbers with the usual order can be modeled using
%the d-diagram $(V, F, R, B)$, where\\
%$V = \{u\}$; $F = \{\}$; $B = \{(u,u)\}$; $R = \{u\}$
%
%Note that this poset has infinite height and width equal to $1$.
%\item %(Figure \ref{fig:ExamplesOfD-Diagrams}(ii))
%The set of natural numbers with no order can be modeled as $(V, F, R, B)$, where\\
%$V = \{u\}$; $F = \{\}$; $B = \{\}$; $R = \{u\}$.
%\end{enumerate} 


Note that acyclic d-diagrams cannot represent all infinite posets. 
For example, any poset $P$ defined by an acyclic d-diagram 
is well-founded. Moreover, there exists a constant $k$ such that
every element in $P$ has the size of the set of its upper covers and lower covers\cite{davey} bounded
by $k$.
Although acyclic d-diagrams cannot represent all infinite posets, they
are sufficient for the purpose of modeling periodic distributed computations.
Let the {\em width} of a directed graph be defined as the 
maximum size of a set of pairwise concurrent vertices. 
A distributed computation generated by a finite number of processes has
finite width and hence we are interested in only those d-diagrams which generate
finite width directed graphs.
The following property of the posets generated by acyclic d-diagrams is easy to show.
%The proof of this and other Lemmas can be found in the appendix.
\begin{lemma}
\label{lem:prop}
A poset $P$ defined by an acyclic d-diagram 
has finite width iff for every
recurrent vertex there exists a cycle in the graph $(R,F \cup B)$ which includes
a shift-edge.
%has the following properties.
%\begin{enumerate}
%\item 
%It is well-founded.
%\item
%There exists a constant $k$ such that
%every element has the size of the set of its upper covers and lower covers\cite{davey} bounded by $k$.
%\item
%It has finite width iff for every
%recurrent vertex there exists a cycle in the graph $(R,F \cup B)$ which includes
%a shift-edge.
%\end{enumerate} 
%\item
%Every principal order ideal of P is finite.
%COMMENT: Doesn't this follow from the well-foundedness ?
\end{lemma}
\begin{proof}
  Let $k>0$ be the number of shift-edges in the shortest cycle involving $u \in
  R$. %Then by transitivity, we know $(u^{i}, u^{i+k}) \in \mypath(G)$.
By transitivity we know that there is a path from vertex  $u^{i}$ to $u^{i+k}$ in $R$. 
   Therefore, at most $k-1$ instances of a vertex $u \in R$ are concurrent.
  Since $R$ is finite, the largest set of concurrent vertices is also
  finite.

  Conversely, if there exists any recurrent vertex $v$ that is not in a cycle
  involving a shift-edge, then $v^{i}$ is concurrent with $v^{j}$ for all
  $i,j$.  Then, the set \[ \{ v^i | i \geq 1 \} \] contains an infinite number of
  concurrent vertices. Thus, $G$ has infinite width.
\end{proof}



%Some properties of the directed graphs generated by d-diagrams are easy to show.
%\begin{lemma}
%\label{lem:dprop}
%A directed graph $G$ defined by a d-diagram has the following properties.
%\begin{enumerate}
%\item 
%  The cycles present in $G$ only involve elements with the same index.
  
%\end{lemma}
   

%The following lemma characterizes the class of
%d-diagrams for which the corresponding directed graphs have finite width. 
%\begin{lemma}
%\label{lem:fwidth}
%\end{lemma}

%We use a d-diagram $(V, R, F, B)$ to represent the infinite directed graph of
%the computation. To generate a d-diagram from a process trace of a periodic
%computation, we identify identical (with respect to the states of the
%processes) consistent cuts. If we find two such consistent cuts $Y$ and $Z$, 
%then using definition
%\ref{def:d-diagram}, we can easily construct a d-diagram. All the events between
%$Y$ to $Z$ are recurrent.

We assume that the
process relation maps all the instances of a vertex in d-diagram to the same
process i.e. $\forall e \in V: proc(e^i) = proc(e^j)$. As a result, we denote
the process for an element $e^i \in E$ simply as $proc(e)$. 
Figure \ref{fig:example1} shows a d-diagram and the corresponding  computation.
Note that for any two
events $x, y$ on a process, either there is a path from $x$ to $y$ or from
$y$ to $x$, i.e., two events on the same process are always ordered. 
To guarantee
this condition, it can be
easily shown that all the recurrent vertices in the d-diagram with the same
process should form a cycle with exactly one shift-edge. We refer to these
shift-edges as \emph{process shift-edges}. 
We further assume that the d-diagram given to us has a non-empty recurrent
part; otherwise the algorithms for the case of finite computations can be used. 
We augment the d-diagram with the presence of a fictitious \emph{global
initial event} denoted by $\perp$. The global initial event occurs before any
other event on the processes and initializes the state of the processes. Note
that for infinite computations we do not have the notion of a global final
event. 

%\begin{figure}[htbp]\begin{center}
%\fbox{\begin{minipage}  {\textwidth}\sf
%\begin{tabbing}
%x\=xxxx\=xxxx\=xxxx\=xxxx\=xxxx\= \kill
%\>$G :=$ initial cut;\\
%\>$found :=$ false;\\
%\>while $\lnot found$\\ 
%\>\>1. Compute global snapshot $H$ (eg. Chandy Lamport's algorithm) ;\\
%\>\>2. if($G==H$)\\
%\>\>\>a. $found := $true;\\
%\>\>\>b. generate d-diagram by adding edges from events in \\
%\>\>\>\> $predecessor(H)$ to events in $G$ ; \\
%\>\>end if \\
%\>end while
%\end{tabbing}
%\end{minipage}
%} %end \fbox
%\end{center}
%\caption{Computing a d-diagram}
%\label{figAlgorithm}
%\end{figure}
\subsection{Index Independence Assumption}
Given a consistent cut, a predicate is evaluated with respect to the values of
the variables resulting after executing all the events in the cut. If a
predicate $p$ evaluates to true for a consistent cut $C$, we say that $C$
satisfies $p$. We further assume that a predicate depends only on the
\emph{labels} of the events in the computation. 
This rules out predicates based
on global state such as channel predicates \cite{DBLP:journals/jpdc/GargCKM97}. We define $\mathcal{L}: G \rightarrow L$ to be an
onto mapping from the set of vertices in d-diagram to a set of labels $L$ with
the constraint that $\forall e \in V: \mathcal{L}(e^i) = \mathcal{L}(e^j)$. In
other words, the label of an element in the directed graph is independent of its
index. This is in line with modeling the recurrent events as repetition of the
same state. We refer to this assumption as the
\emph{index-independence assumption}.

\begin{figure*}[tp]
\begin{center}
\includegraphics[width=6in]{computation.0}
\end{center}
\caption{(a) A d-diagram with process and label information (b) The computation
  corresponding to the d-diagram}
\label{fig:computation}
v\end{figure*}

\figref{computation} shows a computation represented as a d-diagram.
\figref{computation}(a) shows the d-diagram along with the process information.
Along with each process, the local variables $x, y, z$ on processes $P_1, P_2$
and $P_3$ are also listed. For each event the value of the local variable is
listed. The values of local variables can be considered to be labels in this
case.

\subsection{Unrolling of a d-diagram}

We now discuss another aspect of d-diagrams; a directed graph does not
have a unique representation in terms of d-diagram. In fact, we show that there
are countably infinite representations of a directed graph as a d-diagram. We
define the notion of \emph{unrolling} of a d-diagram $Q$ with respect to a
consistent cut $C$.  Intuitively, this operation increases the non-recurrent
part of the d-diagram to include the cut $C$ and rearranges the forward and
shift-edges.

\begin{definition} [unrolling a d-diagram] 
  Let $Q = (V, R, F, B)$ be a d-diagram and $C$ be a consistent cut in the
  corresponding directed graph $\compt$ such that $\forall e^i \in frontier(C): e \in
  R$. Then $\mathscr{U}(Q, C) = (V', R', F', B')$ is the d-diagram:
  \begin{itemize}
    \item $V' = \{ e_k | e \in V \wedge e^k \in C \}$
    \item $R' = \{ e_k | e \in R \wedge k-1 = \textrm{max} \{i | e^i \in C \} \}$
    \item $F' = \{ (e_i,f_j) | e_i,f_j \in V' \wedge e^i \rightarrow f^j \} $
    \item $B' = \{ (e_i, f_j) | e_i, f_j \in R' \wedge e^i \rightarrow f^{j+1} \}$
  \end{itemize}
\end{definition}

It can be easily shown that the unrolled d-diagram generates a directed graph
isomorphic to the original d-diagram. Let $\compt$ be the directed graph
generated by the d-diagram $Q$ and $\langle E', \rightsquigarrow \rangle$ be the
directed graph generated by $\mathscr{U}(Q, C)$. Then we denote the isomorphism
function from elements in $E$ to elements in $E'$ by $\iso{C}$. If the isomorphism
function maps a node in the original directed graph to a node with the same
label, then the two directed graphs are equivalent from the perspective of
predicate detection. For this purpose, we assume that $\mathcal{L}(e^i) =
\mathcal{L}(\iso{C}(e^i))$. 

%The following result is easy to show:
%\begin{lemma}\label{lem:unroll}
  %Let $\langle E', \rightsquigarrow \rangle$ be the graph generated by
  %$\mathscr{U}(Q, C) = (V', R', F', B')$. Let $e^i$ be such that $e^i \in C$ and $\forall j > i:
  %e^j \not \in C$. Then $\iso{C}(e^{i+k}) = h^k$ for some $h \in R'$.
%\end{lemma}

%\begin{theorem}\label{d-diagram:unroll}
%  For a consistent cut $C$ and a directed graph $Q$, $\mathscr{U}(Q, C)$ is well
%  defined and generates the same directed graph as $Q$.
%\end{theorem}

\begin{figure}[hp]
\begin{center}
\includegraphics[width=3in]{unroll.0}
\end{center}
\caption{The d-diagram in \protect{\figref{computation}(a)} unrolled with
  respect to $C = \{d^2, f^1, g^1\}$}
\label{fig:unroll}
\end{figure}

As an example, \figref{unroll} shows the unrolling of the d-diagram in
\figref{computation}(a) with respect to a cut $C = \{d^2, f^1, g^1\}$.

\subsection{Shift of a Cut}

The notion of {\em shift} of a cut is useful for analysis of periodic 
infinite computations.
Intuitively, the shift of
a frontier $C$ produces a new cut by moving the cut $C$ forward or backward by a
certain number of iterations along a set $X$ of recurrent events in $C$.
Formally,

\begin{definition} [d-shift of a cut] 
  Given a frontier $C$, a set of recurrent events $X \subseteq R$ and an integer $d$,
  a \emph{d-shift cut} of $C$ with respect to $X$,  is
  represented by the frontier $S_d(C, X)$
%\begin{itemize}
%\item   $e \not \in X \Rightarrow e^i \in C$
%\item   $e \in X \Rightarrow e^m \in C
%\item 
%\end{itemize}
  \[ \{ e^i | e^i \in C \wedge e \not \in X \} \cup \{ e^{m} | e^i \in C \wedge
  e \in X \wedge m = \textrm{ max} (1, i + d) \} \] 
  We denote $S_d(C, R)$ simply by $S_d(C)$.
\end{definition}

Hence $S_d(C, X)$ contains all events $e^i$ that are not in $X$, and the shifted events for all elements of $X$.
Note that in the above definition $d$ can be negative. Also, for a consistent
cut $C$, $S_d(C, X)$ is not guaranteed to be consistent for every $X$.

\begin{figure*}[tp]
\begin{center}
\includegraphics[width=4.5in]{shift-cut.0}
%\includegraphics[width=4.5in]{shift-cut.fig.eps}
\end{center}
\caption{(a) A d-diagram (b) The computation for the d-diagram showing a cut and the shift of a cut}
\label{fig:shift}
\end{figure*}

As an example, consider the infinite directed graph for the d-diagram in
figure \ref{fig:shift}. Let $C$ be a cut given by the frontier $\{e^1, f^1,
g^1\}$ and $X = \{f, g \}$. Then $S_1(C,X)$ is the cut given by $\{e^1, f^2,
g^2\}$. \figref{shift} shows the cut $C$ and $S_1(C,X)$.  Similarly for $C$
given by $\{a^1, f^1, g^1\}$, $S_1(C) = \{a^1, f^2, g^2\}$. Note that in this
case, $a^1$ remains in the frontier of $S_1(C)$ and the cut $S_1(C)$ is not
consistent.

\section{Vector Clock Timestamps}
%In this section, we consider the problem of slicing a d-diagram with respect to
%a non-temporal regular predicate. It was shown~\cite{GarMit:2001:ICDCS} that for
%computing the slice of a finite computation with respect to a regular predicate
%$p$, it is sufficient to compute $J_p(x)$ for every element $x$ in the
%computation. The result can be easily extended for the case of infinite
%computation when we are dealing with finite consistent cuts. However, the
%problem is that since the computation is infinite, it is not feasible to compute
%$J_p(x)$ for every element. Instead, we show that we can directly operate on the
%d-diagram and compute the slice of the infinite computation as another
%d-diagram. In this section, the examples work on the d-diagram in
%\figref{computation} and assume that the predicate $p$ is $(x = 1) \wedge (y =
%1) \wedge (z = 1)$.

\begin{figure*}
\begin{center}
%\includegraphics[width=4.5in]{vectorclocks.fig.eps}
\includegraphics[width=4.5in]{vectorclocks.0}
%\includegraphics[width=4.5in]{vc.eps}
%\input{figures/myvectorclocks.pstex_t}
\end{center}
\caption{(a) A d-diagram (b) The corresponding computation with vector timestamps}
\label{fig:vectorClocks}
\end{figure*}

In this section, we present algorithms to assign vector timestamps to nodes
in the infinite computation given as a d-diagram. The objective
is to determine dependency between any two events, say $e^i$ and $f^j$,
based on the vector clocks assigned to these events rather than exploring
the d-diagram. Since there are infinite instances of recurrent
events, it is clear that we can only provide an implicit vector
timestamp (or a function to compute vector timestamp) for the events. 
The explicit vector clock can be computed
for any specific instance of $i$ and $j$.

Timestamping events of the computation has many applications in 
debugging distributed programs \cite{Fidge:PartialOrders}. Given the timestamps
of recurrent events $e$ and $f$, our algorithm enables answering queries of the form:

\begin{enumerate}
\item 
Are there any instances of $e$ and $f$ which are concurrent, i.e., are there indices $i$ and
$j$ such that $e^i$ is concurrent with $f^j$? For example, when $e$ and $f$ correspond
to entering in the critical section, this query represents violation of the critical section.
\item
What is the maximum value of $i$ such that $e^i$ happened before a given event
such as $f^{256}$?
\item
Is it true that for all $i$, $e^i$ happened before $f^i$?
\end{enumerate} 



We show in this section, that there exists an efficient algorithm to timestamp
events in the d-diagram. As expected, the vectors corresponding to
any recurrent event $e^i$ eventually become periodic. The difficult
part is to determine the threshold after which the vector clock
becomes periodic and to determine the period.

We first introduce the concept of \emph{shift-diameter} of a d-diagram.
The shift-diameter provides us with the threshold after which the
dependency of any event becomes periodic.

\begin{definition} [shortest path in a d-diagram]
  For a d-diagram $Q$, the shortest path between any two vertices is a path
with the minimum number of shift-edges.
\end{definition}
\begin{definition} [shift-diameter of a d-diagram]
  For a d-diagram $Q$, the shift-diameter $\eta(Q)$ is the maximum of the number
  of shift-edges in the shortest path between any two vertices in the d-diagram.
\end{definition}

When $Q$ is clear from the context, we simply use $\eta$ to denote $\eta(Q)$.
For the d-diagram in \figref{shift}, $\eta = 1$. In figure \ref{fig:vectorClocks}, we can see that $\eta = 2$. We first give a bound on $\eta$.

\begin{lemma}{\label{lem:k-bound}}
  For a d-diagram $Q$ corresponding to a computation with $N$ processes, $\eta(Q) \leq 2N$.
\end{lemma}
\begin{proof}
  Consider the shortest path between two vertices $e, f \in V$. Clearly this
  path does not have a cycle; otherwise, a shorter path which excludes the cycle
  exists. Moreover, all the elements from a process occur consecutively in this path.
As a result, the shift-edges that are between events on the same process
are traversed at most once in the path. Moving from one process to another can have at most
one shift-edge.
Hence, $\eta(Q) \leq 2N$.
%In a cycle-free path every shift-edge is traversed at most once.  Since all events in a process are totally ordered, every process can have at most one shift edge that does not point to another process.
  %As a result, in the path from $e$ to $f$, elements from a process can come
  %from at most two different iterations.  
\end{proof}

%The following lemma provides the relationship that exists between different
%occurrences of recurrent events. In particular, it bounds the number of
%iterations by which an event differs in the history of another event.
%
%\begin{lemma}\label{lem:k}
  %Consider two events $e, f \in R$ such that there are indices $i,j$  for which there is a path from $e^i$ to $f^j$ and $\forall l > i$ there is no path from $e^l$ to $f^j$. Then $(j-i) \leq \eta$.
%\end{lemma}

%\begin{proof}
  %Consider the shortest path $\pi$ from $e$ to $f$ in the d-diagram. The path
  %from $e^i$ to $f^j$ corresponds to $\pi$ otherwise there exists an index $l >
  %i$ such that there exists a path from $e^l$ to $f^j$. The difference $j-i$ is then
  %equal to the number of shift-edges in $\pi$. Therefore by definition of
  %$\eta$, $(j-i) \leq \eta$.
%\end{proof}

%The same result can be stated in a slightly different way.
%\begin{corollary}\label{cor:static}
  %If $e \in V$ and $f \in R$ such that there are indices $i, j$ with $e^i < f^j$ and
  %$\forall l < j: e^i \not < f^{l}$, then $j-i \leq \eta$.
%\end{corollary}

%%% TODO: Finding width of the p-diagram
%The above result allows us to characterize the cut $J(f^j)$ for an event $f^j
%\in \compt$.
For an event $x \in E$, we denote by $J(x)$, the least consistent cut which includes $x$. 
The least consistent cut for $J(e^i)$ will give us the vector clock for event $e^i$.
%Note that the vector timestamp of any event $e$, $V(e)$ is just an 
%alternate representation of $J(e)$. The $i^{th}$ component of $V(e)$
%is simply the number of events in $P_i$ that are in $J(e)$. 
%We analyze the structure of $J(e^i)$, and then later carry those results to $V(e^i)$.
We first show that the cuts $J(e^i)$ \emph{stabilize} after some iterations i.e.
the cut $J(e^j)$ can be obtained from $J(e^i)$ by a simple shift for $j > i$.
This allows us to \emph{predict} the structure of $J(e^i)$ after certain
iterations. 

The next lemma shows that the cut $J(f^j)$ does not contain recurrent events
with iterations very far from $j$.

\begin{lemma}\label{lem:je}
  If $e^i \in frontier(J(f^j))$, $e \in R$, then $0 \leq j-i \leq \eta$.
\end{lemma}
\begin{proof}
  If $e^i \in frontier(J(f^j))$, then there exists a path from 
%$(e^i, f^j) \in \mypath(\compt)$
$e^i$ to $f^j$   and   $\forall k > i$ there is no path from $e^k$ to $f^j$.
%: (e^k, f^j) \not \in \cpath$. 
Therefore the path from $e^i$ to
  $f^j$ corresponds to the shortest path between $e$ and $f$ in the d-diagram.
  Therefore, by the definition of $\eta$, $j - i \leq \eta$.
\end{proof}

The following theorem proves the result regarding the stabilization of the cut
$J(e^i)$. Intuitively, after a first few iterations the relationship between
elements of the computation depends only on the difference between their
iterations. 
%at after some number of iterations, the least
%consistent cut corresponding to an event can be obtained by shifting the cut
%corresponding to a previous iteration of that event.

%\begin{theorem}\label{thm:similar}
%For a node $e \in R$, there exists $j$ such that $J(e^{j+1}) = S_1(J(e^{j}))$.
%\end{theorem}
%\begin{proof}
%  For proving the theorem, we show a stronger result. Let $\beta = \eta + 1$. We
%  show that for a recurrent node $e$, $J(e^{\beta + 1}) = S_1(J(e^{\beta}))$.
%  
%XXX: Is this bound tight
\begin{theorem}\label{thm:similar}
For a recurrent vertex $e \in R$, $J(e^{\beta + 1}) = S_1(J(e^{\beta}))$ for all $\beta \geq \eta + 1$.
\end{theorem}
\begin{proof}  
  We first show that $S_1(J(e^{\beta})) \subseteq J(e^{\beta+1})$.
  Consider $f^j \in S_1(J(e^{\beta}))$. 
If $f \in V \setminus R$ (i.e., $f$ is not a recurrent vertex), then
$f^j \in J(e^{\beta})$, because the shift operator affects only the recurrent
vertices. 
This implies that there is a path from $f^j$ to $e^{\beta}$, which in turn
implies the path from $f^j$ to $e^{\beta +1}$. 
Hence, $f^j \in J(e^{\beta+1})$. 
If $f$ is recurrent, then $f^j \in S_1(J(e^{\beta}))$ implies
$f^{j-1} \in J(e^{\beta})$.
This implies that there is a path from $f^{j-1}$ to $e^{\beta}$, which in turn
implies the path from $f^j$ to $e^{\beta +1}$, from the property of d-diagrams.
  Therefore, $S_1(J(e^{\beta})) \subseteq J(e^{\beta+1})$.
  
  Now we show that $J(e^{\beta+1}) \subseteq S_1(J(e^{\beta}))$. 
  Consider $f^j \in J(e^{\beta+1})$. If $j > 1$, then given a path from
  $f^j$ to $e^{\beta+1}$, there is a path from 
  $f^{j-1}$ to $e^{\beta}$. Hence $f^j \in S_1(J(e^{\beta}))$.
  Now, consider the case when $j$ equals $1$.
  $f^1 \in J(e^{\beta+1})$ implies that there is a path from 
  $f^1$ to  $e^{\beta+1}$. We claim that for $\beta > \eta$, there is also
a path from 
  $f^1$ to  $e^{\beta}$. Otherwise, the shortest path from $f$ to $e$ has more than
$\eta$ shift-edges, a contradiction.
  
%  Hence $J(e^{j+1}) = S_1(J(e^{j}))$.
\end{proof}
% my proof: let f^j in S(J(e^b)). 
% If f^j is non-recurrent, then f^j in J(e^b) (because shift operator does not affect
%non-recurrent events)
%This means that there is a path from f^j to e^b which implies that
% there is a path from f^j to e^b+1. Hence f^j in J(e^b+1)
%
% if f^j is recurrent, then f^j in S(J(e^b)) means that f^{j-1} in J(e^b).
% this implies that there is a path from f^{j-1} to e^b
% implies that there is a path from f^j to e^{b+1}
%
% Conversely, let f^j in J(e^{b+1})
% If j > 1, then given a path from f^j to e^{b+1}, we get that there 
% is a path from f^{j-1} to e^{b}. Hence f^{j-1} in J(e^b). Therefore,
% f^j in S(J(e^b))
% If j = 1, then there is a path from f^1 to e^{b+1}. Since this is the shortest
% path f^1 should also have a path from e^b otherwise the shortest path 
% from f to e has greater than b shift edges
%
%



%\begin{definition}
%  For a node $e \in R$, the \emph{smallest} event $e^{j}$ which satisfies the
%  condition of Theorem~\ref{thm:similar} is called \emph{cut-off} event for $e$
%  and is denoted by $e^{\alpha(e)}$ or simply as $e^{\alpha}$.
%\end{definition}

%In the p-diagram in \figref{example1}, $\alpha = 2$ for $f$ and $g$ and
%$\alpha = 1$ for $d$ and $e$.

%\begin{corollary}
%  For an node $e \in R$, $e^{\alpha} \leq e^{\eta+1}$.
%\end{corollary}

%\begin{corollary}
%For a recurrent event $e$, $J(e^{\alpha + d}) = S_d(J(e^{\alpha}))$.
%\end{corollary}
%\begin{proof}
%By induction on $d$ and using Theorem \ref{thm:similar}.
%\end{proof}

%% Define p-timestamps 

When d-diagram generates a poset, Theorem \ref{thm:similar} can be used to assign
timestamps to vertices in the d-diagram in a way similar to vector clocks. The
difference here is that a timestamp for a recurrent vertex is a concise way of
representing the timestamps of infinite instances of that vertex. 

Each recurrent event, $e$, has a special \emph{p-timestamp} ($PV(e)$) associated with it, which lets us compute the time stamp for any arbitrary iteration of that event. 
Therefore, this result gives us an algorithm for assigning p-timestamp to a recurrent
event. The p-timestamp for a recurrent event $e$, $PV(e)$ would be a list of
the form 
$$(V(e^1), \ldots, V(e^{\beta}) ; I(e))$$ 
where $I(e) = V(e^{\beta + 1}) -
V(e^{\beta})$ and $V(e^j)$ is the timestamp assigned by the normal vector clock
algorithm to event $e^j$. Now for any event $e^j, j > \beta$, $V(e^j) = V(e^{\beta})
+ (j- \beta)*I(e)$.

In figure \ref{fig:vectorClocks}, $\eta =2$, $\beta =3$. $V(a^3) = [5,2]$ and $V(a^4)= [7,4]$. $I(a) = [2,2]$. Hence $PV(a) = ([1,0], [3,0] , [5,2]; [2,2])$. Now, calculating $V(a^j)$ for an arbitrary $j$ is trivial. For example, if $j=6$, then $V(a^6) = [5,2] + (6- 3) *[2,2] = [11,8]$.

  
This algorithm requires $O(\eta n)$ space for every recurrent vertex. Once the
%p-timestamps 
timestamps have been assigned to the vertices, any two instances of recurrent
vertices can be compared in $O(n)$ time.

The notion of vector clock also allows us to keep only the {\em relevant}
events\cite{DBLP:conf/podc/AgarwalG05} of the d-diagram. Any dependency related question on the relevant
events can be answered by simply examining the vector timestamps
instead of the entire d-diagram.

%\begin{lemma}\label{lem:vc}
%Given two events $e^i$ and $f^j$, $V(e^i) < V(f^j)$ iff $e^i < f^j$.
%\end{lemma}
%\begin{proof}
%  Follows from the fact that the standard vector clock satisfies this property.
%\end{proof}

%\begin{figure*}[tp]
%\begin{center}
%\includegraphics[width=6in]{expand.0}
%\end{center}
%\caption{Expansion operation being applied on a cut}
%\label{fig:expand}
%\end{figure*}

\section{Detecting Global Predicates}

%-- Use of vector clocks
%-- Defn of vector clocks for p-diagram
%-- Theorem about unrolling till [e] stabilizes
%-- Bound on the size of this unrolling

%-- Algo, analysis and complexity

%-- Comp finite prefix is not good enough for this, example
We now consider the problem of detecting predicates in
d-diagrams. A predicate is a property defined on the states of the processes.
%and possibly channels. 
An example of a predicate is
``more than one philosopher is waiting.''
Given a consistent cut, a predicate is evaluated with respect to the values of
the variables resulting after executing all the events in the cut. If a
predicate $p$ evaluates to true for a consistent cut $C$, we say that $C$
satisfies $p$. %As opposed to the previous work, 
We further assume that the
truthness of a predicate on a consistent cut is governed only by the
\emph{labels} of the events in the frontier of the cut. This assumption implies
that the predicates do not involve shared state such as the channel state. We
define $\mathcal{L}: G \rightarrow L$ to be an onto mapping from the set of
vertices in d-diagram to a set of labels $L$ with the constraint that $\forall e
\in V: \mathcal{L}(e^i) = \mathcal{L}(e^j)$. This is in agreement with modeling
the recurrent events as repetition of the same event. %We refer to this
%assumption as the \emph{index-independence assumption}.

It is easy to see that it does not suffice to detect the predicate on the d-diagram without unrolling it. As a simple example, consider figure \ref{fig:vectorClocks}, where though $\{a^1,d^1\}$ is not a consistent cut, but $\{a^2,d^1\}$ is consistent.

% TODO: Define notion of an ``instance'' of a vertex
 %In other words, $\forall e^i \in G$ is equivalent to $\forall x \in G$ and
 %$\exists e^i \in G$ is equivalent to $\exists x \in G$.
In this section, we  define a finite extension of our d-diagram which enables
us to detect any property that could be true in the infinite poset
corresponding to the d-diagram.  We show that it is sufficient to perform
predicate detection on that finite part. 
%This result is analogous to the
%concept of complete finite prefix~\cite{McMi93a} in the case of petri-nets. 


We mainly focus on the recurrent part of the d-diagram as that is the piece
which distinguishes this problem from the case of finite directed graph. We
identify certain properties of the recurrent part which allows us to apply the
techniques developed for finite directed graphs to d-diagrams. 


%Given a p-diagram, the set of order ideals can be defined in the usual manner.
%This set forms a distributive lattice. Since the poset is infinite, it is clear
%that the poset representing its order ideals is also infinite.
%Can this poset be represented by a p-diagram?
%Consider the p-diagram given below:
%\begin{verbatim}
%  a* || b*
%\end{verbatim} 
%The infinite poset corresponding to the order ideals of this poset is
%equivalent to the grid poset discussed earlier. Hence there is no
%p-diagram to represent order ideals of the above poset.
%However, for finite state systems the set of global states reached would be
%finite and therefore representable by a p-diagram.
%% A natural question is to determine if the given p-diagram
%% has finite number of global states (i.e. can a channel
%%grow in an unbounded manner)
%In distributed computing applications, we are generally interested only in
%finite order ideals.


%\begin{figure*}[tp]
%\begin{center}
%\includegraphics[width=6in]{shift-gap.0}
%\end{center}
%\caption{(a) A d-diagram and (b) its corresponding computation with a cut $C$}
%\label{fig:gap}
%\end{figure*}


Predicate detection algorithms explore the lattice of global
states in BFS order as in Cooper-Marzullo \cite{CoopMarz:ConsDetGP} algorithm, or a particular
order of events as in Garg-Waldecker \cite{GarWal:wpdd} algorithm.
For finite directed graphs,
once the exploration reaches the final global state it signals that the
predicate could never become true. In the case of infinite directed graphs,
there is no final global state. So, the key problem  is to determine the
stopping rule that guarantees that if the predicate ever becomes true then it
would be discovered before the stopping point. For this purpose, we show that
for every cut in the computation, a subgraph of the computation called the
\emph{core} contains a cut with the same label. The main result of this section is 
that the core of the periodic infinite computation is
simply the set of events in the computation with iteration less than or equal to
$N$, the number of processes.

\begin{definition} [core of a computation]
  For a d-diagram $Q$ corresponding to a computation with $N$ processes, we define $U(Q)$, the \emph{core} of $Q$, as the directed
  graph given by the set of events $E' = \{ e^j | e \in R \wedge 2 \leq j \leq N \} \cup \{e^1 |
  e \in V \}$ and the edges are the restriction of $\rightarrow$ to set $E'$.
\end{definition}

The rest of the section is devoted to proving the completeness of the core of
a computation. 
The intuition behind the completeness of the core is as follows: For any
frontier $C$, we can perform a series of shift operations such that the resulting
frontier is consistent and lies in the core.
We refer to this operation as a
\emph{compression} operation and the resulting cut is denoted by the frontier
$\mathscr{C}(C)$.  \figref{compression} shows the cut $C = \{e^5, f^3, g^1\}$
and the compressed cut $\mathscr{C}(C) = \{e^3, f^2, g^1\}$. 
%It can be shown
%$\mathscr{C}(C)$ is a consistent cut if $C$ is a consistent cut and
%$\mathcal{L}(C) = \mathcal{L}(\mathscr{C}(C))$. 
%Since $\mathscr{C}(C)$
%has at most $N$ elements and every gap in the cut is less than or equal to one,
%the maximum iteration number of any element in the cut is less than or equal to
%$N$.  Therefore, the cut must lie in the core.

%on the cut such that any \emph{gap}
%in the cut is of size at most 1. The resulting 

%equivalent to \emph{compressing} the
%\emph{gaps} in the cut $C$  


%For the d-diagram in \figref{shift}(a), the part of the poset shown in
%\figref{shift}(b) is the core of the d-diagram.
\begin{figure*}[htb]
\begin{center}
  \includegraphics[width=4.5in]{compress.0}
% \includegraphics[width=4.5in]{compress.fig.eps}
\end{center}
\caption{Compression operation being applied on a cut}
\label{fig:compression}
\end{figure*}
For proving the completeness of the core, we define the notion of a
\emph{compression} operation. Intuitively, compressing a consistent cut 
applies the shift operation multiple times such that
the final cut obtained lies in the core of the computation and
has the same labeling.
%removes
%all the gaps between iterations and results in a smaller consistent cut with the
%same labeling. 
%To define {\em compression}, it is convenient to first define
%{\em partial frontier}.
\begin{definition}[Compression] 
  Given a frontier $C$ and index $i$ , define 
  $\mathscr{C}(C,i)$ as shifting of all events with index
greater than $i$ by sufficient iterations such that in the shifted
frontier the event with next higher index than $i$ is $i+1$.
  The cut obtained after all possible compressions is denoted as
  $\mathscr{C}(C)$. 
%  S_{-j}(C, C_i)$. In other words, the operation $\mathscr{C}$ shifts all the
%  events in $C$ with iteration greater than $i$ back by $j$ iterations.  \\
%  We use $\mathscr{C}(C, i)$ to refer to $\mathscr{C}(C, i, gap(C, i) - 1)$. In
%Let $m = |indices(C)|$. Then \\ $\mathscr{C}(C) =
  %\mathscr{C}(\mathscr{C}(\ldots \mathscr{C}(C, indices(C)[m]),
  %indices(C)[m-1]), \ldots)$.
\end{definition}

In \figref{compression},
consider the cut $C =  \{e^5, f^3, g^1\}$. When we apply $\mathscr{C}(C,1)$,
we shift events $e^5$ and $f^3$ back by $1$. This results in the cut $\{e^4, f^2, g^1\}$.
The next higher index in the cut now is $2$ in $f^2$. We now apply another compression
at index $2$, by shifting event $e^4$,
and the compressed cut $\mathscr{C}(C) = \{e^3, f^2, g^1\}$. 
As another example, consider a cut $C = \{e^7, f^4, g^4\}$. We first
apply $\mathscr{C}(C,0)$ to get the cut $\{e^4,f^1,g^1\}$. Applying the
compression at index $1$, we finally get $\{e^2,f^1,g^1\}$.

%\begin{lemma}[Concurrency ]\label{lem:concur}
%  If $e^i \parallel f^j$ where $j \geq i + 1$, then $e^i \parallel f^{i+l}$ for
%  $1 \leq l \leq j - i$.
%\end{lemma}
%\begin{proof}
%  Since $i + l > i$, by the property of the d-diagram $f^{i+l} \not < e^i$.
%  Moreover, $e^i \parallel f^j$ implies $\forall f^{k}, k \leq j: e^i \not <
%  f^{k}$. Therefore, $e^i \parallel f^{i+l}$.
%\end{proof}

Note that the cut resulting from the compression of a cut $C$ has the same
labeling as the cut $C$. The following lemma shows
that it is safe to apply compression operation on a consistent cut i.e.
compressing the gaps in a consistent cut results in another consistent cut.
This is the crucial argument in proving completeness of the core.

\begin{lemma}\label{lem:compress}
  If $C$ is the frontier of a consistent cut, then $\mathscr{C}(C, l)$ corresponds to a consistent cut for
  any index $l$.
\end{lemma}
\begin{proof}
  Let $C' = \mathscr{C}(C,l)$ for convenience. Consider any two events
  $e^i, f^j \in C$. If $i \leq l, j \leq l$ or $i > l, j > l$, then
  the events corresponding to $e^i$ and $f^j$ in $C'$ are also consistent.
  When $i > l$ and $j > l$, events corresponding to $e^i$ and $f^j$ in $C'$
  get shifted by the same number of iterations.
  
  Now assume $i \leq l$ and $j > l$. Then $e^i$ remains unchanged in $C'$
  and $f^j$ is mapped to $f^a$ such that $a \leq j$. Since $i < a$, there is no
  path from $succ(f^a)$ to $e^i$. 
  If there is a path from $succ(e^i)$ to $f^a$,
  then there is also a path from $succ(e^i)$ to $f^j$ as there is a path from
  $f^a$ to $f^j$. This contradicts the fact that $e^i$ and $f^j$ are consistent.
  Hence, every pair of vertices in the cut $C'$ is consistent.
\end{proof}

%The above proof has used the fact that when $i < a$, there is no path from 
%$succ(f^a)$ to $e^i$. When $i$ equals $a$, there may be a path; therefore,
%we cannot reduce the gap between successive indices to $0$ (rather than $1$).

%Repeated application of the above lemma to compress all the gaps leads to the
%following result.
%\begin{corollary}\label{cor:max-compress}
  %If $G$ is the frontier of a consistent cut, then $\mathscr{C}(G)$ is a consistent cut.
%\end{corollary}

Now we can use the compression operation to compress any consistent cut to a 
consistent cut
in the core. Since the resulting cut has the same labeling as the original cut,
it must satisfy any non-temporal predicate that the original cut satisfies. The
following theorem establishes this result.

\begin{theorem}\label{lem:stop}
  If there is a cut $C \in \C(\compt)$, then there exists a cut
  $C' \in \C(U(Q))$ such that $\mathcal{L}(C) = \mathcal{L}(C')$.
\end{theorem}
\begin{proof}
  Let $C' = \mathscr{C}(C)$. 
By repeated application of the lemma \ref{lem:compress}, we get that
$C'$ is a
  consistent cut and $\mathcal{L}(C) = \mathcal{L}(C')$. Moreover, by
repeated compression, no event in $C'$ has index
greater than $N$. Therefore, $C' \in U(Q)$.
\end{proof}

The completeness of the core implies that the algorithms for predicate detection
on finite directed graphs can be used for d-diagrams as well after
unrolling the recurrent events $N$ times. This result
holds for any global predicate that is non-temporal (i.e., defined on
a single global state). Suppose that the global predicate $B$ never becomes
true in the core of the computation, then we can assert that there
exists an infinite computation in which $B$ never becomes true (i.e., 
the program does not satisfy that eventually $B$ becomes true).
Similarly, if a global predicate $B$ is true in the
recurrent part of the computation, it verifies truthness of the temporal 
predicate that $B$ becomes true infinitely often. 



\section{Recurrent Global State Detection Algorithm}

We now briefly discuss a method to obtain a d-diagram from a finite
distributed computation.
The {\em local state} of a process is the value of all the variables 
of the process including the program counter. The {\em channel} state
between two processes is the sequence of messages that have been 
sent on the channel but not received.
A {\em global state} of a computation is defined to be the cross product
of local states of all processes and all the channel states at any
cut.
Any consistent cut of the computation determines a unique
consistent global state. A global state is {\em recurrent} in a
computation, if there exist consistent cuts $Y$ and $Z$
such that the global states for $Y$ and $Z$ are identical
and $Y$ is a proper subset of $Z$.
%for all processes $i$, $Y[i]$ is a proper subset of $Z[i]$.
Informally, a global state is recurrent if 
there are at least two distinct instances of that global state in 
the computation.
%and that some process has executed at least one event between those two instances.

We now give an algorithm to detect recurrent global states
of a computation. 
We assume that the system logs the message order and nondeterministic 
events so that the distributed computation can be exactly replayed.
We also assume that the system supports a vector clock mechanism.

The first step of our recurrent global state detection (RGSD)
algorithm consists of computing the global state
of a distributed system. Assuming FIFO, we could use
the classical Chandy and Lamport's algorithm\cite{ChanLamp:Snap} for this purpose.
Otherwise, we can use any of the algorithms, such as
\cite{Matt:GVT,GGS06,DBLP:conf/cluster/Kshemkalyani09}.
Let the computed global snapshot be $G$. 
Let $Z$ be the vector clock for the global state $G$.
%For RGSD algorithm, it
%will be convenient to compute a global snapshot in which all channels
%are empty. This can be done, for example, by algorithms in 
%\cite{art:hel90}, or by recognizing that the predicate "all channels
%are empty" is a linear predicate and using algorithm for 
%detecting linear predicates\cite{ChaGar:DC}. 
%By using any of the previous approaches, we obtain
%a global state $G$ which consists of local states of all processes
%and all channel states as empty. 
 
The second step consists of replaying the distributed computation
while monitoring the computation to determine the least consistent
cut that matches $G$.
%\footnote{The global state matches $G$ is also a linear
%predicate and therefore there exists the least consistent cut that
%matches $G$}. 
We are guaranteed to hit such a global state because
there exists at least one such global state (at vector time $Z$) in the
computation. Suppose that the vector clock of the detected
global state is $Y$. 
We now have two vector clocks $Y$ and $Z$ corresponding to the global state $G$.
If $Y$ equals $Z$, 
we continue with our computation. Otherwise, we have succeeded
in finding a recurrent global state $G$.

Note that replaying a distributed computation requires
that all nondeterministic events (including the message order) be
recorded during the initial execution \cite{LeBMel87}.
Monitoring the computation to determine the least consistent cut that 
matches $G$ can be done using algorithms for conjunctive predicate
detection \cite{Garg:1994:DWU,DBLP:journals/jpdc/GargCKM97}.

When the second step fails to find a recurrent global state, the first step
of the algorithm is invoked again after certain time interval.
We make the following observation about the recurrent global state detection
algorithm.
\begin{theorem}
\label{thm:RGSD}
If the distributed computation is periodic then the algorithm will detect
a recurrent global state. 
Conversely, 
if the algorithm returns a recurrent global state $G$, then there exists
an infinite computation in which $G$ appears infinitely often.
\end{theorem}
\begin{proof}
The RGSD algorithm is invoked periodically and therefore it will be invoked at least 
once in repetitive part of the computation. This invocation will compute a
global state $G$. Since the computation is 
now in repetitive mode, the global state $G$ must have occurred earlier and the
RGSD algorithm will declare $G$ as a recurrent global state.

We prove the converse by constructing the infinite computation explicitly.
Let $Y$ and $Z$ be the vector clocks corresponding to the
recurrent global state $G$. Our infinite computation will first
execute all events till $Y$. 
After that it will execute
the computation that corresponds to events executed between $Y$ and $Z$.
Since $Y$ and $Z$ have identical global state, the computation after
$Y$ is also a legal computation after $Z$.
By repeatedly executing this computation, we get an infinite legal computation
in which $G$ appears infinitely often.
\end{proof}

The proof of Theorem \ref{thm:RGSD} also shows how we can construct a p-diagram
given the recurrent global state $G$. Let $Y$ and $Z$ be the vector clocks corresponding
to the global state $G$. All the events between $Y$ and $Z$ are modeled as recurrent vertices.
For every process, we add shift-edges from the last event in $Z$ to the first event after $Y$
on that process. In addition, for every message that is in channel at the global state in $Z$, we add 
a shift edge
from the send event on the sending process to the receive event.
An example of this construction is Fig. \ref{fig:pmutex}. The global state after $\beta$ and $\beta$ followed
by $\gamma$ are recurrent. The computation in Fig: \ref{fig:vectorClocks}(a) shows an example in
which the shift edge in p-diagram is from one process to the other.

It is important to note that our algorithm does not guarantee that
if there exists any recurrent global state, it will be detected
by the algorithm. It only guarantees that if the computation is
periodic, then it will be detected.

We note here that RGSD algorithm is also useful
in debugging applications in which the distributed program
is supposed to be terminating and presence of a recurrent global state itself
indicates a bug.

%In this paper, we consider reactive systems that
%may be non-terminating. Thus, presence of an infinite computation itself
%is not an indication of a bug. Our next goal
%is to capture the infinite computation and analyze it
%for user specified properties. 
%The next section goes over
%our method of modeling infinite distributed computation.

%We do not model a distributed computation as a graph of reachable global states
%because there is a combinatorial explosion in the number of global states
%with the number of processes. In other words, the number of global
%states of a computation with $N$ processes may be as large as an
%exponential in $N$. Instead, we model a distributed computation as a partial 
%order of events, such that consistent cuts of the partial order represents
%the global states. Since the global states are not explicit in our
%model of computation, the notion of recurrent global state has to
%be mapped to the notion of recurrent events to capture periodicity.
% TODO: Mention that the detection is for arbitrary predicate so can be used
% after slicing to detect other types of predicates
\newcommand{\kse}{\mbox{\emph{k-shift-edges }}}
\section{Computing Slice of a Computation}
In this section we present an algorithm to compute slice of a periodic computation.
We first provide a brief introduction to slicing, then we generalize the notion
of d-diagrams by introducing \kse because the slice is more conveniently
expressed using generalized d-diagram. Then, we give an algorithm
to compute the slice.
\subsection{Background on Slicing}
In the earlier work~\cite{GarMit:2001:ICDCS,MitGar:2001:DISC}, the notion of
slicing was used for finite directed graphs and was based on the Birkhoff's
Representation Theorem for Finite Distributive Lattices~\cite{DavPri:1990:CUP}.
Informally, a computation slice (or simply a slice) is a concise representation
of all those consistent cuts of the computation that satisfy the predicate.

In this work, we extend the notion of slicing for infinite directed graphs by
focusing only on finite order ideals~\cite{DavPri:1990:CUP}. As mentioned
earlier as well, we deal only with finite consistent cuts and refer to them
simply as consistent cuts.  Similar to the the Birkhoff's representation
theorem~\cite{DavPri:1990:CUP}, the following theorem is known for the case of
finite order ideals of an infinite poset:

\begin{theorem}\label{thm:stanley} [~\cite{Stan:1986:Book}, Proposition 3.4.3] 
  Let $P$ be a poset such that every principal order ideal is finite. Then the
  poset $J_f(P)$ of finite order ideals of $P$, ordered by inclusion, is a
  finitary distributive lattice. Conversely, if $L$ is a finitary distributive
  lattice and $P$ is its subposet of join-irreducibles, then every principal
  order ideal of $P$ is finite and $L = J_f(P)$.
\end{theorem}

We can use the above theorem instead of the Birkhoff's theorem and generalize
the notion of slice for consistent cuts to the following definition.

\begin{definition} [slice] The slice of a directed graph $G$ with respect to a predicate
  $p$ is the directed graph whose consistent cuts form the smallest sublattice
  that contains all the consistent cuts satisfying the predicate $p$.
\end{definition}

This definition is equivalent to the definition of slice in the earlier work for
finite directed graphs. It can be easily shown that the slice for a predicate
always exists and is unique. Since the slice of an infinite directed graph can
again be an infinite directed graph, we use d-diagram to represent the slice of
a computation as well. We later show that if the original computation was
representable using d-diagram, then the slice of the computation is also
representable by d-diagram.

We denote the slice of the computation $\langle E, \rightarrow \rangle$ with
respect to a predicate $p$ by $\slice{\langle E, \rightarrow \rangle}{p}$. Note
that $\langle E, \rightarrow \rangle = \slice{\langle E, \rightarrow
  \rangle}{true}$. Every slice derived from the computation $\langle E, \rightarrow
\rangle$ has the trivial consistent cut $\emptyset$ among its set of consistent cuts. A
slice is \emph{empty} if it has no non-trivial consistent
cuts~\cite{MitGar:2001:DISC}.  In the rest of the paper, unless otherwise
stated, a consistent cut refers to a non-trivial consistent cut.

In general, a slice contains consistent cuts that do not satisfy the predicate
(besides trivial consistent cut $\emptyset$). In case a slice does not contain any such
cut, it is called \emph{lean}. The slice for the class of predicates called
\emph{regular predicates} is always lean. Given a computation, the set of
consistent cuts satisfying a regular predicate forms a sublattice of the set of
consistent cuts of the computation~\cite{GarMit:2001:ICDCS}. Equivalently,

\begin{definition}[regular predicate \cite{GarMit:2001:ICDCS}] A predicate is
  regular if given two consistent cuts that satisfy the predicate, the
  consistent cuts obtained by their set union and set intersection also satisfy
  the predicate. Formally, given a regular predicate $p$,\\
  ($C$ satisfies p) $\wedge$ ($D$ satisfies p) $\implies$ ($C \cap D$ satisfies
  p) $\wedge$ ($C \cup D$ satisfies p)
\end{definition}

%We say that a regular predicate is \emph{non-temporal} if it does not contain
%temporal operators such as $\EF$, $\AG$, and $\EG$, otherwise it is a
%\emph{temporal} regular predicate.

Some examples of regular predicates are conjunction of local
predicates such as ``$P_i$ and $P_j$ are in critical section'', and relational
predicates such as $x_1 - x_2 \leq 5$, where $x_i$ is a monotonically
non-decreasing integer variable on process $P_i$.  From the definition of a
regular predicate we deduce that a regular predicate has a least satisfying cut
as the lattice of order ideals has a bottom element.  Furthermore, the class of
regular predicates is closed under conjunction~\cite{GarMit:2001:ICDCS}.

For a regular predicate $p$ and an element $x \in G$, we define $J_p(x)$ as the
least consistent cut which satisfies $p$ and includes $x$. If there is no cut
that satisfies $p$ and includes $x$, $J_p(x)$ is defined to be $NULL$; otherwise
$J_p(x)$ is well-defined as the regular predicates are closed under
intersection.
\subsection{Generalized d-diagram}
For computing slice of a d-diagram it is covenient to first 
generalize the d-diagrams by having \kse which
increase the iteration of a vertex by $k$ for any arbitrary $k$ instead of a
simple shift-edge. We call such a d-diagram as the \emph{generalized d-diagram}.

\begin{figure*}[tp]
\begin{center}
\includegraphics[width=6in]{generalized.0}
\end{center}
\caption{(a) A generalized d-diagram and (b) its equivalent d-diagram}
\label{fig:generalized}
\end{figure*}

\begin{definition} [generalized d-diagram] A generalized d-diagram is a
  set $(V, R, F, B_1, B_2, \ldots, B_m)$ where $m$ is the maximum $k$ such that
  a \kse is present in the d-diagram and $B_k \subseteq (V \times R)$ is
  the relation of \kse with the property: \\
  If $(e, f) \in B_k$, then $e^i \rightarrow f^{i+k}$.
\end{definition}

Note that in the above definition, we allow the shift edges to be present
between non-recurrent and recurrent vertices as well. Clearly d-diagrams are a
special case of the generalized d-diagrams where $m=1$ and $B_1 \subseteq R \times R$. The following theorem further shows that the generalized d-diagram
are not any more expressive than the d-diagrams. 

\begin{theorem}\label{thm:general-ddiagram}
  Let $(V, R, F, B_1, B_2, \ldots, B_m)$ be a generalized d-diagram and $\compt$
  be the infinite graph generated by it. Then there exists a d-diagram $(V', R',
  F', B')$ such that the graph $\langle E', \rightsquigarrow \rangle$ generated
  by the d-diagram is isomorphic to the graph $\compt$.
\end{theorem}
\begin{proof}
  We construct the d-diagram corresponding to the generalized d-diagram as
  follows. %For every $e \in V \setminus R$, $e$ is added to $V'$. For every $e
%  \in R$, $e_1, \ldots, e_m$ are added to $V'$ and $R'$. The set of forward
%  edges $F'$ is constu in the following way:
  \begin{enumerate}
  \item $V' = \{ e_1 | e \in V \} \cup \{ e_i | e \in R \textrm{ and } 2 \leq i \leq m + 1\}$
  \item $R' =  \{ e_i | e \in R \textrm{ and } 1 \leq i \leq m+1 \}$
  \item $F' = \{ (e_1, f_1) | (e, f) \in F \}$ \\
    $\cup      \{ (e_i, f_{i+k})| (e, f) \in B_k \textrm{ and }
    1 \leq i \leq m+1-k\}$
  \item $B' = \{ (e_i, f_j) | (e, f) \in B_k \textrm{ and } m + 1 - k < i \leq m+1 \textrm{ and } j = (i + k) \textrm{ mod } m+1) \}$
  \end{enumerate}

  Now we show that the graph $\langle E', \rightsquigarrow \rangle$ generated by
  $(V', R', F', B')$ is isomorphic to the graph $\compt$. Let $\mu: E
  \rightarrow E'$ be the isomorphism function between the elements in
  $E$ and $E'$ defined as follows:
  \begin{enumerate}
  \item $\mu(e^1) = e_1^1$ if $e \in V \setminus R$.
  \item $\mu(e^i) = e_k^l$ if $e \in R$. Here $k = 1 + (i-1) \textrm{ mod } m+1$ and $l = 1 + (i-1)/(m+1)$.
  \end{enumerate}
  
  With this isomorphism function, it is easy to show that $(e^i, f^j) \in
  \mypath( \langle E', \rightsquigarrow \rangle)$ iff $(\mu(e^i), \mu(f^j)) \in
  \mypath( \compt )$.
\end{proof}  \eosqed

\figref{generalized} shows an example of this conversion. The dotted edges
labeled with a number $k$ denote the \kse and the unlabeled dotted
edges denote the simple shift edges. We have essentially created multiple copies of
the recurrent vertices and redrawn the \kse in terms of simple
shift-edges.

\subsection{Computing Join-Irreducibles of the Lattice Satisying $p$}
\begin{figure*}[tp]
\begin{center}
\includegraphics[width=6in]{expand.0}
\end{center}
\caption{Expansion operation being applied on a cut}
\label{fig:expand}
\end{figure*}

We first define an expansion function analogous to the compression operation. The
expansion function allows expansion of a cut while maintaining the labeling.

\begin{definition} [expansion of a cut]
  Given a cut $G$ and $i \in indices(G)$ , define $\mathscr{E}(G, i, j) =
  S_{j}(G, G_i)$. In other words, the operation $\mathscr{E}$ shifts all the
  events in $G$ with iteration greater than $i$ forward by $j$
  iterations.
\end{definition}

As opposed to the compression operation, expansion cannot be applied to any
event in the frontier of a cut while maintaining its consistency. We define the
notion of an \emph{expansion point} in a cut which gives a safe way of expanding
a cut.

\begin{definition} [expansion point]
  We define $\rho \in indices(G)$ to be an expansion point for a consistent cut
  $G$ if $\forall e^{i}, f^{j} \in G$ with $i \leq \rho$ and $j > \rho$, $(e^i,
  f^{k}) \not \in \cpath$ for any $k \geq j$.
\end{definition}

As an example, let $C = \{e^3, f^1, g^1\}$ as shown in \figref{shift}. Then
$\rho = 1$ is an expansion point as $f^1 \parallel e^3$ and $g^1 \parallel e^3$.
The expansion operation $\mathscr{E}(G, \rho, 1)$ results in the frontier
$\{e^4, f^1, g^1\}$ which is also consistent. The next lemma shows that this is
true in general;a cut always allows expansion around the expansion point.

\begin{lemma}\label{lem:expand}
  Let $G$ be a consistent cut such that it has an expansion point $\rho$.
  Then the cut $G' = \mathscr{E}(G, \rho, l)$ is a consistent cut for any $l \geq 0$.
\end{lemma}
\begin{proof}
  We show that events in the frontier of the cut $G'$ are consistent. Any two
  events $e^i, f^j \in G$ with $i \leq \rho, j \leq \rho$ or $i > \rho, j >
  \rho$ are still consistent in $G'$ as the relationship between these events
  remains the same as in $G$. When $i \leq \rho$ and $j > \rho$, $e^i$ is mapped
  to $e^i$ and $f^j$ is mapped to $f^{j+l}$ in $G'$. By definition of an
  expansion point, $(e^i, f^{j+l}) \not \in \cpath$. Hence, all the pairs of events in
  frontier of $G'$ are consistent.
\end{proof}  \eosqed

The above result provides a way to expand a cut while maintaining the
consistency of the cut. Using the expansion and compression operations, we can
move back and forth in the computation while maintaining the labeling of the
cut.

% **********************************************

%The following lemma shows that 

%\begin{lemma}\label{lem:j-include}
%  If $J_p(e^i)$ exists, then $e^{i+1} \not \in J_p(e^i)$ for $i \geq N + 1$ .
%\end{lemma}
%\begin{proof}
%  Let $f^j \in frontier(J_p(e^i))$ such that $proc(f^j) = proc(e^i)$. If
%  $e^{i+1} \in J_p(e^i)$, then $j \geq i+1$. Then there exists $l \in
%  indices(J_p(e^i))$ such that $l \leq j$ and $gap(J_p(e^i), l) > 1$ as $j > N +
%  1$. Consider the cut $C = \mathscr{C}(J_p(e^{i}), l, 1)$. $C$ has $f^{j-1}$ in
%  its frontier as $l < j$. Since $(e^i, f^{j-1}) \in \cpath$ and
%  $\mathcal{L}(J_p(e^i)) = \mathcal{L}(C)$, $C$ is a cut smaller than $J_p(e^i)$
%  which contains $e^i$ and satisfies $B$. This leads to contradiction and so
%  $e^{i+1} \not \in J_p(e^i)$.
%\end{proof}

% ****************************************************

%We now present some results which show that $J_B(e^i)$ acquires a repeating
%structure for all $i > i_0$ and thus can be captured by using p-timestamps. %For
%%this discussion, we assume that the $B$ is a conjunction of local predicates.
%%Since we are not considering channel predicates, the most common predicates
%%in linear predicates can be captured through this class.

%%\begin{definition} 
%%  Let $C$ be a consistent cut with at least one expansion pair. Let $(e^i,
%%  f^j)$ be the \emph{least} expansion pair in $C$. Then define $\zeta(C) =
%%  S_1(C,F)$ with $F = \{g | g^l \in frontier(C) \wedge l \geq j \}$ as the .
%%\end{definition}


%% Define the new shifting and then show the rule about the shift invariance of
%% the thing.

% Lem : J_p(e^i) and J_p(e^{i+1}) differ by at most 1 iteration at some places.
% Also the difference starts before e and continues for all elements with
% iterations greater than i.

%The next lemma shows that after certain number of iterations, every cut
%$J_p(e^i)$ contains at least one expansion pair occuring before $i$.

While the compression and expansion operations are general operations which are
applicable to any cut in the poset, we now examine the structure of the cuts
$J_p(e^i)$. For this purpose, we define the notion of helper processes for an
event $e^i$. Intuitively, there is an event $f^j$, $f \in R$, in every helper
process such that there is a path from the event $f^j$ to $e^i$. Therefore, as
a cut advances along $proc(e)$, it must advance along the helper processes as
well.

\begin{definition} [helper processes]
  For an event $e^i$, we define the helper processes for $e^i$ as $H(e^i) = \{
  P_k | \exists f \in R \wedge f^j \in J(e^i) \wedge proc(f) = P_k \}$.
\end{definition}

For our example d-diagram in \figref{shift}, $H(f^2) = \{ P_1, P_2 \}$. Some
properties of helper processes are easy to show.

\begin{lemma} \label{lem:comp-prop}
  The following properties relating to helper processes hold:
  
  \begin{itemize}
  \item For all $i,j > \eta$, $H(e^i) = H(e^j)$. For $i > \eta$, $H(e^i)$ is
    denoted simply by $H(e)$. 
  \item For event $e^i, f^i$ with $i > \eta$ and $proc(e) = proc(f)$, $H(e) =
    H(f)$.
  \item Let $f^j$ be an event such that $proc(f) \not \in H(e)$ and
    $g^l$ be an event such that $proc(g) \in H(e)$ with $j < l$ and $l > 1$.
    Then $(f^j, g^l) \not \in \cpath$.
  \end{itemize}
\end{lemma}

The first property says that the set of helper processes becomes fixed for
different instances of an event after a certain number of iterations. This
follows from the fact that the cut $J(e^i)$ stabilizes after some iterations.
The second property says that after certain number of iterations, the set of
helper processes becomes the same for every event on a process. This follows
from the first property and the fact that there is a path between every two
events in a process. The third property establishes the transitivity of the
relation of helper processes.

%\begin{proof}
%  Follows from the fact that $J(e^{i+1}) = S_1(J(e^i))$ for $i > \eta$.
%\end{proof}

%As a consequence of the above result, we would denote $H(e^i)$ simply by $H(e)$
%for $i > \eta$.

%\begin{lemma}\label{lem:history}
  
%\end{lemma}
%\begin{proof}
%  First assume that $\mathcal{P}(f) \in H(e)$. By definition of $H(e)$,
%  $\exists i: \exists g^{j+1} \in J(e^i): \mathcal{P}(f) =
%  \mathcal{P}(g)$. By the definition of a process, $f^{j} < g^{j+1} < e^i$.
  
%  Now assume that $f^j < e^i$ for some $i > \eta$. Then clearly $f^j \in J(e^i)$
%  and hence $\mathcal{P}(f) \in H(e)$.
%\end{proof}

%\begin{corollary}\label{cor:hist-parallel}
  
%\end{corollary}
%\begin{proof}
%  Since $j < l$, $f^j \parallel g^l$ or $f^j < g^l$. If $f^j < g^l$, then by
%  Lemma~\ref{lem:history} there exists $i > \eta$ such that $f^j < g^l < e^i$.
%  This implies that $f^j \in H(e)$ which leads to contradiction. Hence $f^j
%  \parallel g^l$.
%\end{proof}

%The above result is reminiscent of the property of the expansion point. In the
%subsequent part, we show that $J_p(e^i)$ has an expansion point which is based
%on the split between processes in $H(e)$ and outside $H(e)$.

%\begin{definition}
%  We can consider a predicate $B$ as a set of labelings on which the predicate
%  is true in the poset i.e. $B = {L_1, L_2, L_m}$. Then we define the projection
%  of $B$ on a set of processes $S$, $B_S$, as the set of labelings projected on
%  the set of the processes in $S$. 
%\end{definition}

% 1. All events in H(e) are connected
% 2. For strongly connected components, J_p(e) is incremented on all events

Now we can give a characterization of the cut $J_p(e^i)$ in terms of the
helper processes. In all the following results, we assume that $J_p(e^i)$
exists for the event $e^i$ under consideration. We deal with the case when
$J_p(e^i)$ does not exist later. The following lemma shows that after certain iterations
only the events from helper processes in $frontier(J_p(e^i))$ have iterations ``close''
to $i$ and other events always have iterations less than $N - |H(e)|$. This follows our
intuition that helper processes advance along with the event $e^i$.

\begin{lemma}\label{lem:J-struct}
  For $i > N - |H(e)| + \eta$, $frontier(J_p(e^i))$ can be written as $C \cup D$,
  where
  \begin{enumerate}
  \item $f^j \in C \Rightarrow (proc(f) \not \in H(e)) \wedge (j \leq N - |H(e)|)$

  \item $f^j \in D \Rightarrow (proc(f) \in H(e)) \wedge (j > N - |H(e)|)$
\end{enumerate}
\end{lemma}
\proofsketch Let $C'$ be the projection of $frontier(J_p(e^i))$ on the set of
processes $P \setminus H(e)$. Then let $C = \mathscr{C}(C')$ and $D$ be the
projection of $frontier(J_p(e^i))$ on the processes $H(e)$. Since $J(e^i)
\subseteq J_p(e^i)$, for an event $f^j \in D$, $i - j \leq \eta$. Therefore, if
$f^j \in D$, $j > N - |H(e)|$. On the other hand, $C$ must belong to the core $U(Q)$ and
therefore, if $f^j \in C$, then $j \leq N - |H(e)|$. This further implies that for all
$f^j \in C$ and $g^l \in D$, $j < l$. By \lemref{comp-prop}, this implies that
$f^j$ and $g^l$ are consistent. Therefore, every pair of vertices in the set $C
\cup D$ is consistent and so it forms the frontier of a consistent cut. Let the
cut given by $C \cup D$ be $C''$. Then, $\mathcal{L}(J_p(e^i)) =
\mathcal{L}(C'')$ and so $C''$ also satisfies the predicate $p$. It includes
$e^i$ as $e^i \in D$.  Therefore, $C''$ is a consistent cut which includes $e^i$
and satisfies $p$. By definition of $J_p(e^i)$, $J_p(e^i) \subseteq C''$.
However, $C'' \subseteq J_p(e^i)$ as $C''$ was obtained by applying compression
on the cut $J_p(e^i)$. Therefore, $J_p(e^i) = C''$.
\eosqed

\begin{figure*}[tp]
\begin{center}
\includegraphics[width=4in]{companion.0}
\end{center}
\caption{The cuts $J_p(f^2)$ and $J_p(f^3)$ where $p$ is $(x=1) \wedge (y=1) \wedge (z=1)$}
\label{fig:companion}
\end{figure*}

\figref{companion} shows the cuts $J_p(f^2)$ and $J_p(f^3)$ where $p$ is $(x=1)
\wedge (y=1) \wedge (z=1)$. Here $H(f^3) = \{ P_1, P_2 \}$ and so we can
decompose $J_p(f^3)$ into subsets $C$ and $D$ of \lemref{J-struct} as $C = \{
c^1 \}$ and $D = \{ d^3, f^3 \}$.

%Now we show that the cut $J_p(e^i)$ stabilizes for $i > \eta + N$.
%\begin{theorem}\label{thm:repeat-structure}
%  For all $i \geq \eta + N$, $J_p(e^{i+1}) = C \cup S_1(D)$ where $(C, D)$ is
%  the expansion pair for $J_p(e^i)$.
%\end{theorem}
%\begin{proof}
%  Consider $C_1 = \mathscr{E}(J_p(e^i), \rho, 1)$. By Lemma~\ref{lem:expand}
%  $C_1$ is consistent.  Since $C_1$ includes $e^{i+1}$ and satisfies $B$,
%  $J_p(e^{i+1}) \subseteq C_1$. Moreover, $J_p(e^i) \subseteq J_p(e^{i+1})$. As
%  a result, $f^j \in frontier(J_p(e^{i+1}))$ can be characterized as follows:
%  \begin{enumerate}
%  \item If $j \leq \rho$, then $f^j \in frontier(J_p(e^{i}))$
%  \item If $j > \rho$, then $\exists g^k \in frontier(J_p(e^i)): g^k \leq f^j \leq
%    g^{k+1}$. This also implies that $j = k$ or $j = k + 1$.
%  \end{enumerate}

%%  In particular, $x^a \in frontier(J_p(e^{i+1}))$ and $\exists z^k \in
%%  frontier(J_p(e^{i+1}))$ such that $y^b \leq z^k \leq y^{b+1}$. Therefore,
%%  $x^a$ and $z^k$ form the expansion pair for $J_p(e^{i+1})$ with $a \leq i+1$.

%  Now consider $C_2 = \mathscr{C}(J_p(e^{i+1}, \rho, 1)$. $C_2$ is a consistent
%  cut, includes $e^i$ and satisfies $B$. Therefore, $J_p(e^i) \subseteq C_2$.
%  Based on the operation $\mathscr{C}$, an event $f^j \in frontier(C_2)$,
%  satisfies the following:
%  \begin{enumerate}
%  \item If $j \leq \rho$, then $f^j \in frontier(J_p(e^{i+1}))$
%  \item If $j > \rho$, then $f^{j+1} \in frontier(J_p(e^{i+1}))$
%  \end{enumerate}
  
%  From the characterization of $J_p(e^{i+1})$, it is clear that for $j \leq
%  \rho$, $f^j \in frontier(J_p(e^i))$. For $j > \rho$, we have $g^k \leq f^j
%  \leq f^{j+1} \leq g^{k+1}$ for some $g^k \in frontier(J_p(e^i))$. This implies
%  that $f^j = g^k$ and so $f^j \in frontier(J_p(e^i))$. Therefore, $C_2 =
%  J_p(e^{i})$ and also, $C_1 = J_p(e^{i+1})$. Inductively using the above
%  argument for $j > i$, we get that for all $j \geq i$, $J_p(e^{j+1}) =
%  \mathscr{E}(J_p(e^j), \rho, 1)$.
%\end{proof}

%\end{proof}

The above result can also be interpreted in terms of the presence of an
expansion point in the cut $J_p(e^i)$ as the events in $J_p(e^i)$ from the
helper processes lie after iteration $N$ and are disconnected from the rest
of the vertices in $J_p(e^i)$. Henceforth, we relax the condition on $i$ in
\lemref{J-struct} to $i > N + \eta$. This makes the bound independent of $e$ and allows
us to deal with all vertices uniformly.

\begin{corollary}\label{cor:expand-limit}
  If $i > N + \eta$, then $J_p(e^i)$ contains an expansion point $\rho \leq
  N$.
\end{corollary}

%For some of the following results, we use a restricted notion of compression
%which can be interpreted in terms of a compression operation followed by an
%expansion operation (or vice-versa).

%\begin{definition} 
%  For a cut $G$ and iterations $i, j$ with $i < j$, we define the operation
%  $\mathcal{RC}(G, i, m, j) = \mathscr{E}(\mathscr{C}(G, i, m), j, m)$. In other
%  words, this operation compresses the cut $G$ between the iterations $i$ and
%  $j$ by $m$. Analogous to the notion of $\mathscr{C}(G, i)$, we also have the
%  notion of $\mathcal{RC}(G, i, j)$ which does the maximum compression after $i$. 
%\end{definition}

%\begin{corollary}\label{cor:rcompress}
%  If $G$ is a consistent cut and there is an expansion pair $(f^j, g^l)$ in
%  $G$, then $\mathcal{RC}(G, i, j)$ is also a consistent cut for all $i < j$.
%\end{corollary}
%\begin{proof}
%  This follows from the results that it is safe to compress about any gap and to
%  expand about an expansion pair.
%\end{proof}

%%% Actually it has only expansion pair for any values

%The next lemma shows that there can be at most one expansion pair $(a, b)$
%in $J_p(e^i)$ such that $a < i$.

%\begin{lemma}\label{lem:one-expand}
%  $J_p(e^i)$ has at most one expansion pair $(a, b)$ such that $a < i$.
%\end{lemma}
%\begin{proof}
%  Suppose that $J_p(e^i)$ has two expansion pairs $(a, b)$ and $(j, l)$
%  such that $a < i$ and $j < i$. Wlog assume $b < j$. Then consider $C =
%  \mathcal{RC}(C, a, j)$. $C$ is consistent cut, includes $e^i$ and satisfies
%  $B$. Moreover, it is smaller than $J_p(e^i)$ due to the applied compression.
%  This leads to a contradiction as $J_p(e^i)$ is the smallest cut including
%  $e^i$ and satisfying $B$. Hence, $J_p(e^i)$ has at most one expansion pair
%  $(x^a, y^b)$ such that $a < i$.
%\end{proof}

%The next lemma gives an important property of $J_p(e^i)$ relating to compression.
%\begin{lemma}\label{lem:no-compress}
%  $J_p(e^i)$ be a cut with one expansion pair $(a, b)$ such that $a < i$.  Then
%  $\forall j \in indices(J_p(e^i)), j < a: gap(J_p(e^i), j) = 1$. In other
%  words, there is no gap in the cut $J_p(e^i)$ before the iteration $a$.
%\end{lemma}
%\begin{proof}
%  Suppose $\exists j \in indices(J_p(e^i)), j < a: gap(J_p(e^i), j) > 1$. Then
%  consider $C = \mathcal{RC}(C, j, a)$. Since $a < i$, $C$ includes $e^i$,
%  satisfies $B$ and is smaller than $J_p(e^i)$. This leads to contradiction.
%  Hence, there are no gaps in the sequence $PI(J_p(e^i), a)$.
%\end{proof}

The next theorem shows that the presence of an expansion point in the cut
$J_p(e^i)$ is a sufficient condition for $J_p(e^i)$ to acquire a repeating
structure.

\begin{theorem}\label{thm:repeat-structure}
  Let $i$ be the smallest iteration such that $J_p(e^i)$ has an expansion point
  $\rho$. Then for all $j \geq i$, $J_p(e^{j+1}) = \mathscr{E}(J_p(e^j),
  \rho, 1)$.
\end{theorem}
\begin{proof}
  Consider $C = \mathscr{E}(J_p(e^i), \rho, 1)$. By Lemma~\ref{lem:expand},
  $C$ is consistent. Since $C$ includes $e^{i+1}$ and satisfies $B$,
  $J_p(e^{i+1}) \subseteq C$. Moreover, $J_p(e^i) \subseteq J_p(e^{i+1})$. As
  a result, $f^j \in frontier(J_p(e^{i+1}))$ can be characterized as follows:
  \begin{enumerate}
  \item If $j \leq \rho$, then $f^j \in frontier(J_p(e^{i}))$
  \item If $j > \rho$, then $\exists g^k \in frontier(J_p(e^i)): g^k \leq f^j \leq
    g^{k+1}$ and $proc(g) = proc(f)$. This also implies that $j = k$ or $j = k + 1$.
  \end{enumerate}

%  In particular, $x^a \in frontier(J_p(e^{i+1}))$ and $\exists z^k \in
%  frontier(J_p(e^{i+1}))$ such that $y^b \leq z^k \leq y^{b+1}$. Therefore,
%  $x^a$ and $z^k$ form the expandable pair for $J_p(e^{i+1})$ with $a \leq i+1$.

  Now consider $D = \mathscr{C}(J_p(e^{i+1}, \rho, 1)$. $D$ is a consistent
  cut, includes $e^i$ and satisfies $B$. Therefore, $J_p(e^i) \subseteq D$.
  Based on the operation $\mathscr{C}$, an event $f^j \in frontier(D)$,
  satisfies the following:
  \begin{enumerate}
  \item If $j \leq \rho$, then $f^j \in frontier(J_p(e^{i+1}))$
  \item If $j > \rho$, then $f^{j+1} \in frontier(J_p(e^{i+1}))$
  \end{enumerate}
  
  From the characterization of $J_p(e^{i+1})$, it is clear that for $j \leq
  \rho$, $f^j \in frontier(J_p(e^i))$. For $j > \rho$, we have $g^k \leq f^j
  \leq f^{j+1} \leq g^{k+1}$ for some $g^k \in frontier(J_p(e^i))$. This implies
  that $f^j = g^k$ and so $f^j \in frontier(J_p(e^i))$. Therefore, $D =
  J_p(e^{i})$ and also, $C = J_p(e^{i+1})$. Inductively using the above
  argument for $j > i$, we get that for all $j \geq i$, $J_p(e^{j+1}) =
  \mathscr{E}(J_p(e^j), \rho, 1)$.
\end{proof}  \eosqed

For the computation in \figref{companion}, it can be seen that $J_p(f^2)$ has an
expansion point at $\rho = 1$. Therefore, we can write $J_p(f^3) =
\mathscr{E}(J_p(f^2), 1 , 1)$.

The above result essentially establishes the correspondence between the cuts
$J_p(e^i)$ and $J_p(e^{i+1})$ for some large enough $i$. It says that the cuts
have the same iteration of some elements and for the others, the iterations
differ by exactly one. Hence the structure of $J_p(e^i)$ becomes repetitive
once $J_p(e^i)$ has an expansion point. Corollary~\ref{cor:expand-limit} gives
an upper bound ($N + \eta $) on the expansion point for $J_p(e^i)$. Also, note
that this upper bound is independent of the predicate $p$ and just depends on
the d-diagram. For a d-diagram, let $\gamma$ be the maximum over the expansion
points of all the recurrent events. Again, $\gamma$ is bounded by $N + \eta$.

\begin{lemma}\label{lem:J-reln}
  Let $J_p(e^i) \subseteq J_p(f^j)$ with $i, j > \gamma$. Then $J_p(e^{i+1}) \subseteq
  J_p(f^{j+1})$.
\end{lemma}
\begin{proof}
  By Lemma~\ref{lem:J-struct}, $J_p(e^i)$ can be written as $C_1 \cup D_1$ such
  that $g^k \in C_1 \Rightarrow (proc(g) \not \in H(e)) \wedge (k \leq N -
  |H(e)|)$ and $g^k \in D_1 \Rightarrow (proc(g) \in H(e)) \wedge (k > N -
  |H(e)|)$.  Similarly, $J_p(f^j)$ can be written as $C_2 \cup D_2$ with similar
  constraints. Since $J_p(e^i) \subseteq J_p(f^j)$, the above constraints imply
  that $C_1 \subseteq C_2$ and $D_1 \subseteq D_2$. Furthermore, $J_p(e^{i+1})$
  and $J_p(f^{j+1})$ can be decomposed as $C_3 \cup D_3$ and $C_4 \cup D_4$
  respectively. By theorem~\ref{thm:repeat-structure}, $C_1 = C_3$ and $C_2 =
  C_4$. Moreover, if $g^k \in D_1 \Rightarrow g^{k+1} \in D_3$ and similarly,
  $g^k \in D_2 \Rightarrow g^{k+1} \in D_4$. Therfore, $D_1 \subseteq D_2
  \Rightarrow D_3 \subseteq D_4$. Therefore, $J_p(e^{i+1}) \subseteq
  J_p(f^{j+1})$.
\end{proof}  \eosqed

\subsection{A Slicing  Algorithm}
A slice of a computation can have multiple representations. The \emph{skeletal
  representation}~\cite{MitGar:2001:DISC} of the slice has the advantage of
having at most $N$ edges per event in the graph and provides us a compact
representation. Let $F_p(e^i,k)$ denote the earliest event $f^k$ on $P_j$ such
that $J_p(e^i) \subseteq J_p(f^j)$. If no such event exists, then $F_p(e^i, k)$
is considered to be $NULL$. Then the skeletal representation of
$\slice{\compt}{p}$ can be obtained by constructing a graph $\langle E',
\rightsquigarrow \rangle$ as follows: (1) $E' = E \setminus D$ where $D$ is the
set of events $e^i$ for which $J_p(e^i)$ does not exist (2) For an event $e^i
\in E'$, edges are added are from $e^i$ to $succ(e^i)$ and to $F_p(e^i, k)$ for
every process $P_k$. Again we want to represent $\slice{\compt}{p}$ in terms of
a d-diagram as $\slice{\compt}{p}$ may be an infinite graph.

We now show the procedure to obtain the slice of the computation $\compt$ with
respect to the predicate $p$. For this purpose, we define the notion of
\emph{reset cut}.

\begin{definition}[reset cut]
  Let $T \subseteq R$ be the set of recurrent vertices $e$ for which
  $J_p(e^{\gamma})$ exists. Then the reset cut, $\rcut$, for a predicate $p$ is
  the consistent cut given by $\{ \bigcup_{e \in T} J_p(e^{\gamma}) \} \cup \{
  \bigcup_{e \in R \setminus T} J(e^{\gamma}) \}$.
\end{definition}

Note that in the definition of the reset cut we use $J(e^{\gamma})$ if
$J_p(e^{\gamma})$ does not exist for some $e^{\gamma}$. This is done to ensure
that the frontier of the reset cut always contains elements corresponding to
recurrent vertices. The reset cut is a consistent cut as it is a union of
consistent cuts. For our example computation, it can be shown that $\gamma = 3$.
The following cuts can also be computed easily:
\begin{itemize}
\item $J_p(d^3) = \{ d^3, b^1, c^1 \}$
\item $J_p(e^3) = \{ d^4, b^1, c^1 \}$
\item $J_p(f^3) = \{ d^3, f^3, c^1 \}$
\item $J_p(g^3) = \emptyset$, $J(g^3) = \{e^2, f^3, g^3 \}$
\item $J_p(a^1) = \{ d^1, b^1, c^1 \}$
\item $J_p(b^1) = \{ d^1, b^1, c^1 \}$
\item $J_p(c^1) = \{ d^1, b^1, c^1 \}$
\end{itemize}

Then the reset cut $\rcut$ is given by $\{ d^4, f^3, g^3 \}$. 

The d-diagram obtained by unrolling $Q$ about $\rcut$, $\unroll{\rcut}$, has a
crucial property:

\begin{lemma}\label{lem:rcut-prop}
  Let $\langle E', \rightsquigarrow \rangle$ be the directed graph generated by
  $\unroll{\rcut}$. Let $e^i \in \langle E', \rightsquigarrow \rangle$. Then
  $J_p(f^j) \not \subseteq J_p(e^i)$ for all $f^j \in \langle E',
  \rightsquigarrow \rangle$ with $j > i$.
\end{lemma}
\begin{proof}
  Let the d-diagram $\unroll{\rcut}$ be $(V', R', F', B')$. Consider $g^k, h^l
  \in \compt$ such that $J_p(g^k) \subseteq J_p(h^l)$. If $h^l \in \rcut$, then
  by definition of $\rcut$, $g^k \in \rcut$ and hence $\iso{\rcut}(h^l) = a^1$
  and $\iso{\rcut}(g^k) = b^1$ for some $a, b \in V'$. Now consider the case
  when $h^l \not \in \rcut$. Let $m = \textrm{max} \{ i | h^i \in \rcut \}$ and
  $n = \textrm{max} \{ i | g^i \in \rcut \}$. First assume that $l-m < k-n$.
  Then $J_p(g^r) \subseteq J_p(h^m)$ where $r = k - (l-m)$. However, in this
  case $h^m \in \rcut$ and $g^r \not \in \rcut$ which violates the definition of
  $\rcut$. Therefore, $l-m \geq k-n$. For this case, if $\iso{\rcut}(h^l) = a^i$
  and $\iso{\rcut}(g^k) = b^j$, then $i = l - m$ and $j = k - n$. Therefore,
  $\forall e^i, f^j \in \langle E', \rightsquigarrow \rangle$, $J_p(f^j)
  \subseteq J_p(e^i) \Rightarrow j \leq i$.
\end{proof}  \eosqed

\begin{figure*}[tp]
\begin{center}
\includegraphics[width=6in]{unroll2.0}
\end{center}
\caption{The unrolled d-diagram $\unroll{\rcut}$}
\label{fig:unrolled2}
\end{figure*}

%TODO: Check the comment about process shift-edges

This property is similar to the property of the d-diagram where it is required
that there should not be any edge from an element with higher iteration to an
element with lower iteration. \figref{unrolled2} shows the unrolled d-diagram
$\unroll{\rcut}$. Note that the process shift-edge on the process $P_1$ is now
going from $d$ to $e$ instead of from $e$ to $d$. This change has essentially
renumbered the indices of elements corresponding to $d$ and $e$ such that in the
new d-diagram, $J_p(e^1) = \{ d^1, b^1, c^1 \}$.

We can now construct the slice of the original d-diagram $Q$
using the unrolled d-diagram $\unroll{\rcut}$ as both of them generate the same
computation. We slice the computation $\unroll{\rcut}$ by introducing additional
edges in the computation and removing vertices for which $J_p(e^i)$ does not
exist. Intuitively, the additional edges make the cuts which do not satisfy the
predicate, inconsistent in the new computation and removing the elements $e^i$
for which $J_p(e^i)$ does not exist is equivalent to removing any consistent cut
which includes the element $e^i$. Note that if an element $e^i$ is removed from
the slice, then any element $f^j$ which has a path from $e^i$ must be removed as
well.

%It was shown~\cite{MitGar:2001:DISC} that an additional edge is introduced in
%the slice between $e^i$ and $f^j$ if $J(e^i)$ lower covers $J(f^j)$ in the
%sliced computation $\langle \{ J_p(e^i) | e^i \in E \}, \subseteq \rangle$.
%Furthermore, as a simple extension of the \lemref{J-struct}, it can be shown
%that if $J(e^i)$ lower covers $J(f^j)$ in the directed graph $\langle \{
%J_p(g^l) | g^l \in E \}, \subseteq \rangle$, then $j -i \leq N + \eta$.

Using these results, we can construct a \emph{generalized} d-diagram for the
slice of $\unroll{\rcut}$ as follows. The set of vertices $V'$ in the d-diagram for $\slice{\compt}{p}$ is the set $V
\setminus D$ where $V$ is the set of vertices for $\unroll{\rcut}$ and $D$ is
the set of vertices for which $J(e^1)$ does not exist. The set $R'$ is also
constructed similarly using the set of recurrent vertices in $\unroll{\rcut}$.
Note that if $e$ was a recurrent vertex, then by removing $e$ we are not only
removing the element $e^1$ from the computation but all $e^i, i \geq 1$.
However, if $J_p(e^1)$ does not exist then $J_p(e^i)$ does not exist as $e^i$ is
reachable from $e^1$. On the other hand, if $J_p(e^1)$ exists, then $J_p(e^i)$
exists for all $e^i$ as the cut $J_p(e^1)$ has stabilized in $\unroll{\rcut}$.

Edges are added between the vertices in $V'$ based on the skeletal
representation of $\slice{\compt}{p}$ as follows: \\
(1) If there is an edge from $J_p(e^1)$ to $J_p(f^1)$, then add a forward edge from $e$ to $f$. \\
(2) If there is an edge from $J_p(e^1)$ to $J_p(f^j)$, then add a $j-1$ shift edge
  from $e$ to $f$. 

%Now the edges are added between the vertices in $V'$ as follows:

%\begin{itemize}
%\item If $J(e^1)$ exists but does not have a lower cover, then add an edge
%from $e$ to $\bot$.
%\item If $e, f \in R'$ and $J(e^i)$ covers $J(f^j)$, then add a $j-i$ shift edge
%  from $e$ to $f$.
%\item If $e, f \in V' \setminus R'$ and $J(e^1)$ covers $J(f^1)$, then add a
%  forward edge from $e$ to $f$.
%\item If $e \in V' \setminus R', f \in R$ and $J(e^1)$ covers $J(f^i)$, then add a
%  $i-1$ shift edge from $e$ to $f$.
%\end{itemize}

  Intuitively, it is safe to add these edges in the recurrent part of the
  d-diagram as the cuts $J_p(e^i)$ have stabilized and so the relationships
  between the cuts acquires a repeating structure. Note that we would not need
  to add an edge from a recurrent element to $\bot$ as the cuts $J_p(e^i)$ have
  stabilized and therefore for any $e^i, i \geq 2$, $e^{i-1}$ can serve as the
  lower cover. The following result is a direct consequence of the construction.
  
\begin{theorem}\label{thm:slicing}
  The generalized d-diagram as constructed above represents $\slice{\compt}{p}$
\end{theorem}
\begin{proof}
  Follows from the construction and Lemma~\ref{lem:J-reln}.
\end{proof}  \eosqed

\begin{figure*}[tp]
\begin{center}
\includegraphics[width=6in]{slicep.0}
\end{center}
\caption{The slice of the d-diagram in \figref{computation} with respect to $(x = 1) \wedge (y = 1) \wedge (z = 1)$}
\label{fig:slicep}
\end{figure*}

\figref{slicep} shows the slice of the original d-diagram with respect to the
predicate $p = (x = 1) \wedge (y=1) \wedge (z=1)$. Note that in the slice, we
have removed the recurrent vertex $g$ and added some edges according to the
above rules. 

The above construction can be done in time polynomial in the size of the
d-diagram as it requires unrolling the d-diagram for a polynomial number of
iterations and then computing the $J_p(e^i)$ for a polynomial set of elements.
Furthermore, if the slice of the computation becomes finite during the
processing of a predicate, then we can simply use the algorithms for the finite
directed graphs directly on the new poset. This is safe to do as slicing with
respect to a regular predicate only adds edges to the slice.

\section{Related Work}
\label{sec:related}
A lot of work has been done in identifying the classes of predicates which can
be efficiently detected~\cite{G02:EDC,MitGar:2001:DISC}.
However, most of the previous work in this area is mainly restricted to finite
traces. 
%Computational slicing has also been applied to only finite traces. In
%this paper, we address the problem of predicate detection and slicing on
%infinite traces.




Some examples of the predicates for which the predicate
detection can be solved efficiently are: \textit{conjunctive}
\cite{G02:EDC,hurfin98efficient}, \textit{disjunctive} \cite{G02:EDC},
\textit{observer-independent} \cite{Charron-Bost:1995:LTP,G02:EDC},
\textit{linear} \cite{G02:EDC}, \textit{non-temporal regular}
\cite{GarMit:2001:ICDCS,MitGar:2001:DISC} predicates and \textit{temporal
  }~\cite{SenGar:2003:OPODIS,SenGar:2002:IPDPS,DBLP:conf/wdag/OgaleG07}. 

\begin{figure}[tp]
\begin{center}
\includegraphics[width=3in]{msc.0}
\end{center}
\caption{A poset which cannot be captured using MSC graphs or HMSC}
\label{fig:msc}
\end{figure}

Some representations used in verification explicitly model concurrency in the
system using a partial order semantics. Two such prominent models are message
sequence charts (MSCs)~\cite{ITS} and petri nets~\cite{petri:thesis}. MSCs and
related formalisms such as time sequence diagrams, message flow diagrams, and
object interaction diagrams are often used to specify design requirements for
concurrent systems. An MSC represents one (finite) execution scenario of a
protocol; multiple MSCs can be composed to depict more complex scenarios in
representations such as MSC graphs and high-level MSCs (HMSC). These
representations capture multiple posets but they cannot be used to model all the
posets (and directed graphs) that can be represented by d-diagrams. In
particular, a message sent in a MSC node must be received in the same node in
MSC graph or HMSC. 
Therefore, some infinite posets which can be represented
through d-diagrams cannot be represented through MSCs. 
Therefore, an infinite poset such as the one shown
in figure \ref{fig:msc} is not possible to represent through MSCs.
%an example of such a poset is given in the
%Appendix in ~\figref{msc}.
%Therefore an infinite poset such as the one shown in~\figref{msc} is
%not possible to represent through MSCs.  
%Furthermore, the problem of model checking MSCs~\cite{alur99model,Ben:1997:MSC}
%is in general intractable. In this paper, we deal with only one poset or a
%directed graph but we give a provably efficient algorithm for predicate
%detection for a class of predicates.

Petri nets~\cite{petri:thesis} are also used to model concurrent systems.
Partial order semantics in petri nets are captured through net
unfoldings~\cite{Niel:1980:Unfolding}. Unfortunately, unfoldings are usually
infinite sets and cannot be stored directly. Instead, a finite initial part of
the unfolding, called the finite complete prefix~\cite{McMi93a} is generally
used to represent the unfolding.  McMillan showed that reachability can be
checked using the finite prefix itself. Later Esparza~\cite{Esparza:1994}
extended this work to use unfoldings to efficiently detect predicates from a
logic involving the $\EF$ and $\AG$ operators. Petri nets are more suitable to
model the behavior of a complete system whereas
d-diagrams are more suitable for modeling distributing computations in which the set of 
events executed by a process forms a total order.  They 
are a simple extension of process-time diagrams\cite{Lamp:HappenBefore} which have
been used extensively in distributed computing literature.
%However, along with being simpler,
%d-diagrams have some other advantages over petri nets. They allow some
%\emph{unsafe} petri nets to be model-checked which was not possible to do
%efficiently using earlier techniques for petri nets. 
%It is also possible to detect $\EG(p)$ with our methods. This facilitates
%checking violation of progress properties; violation of progress properties
%could not be expressed using Esparza's logic.




%can be used to do efficient predicate
%detection on some unsafe petri nets as well which cannot be done using Esparza's
%techniques.  Moreover, the logic RCTL also contains the $\EG$ operator which
%allows us to check for violation of safety properties.



\section{Conclusions}
In this paper, we introduce a method for detecting violation
of liveness properties in spite of observing a finite
behavior of the system. Our method is based on (1) determining
recurrent global states, (2) representing the infinite computation
by a d-diagram, (3) computing vector timestamps for
determining dependency and (4) computing the core of the computation for
predicate detection. We note here that intermediate
steps are of independent interest. Determining
recurrent global states can be used to detect if a terminating system has
an infinite trace. Representing an infinite poset with d-diagram
is useful in storing and replaying an infinite computation. 

Our method requires that the recurrent events be unrolled $N$ times. For certain 
computations, it may not be necessary to unroll recurrent event $N$ times. It would be interesting
to develop a method which unrolls each recurrent event just the minimum number of times required for that
prefix of the computation to be core.

%In this paper, we have restricted ourselves to very simple unnested temporal logic 
%formulas. Detecting a general temporal logic formula efficiently in the model of
%d-diagram is a future work.
\section{Acknowledgments}
We are grateful to the reviewers of this paper for many helpful comments and suggestions.
\bibliography{references}
%\pagebreak
%{\bf Appendix}
%{\bf Proof} of Lemma \ref{lem:prop}\\
\end{document} 
