\documentclass{elsart}
\usepackage{xspace,amsfonts}
\usepackage[curve,cmtip,matrix,arrow]{xy}

%%%%%%%%%%%%%%%%%%%%%%%%%%%
%   Definition of macros  %
%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newcommand\bool{\mathcal{B}} % the set {true,false}
\newcommand\TRUE{\texttt{true}\xspace}
\newcommand\FALSE{\texttt{false}\xspace}
\newcommand\REC{\texttt{iter}\xspace}
\newcommand\tinytrue{\texttt{\scriptsize true}}
\newcommand\tinyfalse{\texttt{\scriptsize false}}
\newcommand\tinyrec{\texttt{\scriptsize iter}}
\newcommand\eqdef{\stackrel{\mbox{\tiny def}}{=}}
\newcommand\deffonc[2]{#1\!\rightarrow\! #2}
\newcommand\ensembletq[2]{\left\{\left. #1 \: \right| \:#2\right\} }
\newcommand\nat\Nset
\newcommand\proj[2]{{{#1}_{(#2)}}}
\newcommand\projval[3]{\fonction{#1}|_{#2\mkern-1mu\leftarrow\mkern-1mu #3}} % �valuation partielle d'une relation
\newcommand\taille[1]{|#1|}
\newcommand\motvide{\varepsilon}
\newcommand\domaine{\mathop{dom}}
\newcommand\name[2]{\textrm{name}_{\fonction{#1}}(#2)}
\newcommand\subtree[2]{{#1}_{[#2]}}
\newcommand\recursif[1]{\Omega\left(\fonction{#1}\right)}
\newcommand\recursifset[2]{\Omega\left(\ensembletq{#1}{#2}\right)}
\newcommand\recrel[1]{\mathop{\mathrm{iter}}(\fonction{#1})}
\newcommand\cartesien{\bigotimes}
\newcommand\ceiling[1]{\left\lceil #1 \right\rceil}
\newcommand\iterbehave[2]{\fonction{#1}^\Omega_{[#2]}}
\newcommand\variable[1]{\texttt{#1}} % Pour la pr�sentation
\newcommand\fonction[1]{\mathcal{#1}}

\newcommand\moyengraphe[1]{\vcenter{\xymatrix @C-0.4pc @R-0.4pc {#1}}}
\newcommand\moyenarbre[1]{\vcenter{\xymatrix @C-1.8pc @R-1pc {#1}}}
\newcommand\topmoyenarbre[1]{\xymatrix @C-1.8pc @R-1pc {#1}}
\newcommand\petitarbre[1]{\def\objectstyle{\scriptstyle}
  \vcenter{\xymatrix @C-2.2pc @R-1.5pc {#1}}}

\newenvironment{samexample}{\begin{pf*}{Example \arabic{thm}
(continued). }\itshape}{\end{pf*}}
\newenvironment{samexmp}[1]{\begin{pf*}{Example #1
(continued). }\itshape}{\end{pf*}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\CompilePrefix{xy/bdg-}
%\CompileMatrices

\begin{document}

\begin{frontmatter}
\title{Infinitary Relations and Their Representation}
\author{Laurent Mauborgne\thanksref{DAEDALUS}}
\thanks[DAEDALUS]{
This work was supported by the RTD project
IST-1999-20527 ``DAEDALUS'' of the european
FP5 program.  }
\address{DI, \'{E}cole Normale Sup\'{e}rieure, 45 rue d'Ulm, 
75\,230 Paris cedex 05, France\\
Email: Laurent.Mauborgne@ens.fr\\
WWW home page: \texttt{http://www.di.ens.fr/\~{ }mauborgn/} }

\begin{abstract}
This papers presents extensions of Binary Decision Diagrams to
represent some infinitary relations (coded as infinite boolean functions). 
Four classes of infinitary relations are presented, and their representations 
are discussed. The widest class is closed under all boolean operations. The three 
others give rise to a canonical representation, which, when restricted to 
finite relations, are the classical BDDs. The paper
also gives new insights in to the notion of variables and the possibility 
of sharing variables that can be of interest in the case of finite 
relations.
\end{abstract}

\begin{keyword}
BDD. 
Infinite Functions. 
Model Checking. 
Static Analysis. 
\end{keyword}

\end{frontmatter}

\section{Introduction}
Binary Decision Diagrams (BDDs) were first introduced by Randal E. Bryant
in \cite{bryant86}. They turned out to be very useful in many areas where
manipulation of boolean functions ---or equivalently finite relations--- was 
needed. They allowed a real breakthrough of model checking 
\cite{burch:clarke:mcmillan:dill:hwang90}, they have been used successfully in 
artificial intelligence \cite{madre:coudert91} and in program analysis 
\cite{corsini:musumbi:rauzy92,lecharlier:vanhentenryck93,bagnara96,mauborgne98}.

One limitation of BDDs and its variants is that they can only represent
finite relations. Indeed, it induces a well-known and quite annoying
restriction on model checking, and it restrains its use in program analysis. 
This paper explores the possibility of extending BDDs so that they can also
represent infinitary relations. This extension will allow the model checking
of some infinite state systems or unbounded parametric systems, or the static 
analysis of the behavior of infinite systems, where the expression of infinite
properties such as fairness is necessary.

During the exploration of such extensions, we will define new classes of 
infinitary relations (which imply languages of infinite words). For those 
classes, we will propose two efficient extensions of BDDs: Open Binary 
Decision Graphs (and dually Closed Binary Decision Graphs), and the more 
powerful Binary Decision Graphs (BDGs). BDGs correspond to the class of 
$\omega$-deterministic relations.

The goal of these data structures is to represent infinitary relations with
variables (BDDs represent finite relations with variables) in an efficient 
way. As efficiency is a concept relative to the use of the data structure,
we need to tell more about it.
What we need in static analysis (and model checking) is an expressive data
structure (to give more precise results) and to perform inclusion testing
(so emptiness testing should be fast). Other operations are application
dependant, but most of the time, they can benefit from a good memoizing, which
means that we can use a good equality testing. The data structures we propose
are canonical, which means equality testing and emptiness testing in constant
time. There is a hidden complexity, though, due to the fact that we need to
compute the memory location for each new data (to recognize whether it had
been encountered before), but this is computed in an incremental way. 

After a presentation of our notations, sections~\ref{entry} and \ref{dtree} 
present the main ideas that allow this extension: the first idea is 
the possibility of sharing variables for different entries, while 
preserving a sound elimination of redundant nodes. The second idea is the 
possibility of looping in the representation (thus the term of Binary 
Decision Graph instead of Binary Decision Diagram), while preserving
the uniqueness of the representation. Section~\ref{simple} presents the first
class of functions and their representation. This first class is simple and
closed under union and intersection. The next section presents
a way of representing more complicated infinite functions by giving a new
semantics to the graphs. The widest class of functions is defined in
section~\ref{regular}. This class is very expressive and with good algebraic
properties, but the representation as an extension of BDDs does not seem
efficient enough. For a better efficiency, a restriction of this class is
defined in section~\ref{bdg}. These functions can be represented by extensions
of BDDs, in the sense that if the same representation is applied to finite
functions we obtain classical BDDs. This class is quite powerful but not closed
under all boolean operations. We propose the use of results on approximation 
properties of this class that can easily be exploited in abstract 
interpretation \cite{cousot:cousot77,cousot78}, a direction that is very promising for
its usefulness in program analysis. 

\section{Definitions and Notations}\label{definition}
\subsection{Relations and Boolean Functions}
\begin{defn}
A \emph{relation} $\fonction{R}$ over the family $(E_i)_{i\in I}$ of finite sets is a
subset of the cartesian product $\cartesien_{i\in I} E_i$ of the sets.
\end{defn}
An element of $\cartesien_{i\in I} E_i$ is called a \emph{vector}, thus a 
relation is a set of vectors of the same length. If $I$ is finite of
cardinality 
$n$, the relation is said to be \emph{$n$-ary}. If $I$ is infinite, the 
relation is called \emph{infinitary}. In this article we will restrict
infinitary relations to countable infinitary relations, i.e. $I$ will be
countable.

Relations over families of finite sets can be encoded into relations over
families of boolean sets (sets of cardinality 2). We just have to replace
each set $E_i$ of cardinality $n_i$ by $\ceiling{\log_2(n_i)}$ boolean sets.
This binary encoding is used in \cite{skmb90} to represent finite relations
with BDDs. In order to simplify our problems, we will just consider
relations over families of boolean sets, keeping in mind that we can always
come back to the general case.

Let $\bool\eqdef\{\TRUE,\FALSE\}$ be the set of boolean values. $\bool^n$
denotes the set of boolean vectors of length $n$.  A finite boolean function is 
a function of $\deffonc{\bool^n}{\bool}$. The set of infinite boolean vectors 
will be written $\bool^\omega$. An infinite boolean function is a function of
$\deffonc{\bool^\omega}{\bool}$.

A boolean function $\fonction{F}$ is entirely characterized by a set of 
vectors, which is defined as $\ensembletq{u}{\fonction{F}(u)=\TRUE}$. This set 
of vectors of same length $n$ can be seen as an $n$-ary relation between 
elements of $\bool$. If the vectors are infinite, this set forms an infinitary 
relation. Thus, we will indifferently write $u\in \fonction{F}$ or 
$\fonction{F}(u)=\TRUE$, and consider relations as boolean functions and vice 
versa.
If for all vectors $\fonction{F}$ is false, we will write $\fonction{F}=\emptyset$.

\subsection{Entries}
An important aspect of relations is the indexes in the cartesian product.
The corresponding concept in functions is the rank of the parameters used to
compute the value of the function. We use the term ``entry'' for this
concept. In the case of functions, this concept is often mixed up with the
variables used in the description of the functions (as in
$f(x,y,..)=\ldots$). What we want here is to distinguish
between the variables of the functions and their position in the function, 
which we call its \emph{entries}. If $\fonction{F}:\deffonc{\bool^n}{\bool}$,
then the entries of $\fonction{F}$ are the integers between 0 and $n-1$. If
$\fonction{F}:\deffonc{\bool^\omega}{\bool}$, then the entries of 
$\fonction{F}$ are $\nat$, the set of all natural numbers. 

\begin{exmp}\label{ex1}
let $\fonction{F}$ be the boolean function defined as 
$\fonction{F}(\variable{x},\variable{y},\variable{z})=
(\variable{y}\wedge \variable{z})\vee (\neg \variable{x}\wedge \neg 
\variable{y}\wedge \neg \variable{z})$. The function 
$\fonction{F}$ is in $\deffonc{\bool^3}{\bool}$. Thus its entries are $0$,
$1$ and $2$, and in the definition shown above, the variable $\variable{x}$ is 
associated with the entry $0$ (is at position $0$), $\variable{y}$ with $1$ 
and $\variable{z}$ with $2$.
\end{exmp}

We write $\proj{u}{i}$ for the $i^\mathrm{th}$ component of $u$. 
Given a set $I$ of entries, $\proj{u}{I}$ denotes the subvector of $u$ with 
$I$ as its set of entries. The \emph{restriction} of $\fonction{F}$ 
according to one of its entries $i$ and to the boolean value $b$ is denoted 
$\projval{F}{i}{b}$ and is defined as the set of vectors: $\ensembletq{u}
{\exists v\in \fonction{F},\: \proj{v}{i}=b\mbox{ and }
\proj{v}{\ensembletq{j}{j\neq i}}=u}$. A special case is when $i=0$. In this 
case, we simply write $\fonction{F}(b)$.

\subsection{Vectors and Words}\label{vect-word}
It is sometimes convenient to consider a boolean vector as a word over
$\bool^*$ or $\bool^\omega$. It allows the use of concatenation of vectors. If $u$ is a finite
vector and $v$ a vector, the vector $u.v$ corresponds to the
concatenation of the words equivalent to the vectors $u$ and $v$. The size of a
vector $u$ is written $\taille{u}$. The empty word is denoted $\motvide$. We 
define formally the notation $\fonction{F}(u)$:
\[\fonction{F}(u)\eqdef\ensembletq{v}{u.v\in \fonction{F}}\mbox{ if }\fonction{F}:\deffonc{\bool^\omega}{\bool}
\mbox{ or }\fonction{F}:\deffonc{\bool^n}{\bool}\mbox{ and }\taille{u}<n\]
Note that this definition is consistent with the notation $\fonction{F}(b)$ 
above: if $\taille{u}=1$, $w=u.v$ means that $\proj{w}{0}=u$ and 
$\proj{w}{\ensembletq{i}{i>0}}=v$. Thus $\fonction{F}(u)=\projval{F}{0}{u}$.


We extend the concatenation to sets of vectors: for example, if $\fonction{F}$ 
is a set of vectors and $u$ a vector, $u.\fonction{F}\eqdef
\ensembletq{u.v}{v\in \fonction{F}}$.

This point of view allows the comparison between classes of infinitary
relations and classes of $\omega$-languages. Although those classes look very
similar, they are not exactly the same, because of the presence of entries
in functions and relations. It is important for such datas that we have a way
of naming and accessing them. If we enriched word languages with a structure 
to name entries, it
would be possible to represent infinitary relations using B\"{u}chi automata
\cite{buchi60}. A problem of this representation is the well known 
lack of efficiency \cite{sistla:vardi:wolper85}. Because this class has
been well studied, we do not try to go beyond it but we will define smaller
classes with better representations for practical use.

\subsection{Notations}
We adopt the following conventions:
\begin{description}
\item[$a,b,c$]  represent boolean values,
\item[$\fonction{E},\fonction{F},\fonction{G}$]  represent boolean functions, or equivalently relations,
\item[$u,v,w$]  represent vectors (finite or infinite). In a context where we 
have infinite vectors as described below, represent finite vectors,
\item[$\alpha,\beta,\gamma$] represent infinite vectors,
\item[$\variable{x},\variable{y},\variable{z}$]  represent variables (or entry names),
\item[$r,s,t$] represent binary trees,
\item[$i,j,k,n$] represent natural numbers.
\end{description}

In the description of vectors, to reduce the size of the description, we will
write 0 for \FALSE, and 1 for \TRUE.

\section{Entry Names}\label{entry}
As mentioned earlier, it is important for relations and functions to be able
to access easily the different entries, so that we can have efficient
restrictions or computations of the result. A common way of doing so is by
naming the entries, using variables.

\begin{defn}[Named Function]
A \emph{named function} $\fonction{F}$ is a function associated with a naming
of its entries. This function, mapping entries to names, will be denoted
$\textrm{name}_\fonction{F}$.
\end{defn}

\begin{samexmp}{\ref{ex1}}
If $\fonction{F}(\variable{x},\variable{y},\variable{z})=\ldots$ is our named
function, then $\name{F}{0}=\variable{x}$, $\name{F}{1}=\variable{y}$ and
$\name{F}{2}=\variable{z}$.
\end{samexmp}

In classical BDDs, boolean functions are described by boolean expressions using
variables corresponding to the different entries of the functions. The 
Binary
Decision Diagrams are ordered, so that the ordering imposed on the variables
follows the order of the entries of the function. The variable of rank
$i$ is called the name of the entry $i$. In many cases, the variables
correspond to some entities related by the boolean function. A consequence
is that we can have the same information while changing the ordering on the 
variables and the boolean functions that bind them (so that a given 
entry always corresponds to the same variable, and the ordering on the
variables is the same as the entries ordering). Different optimizations 
follow that depend on the choice of this ordering 
\cite{fujita:fujisawa:kawato88,jeong+:91}.

\subsection{Equivalent Entries}
In the case of infinite functions, we cannot assign a different variable
to all the entries of the boolean function, because we want a finite 
representation. The idea is that the set of variables associated with
a given function is finite and to achieve that, some entries can share the 
same name. However, not every entry can share the same name: to share the same 
name, two entries must be in a sense equivalent.

This idea is necessary to have a representation of infinite functions with
named entries. But, as shown in example~\ref{bdd_ex} (page~\pageref{bdd_ex}
and next), the equivalence of entries can even be used in the representation
of finite functions with named entries, such as BDDs. It might be easier to
think of the entry names in BDDs to follow this sections. In BDDs, entry names
are� the variables which are the labels of the nodes. What we propose to do here
is to rename some of those labels, in a way compatible with the decision
semantics of BDDs. Note that this would not change the size of the BDD.

A permutation is a bijection of $\deffonc{\nat}{\nat}$. If $I\subset\nat$,
a permutation of the entries in $I$ is a permutation $\sigma$ such that
$\forall i\not\in I$, $\sigma(i)=i$. A permutation
$\sigma$ defines a function from vectors to vectors, $\overrightarrow{\sigma}$,
defined by : $\proj{\overrightarrow{\sigma}(u)}{i}=\proj{u}{\sigma(i)}$ for
all $i$ entry of $u$.

\begin{defn}[Equivalent entries]
Let $\fonction{F}$ be a boolean function. The entries contained in the set 
$I\subset\nat$ are equivalent if and only if for any permutation $\sigma$ 
of the entries in $I$, for any vector $u\in\domaine(\fonction{F})$, 
$\fonction{F}(u)=\fonction{F}(\overrightarrow{\sigma}(u))$
\end{defn}

There are two ideas underlying the definition of equivalent entries: the 
restriction according to any equivalent entry is the same, so
$\projval{F}{\variable{x}}{b}$, where $\variable{x}$ is an entry name, is not 
ambiguous (see property~\ref{restrict}); and
whatever the order in which we read the equivalent entries, the function is 
the same.
The following example shows that this property imposes that we allow 
infinite permutations.

\begin{exmp}
Consider the infinite function that is true on any infinite vector 
containing two consecutive 0's infinitely many times. This function contains
$(001)^\omega$ but not $(01)^\omega$. If we only considered finite permutations,
that is permutations generated from finite exchange of entries, then all
entries of this function are equivalent. But there is an infinite permutation that
transforms $(001)^\omega$ into $(01)^\omega$:
\[\!\begin{array}[t]{l}
\sigma(3\times k)=4\times k \\
\sigma(3\times k+1)=4\times k+2 \\
\sigma(3\times k+2)=2\times k+1
\end{array} \quad
\xymatrix @C-1.6pc @R+0.6pc {0 \ar@{-}[d] & 0 \ar@{-}[dr] & 1 \ar@{-}[dl] &
0 \ar@{-}[dr] & 0 \ar@{-}[drr] & 1 \ar@{-}[dll] & 0 \ar@{-}[drr] &
0 \ar@{-}[drrr] & 1 \ar@{-}[dlll] & 0 \ar@{-}[drrr] & 0 \ar@{.}[drrrr] &
1 \ar@{-}[dllll] & 0 \ar@{.}[drr] & 0 \ar@{.}[dr] &\ldots \\ 0&1&0&1&0&1&0&1&0&
1 \ar@{.}[urrrrr]&0&1 \ar@{.}[urrr]&0&1 \ar@{.}[ur]&\ldots}
\]
The meaning of this substitution is that, if a function with all entries 
equivalent contains $(001)^\omega$ then there is a way of giving the values of 
$(01)^\omega$ such that it is accepted by the function. Concerning our 
function, because $\fonction{F}\left((001)^\omega\right)\neq 
\fonction{F}\left((01)^\omega\right)$, we must forbid the equivalence of all 
entries.
\end{exmp}

As an immediate consequence, we have the following properties for functions $\fonction{F}$
where all entries are equivalent:
\begin{prop} \label{va_omega_ae}
Let $\fonction{F}:\deffonc{\bool^\omega}{\bool}$, such that the entries of
$\fonction{F}$ are all equivalent.
Let $v$ be a word, $b$ a boolean value in $v$, $\alpha$ be a word where
the boolean value $a$ appears infinitely often. Then $v^\omega\in
\fonction{F}$
if and only if $(vb)^\omega\in \fonction{F}$ and
$\alpha\in \fonction{F}$ if and only if $b.\alpha\in \fonction{F}$.
\end{prop}
\begin{pf}
In both cases, we have an infinite permutation of the entries that transforms
the first vector into the other one. In the second case, we just have to shift
the $a$'s of $a.\alpha$ to the right, each $a$ going to the entry of the next 
one.  In the first case, we keep shifting by one more $b$ for each $v.b$.
\qed\end{pf}

The following property proves that the notation
$\projval{F}{\variable{x}}{b}$ is not ambiguous:
\begin{prop}\label{restrict}
Let $I$ be a set of equivalent entries of the function $\fonction{F}$.
Whatever $i,j\in I$ and $b\in\bool$, $\projval{F}{i}{b}=\projval{F}{j}{b}$. 
\end{prop}
\begin{pf}
By definition of the restriction, $\projval{F}{i}{b}(u)= 
\exists v\in \fonction{F},\: \proj{v}{i}=b$ and 
$\proj{v}{\ensembletq{k}{k\neq i}}=u$. If $\projval{F}{i}{b}(u)=\TRUE$, let $v$
be the vector defined above. Let $\sigma$ be the permutation that exchanges
$i$ and $j$. By equivalence of $i$ and $j$ in $\fonction{F}$,
$\overrightarrow{\sigma}(v)\in \fonction{F}$. Moreover, by the action of the
permutation, $\proj{\overrightarrow{\sigma}(v)}{j}=b$ and
$\proj{\overrightarrow{\sigma}(v)}{\ensembletq{k}{k\neq j}}=u$, so
$\projval{F}{j}{b}(u)=\TRUE$. The converse is true by symmetry of the property,
which proves the equality of $\projval{F}{i}{b}$ and $\projval{F}{j}{b}$.
\qed\end{pf}

\subsection{Equivalent Vectors of Entries}
In order to be able to represent a wider class of infinite functions (while 
keeping the number of entry names finite), we extend the notion of equivalent 
entries
to equivalent vectors of entries. We just consider as one entry a whole set
of entries of the form $\ensembletq{i\in\nat}{k\leq i <k+n}$. It will allow
the iteration over whole vectors of entries. The set of equivalent
entries is described by a set $I$ of indexes and a length $n$ such that
$\forall k\in I$, $\forall i$ such that $k<i<k+n$, $i\not\in I$. A substitution
$\sigma$ over such a set is such that $\forall k\in I$, $\sigma(k)\in I$, and
$\forall i<n$, $\sigma(k+i)=\sigma(k)+i$. For all other numbers $j$,
$\sigma(j)=j$.

\begin{defn}[Equivalent Vectors of Entries]
Let $\fonction{F}$ be a boolean function. The vectors of entries contained in the set 
$I$ with length $n$ are
equivalent if and only if for any permutation $\sigma$ of the entries in
$I$, for any vector $u\in\domaine(\fonction{F})$, $\fonction{F}(u)=\fonction{F}(\overrightarrow{\sigma}(u))$
\end{defn}

Two entries can have the same name if and only if they are at the same position
in a set of equivalent vectors of entries. 
In the remainder, when considering named functions, and to simplify the
presentation and the proofs, we will only consider simple equivalent entries, 
but the results extend easily to equivalent vectors of entries.

\subsection{Equivalent Entries and Redundant Choices}
Redundant choices are used in BDDs to reduce the size of the representation.
The good news is that giving the same name to equivalent entries is compatible
with the elimination of redundant choices. There is a redundant choice at
a subvector $u$ of $\fonction{F}$ if and only if
$\fonction{F}(u.0)=\fonction{F}(u.1)$. 

\begin{thm} \label{eq_entry}
Let $\fonction{F}$ be a named boolean function, and $u$ be a vector such that 
$\fonction{F}(u.0)=\fonction{F}(u.1)$.
Then, whatever $v$ such that $\name{F}{\taille{u.v}}=\name{F}{\taille{u}}$, 
$\fonction{F}(u.v.0)=\fonction{F}(u.v.1)$.
\end{thm}
\begin{pf}
$v=a.w$. We have $\fonction{F}(u.a.w.0)=\fonction{F}(u.0.w.a)$ because of the equivalence of the
entries. $\fonction{F}(u.0.w.a)=\fonction{F}(u.1.w.a)$ by redundancy of the choice, and $\fonction{F}(u.1.w.a)$
$=\fonction{F}(u.a.w.1)$ by equivalence of the entries. Thus $\fonction{F}(u.v.0)=\fonction{F}(u.v.1)$.
\qed\end{pf}

\subsection{Periodicity of the Entries}
In order to be finitely representable, we impose some regularity to the entry
names. The entry names are said to be \emph{periodic} if and only if there is
a period $k$ on the entry names, that is, for all $i$, the name of $i+k$ is the
same as the name $i$. The entry names are said to be \emph{ultimately
periodic} if, after some point, they are periodic. 

\begin{defn}
A named function $\fonction{F}$ is said to have \emph{ultimately periodic
entry names} iff there is a period $k$ and an entry $j$ such that for
all entry $i>j$, $\name{F}{i}=\name{F}{i+k}$.
\end{defn}

In the remainder, we will define new classes of infinitary relations which could
be represented by extensions of BDDs. A direct consequence of this discussion
over entries and entry names is that for each such class of relations, the 
entry names will have to be ultimately periodic. It is a strict restriction,
in particular for $\omega$-regular languages of B\"{u}chi.

\begin{prop} \label{buchi-relation}
The class of $\omega$-regular languages of B\"{u}chi such that there exists a 
named function with ultimately periodic entries of domain the same set of 
words is a strict subset of the class of $\omega$-regular languages of 
B\"{u}chi.
\end{prop}

\begin{pf}
The set $\{0,11\}^\omega$ is an $\omega$-regular language. Suppose there is a
named function with ultimately periodic entries which is \TRUE on exactly that
set. As the entries are ultimately periodic, there must be at least two 
equivalent entries $i<j$. Then $0^{j}110^\omega$ is in the function, so 
$0^{i}10^{j-i}10^\omega$ should be in the function too, because of the 
equivalence of entries $i$ and $j$. It means that $i$ and $j$ are not 
equivalent.
\qed \end{pf}

\section{Decision Trees}\label{dtree}
\subsection{Finite Decision Trees}
BDDs are based on decision trees. A decision tree is a structured representation
based on Shannon's expansion theorem: $\fonction{F}=0.\fonction{F}(0)\cup 
1.\fonction{F}(1)$. This observation is the basis of a decision procedure: to 
know whether a given vector is in a relation, we look at its first value. If 
it is a 0, we iterate the process on the rest of the vector and 
$\fonction{F}(0)$, and if it is a 1, we iterate on the rest of the vector and 
$\fonction{F}(1)$. This procedure can be represented by a binary tree
labeled by the entry names, and with either \TRUE or \FALSE at the leaves.

The construction of a decision tree for a finite function is classical, but we
will rephrase it in our terminology. This will allow us to show how entries 
and entry names are used, and then how the distinction between those two
concepts (which are usually mixed in the term ``variable'') can give more
freedom in the construction of those decision trees.

We define a labeled binary tree $t$ as a partial function of $\deffonc{\{0,
1\}^*}{L}$ where $L$ is the set of labels, and such that whatever
$u.v\in\domaine(t)$, $u\in\domaine(t)$. The subtree of $t$ rooted at $u$ is 
the tree denoted $\subtree{t}{u}$ of domain $\ensembletq{v}
{u.v\in\domaine(t)}$, and defined as $\subtree{t}{u}(v)\eqdef t(u.v)$. The 
decision tree defined by a named boolean function 
$\fonction{F}:\deffonc{\bool^n}{\bool}$ is 
the binary tree of domain $\bigcup_{k\leq n}\{0,1\}^k$, such that if 
$\taille{v}=n$, then $t(v)=\fonction{F}(v)$, and if $\taille{v}<n$, 
$t(v)=\name{F}{\taille{v}}$. Note that this definition does not impose that
all entry names be different. 

\begin{exmp}\label{bdd_ex}
Let $\fonction{F}=\{000,011,111\}$. If we associate the variables 
$\variable{x}$ to entry 0,
$\variable{y}$ to entry 1 and $\variable{z}$ to entry 2, then $\fonction{F}$ can be described by the formula:
$(\variable{y}\wedge \variable{z})\vee(\neg \variable{x}\wedge\neg \variable{y}\wedge\neg \variable{z})$. The decision tree for $\fonction{F}$ is:
\[\xymatrix @C-1.8pc @R-0.5pc {&&&&&&& \variable{x} \ar[dllll]_0 \ar[drrrr]^1 \\
&&& \variable{y} \ar[dll]_0 \ar[drr]^1
&&&&&&&& \variable{y} \ar[dll]_0 \ar[drr]^1 \\ 
& \variable{z} \ar[dl]_0 \ar[dr]^1 &&&& \variable{z} \ar[dl]_0
\ar[dr]^1 &&&& \variable{z} \ar[dl]_0 \ar[dr]^1 &&&& \variable{z} \ar[dl]_0 \ar[dr]^1 \\ \TRUE &&
\FALSE && \FALSE && \TRUE && \FALSE && \FALSE && \FALSE
&& \TRUE}\]
\end{exmp}

\subsection{Semantics of the Decision Trees}
The decision tree of a named boolean function is used as a guide for a decision
process that decides the value of the function on a given vector. If $t$ is
the decision tree associated with the named function $\fonction{F}$, then to 
decide whether the vector $u$ is in $\fonction{F}$, we ``read'' the first 
value of $u$. Say $u=b.v$. If 
$b$ is a 0, we iterate on $v$, $\subtree{t}{0}$, and if it is a 1, we iterate
on $v$, $\subtree{t}{1}$. The entire decision process goes through the
tree, following the path defined by $u$, and the result of the decision 
process is the value of the leaf, $t(u)$. Binary Decision Diagrams are
based on two remarks: first we can represent any tree in a form where
equivalent subtrees are shared (a directed acyclic graph), and
second if a choice is redundant, then we can ``jump it''. The second remark 
modifies slightly the decision process: we must have separate information
on the entries of a function. Without the elimination of redundant nodes,
the entry names labeling the tree would be of no use. But if we allow the
elimination of redundant nodes, then they allow to keep track of the current 
entry that is read from $u$. If it is ``before'' the entry named $t(\motvide)$,
we can skip the first value of $u$ and iterate on $v$, $t$.
It means also that we need a way of representing
$\textrm{name}_{\fonction{F}}$. In classical BDDs, where all entry names are
different, we can represent $\textrm{name}_{\fonction{F}}$ by an ordering of
the entry names: $\name{F}{i}$ is the $i^\mathrm{th}$ entry name in the
ordering. If we allow to have the same entry names at different entries, then
we can use a sequence of entry names, and $\name{F}{i}$ is the $i^\mathrm{th}$
entry name in the sequence.

\begin{samexample}
The two steps of sharing equivalent subtrees and eliminating redundant nodes
give the following diagrams:
\[\xymatrix @C-1.8pc @R-1pc{&& \variable{x} \ar[dl]_0 \ar[dr]^1 \\
& \variable{y} \ar[dl]_0 \ar[dr]^1
&& \variable{y} \ar[dl]_1 \ar[dr]^0 \\
\variable{z} \ar[dr]^0 \ar@(d,dl)[drrr]_1 && \variable{z} \ar[dl]_1
\ar[dr]^0 && z \ar@/_/[dl]_0 \ar@/^/[dl]^1 \\ & \TRUE && \FALSE}\qquad
\xymatrix @C-1.8pc @R-1pc{&& \variable{x} \ar[dl]_0 \ar[dr]^1 \\
& \variable{y} \ar[dl]_0 \ar[dr]^1
&& \variable{y} \ar[dl]_1 \ar@/^/[dd]^0 \\
\variable{z} \ar[dr]^0 \ar@(d,dl)[drrr]_1 && \variable{z} \ar[dl]_1
\ar[dr]^0 \\ & \TRUE && \FALSE}\]
The decision process on the vector $101$ can reach \FALSE after reading the
first 1 and the first 0. The entry names of the BDD are represented by
$\variable{x}<\variable{y}<\variable{z}$, or equivalently by $\variable{x}\variable{y}\variable{z}$. If we realize that the entry 1 and the entry
2 are equivalent, we can give the same name $\variable{y}$ to both entries. 
Then the BDD becomes:
\[\moyenarbre{&& \variable{x} \ar[dl]_0 \ar[dr]^1 \\
& \variable{y} \ar[dl]_0 \ar[dr]^1
&& \variable{y} \ar[dl]_1 \ar@/^/[dd]^0 \\
\variable{y} \ar[dr]^0 \ar@(d,dl)[drrr]_1 && \variable{y} \ar[dl]_1
\ar[dr]^0 \\ & \TRUE && \FALSE}\]
with entry names described as $\variable{x}\variable{y}\variable{y}$. Note that
this cannot change the size of the BDD. There can be an interest in it,
though, even for finite functions. To compute a restriction, one needs to go
through the diagram up to the nodes labeled by the corresponding name, so the
farther the name in the diagram, the more complex the restriction.
It is easy to see that this description
will lead to a more efficient algorithm to compute $\projval{F}{2}{0}$
which corresponds to $\projval{F}{\variable{z}}{0}$ with the entry names 
$\variable{x}\variable{y}\variable{z}$, and
to $\projval{F}{\variable{y}}{0}$ with the entry names 
$\variable{x}\variable{y}\variable{y}$. Concerning the meaning of the diagram,
note that we don't test $\variable{y}$ twice, but we test the entries $1$ and
$2$, and the fact that they have the same name means that we can test them in
any order and obtain the same result.
\end{samexample}

It is an established fact \cite{bryant86}\footnote{Although we rephrase it
with entry names instead of variables.}, that given a boolean function
and a naming of the entries with all names different, such a representation
is unique, leading to trivial equivalence testing. From 
Theorem~\ref{eq_entry}, we can add that this representation is still unique
if the naming of the entries respects the equivalences of the entries.

\subsection{Infinite Trees}
To extend this definition to infinite boolean functions, there are two
problems: for all $\alpha\in \fonction{F}$, $\alpha\not\in\domaine(t)$, 
because binary tree domains are limited to finite words. This is the problem 
of the \emph{infinite behavior} of the function. We can represent $t(v)$ for
all $v$ a prefix of a vector in $\fonction{F}$, but then the tree is infinite. 
This is the
second problem, treated in this section: how to represent an infinite tree.

As we have seen, a BDD is a decision tree on which we have performed two 
operations: first the sharing of equivalent subtrees, second the elimination 
of redundant choices. In fact, following this process would be too inefficient,
and when manipulating BDDs, these operations are performed incrementally:
each time we build a tree $\!\!\petitarbre{& x \ar[dl] \ar[dr] \\ 
t &\hspace{0.1cm}& t}\!\!$, we
return $t$, and each time we build another tree $\!\!\petitarbre{& x \ar[dl] 
\ar[dr]\\ t_0 && t_1}\!\!$, we first look if the tree has already been 
encountered, through a hash table for example, and if it is the case, we 
return the tree already encountered, if not we add it in the table.

The same operations, albeit a little more complex, can be performed to
represent an infinite tree with maximal sharing of its subtrees
\cite{mauborgne00a}. First we
only represent \emph{regular} trees, that is trees with a finite number of
distinct subtrees. The only difference with finite trees, which are represented
by directed acyclic graphs, is that infinite trees are represented by directed
graphs that contain cycles. The added complexity introduced by the cycles
is not intractable, and efficient incremental algorithms can be devised.
The ideas are the following: when we are not in a cycle, the algorithm is
the same as in the finite case. When we isolate a strongly connected subgraph
(a ``cycle''), we first see if this cycle is not the unfolding of another
cycle that is reachable from the subgraph. If it is the case, we return this
other cycle (we fold the subgraph on the cycle). If not, we reduce the
subgraph to an equivalent one with maximal sharing, and then we compute
unique keys for the subgraph, so that we can see if it had already been 
encountered, or so that we can recognize it in the future. We have one key
for each node of the subgraph. The detailed algorithms and their proofs can be
found in \cite{mauborgne00c}.  

Examples of infinite trees represented this way will be displayed in the next
sections. The trees will be progressively enriched so that the BDGs represent
wider classes of infinite functions.

\section{Simple Infinite Behaviors}\label{simple}
Using the ideas of the last two sections, we can extend BDDs to represent
classes of infinitary relations with simple infinite behavior. This extension
consists in allowing the sharing of entry names (to have an infinite number
of entries represented by a finite number of entry names), and in allowing
loops in the diagrams. We need to define the classes of boolean functions which
can be represented by these extensions of BDDs. The first class we define
is a superset of those classes derived from the necessity that the decision 
tree be representable, that is regular.

\begin{defn}
Let $\fonction{F}$ be a named boolean function. $\fonction{F}$ is said to be 
\emph{prefix regular} if and only if the number of distinct $\fonction{F}(u)$ 
(as defined in section~\ref{vect-word})
is finite and its entry names are ultimately periodic.
\end{defn}
Because we will have only one possible representation for a given function,
and $\fonction{F}(u)$ corresponds to $t(u)$ if $t$ represents $\fonction{F}$, 
it means that $t$ is regular.

Note that prefix regularity of a funtion $\fonction{F}$ does not necessarily 
means that its domain is $\omega$-regular: suppose we have a non
$\omega$-regular language $\fonction{L}$. Then $\fonction{F}=
\{0,1\}^*.\fonction{L}$ is non $\omega$-regular either, but all
$\fonction{F}(u)=\fonction{F}$.

\subsection{Open Functions and Closed Functions}
We mentioned earlier that the representation of the decision tree for
infinite functions presented two problems: the representation of each partial
evaluation of the function (solved by a regular tree), and the problem of the
decision process which must be infinite and cannot be represented in general
by a mere regular tree. The idea, to solve this infinite behavior problem
simply, is to give a uniform meaning to the possible infinite decision
processes, that is the infinite loops in the decision tree. And to keep
as close as possible to classical BDDs, if the decision process is finite,
then the result should be the same as with BDDs. In particular, if we arrive
at a \FALSE node after reading the start $u$ of the vector, then there is no 
need to go further since no vector starting by $u$ will be in the relation
($\fonction{F}(u)=\emptyset$), and if we come to a \TRUE, then any vector
starting by $u$ will be in this relation ($\fonction{F}(u)=\bool^\omega$).

We can define two classes of boolean functions, corresponding to two possible
meanings for infinite loopings (we never reach \TRUE nor \FALSE), namely 
exclusive (for open functions) and inclusive (for closed functions).

\begin{defn}[Open Function]
Let $\fonction{F}:\deffonc{\bool^\omega}{\bool}$. The function $\fonction{F}$ 
is said to be \emph{open} if and only if $\fonction{F}$ is prefix regular and:
\[\forall \alpha\in \fonction{F},\: \exists u,\,\beta\mbox{ such that }
\alpha=u.\beta \mbox{ and } \fonction{F}(u)=\bool^\omega\]
\end{defn}

Recall that $\fonction{F}(u)=\bool^\omega$ means that whatever $\gamma$, $\fonction{F}(u.\gamma)=
\TRUE$. It means that the only vectors in the relation will lead finitely to
a \TRUE. The dual definition is:

\begin{defn}[Closed Function]
Let $\fonction{F}:\deffonc{\bool^\omega}{\bool}$. The function $\fonction{F}$ is said to be 
\emph{closed} if and only if $\fonction{F}$ is prefix regular and:
\[\forall \alpha\not\in \fonction{F},\: \exists u,\,\beta\mbox{ such that }
\alpha=u.\beta \mbox{ and } \fonction{F}(u)=\emptyset\]
\end{defn}

As those two definitions are dual, we will mainly describe the representation
and properties of one of them, say open functions. The results on open functions
can be translated for closed functions by exchanging the roles of \TRUE and
\FALSE. The choice between one class of relations or the other will depend on
the particular applications, but we cannot mix them.

\subsection{Open BDGs}
Because we chose that cycling in the decision process is rejecting, there is
one new source of non-uniqueness that is not taken care of by simply sharing
every subtree of the decision tree. We must also replace by \FALSE every
cycle from which no \TRUE is reachable. This is easily performed while
treating cycles in the representation of regular trees. 

We define the notion of decision tree representing an open function:
\begin{defn}\label{dt}
A decision tree \texttt{dt} represents a named open function $\fonction{F}$ if 
and only if the labels of the inner nodes of \texttt{dt} are
$\texttt{dt}(u)=\name{F}{\taille{u}}$
and $\forall \alpha\in \fonction{F}$, 
$\exists u,\,\beta$ such that $\alpha=u.\beta$ and
\texttt{dt}$(u)=$\TRUE, and $\forall u$ such that \texttt{dt}$(u)=$\TRUE,
$\fonction{F}(u)=\bool^\omega$.
\end{defn}

Now, we can prove that we have a unique representation for open functions:

\begin{thm}
There is exactly one decision tree \texttt{dt} representing the named open 
function $\fonction{F}$ such that for all $r$ subtree of \texttt{dt}, either 
$r=\FALSE$ or at least one leaf of $r$ is \TRUE, and if $r$ is finite, it is \TRUE, 
\FALSE or both leaves appear.
\end{thm}
The last condition just corresponds to the elimination of redundant nodes
before \TRUE and \FALSE, because we could have any number of such nodes.
\begin{pf}
It is obvious from definition~\ref{dt} that there exists at least one
decision tree \texttt{dt} representing $\fonction{F}$.
Suppose there is another decision tree \texttt{dt'} representing also
$\fonction{F}$ with
the same conditions, then there must be a $u$ such that one of the trees,
say \texttt{dt} is labeled by \TRUE or \FALSE at $u$, and \texttt{dt'} is
labeled by an entry name. Let $r$ be the subtree of \texttt{dt'} at $u$.
If \texttt{dt}$(u)=$\TRUE, then $\fonction{F}(u)=\bool^\omega$, so $r$ cannot contain any
loop (which would exclude a vector), and the only possible leaves are \TRUE.
This contradicts the second condition. If \texttt{dt}$(u)=$\FALSE, then, in
the same way, no leaf of $r$ can be \TRUE, so, by the first condition, $r$
must be \FALSE.
\qed \end{pf}

The \emph{open BDG} for a function is defined as the the unique representation 
(see \cite{mauborgne00c} for a proof) of this decision tree, with the
elimination of the redundant nodes. Open BDGs are indeed extensions of BDDs,
because they have the same unique incremental representation principle, and
if we apply the open BDG representation to finite functions (which are both
open and closed), we obtain the classical BDDs.

\begin{exmp}
The function $\fonction{F}$ defined in example~\ref{bdd_ex} can be extended to 
the function $\fonction{G}:\deffonc{\bool^\omega}{\bool}$, defined as: 
$\fonction{G}(u.\alpha)=\TRUE$ if $u\in \fonction{F}$. Then $\fonction{G}$ is represented
with the same diagram as $\fonction{F}$, with an additional entry name $z'$, and the
entry names are $\variable{x}\variable{y}\variable{y}(\variable{z}')^\omega$.
\end{exmp}
\begin{exmp}
Let $\fonction{F}$ be \TRUE on $\alpha$ if and only if $\alpha$ contains at 
least one 1. All entries of $\fonction{F}$ are equivalent, so its entry names
can be described as $\variable{x}^\omega$. Since $\fonction{F}$ is open, it can be represented by the
following graph:
\[\moyenarbre{\variable{x} \ar@(dl,ul)^0 \ar[dr]^1 \\ & \TRUE} \]
Note that this diagram would not be a correct representation for a closed 
function, because there is no path leading to \FALSE (the dual of \TRUE).
\end{exmp}

\subsection{Boolean Operators}

We will write $\fonction{F}\wedge\fonction{G}$ to denote the intersection of
two relations $\fonction{F}$ and $\fonction{G}$, and
$\fonction{F}\vee\fonction{G}$ for their union.

\begin{thm}
Let $\fonction{F}$ and $\fonction{G}$ be two open functions. Then the 
functions $\fonction{F}\wedge \fonction{G}$ and
$\fonction{F}\vee \fonction{G}$ are open. Moreover, if $(\fonction{F}_i)_{i\in\nat}$ is a family of open
functions, then $\bigvee_{i\in\nat}\fonction{F}_i$ is an open function.
\end{thm}
$\fonction{F}\wedge \fonction{G}(\alpha)\eqdef \fonction{F}(\alpha)\wedge 
\fonction{G}(\alpha)$, and $\fonction{F}\vee \fonction{G}(\alpha)
\eqdef \fonction{F}(\alpha)\vee \fonction{G}(\alpha)$. So, if we consider 
$\fonction{F}$ and $\fonction{G}$ as sets of
vectors, $\fonction{F}\wedge \fonction{G}$ is the intersection of $\fonction{F}$ and $\fonction{G}$, and $\fonction{F}\vee \fonction{G}$ is
the union of $\fonction{F}$ and $\fonction{G}$.
\begin{pf}
Let $\alpha\in \fonction{F}\vee \fonction{G}$. There is a $u$ such that $\alpha=u.\beta$, and either
$\fonction{F}(u)=\bool^\omega$ or $\fonction{G}(u)=\bool^\omega$. In any case, $\fonction{F}\vee \fonction{G}(u)=
\bool^\omega$. If $\alpha\in \fonction{F}\wedge \fonction{G}$, there is $u$ and $v$ such that
$\alpha=u.\beta$, $\alpha=v.\gamma$, and $\fonction{F}(u)=\bool^\omega$ and
 $\fonction{G}(v)=\bool^\omega$. If $\taille{u}\leq\taille{v}$, then $v=u.w$. So
$\fonction{F}(v)=\bool^\omega$. So, $\fonction{F}\wedge \fonction{G}(v)=\bool^\omega$. If $\alpha\in
\bigvee_{i\in\nat}\fonction{F}_i$, then there is a least $u$ prefix of $\alpha$
such that there is a $i$, $\fonction{F}_i(u)=\bool^\omega$. We have 
$\bigvee_{i\in\nat}\fonction{F}_i(u)=\bool^\omega$.
\qed \end{pf}

Dually, the finite union of closed functions is a closed function, and the
infinite intersection of closed functions is a closed function.

\begin{cor}
Whatever the boolean function $\fonction{F}$, there is a greatest open function contained 
in $\fonction{F}$, and there is a least closed function containing
$\fonction{F}$.
\end{cor}

Algorithmically, it is easy to compute the \texttt{and} or the \texttt{or}
of two open functions. The algorithms are the same as in the finite case
\cite{bryant92}, with
the possibility of memoizing \cite{michie68}, except that we must take
care of cycles. When a cycle is encountered, that is when we recognize that
we already have been through a pair of subtrees $(s,t)$, we build a loop in
the resulting tree.

Open functions are not closed under negation: the negation of the function that 
is true on all vectors containing at least one 1 is the function containing only
$0^\omega$. Such a function is not open (but it is closed, of course), because 
the only infinite behavior that is possible for an open function is trivial. 
In order to be more expressive, we introduce more infinite behaviors.

\section{More Infinite Behaviors}\label{iterative}
To allow more infinite behaviors, we need to have more than one kind of loop,
so that in some loop it is forbidden to stay forever, and in some others,
we can. We introduce a new kind of loop: loops over open functions.
This new kind of loop defines a new set of infinite behaviors, defining
what we call iterative functions.
Iterative functions are functions that start over again and again infinitely
often. Thus entry names will have to be periodic.

\subsection{Definition}
\begin{defn}[Iteration]
Let $\fonction{F}:\deffonc{\bool^\omega}{\bool}$ be a named function. The 
iteration of $\fonction{F}$, noted $\recursif{F}$, is defined as the set of 
vectors $\alpha$ such that there is an infinite sequence of vectors 
$(u_i)_{i\in\nat}$ and $\alpha=u_0.u_1\ldots u_i \ldots$ and each $u_i$ has 
the minimal length such that:
\begin{enumerate}
\item $\taille{u_i}>0$
\item $\fonction{F}(u_i)=\bool^\omega$
\item $\name{F}{\taille{u_i}}=\name{F}{0}$
\end{enumerate}
\end{defn}
\begin{defn}[Iterative Function]
Let $\fonction{F}:\deffonc{\bool^\omega}{\bool}$ be a named function. 
$\fonction{F}$ is said to be \emph{iterative}
if and only if the entry names of $\fonction{F}$ are periodic, and there is an open
function $\fonction{G}$ such that $\fonction{F}=\recursif{G}$.
\end{defn}

Hence an iterative function is represented by an open function. We will use the
decision tree of the open function to represent the iterative function. But
in the context of iterative functions, the decision tree will have a different 
meaning, corresponding to a slightly different decision process. The decision
process is the following: we follow the decision tree in the path corresponding
to the vector, but when we reach a \TRUE, we start again at the root of the
tree. To be a success, the decision process must start again an infinite number
of times.

\begin{exmp}[Safety]\mbox{ }\\
\begin{tabular}{p{3.45cm}p{9.62cm}}
$\moyenarbre{& \variable{x} \ar[dl]_0 \ar[dr]^1\\\TRUE&&\FALSE}$ & represents the 
function that is true on $0^\omega$ only.
\end{tabular} \end{exmp}
\begin{exmp}[Liveness]\mbox{ }\\
\begin{tabular}{p{3.45cm}p{9.62cm}}
$\topmoyenarbre{& \variable{x} \ar[dl]_0 \ar@(dr,r)_1\\ \TRUE}$  & represents the function
that is false only on those vectors that end with $1^\omega$. That is, the 
function is true on any vector containing an infinite number of 0's.
\end{tabular} \end{exmp}
\begin{exmp}[Fairness]\mbox{ }\\
\begin{tabular}{p{3.45cm}p{9.62cm}}
$\topmoyenarbre{&\variable{x} \ar[dl]_0 \ar[dr]^1 \\
\variable{x} \ar@(dl,ul)^0 \ar[dr]^1 &&
\variable{x} \ar[dl]_0 \ar@(dr,ur)_1 \\&\TRUE}\!\!$ &
represents the function that is true on any vector containing an infinite number
of 0's and 1's.
\end{tabular} \end{exmp}

These examples show that iterative functions can be used to represent a wide
variety of infinite behaviors. Note that $\emptyset$ and $\bool^\omega$
are at the same time open and iterative. Another remark: the equivalence
of the entries restraining the use of shared entry names is only applied to
the iterative function, not the open function that represents the iterative
function. 

\begin{thm}
An iterative function is prefix regular.
\end{thm}
\begin{pf}
If $\fonction{F}=\recursif{G}$, $g$ is open, so prefix regular. Let $u$ be a finite vector
such that there is a $v$, $\fonction{G}(u)=\fonction{G}(v)$ and $\taille{u}>\taille{v}$. If
$\fonction{G}(u)\neq\bool^\omega$ then $\fonction{F}(u)=\fonction{F}(v)$.  If 
$\fonction{G}(u)=\bool^\omega$ then there
is a $u_0$ prefix of $u$ and minimal such that $\taille{u_0}>0$, 
$\fonction{G}(u_0)=\bool^\omega$ and $\name{G}{\taille{u_0}}=\name{G}{0}$. Let
$u=u_0.u_1$. We have $\fonction{F}(u_0)=\fonction{F}$, so $\fonction{F}(u)=
\fonction{F}(u_1)$, with
$\taille{u}>\taille{u_1}$. If we take a $u$ of size greater than the number
of distinct $\fonction{G}(u)$, then there exists a $v$ as described above, and so there
is a $w$ (either $v$ or $u_1$ above) such that $\fonction{F}(u)=
\fonction{F}(w)$ and
$\taille{u}>\taille{w}$. So the number of distinct $\fonction{F}(u)$ is bounded.
Thus, $\fonction{F}$ is prefix regular.
\qed\end{pf}

\subsection{Uniqueness}
Many possible open functions can represent the same iterative function:
\begin{exmp}
The function that is true on every vector with an infinite number of 0's and 1's
could also be represented by the following open function:
\[\moyenarbre{ & \variable{x} \ar[dl]_0 \ar@(dr,ur)_1 \\ \variable{x} \ar@(dl,ul)^0 \ar[dr]^1 \\ & 
\TRUE}\qquad\moyenarbre{& \variable{x} \ar@(dl,ul)^0 \ar[dr]^1 \\ && \variable{x} \ar[dl]_0 
\ar@(dr,ur)_1 \\ & \variable{x} \ar[dl]_0 \ar@(dr,ur)_1 \\ \TRUE}\]
\end{exmp}
In fact, there is a ``best'' open function representing a given iterative 
function. If we always choose this best open function, as the representation
of open function is unique, the representation of iterative function is
unique too. 
\begin{thm}\label{best_open}
Let $\fonction{F}$ be an iterative function. The function $\fonction{G}$ which 
is true on the set $\left\{u.\alpha \right| u^\omega\in \fonction{F}
\mbox{ and } \fonction{F}(u)=\fonction{F}\}$ is the greatest (for set 
inclusion) open function such that $\fonction{F}=\recursif{G}$.
\end{thm}
In order to simplify the proofs, we will suppose that all entries of 
$\fonction{F}$
are equivalent, so that there is only one entry name, and we can get rid of
the test $\name{F}{\taille{u}}=\name{F}{0}$. To reduce the problem to this
case, we can use a function over larger finite sets described by
$\bool^k$, where $k$ is a period of the entry names of $\fonction{F}$.
\begin{lem}\label{best_open_lemma}
Let $u$ be a vector such that $g(u)=\bool^\omega$, $\taille{u}>0$ and for all 
$v$ prefix of $u$,
$\fonction{G}(v)\neq\bool^\omega$. Then $u^\omega\in \fonction{F}$ and 
$\fonction{F}(u)=\fonction{F}$.
\end{lem}
\begin{pf}[Lemma~\ref{best_open_lemma}]
Whatever $\alpha$, $u.\alpha\in \fonction{G}$. Because of the minimality of $u$ with 
respect to the property $\fonction{G}(u)=\bool^\omega$, for each $\alpha$, there is a $v$ 
prefix of $\alpha$ such that $(u.v)^\omega\in \fonction{F}$ and $\fonction{F}(u.v)=\fonction{F}$. Let $b$ be a 
boolean value in $u$. We choose $\alpha=b^\omega$. There is an $l$ such that 
$(u.b^l)^\omega\in \fonction{F}$. Because all entries of $\fonction{F}$ are equivalent, by 
Proposition~\ref{va_omega_ae}, $u^\omega\in \fonction{F}$. 

Let $\alpha\in \fonction{F}$. The vector $\alpha$ is
infinite, so there is a boolean value $b$ that is repeated infinitely often in 
$\alpha$. But there is an $l$ such that $\fonction{F}(u.b^l)=\fonction{F}$. 
So $u.b^l.\alpha\in \fonction{F}$, 
and by the equivalence of all entries (Proposition~\ref{va_omega_ae}), 
$u.\alpha\in \fonction{F}$, which means that $\alpha\in \fonction{F}(u)$. Conversely, if $\alpha\in 
\fonction{F}(u)$, $u.b^l.\alpha\in \fonction{F}$, and so $\alpha\in \fonction{F}$. Thus $\fonction{F}=\fonction{F}(u)$.
\end{pf}

\begin{pf}[Theorem~\ref{best_open}]
$\fonction{G}$ is an open function, because for any element $\alpha$ of 
$\fonction{G}$, there is
a $u$ prefix of $\alpha$ such that $\forall \beta$, $u.\beta\in \fonction{G}$.
$\fonction{F}$ is iterative, so there is an open function $\fonction{G'}$ such 
that $\fonction{F}=\recursif{G'}$. $\forall \alpha\in \fonction{G'}$, there is 
a $u$ prefix of $\alpha$ such 
that $\fonction{G'}(u)=\bool^\omega$ and $\taille{u}>0$. Let $u_0$ be the least such $u$. 
Because
$\fonction{F}=\recursif{G'}$, ${u_0}^\omega$ is in $\fonction{F}$, and
$\fonction{F}(u_0)=\fonction{F}$. So $\alpha\in \fonction{G}$, which means 
that $\fonction{G'}\subset \fonction{G}$. To prove the
theorem, we just have to prove that $\fonction{F}=\recursif{G}$. We will start by
$\fonction{F}\subset\recursif{G}$, then prove $\recursif{G}\subset
\fonction{F}$.

Let $\alpha\in \fonction{F}$. We suppose $\alpha\not\in\recursif{G}$. If there is a $u$ 
prefix of $\alpha$ such that $\fonction{G}(u)=\bool^\omega$, let $u_0$ be the least such 
$u$. $\alpha=u_0.\beta$. Then $\beta\not\in\recursif{G}$, but 
$\fonction{F}(u_0)=\fonction{F}$,
so $\beta\in \fonction{F}$. So we can iterate on $\beta$. This iteration is finite because
$\alpha\not\in\recursif{G}$, so we come to a point where there is no $u$ prefix
of $\alpha$ such that $\fonction{G}(u)=\bool^\omega$. But $\alpha\in \fonction{F}$, so there is
a $u_0$ prefix of $\alpha$ such that $\fonction{G'}(u_0)=\bool^\omega$, and
$u_0^\omega\in \fonction{F}$ and $\fonction{F}(u_0)=\fonction{F}$, and so 
$\fonction{G}(u_0)=\bool^\omega$, which 
contradicts the hypothesis. Thus $\fonction{F}\subset\recursif{G}$.

Let $\alpha\in\recursif{G}$. Let $(u_i)_{i\in\nat}$ be the sequence of words
such that $\fonction{G}(u_i)=\bool^\omega$, $\alpha=u_0.u_1\ldots u_i\ldots$,
$\taille{u_i}>0$ and $u_i$ minimum. Some letters appear infinitely often in
$\alpha$, and some others appear only finitely often. But there is a finite
number of $u_i$ containing the latter ones. Hence there is a permutation of the 
entries such that the result of the permutation on $\alpha$ is $v.\beta$, 
where $v$ is the concatenation of all $u_i$ that contain the letters that
appear finitely in $\alpha$ ($v$ can be empty), and $\beta$ is composed of 
those $u_i$ that 
contain just letters that appear infinitely in $\alpha$. By definition of 
$\recursif{G}$, $\beta\in \recursif{G}$, and because all entries of 
$\fonction{F}$ are 
equivalent, $v.\beta$ is in $\fonction{F}$ if and only if $\alpha$ is in 
$\fonction{F}$. But 
whatever $u_i$, $\fonction{F}(u_i)=\fonction{F}$ (see the lemma). So 
$\fonction{F}(v)=\fonction{F}$. And so $\alpha$ is in 
$\fonction{F}$ if and only if $\beta$ is in $\fonction{F}$. Either $\beta$ contains a
finite number of distinct $u_i$, or an infinite one.

If $\beta$ contains a finite number of distinct $u_i$, we call them
$(v_i)_{i\leq m}$. Then there is a permutation of the indexes such that
the result of the permutation on $\beta$ is $(v_0.v_1\ldots v_m)^\omega$.
We know that ${v_m}^\omega\in \fonction{F}$ (see the lemma), and for all $i$,
$\fonction{F}(v_i)=\fonction{F}$, so $v_0.v_1\ldots v_{m-1}.(v_m)^\omega\in \fonction{F}$. We call
$\gamma=v_0.v_1\ldots v_{m-1}.(v_m)^\omega$. Because $\gamma\in \fonction{F}$, there is a
sequence $(u'_i)_{i\in\nat}$ such that $\fonction{G'}(u'_i)=\bool^\omega$, $\gamma=u'_0.
u'_1\ldots u'_i\ldots$ and $u'_i$ minimum. So there is a $j$
such that $u'_0.u'_1\ldots u'_j=v_0.v_1\ldots v_{m-1}.{v_m}^n.w$ with
$w$ prefix of $v_m$. Whatever $i$, $(u'_0.u'_1\ldots u'_i)^\omega\in \fonction{F}$, because
$\fonction{F}=\recursif{G'}$. So, by Proposition~\ref{va_omega_ae}, $(v_0.v_1\ldots 
v_m)^\omega \in \fonction{F}$. This in turn means that $\beta\in \fonction{F}$.

If $\beta$ contains infinitely many distinct $u_i$, we call them 
$(v_i)_{i\in\nat}$. Necessarily, there is infinitely many 0's and 1's in 
$\beta$. So we have two $v_i$, $w_0$ and $w_1$ such that $w_0$ contains a 0 and
$w_1$ contains a 1. As $\beta$ is composed of $0$ and $1$, there is a 
permutation of the entries that transforms $\beta$ in $(w_0.w_1)^\omega$. So 
we are back to the problem with $\beta$ containing a finite number of $u_i$.

Thus, $\beta\in \fonction{F}$ whatever the case, which proves that $\alpha\in 
\fonction{F}$. We 
started from $\alpha\in\recursif{G}$, so $\recursif{G}\subset \fonction{F}$. Because we 
already proved $\fonction{F}\subset\recursif{G}$, we have $\fonction{F}=\recursif{G}$.
\qed \end{pf}

It is possible to compute effctively the best open function representing an
iterative function $\fonction{F}$, provided we already have a representation, 
that is an open function. The idea is to detect the $u$ such that 
$u^\omega\in\fonction{F}$ and $\fonction{F}(u)=\fonction{F}$. How we can do
this without looping is explained in \cite{mauborgne99}.

\section{A New Class: Regular Functions}\label{regular}
Now that we have a wide variety of infinite behaviors, we will try to
incorporate them with the finite behavior to obtain closure by boolean
operations, and thus a very wide variety of infinite functions.
The idea is to allow a finite set of iterative functions to describe
the infinite behavior at a given point in the function.

\begin{defn}
Let $\fonction{F}:\deffonc{\bool^\omega}{\bool}$ be a named function. The 
function $\fonction{F}$ is said to be \emph{regular} if
and only if $\fonction{F}$ is prefix regular and there is a finite set of non-empty 
iterative functions $\recrel{F}$ \label{recrel} such that $\forall \alpha\in 
\fonction{F}$,
$\exists u$, $\exists \fonction{G}\in\recrel{F}$, $\alpha\in u.\fonction{G}$ and $\fonction{G} \subset \fonction{F}(u)$.
\end{defn}

The informal meaning of this definition is that for any vector in the
relation, there is a finite point in the vector such that the tail of the 
vector is in one of the infinite behaviors (iterative functions) of the 
relation.

\begin{exmp}
Let $\fonction{F}$ be $\{0^\omega,1^\omega\}$. This function is prefix regular
(the different $\fonction{F}(u)$ are just $\fonction{F}$, $\fonction{F}(0)$,
$\fonction{F}(1)$ and $\emptyset$). The functions
$\fonction{F}_0=\{0^\omega\}$ and $\fonction{F}_1=\{1^\omega\}$ are iterative
functions. Any vector in $\fonction{F}$ is either in $\fonction{F}_0$ or
$\fonction{F}_1$. So $\fonction{F}$ is regular.

Let $\fonction{G}$ be the function \TRUE{} on any vector ending with
$0^\omega$ or $1^\omega$. Whatever the vector $\alpha$ in $\fonction{G}$,
there is a $u$ such that $\alpha=u.0^\omega$ or $\alpha=u.1^\omega$. In any
case, $\alpha\in u.\fonction{F}_i$ ($i=0,1$). Moreover, $\fonction{F}_i
\subset \fonction{G}(u)$. So $\fonction{G}$ is also regular.
\end{exmp}

\subsection{Expressive Power}
These functions are called regular because of the analogy with $\omega$-regular
sets of words of B\"{u}chi \cite{buchi60}. The only  restriction imposed by
the fact that we consider functions lies in the entry names, namely the entry
names must be ultimately periodic to be finitely representable. 

\begin{thm}
A named function $\fonction{F}$ is regular if and only if its entry names are 
ultimately periodic and the set of words in $\fonction{F}$ is $\omega$-regular in the sense of B\"{u}chi.
\end{thm}
The idea is that open functions define regular languages. If $U$ is the
regular language defined by an open function, then the associated iterative
function is $U^\omega$. The idea of the proof of the theorem is that an
$\omega$-regular language can be characterized as a finite union of
$U.V^\omega$, with $U$ and $V$ regular languages.

\begin{pf}
Let $\fonction{F}$ be a regular function. Because it is prefix regular, its
entry names are ultimately periodic. Let $\recrel{F}$ be $(\fonction{F}_i)_{i\in C}$. 
Each iterative function defines an $\omega$-regular language: the 
B\"uchi automaton that accepts the language defined by an iterative function 
represented by the open function $\fonction{G}$ is 
$(Q,E,\{\fonction{G}\},\{\fonction{G}\})$ with:
\begin{eqnarray*}
Q&=&\ensembletq{\fonction{G}(u)}{u\in\bool^*}\\
E&=&\ensembletq{\left(\fonction{G}(u),b,\fonction{G}_{ub}\right)}{b\in\bool,\: u\in\bool^*} \\
&&\mbox{where } \fonction{G}_v =\mbox{if } \left( \fonction{G}(v)=\bool^\omega \mbox{ and } 
\name{G}{\taille{v}}= \name{G}{0}\right) \mbox{ then } \fonction{G}\\
&&\qquad\qquad\qquad \mbox{ else } \fonction{G}(v)
\end{eqnarray*}
The state set $Q$ and the transition set $E$ are finite because of the prefix 
regularity of $\fonction{G}$.

$\fonction{F}=\bigcup_{u\in U}\bigcup_{i\in\ensembletq{j\in C}{\forall \alpha\in 
\fonction{F}_i,\: u\alpha\in \fonction{F}}}\ensembletq{u\alpha}{\alpha\in \fonction{F}_i}$ by 
definition of the regularity of $\fonction{F}$. Each set $\ensembletq{u\alpha}
{\alpha\in \fonction{F}_i}$ is $\omega$-regular because $\omega$-regularity of
words is closed under concatenation, and the number of such sets is finite by
prefix regularity of $\fonction{F}$. Being a finite union of $\omega$-regular languages,
$\fonction{F}$ represents an $\omega$-regular language.

Now let $(Q,E,I,F)$ be a B\"uchi automaton such that there is a boolean function
$\fonction{F}$ representing the same set of words and the entry names of 
$\fonction{F}$ are 
ultimately periodic. Let $\fonction{F}_q$ be the set of words corresponding to the
B\"{u}chi automaton $(Q,E,\{q\},\{q\})$. We define $L^*(Q,E,\{q\},\{q\})$ to
be the set of finite words represented by this automaton. Each $\fonction{F}_q$ is an 
iterative function represented by the open function:
\[ \fonction{G}_q=\ensembletq{\alpha\in\bool^\omega}{\exists u,\:
\alpha=u\beta,\; u \in L^*\left(Q,E,\{q\},\{q\}\right)}\]
These functions are prefix regular because the
automaton is finite and the entry names are ultimately periodic. They are 
obviously open because a finite decision procedure is enough to find out
that a given infinite vector is in the relation. Whatever $\alpha$ in the set
represented by the B\"{u}chi automaton, $\alpha$ is the label of an infinite 
path such that there is a $q$ in $F$ and $q$ is in the set of infinitely 
repeated states of the path.
Thus, there is an $u$ such that $\alpha=u\beta$ and $\beta$ is
in $\fonction{F}_q$, and for all $\gamma\in \fonction{F}_q$, $u\gamma$ is in the language of the
B\"{u}chi automaton $(Q,E,I,F)$. So $\fonction{F}$ is a regular
function and $\recrel{F}=(\fonction{F}_q)_{q\in F}$.
\qed \end{pf}

\begin{cor}
If $\fonction{F}$ and $\fonction{G}$ are regular functions, then 
$\fonction{F}\wedge \fonction{G}$, $\fonction{F}\vee \fonction{G}$ and
$\neg \fonction{F}$ are regular functions.
\end{cor}
It is an immediate consequence of the theorem, the closure properties of
$\omega$-regular languages, and the closure properties of the fact that the
set of entry names is ultimately periodic.

\subsection{Attempting a Representation}
Let us recall the definition of a regular function $\fonction{F}$: $\forall 
\alpha\in \fonction{F}$, $\exists u$, $\exists \fonction{G}\in\recrel{F}$, 
$\alpha \in u.\fonction{G}$ and
$\fonction{G}\subset \fonction{F}(u)$. It provides a natural decision process (possibly infinite if
the vector is not in the relation): for each prefix $u$ of $\alpha$ (in
increasing order), we test $\fonction{F}(u)$. If is is empty, then $\alpha$ is not in
the relation. Otherwise, for each $\fonction{G}\in\recrel{F}$ such that 
$\fonction{G}\subset \fonction{F}(u)$,
we test if the remaining of $\alpha$ is in $\fonction{G}$. If one of these tests is 
positive, $\alpha$ is in the relation.

If we try to insert the necessary informations in the decision tree, we need
to store at each point in the decision process the set of possible iterative
functions. Representing an iterative function is easy and unique (see previous
section). The first problem is that we do not have such uniqueness results
for finite unions of iterative functions. The second problem is the non
deterministic nature of the decision process, which consists in quite 
inefficient
tries and backtrackings. Such a representation extending BDDs would be
possible, but we would loose (as far as the author tried) too many good
properties of the BDDs. So we will try in the next section to define a smaller
class of infinite functions (but bigger than mere open functions) that could
have a good representation.

\section{BDGs with \REC nodes: $\omega$-deterministic Functions}\label{bdg}
In order to obtain a tractable class of functions, we restrict the class
of regular functions. We call these functions $\omega$-deterministic because
we restrict the number of possible infinite behaviors at a given $u$ to at
most one iterative function.

\begin{defn}
Let $\fonction{F}:\deffonc{\bool^\omega}{\bool}$ be a named function. 
$\fonction{F}$ is $\omega$-deterministic if and
only if $\fonction{F}$ is prefix regular and 
\[\forall u,\: 
\recursifset{v.\alpha}{u.v^\omega\in \fonction{F}\mbox{ and } 
\fonction{F}(u.v)=\fonction{F}(u)} \subset \fonction{F}(u)\]
\end{defn}

The iterative function $\iterbehave{F}{u}\eqdef\recursifset{v.\alpha} 
{u.v^\omega\in \fonction{F}\mbox{ and } \fonction{F}(u.v)=\fonction{F}(u)}$ is the only infinite behavior
possible at $u$. Any other iterative function in the infinite behavior at this
point would be included into $\iterbehave{F}{u}$.

\begin{thm}
An $\omega$-deterministic function $\fonction{F}$ is regular, and whatever the 
functions in $\recrel{F}$ representing the infinite behavior at a given point 
$u$, there is an iterative function representing the infinite behavior at $u$ 
and containing all of them.
\end{thm}

\begin{pf}
Let $\fonction{F}$ be an $\omega$-deterministic relation. We first prove that
$\fonction{F}$ is 
regular. We define $\recrel{F}=\ensembletq{\iterbehave{F}{u}}{
\iterbehave{F}{u}\neq\emptyset}$. This set is finite because $\fonction{F}$ is 
prefix regular. Let $\alpha\in \fonction{F}$. If $\alpha$ is ultimately periodic, as $\fonction{F}$ is prefix
regular, there is an $u$ and a $v$ such that $\fonction{F}(u.v)=\fonction{F}(u)$
and $\alpha=u.v^\omega$. Then $\iterbehave{F}{u}\neq\emptyset$, and
for all $\beta\in\iterbehave{F}{u}$, $u.\beta$ is in $\fonction{F}$ because
$\fonction{F}$ is $\omega$-deterministic. If $\alpha$ is not ultimately periodic, as the
entry names are ultimately periodic, there is a permutation of the entries
which transforms $\alpha$ in $\beta$ which is ultimately periodic. Moreover, 
it is possible to choose the permutation that it leaves $u$ unchanged (we 
start after the last letter that appears finitely many times and after the 
looping of the relation) such that $\beta=u.v^\omega$ as above. As the 
$\iterbehave{F}{u}$ have the same equivalence of entries as $\fonction{F}(u)$ (at least),
we have the postfix of $\alpha$ after $u$ is in $\iterbehave{F}{u}$.

Concerning the canonicity of the iterative function at a given point, we have
the fact that for all iterative function at $u$ of $\fonction{F}$, the iterative function
is included in $\iterbehave{F}{u}$.
\qed \end{pf}


\subsection{The Decision Tree}
If the set $\ensembletq{v}{u.v^\omega\in \fonction{F}\mbox{ and }
\fonction{F}(u.v)=\fonction{F}(u)}$ is not
empty, then it is possible, in the decision process, that we enter an
infinite behavior. It must be signaled in the decision tree. To this end, we
introduce a new kind of node in the decision tree, the \REC node. The \REC
node signals that we must start a new infinite behavior, because before this
node, we were in fact in the finite part of the function. The \REC node has
only one child. In the graphical representation, we will sometimes write 
$\petitarbre{x \ar@{>|}[d]\\t}$ for $\petitarbre{x \ar[d]\\ \tinyrec\ar[d]\\t}$.
After a \REC node, we start the decision tree representing the iterative
function. We know that when this decision tree comes to a \TRUE, we must
start again just after the previous \REC node. \FALSE nodes in the decision tree
are replaced by the sequel of the description of the $\omega$-deterministic
function. As iterative functions of the $\omega$-deterministic function are
uniquely determined, and their representation is unique, the decision tree
of the $\omega$-deterministic function is unique.

Note that open functions are $\omega$-deterministic. Their representation as
an $\omega$-deterministic function is the same as in the previous section,
but with a \REC preceding every \TRUE. It means also that the restriction of
this representation to finite functions give the classical BDD, except for the
\REC preceding the \TRUE. 

\subsection{The Semantics of the Decision Tree}
The semantics of the decision tree is defined in terms of a pseudo-decision 
process (it is not an actual decision process because it is infinite). The 
decision process reads a vector and uses a stack $S$ and a current
iterative tree, $r$. At the beginning, the stack is empty and
$r$ is the decision tree. When we come to a \TRUE node, we stack it and start
again at $r$. When we come to a $\petitarbre{\tinyrec \ar[d]\\t}$ node, $r$
becomes $t$ and we empty the stack. If we come to a \FALSE\ node, we stop the
process. The process is a success if it doesn't stop and the stack is
infinite. 
 
\begin{exmp}\mbox{ }\\
\begin{tabular}{p{2.66cm}p{10.41cm}}
$\topmoyenarbre{& \variable{x} \ar@{>|}[dl]_0 \ar@{>|}[dr]^1 \\
\variable{x} \ar[d]_0 \ar[drr]^<<1 &&\variable{x} \ar[dll]_<<1 \ar[d]^0 \\ \TRUE && \FALSE}\!\!$ &
when we read a 0, the current iterative tree becomes $\!\!\petitarbre{ & x \ar[dl]
\ar[dr] \\ \tinytrue && \tinyfalse}\!\!$. If we read a 1 after that, we stop on
a failure, and if we read a 0, we stack a \TRUE and start again with the same
iterative tree. So, after a 0, we can only have $0^\omega$. After a 1, the
iterative tree becomes $\!\!\petitarbre{ & x \ar[dl] \ar[dr] \\ \tinyfalse &&
\tinytrue}\!\!$, and this time, we can only have $1^\omega$. So this function 
is $\{0^\omega,1^\omega\}$.
\end{tabular}
\end{exmp}
\begin{exmp}\mbox{ }\\
\begin{tabular}{p{2.66cm}p{10.41cm}}
$\topmoyenarbre{& \variable{x} \ar[dl]_0 \ar@{>|}@(dr,r)_1 \\ \TRUE} $ &
during the decision process, the iterative tree never changes. When we read a
0, we stack a \TRUE\ and start again. But each time we read a 1, we empty the
stack. So the only vectors that stack an infinite number of \TRUE are the
vectors ending by $0^\omega$.
\end{tabular}
\end{exmp}

\subsection{Boolean Operators}
\begin{prop}
Let $\fonction{F}$ and $\fonction{G}g$ be two $\omega$-deterministic 
functions. Then $\fonction{F}\wedge \fonction{G}$ is $\omega$-deterministic.
\end{prop}

This property is derived from the fact that iterative functions are closed
under intersection, so the infinite behavior at each point is an iterative
function. Moreover, intersection preserves prefix regularity, so the result
is $\omega$-deterministic.

The algorithm building the decision tree representing $\fonction{F}\wedge 
\fonction{G}$ identifies
the loops, that is we come from a $(t,u)$, which are subtrees of the decision 
trees representing $\fonction{F}$ and $\fonction{G}$, and return to a $(t,u)$. If in such a loop, we 
have not encountered any new \TRUE in any decision tree, we build a loop,
if one decision process has progressed, we keep building the decision tree,
and when both have been through a \TRUE, we add a \TRUE in the intersection.

$\omega$-deterministic functions are not closed under union. As they are
closed under intersection, it means that they are not closed under negation either.

\begin{exmp}[Impossible Union]
Let $\fonction{F}_1$ be the set of all vectors with a finite number of 1's, and  
$\fonction{F}_2$ the set of all vectors with a finite number of 0's. 
$\fonction{F}_1$ and $\fonction{F}_2$ are 
represented by:
\[\moyenarbre{ & \variable{x} \ar[dl]_0 \ar@{>|}@(dr,ur)_1 \\ \TRUE}\quad\mbox{ and }\quad
\moyenarbre{ \variable{x} \ar@{>|}@(dl,ul)^0 \ar[dr]^1 \\ & \TRUE}\]
Let $\fonction{F}=\fonction{F}_1\vee \fonction{F}_2$. The set 
$\recursifset{u.\alpha}{u^\omega\in \fonction{F}\mbox{ and } 
\fonction{F}(u)=\fonction{F}}$ is the set of all vectors, but 
$(01)^\omega\not\in \fonction{F}$,
so $\fonction{F}$ is not $\omega$-deterministic.
\end{exmp}

\subsection{Approximation}
\begin{prop}
Whatever $\fonction{F}$ prefix regular function, there is a least (for set inclusion)
$\omega$-deterministic function containing $\fonction{F}$.
\end{prop}
The process of building the best $\omega$-deterministic function approximating
a prefix regular function consists in adding the iterative functions defined
by $\left\{v.\alpha\right|u.v^\omega\in \fonction{F}\mbox{ and } 
\fonction{F}(u.v)=\fonction{F}(u)\}$ to $\fonction{F}(u)$. We define 
$\fonction{F}^+\eqdef \fonction{F}\cup \bigcup_w w.\iterbehave{F}{w}$. We just 
add the minimum number of vectors so that the infinite behaviors at each point 
is an iterative function. This function is also prefix regular, by prefix 
regularity of $\fonction{F}$, and as such it is $\omega$-deterministic.

If we start from an $\omega$-deterministic function and perform operations
that preserve prefix regularity, such as union, we can give best
approximations of these operations. It means that we can have a kind of
abstract behavior, keeping as close as possible to the desired operations, while
keeping the good representation as BDGs.

\section{Conclusion}\label{conclusion}
To achieve the representation of infinite functions, we presented a new insight
on variables which allows the sharing of some variables. This
sharing is compatible with every operation on classical BDDs, at no
additional cost. It is even an improvement for classical BDDs, as it speeds up
one of the basic operations on BDDs, the restriction operation.

We presented three classes of infinite functions which can be represented
by extensions of BDDs. So far, the only extension that allowed the
representation of infinite function was presented by Gupta and Fisher in
\cite{gupta:fisher93} to allow inductive reasoning in circuit representation.
Their extension  corresponds to the first class (open functions), but without
the uniqueness of the representation, because the loops have a name, which is
arbitrary (and so there is no guarantee that the same loop encountered twice
will be shared). 

Our representation for open functions and $\omega$-deterministic
function have been tested in a prototype implementation in Java. Of course,
this implementation cannot compete with the most involved ones on BDDs. It is,
however, one of the advantages of using an extension of BDDs: many useful
optimizations developed for BDDs could be useful, such as complement
edges \cite{billon87} or differential BDDs \cite{anuchitanukul:manna:uribe95}. 
This last extension could lead to wider classes of functions by releasing
some of the restrictions imposed by the equivalence of entries.
This is a direction for future work. 
Another direction for future work concerns the investigation over regular
functions. These functions are closed under boolean operations, but we did not
find a satisfactory unique representation with a decision tree yet. We
believe the first two classes will already be quite useful. For example the
first class (open function) is already an improvement over 
\cite{gupta:fisher93}, and the second class ($\omega$-deterministic) can
express many useful properties of temporal logic \cite{manna:pnueli88}.
This work is a step towards model checking and static analysis of the
behavior of infinite systems, where properties depending on fairness can be 
expressed and manipulated efficiently using BDGs \cite{mauborgne00b}.

%\begin{ack}
%Many thanks to Patrick Cousot for reading this
%work carefully and for many useful comments. Ian Mackie corrected many English
%mistakes in the paper.
%\end{ack}

\bibliographystyle{elsart-num}
\bibliography{bdg}

\end{document}
