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.

@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)