# Foundations of Timed Concurrent Constraint Programming

Vijay A. Saraswat, Radha Jagadeesan, Vineet Gupta
### Abstract

We develop a model for timed, reactive computation by extending
the asynchronous, untimed concurrent constraint programming model
in a simple and uniform way. In the spirit of process algebras,
we develop some combinators expressible in this model, and
reconcile their operational, logical and denotational character.
We show how programs may be compiled into finite-state machines
with loop-free computations at each state, thus guaranteeing
bounded response time.

### Synopsis

Synchronous programming is a powerful approach
to programming reactive systems. Following Abramsky's idea that
``processes are relations extended over time'' we
propose a simple but powerful model for timed, determinate
computation, extending the closure-operator model for untimed
concurrent constraint programming (CCP). The model incorporates a
careful distinction between the detection of information that is
positive (``some event happened'') and negative (``some event did
not happen''). This allows it to circumvent the ``temporality
paradoxes'' of Esterel which arise from the confusion between
causality and temporality that has hitherto seemed to be an
integral part of the synchronous approach to computing.
We identify a basic set of combinators (that constitute the Timed
Concurrent Constraint Programming framework, tcc), and provide a
constructive operational semantics for which the model is fully
abstract. We show that the model is very rich. A basic
combinator allows action to be enabled in the future if certain
events * did not * happen in the past, thus incorporating a
form of ``safe defaults''. We introduce a combinator, **
clock**, that allows processes to be clocked by certain kinds of
other (recursively defined) processes; we show that the
pre-emption and abortion constructs of synchronous programming
languages can be derived as special cases of ** clock**. We
show that ** clock** is itself definable using the basic set of
combinators, by providing a complete set of equational laws. More
generally, tcc can be seen as providing a natural timed
extension of the Kahn framework for data-flow
computation (since untimed CCP generalizes the Kahn framework).

Like the synchronous languages, languages in the tcc family
enjoy the property of multi-form time - the control constructs
do not treat time in a way any more special than any other
signal. In addition, tcc programs can be read as logical
formulas (in intuitionistic temporal logic, InTL), and tcc
computation understood as deriving the ``least'' solution for
these formulas. In addition, we show that InTL is sound and
complete for reasoning about (in)equivalence of tcc programs.

Like the synchronous languages, tcc programs can be compiled
into finite state automata. In addition, the translation can be
specified compositionally. This enables separate compilation of
tcc programs and run-time tradeoffs between partial
compilation and interpretation of the kind not available for
these other synchronous languages.

© IEEE, 1994.

@InProceedings{tcc-lics94,
title = "Foundations of Timed Concurrent Constraint
Programming",
author = "Vijay Saraswat and Radha Jagadeesan and Vineet Gupta"
pages = "71--80",
booktitle = "Proceedings, Ninth Annual {IEEE} Symposium on Logic in
Computer Science",
year = "1994",
month = "4--7 " # jul,
address = "Paris, France",
organization = "IEEE Computer Society Press"
}

Postscript file (139K)

Pdf file (165K)