Default Timed Concurrent Constraint Programming

Vijay A. Saraswat, Radha Jagadeesan, Vineet Gupta

Abstract

We extend the model of tcc to express strong time-outs (and preemption): 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 languages such as Esterel (through instantaneous watchdogs) and Lustre (through the ``current'' operator).

The fundamental conceptual difficulty posed by these operators is that they are non-monotonic. We provide a simple compositional semantics to the non-monotonic version of concurrent constraint programming (CCP) 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 Default Timed CCP as we had used to develop Timed CCP from CCP. Indeed the smooth embedding of CCP processes into Default cc processes lifts to a smooth embedding of tcc processes into Default tcc processes. Interesting tcc properties such as determinacy, multi-form time, a uniform pre-emption construct (``clock''), full-abstraction, and compositional compilation into automata are preserved.

Default tcc thus provides a simple and natural (denotational) model capable of representing the full range of preemption constructs supported in Esterel, Lustre and other synchronous programming languages.

@InProceedings{tdcc-popl95,
  author =       "V.A.Saraswat and R.Jagadeesan and V.Gupta"
  title =        "Default Timed Concurrent Constraint Programming",
  booktitle =    "Conference Record of the 22nd {ACM} {SIGPLAN}-{SIGACT}
                 Symposium on Principles of Programming Languages
                 ({POPL}'95)",
  address =      "San Francisco, California",
  publisher =    "ACM Press",
  month =        jan # " 22--25,",
  year =         "1995",
  pages =        "272--285",
}

Postscript file (294K)
Pdf file (256K)