Synchronous programming is a powerful approach to programming reactive systems. Following the 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). In Saraswat et al 1994 we had proposed a model for this called Timed cc --- here we extend the model of Timed cc to express strong time-outs: if an event A does not happen through time t, cause event B to happen at time t. Such constructs arise naturally in practice (e.g. in modeling transistors) and are supported in synchronous programming languages.
The fundamental conceptual difficulty posed by these operations is that they are nonmonotonic. We provide a simple compositional semantics to the non-monotonic version of concurrent constraint programming (Default cc) obtained by changing the underlying logic from intuitionistic logic to Reiter's default logic. This allows us to use the same construction (uniform extension through time) to develop Timed Default cc as we had used to develop Timed cc from cc. Indeed the smooth embedding of cc processes into Default cc processes lifts to a smooth embedding of Timed cc processes into Timed Default cc processes.
We identify a basic set of combinators (that constitute the Timed Default cc programming framework), and provide a constructive operational semantics (implemented by us as an interpreter) for which the model is fully abstract. We show that the model is very rich by defining several combinators from the synchronous languages. We show that Timed Default cc is compositional and supports the properties of multiform time, orthogonal preemption and executable specifications. In addition, Timed Default cc programs can be read as logical formulas (in an intuitionistic temporal logic) --- we show that this logic is sound and complete for reasoning about (in)equivalence of Timed Default cc programs.
Like the synchronous languages, Timed Default cc programs can be compiled into finite state automata. In addition, the translation can be specified compositionally. This enables separate compilation of Timed Default cc programs and run-time tradeoffs between partial compilation and interpretation.
A preliminary version of this paper was published in POPL 95. Here we present a complete treatment of hiding, along with a detailed treatment of the model.
Keywords: Programming paradigms --- constraint programming, reactive systems, synchronous programming; Formal approaches --- denotational semantics, semantics of concurrency, default logic.
@Article{tdcc-jsc,
author = "V.A.Saraswat and R.Jagadeesan and V.Gupta"
title = "Timed Default Concurrent Constraint Programming",
journal = "Journal of Symbolic Computation",
volume = "22",
number = "5--6",
pages = "475--520",
month = nov # "--" # dec,
year = "1996",
note="Extended abstract appeared in the {\em Proceedings of
the 22nd ACM Symposium on Principles of Programming Languages}, San
Francisco, January 1995"
}
Postscript file (455K)