\section{Future work}
The ideas above open up a new line of attack on the problem of
systematic, model-based design of embedded, reactive, real-time
systems, e.g., those used to control complex electro-mechanical
systems such as airplanes, photo-copiers etc.  Considerable work
lies ahead on several fronts.

\subsection{Developing methods for generating real-time
schedulers from \tcc{} models}

An important use of the \tcc{} is in specifying the behavior of
simple, computationally-controlled physical mechanisms, such as
the paper-path and video-path in a digital photo-copier.  This
leads to the problem of synthesizing optimal controllers for
these physical mechanisms. For example, we can (and, in a
slightly different way, have) specify the components of the
paper-path in a photocopier and the Xerographic subsystem in
\tcc.  The problem of synthesizing a scheduler is now the problem
of synthesizing the time-sequenced control signals that must be
input into the system such that the desired output (the properly
constituted output job, e.g. $4$ double-sided copies, stapled) is
produced as early as possible. This can be solved by extracting
from the \tcc{} program a constraint problem and solving it using
optimization techniques. For example, in the case of some of the
scheduling problems we have looked at, the optimization problems
generated are a subcase of the integer linear programming
problem, and can be solved by dynamic programming. In other
cases, we expect considerably harder optimization problems to
arise.

Another interesting set of problems arise in re-planning. The
schedule, once generated, are pressed into action. Various
exceptions can arise at run-time. Sheets may get delayed because
a roll is slipping, a video-image may be so complicated as to
cause the decompression software to be late in delivering video
bits to the output laser, etc. Thus execution has to be
monitored, and then, in case of exceptions, subsidiary scheduling
problems have to be generated. These are modified versions of the
initial problem (with some of the initial commitments in place,
and some others contradicted). This naturally motivates examining
algorithms for incrementally (re-)solving these optimization
problems.

\subsection{Program Verification}
\def\dor#1\watchingr#2{\mbox{\tt do}\ #1\ \mbox{\bf watching}\ #2
}

The advantages of reasoning with executable specifications is well
known; {\em c.f.} Berry's WYPIWYE principle or executable intermediate
representations for compilers.  \tcc{} can be viewed as an executable
temporal logic, thus permitting programs and properties to be
expressed in the same language.  

For example, let $\tt p$ be the property ``any occurrence of event
$\tt a$ must cause $\tt b$ to be true until the next occurrence of event
$\tt c$''. The property can be directly expressed as the program:
\begin{ccprogram}
  \agent p:: \tt {\bf whenever}\; a\; {\bf do}\; (\do{\always b}\watching{c})..
\end{ccprogram}
An agent $\tt A$ satisfies $p$ iff:
$$ \tt A \vdash p$$

Hence, one may use the logic for reasoning about inequivalence of
\tcc{} programs for establishing that programs posses such
properties. 

We plan to investigate the use of automated tools(theorem provers
and model checkers) to solve this verification problem.  In
particular, since parallel composition is modeled by the logical
operation of conjunction, there is hope of performing
compositional model checking, thus mitigating the state explosion
problem.

For an alternate approach, recall that deterministic safety properties
correspond precisely to safety automata~\cite{Pnueli-Manna90} that
have a single designated failure state.  Combined with the fact that
\tcc{} allows programs and properties to be expressed in the same
language, this leads to the promise of reducing general safety
properties of \tcc{} programs to checking the reachability of a
designated failure state.

From the programming point of view, this suggests a further
integration of the logic and programs.  At present, \tcc{} allows
access only to the {\em current} value of signal variables.  We
will investigate the addition of {\em global} constraints on
signal variables, say in the spirit of \Lustre{} and \Signal{}.
For example, let $X,Y,Z$ be channels that receive one input at
each time instant.  Then, $\uparrow Z = \uparrow X + \uparrow Y$
would indicate that at all time instants, the value of $Z$ is the
sum of the values of $X$ and $Y$.  The utility of this construct
for programming and verification needs to be investigated.

\subsection{Towards a theory of preemption } 
In the traditional theory of sequential programming, preemption
and abortion constructs have not been investigated separately.
The primary reason for this apparent oversight is that control
constructs of this form are ``compilable'' back to traditional
combinators, via the continuation passing transform.  For
example, exceptions in ML are handled this way.

Unfortunately, this oversight has continued in much of the
traditional work on process theory, where there is no obvious
compilation of preemption constructs back into basic combinators.
Indeed, synchronous languages arose in part as an attempt to
remedy this flaw.  However, the problem is now the plethora of
preemption constructs.  For example, what is the relationship, if
any, between the constructs supported by \Esterel and those
supported by \Signal?  The unification of the pre-emption
combinators in \Lustre, \Signal\ and \Esterel\ achieved by \tcc{}
suggests that \tcc{} encapsulates the rudiments of a theory of
pre-emption constructs.  A fully developed theory would identify
the properties of an ambient category of processes that would
allow the ``orthogonal'' addition of pre-emption constructs.  A
first step would be to explore the connections of \tcc{} with
Interaction categories~\cite{IntCat}, a general description of
synchronous processes.

\subsection{Integration of asynchronous and synchronous computation}
This paper has focused on synchronous systems; the reason for
focusing initially on synchronous systems is that they can be
construed as the building blocks for asynchronous systems.
Following the route similar to~\cite{CRP}, an asynchronous model
of computation can be constructed by message passing between
synchronous nodes; message delivery is guaranteed but there are
no bounds on message delivery time.  In our setting, this
translates to a bunch of synchronous nodes running \tcc{}
programs, communicating with each other via constraints, where
the time taken for stores to incorporate constraints can be
unbounded.  Thus, indeterminacy arises naturally as the result of
abstracting away from timing considerations.  From a logical
point of view, this idea is captured by the idea of {\em
eventual} tells, modeled by the ``Eventual'' modality in
(linear-time) temporal logic. As in \tcc{}, this program will
involve development of foundational and pragmatic aspects.

\begin{itemize}
  
\item From a foundational point of view, this language to satisfy
  the same strong properties as \tcc{}; namely, the logical and
  model theoretic readings will enable declarative programming
  styles and direct specification of complex process descriptions,
  and their algebraic manipulation.
  
\item From a programming point of view, the language should
  recover the expressiveness associated with traditional process
  calculi, for example Hoare's CSP, Occam and Milner's CCS.  In
  fact, since the \tcc{} paradigm already incorporates the ability
  to ``pass channel names'' more powerful calculi, say Milner's
  Pi-calculus, should be mimicked.  The significant difference from
  programming in traditional process calculi will be twofold:
  firstly, the ability to program declaratively that is made
  possible by the logical foundations of the language; and
  secondly, the integration of real time into programming and
  reasoning.
\end{itemize}