Computing with Continuous Change

Vineet Gupta, Radha Jagadeesan, Vijay Saraswat

Abstract

A central challenge in computer science and knowledge representation is the integration of conceptual frameworks for continuous and discrete change, as exemplified by the theory of differential equations and real analysis on the one hand, and the theory of programming languages on the other.

We take the first steps towards such an integrated theory by presenting a recipe for the construction of continuous programming languages - languages in which state dynamics can be described by differential equations. The basic idea is to start with an untimed language which admits the detection of positive and negative information (the absence of action), and then extend it uniformly over dense (real) time.

We present a concrete mathematical model and language (the Hybrid concurrent contraint programming model, Hybrid CC ) instantiating these ideas. The language is intended to be used for modeling and programming hybrid systems . The language is declarative - programs can be understood as formulas that place constraints on the (temporal) evolution of the system, with parallel composition regarded as conjunction. It is expressive - it allows the definition of a continuous version of the pre-emption control constructs.

The language is obtained by extending the general-purpose computational formalism of (default) concurrent constraint programming (Default cc) with a single temporal construct, called hence - hence A is read as asserting that A holds continuously beyond the current instant. Various patterns of temporal activity can be generated from this single construct by use of the other combinators in Default cc, in particular instantaneous preemption (as in synchronous programming). We provide a precise operational semantics according to which execution alternates between points at which discontinuous change can occur, and open intervals, in which the state of the system changes continuously. Transitions from such a state of continuous evolution can be triggered either by the establishment of a condition or by the dis-establishment of an existing condition. We show that the denotational semantics is correct for reasoning about the operational semantics, through an adequacy theorem.

Keywords: Reactive systems, hybrid systems, constraint-based programming, specification, concurrent constraint programming, synchronous programming.

@Article{hcc-foundations,
  title =        "Computing with continuous change",
  author =       " Vineet Gupta and Radha Jagadeesan and Vijay Saraswat",
  pages =        "3--49",
  journal =      "Science of Computer Programming",
  month =        jan,
  year =         "1998",
  volume =       "30",
  number =       "1--2"
}
Postscript file (480K)
Pdf file (363K)