Automatic construction of digital controllers/device drivers for electro-mechanical systems using component models

Qualitative reasoning for physical systems, and techniques for automatic code generation are used to automatically construct digital controllers/device drivers for electro-mechanical systems. Such construction uses models of the system's components described as finite state machines, to form a configuration space. Transitions of the configuration space are labelled as external or internal and a state of the system is identified as a desired state while other states are identified as undesirable. From this configuration space a controller is generated to drive the system to the desired state while avoiding the undesirable states.

BACKGROUND OF THE INVENTION 
This application pertains to the construction of digital controllers/device 
drivers and more particularly to a method for automatic construction of 
digital controllers/device drivers to control electro-mechanical systems, 
based on finite state machine (FSM) models of the system components. 
The invention is particularly applicable to generating a model of a system 
which can then be used for a number of different purposes. The system 
model consists of a physical model of the components, their 
interconnections, and a specification of the task to be performed. The 
component models can be obtained from a library of models. Using this 
model, it is possible to generate control code which ensures that during 
operation the system will meet the desired task or will appropriately 
report information regarding a failure. The subject invention combines 
concepts from qualitative reasoning for physical systems with techniques 
for automatic generation of code from finite state machine (FSM) 
descriptions. The following discussion sets forth an example for the 
automatic construction of controllers for controlling a paper supply 
system of a copy machine, and will be described with particular reference 
thereto. However, it will be appreciated that the invention has broader 
applications, including printing machines, IOTs, communication systems, 
automated manufacturing, facility management environments and any other 
system or machine which includes electro-mechanical components. 
Presently, digital controllers/device drivers used for controlling 
electro-mechanical systems such as paper trays and papers paths in a copy 
machine are generated manually by software engineers who have an informal 
understanding of how the devices which they are generating code for, 
operate. The engineers will simulate operation of the devices to the best 
of their ability and understanding to obtain a theoretical understanding 
of the behavior of a system and the components comprising the system. 
Thereafter, software code is hand-produced, usually in a language such as 
C or C++. A system controller generated by these techniques will accept 
power-up signals from the environment, drive motors, set time-outs, and 
prescribe the behaviors to be followed in case of erroneous executions. 
The construction of such coded systems is complex and error prone, and is 
susceptible to the introduction of subtle timing bugs. 
It is noted that although certain terminology of the subject invention may 
appear somewhat similar to what is generally known as "automatic code 
generation", the subject invention is significantly different from 
concepts set forth in this area. Automatic code generation may be 
generally thought of as the automatic generation of compilers from a 
description of a target architecture and a description of language 
symantics. A distinction between this concept and the subject invention is 
that automatic code generation is directed to general purpose programs 
which take as input any programming language and from this input generate 
machine code. 
On the other hand, the subject invention is directed to using as its input 
a description of a physical machine, i.e. electronic and mechanical, in 
order to produce an output such as a finite state machine, that can then 
be implemented as a controller to control the physical machine. The 
present invention is specifically directed to taking advantage of the 
presentation of continuous physical systems, whereas compiler work is 
directed to taking any arbitrary programming language such as Fortran, C, 
C++, etc. and generating a machine code to be used by the computer system. 
Therefore, the subject invention is controlling physical objects existing 
in the real world starting with physical objects existing in the real 
world. The subject invention is not, as is material directed to the 
compiler art, preceding from a description of languages and descriptions 
of computers which are attempting to run those languages. 
The present invention contemplates a new and improved system for 
automatically constructing controllers for an electro-mechanical system 
which overcomes the above-referenced problems, and others, and provides a 
system with enhanced useability and interchangability. 
SUMMARY OF THE INVENTION 
In accordance with the present invention, controllers are automatically 
constructed by identifying the components which make up the 
electro-mechanical system. A dynamic behavior model of the system is 
generated using a set of constraints for each of the components. 
Thereafter a configuration space of the system is constructed using the 
dynamic behavior model of the system to generate a set of states, each of 
which represents a possible configuration of the system, and for 
generating a set of transitions which exist between the states. The 
transitions are labeled as an external transition or an internal 
transition, wherein the external transitions occur due to events beyond 
the control of the controller and wherein the internal transitions can be 
controlled by the controller. A desired state or goal condition of the 
system is identified as are undesirable states of the system. Thereafter, 
using the configuration space a program is automatically generated which 
drives the system from any one of the states of the system towards the 
desired state (goal condition). The program changes states based on 
external events, internal events and predetermined time periods. 
In accordance with a more limited aspect of the present invention, the 
constraints are qualitative and quantitative constraints. 
In yet another aspect of the subject invention, the automatically generated 
program operates to avoid entering undesirable states. 
In accordance with still yet another aspect of the present invention, the 
internal transitions are controllable by the constructed controller. 
In yet another aspect of the subject invention, diagnostic information 
regarding possible failures of the system are obtainable. 
An advantage of the present invention is providing automatically 
constructed digital controllers/device drivers for electro-mechanical 
systems based on component models. Where the method combines concepts of 
qualitative reasoning for physical systems with techniques for automatic 
generation of code from finite state machine (FSM) descriptions. 
Yet another advantage of the present invention is the generation of 
controllers to control components for a number of different purposes. 
Yet another advantage of the present invention is the provision of a 
program to move a system from an initial state to a desired state (goal 
condition) without entering undesirable states. 
Further advantages will become apparent to one of ordinary skill in the art 
upon a reading and understanding of the subject specification.

DETAILED DESCRIPTION OF THE PREFERRED EMBODIMENT 
Turning now to the drawings provided for purposes of illustrating the 
preferred embodiment of the invention only, and not for purposes for 
limiting the same. FIG. 1 illustrates a print engine A which includes a 
plurality of systems B and a data processor unit C for inputting signals 
to the systems of print engine A. As used herein "print engine" includes 
any reprographic machine, such as printers, copiers, facsimile machines, 
and the like. In the discussion following, reference will be made to copy 
machines, copiers, copy operations, etc. 
As will be detailed below, various capabilities provided with each of the 
systems B are ascertained and correlated in the data processor unit C. 
Such correlated and analyzed data is further analyzed in view of user 
input defining a desired copier operation, or series of operations. These 
inputs, which may also be called external events, along with internal 
events and predetermined time-outs are used to control operation of the 
copy machine to most efficiently accomplish a series of copy tasks. It 
should be appreciated that even though the present discussion is directed 
to a print engine, the described controller construction is intended to be 
used in conjunction with other continuous physical systems which include 
eelectro-mechanical components. 
With continuing attention to FIG. 1, print engine A includes a plurality of 
paper storage bins. In the illustration, these include bins 10, 12, and 
14. The plurality of bins may be representative of different paper sizes 
or secondary or reserved storage capabilities. A paper feeder mechanism is 
illustrated schematically at 16. As will be appreciated by one of ordinary 
skill in the art, a paper feeder such as illustrated at 16 will function 
to obtain paper from one or more of the bins. 
The feeder 16 will feed paper to a conveyor 18. The conveyor will in turn, 
feed the paper to a print mechanism 20, the particular construction of 
which will be well known and within the understanding of one of ordinary 
skill in the art. Also illustrated in the figure is an inverter mechanism 
30 that may selectively invert or flip paper that progresses along 
conveyor 18. A feedback-unit 32 is provided for returning the paper to the 
printer mechanism 20 for duplex printing thereof. 
In the illustration, the conveyor 18 provides a path to a stapling 
mechanism 34 for selectively stapling of printed documents. The final, 
illustrated system represent a plurality of output bins designated by bins 
38 and 40. 
Turning to the data processor unit C, included therein is a data 
input/output ("I/O") unit 40 which is in data communication with a central 
processor unit ("CPU") storage scheduling unit 42. A data path is provided 
between the data I/O unit 40 and each of the systems. 
In the preferred embodiment, each system B includes therein a description 
associated with various functions and capabilities thereof. The data path 
between each of the illustrated systems and the data I/O unit allows for 
acquisition to the data processor unit C of all such descriptions. Data 
interconnections between the data I/O unit 40 of the data processor C and 
various systems B also allow for controller activation thereof. 
FIG. 1 has been provided to show at least some of the systems which operate 
in concert to form print engine A. Various ones of these systems are 
electro-mechanical systems having a plurality of component parts. To now 
discuss the subject invention in greater detail, a paper supply system 46 
is shown in FIG. 2, which includes among other components, tray 10, and 
feeder 16 of FIG. 1. Paper supply system 46 includes tray 10 having a flat 
surface on which stacks of paper 52 are placed. Tray 10 can be moved in a 
vertical direction by a constant velocity motor assembly 54. Some distance 
above tray 10 is switch (for paper) 56 and switch (for empty) 58. Switches 
56 and 58 are mechanical switches, which are turned on if pushed up 
physically, for example by the stack of paper. There is a hole in the 
paper tray directly below switch 58. The switches are intended to be 
aligned, however, it is understood that some misalignment is possible and, 
therefore, as discussed later such misalignment is taken into 
consideration by the subject invention. When the paper hits either switch, 
that switch is turned on. Note that if there is no paper in the tray, 
switch 58 is not turned on, because of the hole in the tray. Feeder 16 is 
positioned at a position where, upon proper operation of paper supply 
system 46, paper 54 in tray 10 can be obtained by feeder 16 for further 
processing by other systems of print engine A. 
With the above description of the individual components having been given, 
the paper supply system 46 generally operates as follows: upon a power-up 
situation (wherein the tray may not contain any paper), motor 54 begins 
operation moving the tray 10 in a vertical direction. Assuming there is 
paper in the tray, the switches 56 and 58 are turned on when the paper 
hits them. This indicates that paper 52 is in the tray 10 (switch 58) and 
that the paper is at an appropriate height (switches 56 and 58) such that 
feeder 16 can receive a sheet of the paper 52. It is to be appreciated 
that the motor in this example is powered-up under a timer sequence, such 
that if switch 56 and switch 58 do not sense a change within a certain 
time period, the motor is timed-out and, turned off. This feature is to 
protect switches 56 and 58 should there be a malfunction in the sensors 
and/or motor. 
It is to be appreciated that the above description provides a general 
explanation of the operation of paper supply system 46 and other operation 
characteristics exist as will be expanded upon in the following 
description. 
Initially, automatic construction of the digital controllers/device drivers 
according to the subject invention is achieved in a manner described by 
the flow chart of FIG. 3. Particularly, the components (i.e. sensors, 
motor, tray, paper-feeder, etc.) in the electro-mechanical system are 
identified 60. Next, the dynamic behavior of the system is modeled using a 
set of qualitative and quantitative constraints 62. The dynamic modeling 
of the system includes modeling the components of the system. The modeled 
dynamic behavior is then used to construct a configuration space for the 
system using a compilation algorithm 64. In this description, a 
configuration space is a set of states each of which represents a possible 
configuration of the system. For example, in the paper supply system 46, 
one configuration of the system would have motor 54 at its bottom position 
and tray 10 sitting at its minimal height. In this configuration, switches 
56 and 58 are in an OFF state and feeder 16 is also OFF. Another 
configuration would be that the motor 54 is ON and has raised tray 10 up 
to a height such that switch 56 is tripped into an ON state. There are 
numerous types of configurations as well as transitions between such 
configurations. The sum of these configurations and transitions represent 
the configuration space. A configuration space is used to determine what 
states are reachable from an initial state, and under which of the 
transitions. Essentially, the configuration space is a finite state 
machine providing a succinct representation of all possible evolutions of 
the system. 
With continuing reference to FIG. 3, upon generation of a configuration 
space, the transitions existing within such space are labeled as external 
or internal transitions 66. Internal transitions will take place due to 
the occurrence of an event which is under the control of the controller. 
On the other hand, external transitions occur due to events which are 
beyond the control of the system, but whose occurrence affects the 
operation of the system. 
Thereafter, a "desired state" or "goal condition" of the system is 
identified 68. It is to be appreciated that the desired state can change 
over time, depending on the past history of interactions between the 
controlled system and its environment. Whereas, the desired state is the 
ultimate state of the system which is to be reached, "undesirable states" 
of a system are those configurations into which the system should not 
enter (e.g. a configuration which results in the damage of switches 56 
and/or 58). Using the constructed configuration space, the labeled 
transitions, the identified desired state and identified undesirable 
states, a program is generated 69. The generated program drives the system 
from any state towards the desired state, avoiding the undesirable states. 
It is to be appreciated that various ones of the transitions will be 
dependent upon external variables (e.g. sensors turning ON and OFF, etc.), 
and some based on changes of internal variables (e.g. motor turning ON and 
OFF, etc.), and other transitions based on time-outs whose value is 
computed by the controller generator. Following the flow chart described 
in FIG. 3, digital controller/device drivers for electro-mechanical 
systems can be automatically constructed. 
The above method combines concepts of qualitative reasoning for physical 
systems with techniques for automatic generation of code from finite state 
machine (FSM) descriptions. 
As noted above, the method starts from a description of the components 
(e.g. motor, tray, switches, feeder and paper) and their interaction paths 
(i.e. transitions). By using qualitative envisionment of system 46, 
identification of crucial states of the system and transitions between the 
states are identified. The concepts of qualitative envisionment has been 
described for example in the document Qualitative Reasoning About Physical 
Systems, by Johan de Kleer and John Seely Brown, see Qualitative Physics 
Based on Confluences, MIT Press, 1985. Also published in AIJ, 1984. 
Qualitative envisionment is commonly understood as the exploration of all 
potential behaviors of a system by, for example, repeatedly and in various 
ways exercising simulation or partial evaluation of its models. The 
resulting component behavior is comprised of an output produced by a 
particular behavior, inputs from which the output is produced, individual 
operations required to produce it (its "itinerary"), as well as various 
constraints on resources and timings to be observed when performing the 
operations. Some or all of this information may advantageously be 
precompiled. By way of example, this information may be compiled to finite 
state machine or configuration space described above. 
In connection with FIG. 2, constraints of paper supply system 46 include 
that when sensors 56' and 58' are OFF, motor 54 causes paper tray 50 to 
rise in a vertical direction, and when both switches 56 and 58 are changed 
to an ON state, motor 54 will turn off. Other constraints include, timing 
constraints where after a certain time period without any change, the 
motor turns off. Still a further constraint acknowledges that sensors 56' 
and 58' may be at different heights. So even if the sensor of switch 58 
(empty) is moved to an ON state, indicating the existence of paper in 
paper tray 10, the sensor of switch 56 (paper) may not be at the same 
height location. Therefore, a constraint condition needs to exist to 
compensate for height differences between sensors 56' and 58'. 
In view of the above, it is necessary to develop a set of constraints which 
capture the different operations, errors, etc. of system 46. 
FIG. 4 provides a representation of this physical scenario in Hybrid cc 
syntax. A discussion concerning the Hybrid cc language is set forth in the 
following section of this paper under the heading, Programming in hybrid 
constraint languages. 
In Hybrid cc, intuitively, "," separates agents that are run in parallel, 
if c then A describes an agent that reduces to A if the constraint c holds 
in a current state, if c else A describes an agent that reduces to A if c 
will not be entailed in the current time instant, hence A executes a copy 
of A at every real time point after the current one, while always A 
executes a copy of A. The term do A watching c executes A until it sees a 
c, then A is immediately ended. 
It is to be appreciated that while the present embodiment has used Hybrid 
cc language to represent the above physical scenario other languages may 
also be used. 
The last four lines of FIG. 4 sets forth the desired state or goal 
condition 70a of system 46. The control statement 70b states that control 
of the motor (motor ON/motor OFF) are internal actions which can be 
controlled by the controller generated in the subject example. The desired 
state is when the feeder is equal to ON 70c, and an example of an 
undesirable state is one which would result in the breaking of switches 
70d. 
The system representation in FIG. 4 can be compiled into a configuration 
space using a compilation algorithm such as one described in the following 
section of this paper under the heading, Computing with continuous change. 
This compilation algorithm produces the set of configurations of the 
system, and the transitions between them. The finite state machine thus 
produced is a succinct representation of all possible evolutions of the 
system. 
From the above description of FIG. 4 and having looked at the goal 
condition, each of the transitions between the configurations may be 
labeled as being caused by internal events or external events. It is 
further determined that some of the events will result in a "good" 
configuration which is desirable and which the system should be forced to 
reach, and some of the events are determined to cause "bad" configurations 
which are to be avoided (such as switches 56, 58 breaking). 
To avoid the bad configurations, the system is forced to take a step such 
as switching the motor off after a certain time period (i.e. move to a 
state to avoid a bad configuration). Therefore, labeling each of the 
transitions will indicate internal events which the controller can control 
(i.e. switching motor ON/OFF) and external events, which are beyond 
control of the controller. After having labeled the transitions as being 
internal or external, the goal condition 70a is reviewed and it is 
determined that configurations in which the goal condition is true are 
"good" configurations. All the information necessary regarding the goal 
condition and the "good" or "bad" configurations is determined from the 
information in the configuration space. 
From the input model and prescribed goal condition of FIG. 4 an 
automaton/controller 80 of the form in FIG. 5 is produced. From this 
controller 80 it is shown that switches 56 and 58 are controlled 
externally 82, while the signals motor (on) 84, motor (off) 86, are 
generated by the controller 80. The values of the time-outs 88 are 
generated from the physical description of the code generation process. 
The controller 80 is activated in a START state, which switches the motor 
ON. When one of the switches is tripped, the controller goes into a 
wait.sub.-- for.sub.-- P 90 or wait.sub.-- for.sub.-- E state 92, 
depending on which switch has been tripped. When the other switch is 
tripped, the feeder can be switched on until the paper level drops and one 
or both switches 56, 58 re-enter a state of 0. This is repeated until the 
paper tray 10 is empty, then switch 58 does not trip, and a time-out 
ensures that a message is sent to refill the paper. The other time-outs in 
the automaton controller 80 ensure that the motor does not run for an 
extended period of time which would cause the breaking of switches 56' and 
58'. 
Based on this automaton generated from the configuration space in FIG. 4, a 
separate, uniform compilation algorithm generates controller control code 
94 as set forth in FIG. 6. The control code of the controller is used to 
force the operation represented by the automaton controller along a path. 
This control code is generated automatically from the configuration space 
description. 
In many systems the state of the system is not known unambiguously, in such 
situations controller 80 is constructed so that at least some of its 
actions are directed to identifying the current state or otherwise reduce 
ambiguity, by moving to a known state. 
In addition to the assumed correct function of the individual components, 
in another embodiment, knowledge is also incorporated regarding potential 
failure modes, for example, considering one possible fault in the system 
at a time. 
It is also known that not all states can be sensed, so the system in yet 
another embodiment is implemented with some inference capabilities to 
determine whether the system is broken and, if so, what component may be 
at fault. Implementation of such an embodiment uses an extended 
description allowing an elaboration of the finite state machine to provide 
diagnostic information for possible failures. 
The concepts of Hybrid cc constraint programming are more particularly set 
forth in the following sections entitled, Programming in hybrid constraint 
languages and Computing with Continuous Change. 
Programming in hybrid constraint languages 
1 Introduction and Motivation 
The constant marketplace demand of ever greater functionality at ever lower 
price is forcing the artifacts of our industrial society designs to become 
ever more complex. Before the advent of silicon, this complexity would 
have been unmanageable. Now, the economics and power of digital 
computation make it the medium of choice for gluing together and 
controlling complex systems composed of electro-mechanical and 
computationally realized elements. 
As a result, the construction of the software to implement, monitor, 
control and diagnose such systems has become a gargantuan, nearly 
impossible, task. For instance, traditional product development methods 
for reprographics systems (photo-copiers, printers) involve hundreds of 
systems engineers, mechanical designers, electrical, hardware and software 
engineers, working over tens of months through several hard-prototyping 
cycles. Software for controlling such systems is produced by 
hand--separate analyses are performed by the software, hardware and 
systems engineers, with substantial time being spent in group meetings and 
discussions coordinating different design decisions and changes, and 
assessing the impact these decisions will have on the several teams 
involved. Few, if any, automated tools are available to help in the 
production of documentation (principles of operation, module/system 
operating descriptions), or in the analysis and design of the product 
itself. A different team--often starting from little else than the product 
in a box, with little "documentation"--produces paper and computational 
systems to help field-service representatives diagnose and fix such 
products in the field. 
Such work practices are unable to deal with the increasing demand for 
faster time to market, and for flexibility in product lines. Instead of 
producing one product, it is now necessary to produce a family of 
"plug-and-play" generic components--finishers (stackers, staplers, 
mailboxes), scanners, FAX modules, imaging systems, paper-trays, 
high-capacity feeders--that may come together for the very first time at 
customer-site. The software for controlling such systems must be produced 
in such a way that it can work even if the configuration to be controlled 
is known only at run-time. 
To address some of these problems, we are investigating the application of 
model-based computing techniques. The central idea is to develop 
compositional, declarative models of the various components of a 
photo-copier product family, at different levels of granularity, 
customized for different tasks. For instance, a marker is viewed as a 
transducer that takes in (timed) streams of sheets S and video images V, 
to produce (timed) streams of prints P. A model for the marker, from the 
viewpoint of the scheduler, is a set of constraints that capture precisely 
the triples (S,V,P) which are in fact physically realizable on this 
marker. The marker model is itself constructed from models for nips, 
rollers, motors, belts, paper baffles, solenoids, control gates etc.; the 
models are hooked together in exactly the same way as the corresponding 
physical components are linked together. Together with this, software 
architectures are developed for the tasks that need to be accomplished 
(such as scheduling, simulation, machine control, diagnostic tree 
generation). Finally, linking the two are special-purpose reasoners 
(operating at "configuration-time") that produce information of the right 
kind for the given task architecture, given the component models and 
system configurations. 
We expect this approach to be useful for a variety of tasks: 
Scheduling. A model of the system specifies what outputs will be produced 
given (perhaps continuous) input and control commands. In principle, the 
same model can be used to search the space of inputs and control commands, 
given a description of system output. In practice, the design of such an 
inference engine is made complex by the inherent combinatorial complexity 
of the search process. With a formal model in hand, it becomes possible to 
use automated techniques to better understand the search-space and design 
special-purpose reasoners. This approach is currently being deployed, in 
collaboration with several other teams, in the development of schedulers 
for a new generation of products from Xerox Corporation. 
Code Generation. A physical model of a system can be used for 
envisionments--studying the possible paths of evolution of the system. 
Since some of the parameters of a system can be controlled, it becomes 
possible to develop automatically controllers which would specify these 
parameters leading the system to a desirable state, and away from paths 
which lead to unsafe states. 
Diagnostic-tree generation. Given a model of components, their 
interconnection, and their correct (and possibly faulty) behavior--perhaps 
with other information such as prior probabilities for failure--it is 
possible to construct off-line repair-action procedures. These can be used 
by service technicians as guides in making probes to determine root cause 
for the manifest symptom. 
Explanation. Given a simulation-based model, it is possible to annotate 
behavioral rules with text in such a way that the text can be 
systematically composed to provide natural-language explanations for why 
an observable parameter does or does not have a particular value. 
Productivity Analysis. Models may be analyzed to determine how 
corresponding product designs will perform on different job mixes (e.g., a 
sequence of all single-sided black & white jobs, followed by all 
double-sided, color, stapled jobs). 
The model-based computing approach places a set of requirements on the 
nature of the modeling language. We motivate these demands by considering 
a concrete example--the paper path of a simple photocopy as illustrated in 
FIG. 7. 
EXAMPLE 1 
Paper Transportation in a Photocopier 
In the photocopier of FIG. 7, paper is loaded in a paper tray at the left 
of the machine. When a signal is received, the acquisition roll (Acq Roll) 
is lowered onto the paper and pulls the top sheet of paper towards the 
first set of rollers (R1). After the paper is grasped by the first set of 
rollers, the acquisition roll (Acq Roll) is lifted, and the rollers 
(R2,R4) pull the paper forward, till it reaches the registration clutch 
(R3). This starts at a precise moment for prefect alignment with the toner 
image on the belt. The toner is transferred electrostatically onto the 
paper by the image transfer mechanism. The vacuum belt (5) transports it 
to the fuser roll (R6) which fuses the toner into the paper, and from 
there it exists. 
Hybrid modeling 
The photocopier of FIG. 7 has a collection of components with continuous 
behavior, for example, the rollers and belts. The control program of the 
photocopier is a discrete event driven system. Therefore, the modeling 
language should be able to describe the interaction of the control program 
and the continuous components--thus, the modeling language has to fall in 
the framework of hybrid systems. 
Executability 
Given a model of the system, it should be possible to predict the behavior 
of the system when inputs are supplied. Thus, the model should be 
executable, i.e. it should also be possible to view models as programs. 
This would allow hybrid control programs to be written using the same 
notation as component models. If sensors and actuators coupling the 
language implementation with the physical environment are provided then, 
in fact, it should be possible to use programs in this notation to drive 
physical mechanisms. 
Compositional modeling 
Out of consideration of reuse, it seems clear that models of composite 
systems should be built up from models of the components, and that models 
of components should reflect their physics, without reflecting any 
pre-compiled knowledge of the structure (configurations) in which they 
will be used (the "no function in structure principle"). Concretely, this 
implies that the modeling language must be expressive enough to modularly 
describe and support extant control architectures and techniques for 
compositional design of hybrid systems. From a programming language 
standpoint, these modularity concerns are addressed by the analysis 
underlying synchronous programming language, (adapted to dense discrete 
domains); this analysis leads to the following demands on the modeling 
language. 
The modeling should support the interconnection of different components, 
and allow for the hiding of these interconnections. For example, the model 
of the copier is the composition of the control program and the model of 
the paper path. The model of the paper path in turn, is the composition of 
the models of the rollers, clutches, etc. 
Furthermore, in the photocopier example, if paper jams, the control program 
should cause the rollers to stop. However, the model of the rollers, in 
isolation, does not need to have any knowledge of potential error 
conditions. Thus, the modeling language should support orthogonal 
preemption--any signal can cause preemption. 
Finally, the language should allow the expression of multiple notions of 
logical time--for example, in the photocopier the notice of time relevant 
to the paper tray is (occurrences of) the event of removing paper from the 
tray; the notion of time relevant to the acquisition roll is determined by 
the rotation rate of the roller; the notion of time of the image transfer 
mechanism is the duration of the action of transferring images etc. 
Thus, we demand that the modeling language be an algebra of processes, that 
includes concurrency, hiding, preemption and multiform time. 
Declarative view 
It must be possible for systems engineers--people quite different in 
training and background from software engineers--to use such a formalism. 
Typically, systems engineers understand the physics of the system being 
designed or analyzed, and are used to mathematical or constraint-based 
formalisms (equational and algebraic models, transfer functions, 
differential equations) for expressing that knowledge. This suggests that 
it must be possible to view a model (fragment) expressed in the language 
as a declaration of facts in a (real-time) (temporal) logic. 
Reasoning 
Given a model of the paper-path, and the control procedures governing it, 
it should be possible to perform a tolerance analysis--establish the 
windows on an early/late arrival of sheets of papers at various sensors on 
the paper-path, given that a particular physical component may exhibit any 
behavior within a specified tolerance. This, and other such engineering 
tasks, suggest that the modeling language must be amenable to (adapting) 
the methodology developed in the extensive research on reasoning about 
hybrid and real-time systems--for example, specification and verification 
of properties of hybrid systems, qualitative reasoning about physical 
systems, and envisionment of qualitative states. 
1.1 This discussion 
This discussion describes programming in the modeling language, Hybrid 
cc--hybrid concurrent constraint programming. Intuitively, Hybrid cc is 
obtained by "freely extending" an untimed non-monotonic language Default 
cc over continuous time. Hybrid cc has the following key features: 
The notion of a continuous constraint system describes the continuous 
evolution of system trajectories. 
Hybrid constraint languages--developed generically over continuous 
constraint systems are obtained by adding a single temporal construct, 
called hence. Intuitively, a formula hence A is read as asserting that A 
holds continuously beyond the current instant. 
Continuous variants of preemption-based control constructs and multiform 
timing constructs are definable in Hybrid cc. 
The formula foundations of Hybrid cc are discussed in the following 
discussion computing with continous change. 
The rest of this discussion is organized as follows. First, we describe the 
computational intuitions underlying Hybrid cc. We follow with a brief 
description of an interpreter for a language in the Hybrid cc framework. 
We then describe a series of examples, and show traces of the execution of 
the interpreter. These examples illustrate the programming idioms and 
expressiveness of Hybrid cc. 
2 Hybrid cc: Computational Intuitions 
2.1 Background 
Concurrent Constraint Programming 
As mentioned in the previous section, some of the crucial characteristics 
in a hybrid programming language are easy specification and composition of 
model fragments. This led us to consider Concurrent Constraint Programming 
languages as a starting point, since these languages are built on top of 
constraint systems, which can be made as expressive as desired, and they 
have very fine-grained concurrency, so compositionality is achieved 
without effort. Recently, several concrete general-purpose programming 
languages have been implemented in this paradigm. 
Concurrent Constraint Programming (cc) languages are declarative concurrent 
languages, where each construct is a logical formula. cc replaces the 
traditional notion of a store as a valuation of variables with the notion 
of a store as a constraint on the possible values of variables. Thus the 
store consists of pieces of information which restrict the possible values 
of the variables. A cc program consists of a set of agents (we use the 
words agent and program interchangeably in this paper, usually referring 
to fragments of a program as agents) running concurrently and interacting 
with the shared store. Agents are of two basic kinds--tell agents which 
add information to the store (written a) and ask agents, or conditionals 
(written if a then A), which query the store about the validity of some 
information, and reduce to other agents if it is valid. (There are also 
hiding agents new X in A which hide any information about X from everyone 
else, these are needed for modularity.) This yields the grammar: 
EQU A::=a.vertline.if a then A.vertline.new X in A.vertline.A,A 
Computation is monotonic--information can only be added to the store. Ask 
actions are used for synchronization--if a query is answered positively, 
then the agent can proceed, otherwise it waits (possibly forever) till 
there is enough information in the store to entail the information in the 
query. When no more computation is being performed (a state of quiescence 
is reached), the store is output. 
The information that is added to the store consists of constraints which 
are drawn from a constraint system. Formally, a constraint system C is a 
system of partial information, consisting of a set of primitive 
constraints or tokens (Tokens are denoted by a, b, . . . in this 
discussion) D with minimal first order structure--variables and 
existential quantification. Associated with a constraint system is an 
entailment relation (denoted .perp-right..sub.c) which specifies when a 
token a can be deduced from some others b.sub.a, . . . b.sub.n, denoted by 
b.sub.a, . . . b.sub.n .perp-right.ca. Examples of such systems are the 
system herbrand, underlying logic programming--here tokens are equalities 
over terms which are finite trees with variables ranging over trees--and 
FD or finite domains, its tokens are equalities of variables and 
expressions saying that the range of a variable is some finite set. 
A salient aspect of the cc computation model is that agents may be thought 
of as imposing constraints on the evolution of the system. The agent a 
imposes the constraint a. (A,B) imposes the constraints of both A and 
B-logically, this is the conjunction of A and B. new X in A imposes the 
constraints of A, but hides the variable X from the other 
agents--logically, this can be thought of as a form of existential 
quantification. The agent if a then A imposes the constraints of A 
provided that the rest of the system imposes the constraints a--logically, 
this can be thought of as intuitionist implication. 
This declarative way of looking at programs is complemented by an 
operational view. The basic idea in the operational view is that of a 
network of agents interacting with a shared store of primitive 
constraints. The agent a is viewed as adding a to the store 
instantaneously. (A,B) behaves like the simultaneous execution of both A 
and B. new X in A starts A but creates a new local variable X, so no 
information can be communicated on it outside. The agent if a then A 
behaves like A if the current store entails a. 
The main difficultly in using cc languages in modeling is that the cc 
programs can detect only the presence of information, not its absence. 
However, in reactive systems, it is important to handle information saying 
that a certain event did not occur--examples are timeouts in UNIX or the 
presence of jams in photocopier (usually inferred by the paper not 
reaching a point by some specified time). The problem in assuming the 
absence of information (called negative information) during a computation 
is that it may be invalidated later when someone else adds that 
information, leading to invalidation of the subsequent computation. 
Our first attempt at fixing this problem was the addition of a sequence of 
phases of execution to the cc paradigm. At each phase we executed a cc 
program, and this gave the output for the phase, and also produced the 
agents to be executed in subsequent phases. At the end of each phase we 
detected the absence of information, and used it in the next phase, giving 
us a reactive reprogramming language, tcc. Each phase was denoted by a 
time tick, so we had a discrete model of time. 
Default cc. The addition of time to cc however still left us with a 
problem--how can we detect negative information instantaneously? This is 
necessary because in some applications we found that it was not acceptable 
to wait until the next phase to utilize negative information. 
Since the negative information is to be detected in the same time step, it 
must be done at the level of the untimed language, cc. However, the cc 
paradigm is inherently opposed to instantaneous negative information 
detection. Thus in order to allow negative information to be detected 
within the same computation cycle, we have to modify cc--we have to use 
Default cc. The basic idea behind Default cc is--if the final output of a 
computation is known, then any negative information can be obtained from 
this output, and this negative information can never be invalidated, as 
the final output has all the information ever added. So a Default cc 
program executes like a cc program, except that before the beginning of 
the execution, it guesses the output store. All negative information 
requests are resolved with respect to this guess, other than the Default 
cc program adds information to the store and queries the store for 
positive information just like a cc program. At the end of the 
computation, if the store is equal to the guess, then the guess was 
correct, and this is a valid answer. Otherwise, this branch of execution 
is terminated (or we can do backtracking). In an actual implementation, 
this backtracking is done at compile time, so at runtime we have to do a 
simple table look-up. 
The Default cc paradigm augments the cc paradigm with the ability to detect 
negative information, so the only new syntax we need to add to the cc 
syntax is the negative ask combinator if a else A, this reduces to A if 
the guessed output e does not imply a. Thus the Default cc syntax is given 
by the grammar 
EQU A::=a.vertline.if a then A.vertline.A,A.vertline.new X in A.vertline.if a 
else A 
The agent if a else A imposes the constraints of A unless the rest of the 
system imposes the constraint a--logically, this can be thought of as a 
default. Note that if a else A is quite distinct from the agent 
if.fwdarw.a then A (assuming that the constraint system is closed under 
negation). The former will reduce to A if the final store does not entail 
a; the latter will reduce to A if the final store entails.fwdarw.a. The 
difference arises because, by their very nature, stores can contain 
partial information; they may not be strong enough to entail either a 
or.fwdarw.a. (In the time contexts discussed below, the subtlety of the 
non-monotonic behavior of programs--intimately related to the casualty 
issues in synchronous programming languages--arises from this combinator.) 
To see this, note that A may itself cause further information to be added 
to the store at the current time instant; and indeed, several other agents 
may simultaneously be active and adding more information to the store. 
Therefore requiring that information a be absent amounts to making a 
demand on "stability" of negative information. 
Thus we now have a language that permits instantaneous negative information 
detection. This enables us to write strong timeouts--if a signal is not 
produced at a certain time, the execution of the program can be terminated 
at that very time, not at some later time as we did for timed cc. Now in 
order to get a language for modeling discrete reactive systems, we again 
introduce phases in each of which a Default cc program executes. To extend 
Default cc across time, we need just one more construct, hence A, which 
starts a copy of A in each phase after the current one. We extend Default 
cc across real time to get a language for hybrid reactive systems in the 
next subsection. 
2.2 Continuous evolution over time 
We follow a similar intuition in developing Hybrid cc: the continuous timed 
language is obtained by uniformly extending Default cc across real 
(continuous) time. This is accomplished by two technical developments. 
Continuous Constraint Systems 
First, we enrich the underlying notion of constraint system to make it 
possible to describe the continuous evolution of state. Intuitively, we 
allow constraints expressing initial value (integration) problems, e.g. 
constraints of the form X=O.sub.1, hence dot(X)=1; from these we can infer 
at time that X=t. The technical innovation here is the presentation of a 
generic notion of continuous constraint system (ccs), which builds into 
the very general notion of constraint systems just the extra structure 
needed to enable the definition of continuous control constructs (without 
committing to a particular choice of vocabulary for constraints involving 
continuous time). As a result subsequent development is parametric on the 
underlying constraint language: for each choice of a ccs we get a hybrid 
programming language. Later we will give an example of a simple constraint 
system and the language built over it. 
Program Combinators 
Second we add to the untimed Default cc the same temporal control 
construct: hence A, but now interpreting it over real time. Declaratively, 
hence A imposes the constraints of A at every real time instant after the 
current one. Operationally, if hence is invoked at time t, a new copy of A 
is invoked at each instant in (t,oo). 
______________________________________ 
Agents Propositions 
______________________________________ 
a a holds now 
if a then A if a holds now, then A holds now 
if a else A if a will not hold now, then A holds 
now 
new X in A exists an instance At/X! that holds now 
A, B both A and B hold now 
hence A A holds at every instant after now 
______________________________________ 
Intuitively, hence might appear to be a very specialized construct, since 
it requires repetition of the same program at every subsequent time 
instant. However, hence can combine in very powerful ways with positive 
and negative ask operations to yield rich patterns of temporal evolution. 
The key idea is that negative asks allow the instantaneous preemption of a 
program--hence, a program hence if P else A will in fact not execute A at 
all of those time instants at which P is true. 
Let us consider some concrete examples. Suppose that we require that an 
agent A be executed at every time point beyond the current one until the 
time at which a is true. This can be expressed as new X in (hence (if X 
else A, if, a then always X)). Intuitively, at every time point beyond the 
current one, the condition X is checked. Unless it holds, A is executed. X 
is local--the only way it can be generated is by the other agent (if a 
then always X) which, in fact generates X continuously if it generates it 
at all. Thus, a copy of A is executed at each time point beyond the 
current one upto (and excluding) the time at which a is detected. 
Similarly, to execute A precisely at the first time instant (assuming there 
is one) at which a holds, execute: new X in hence (if X else if a then A, 
if a then hence X). 
In particular, the continuous version of the general preemption control 
construct clock is definable within Hybrid cc. The patterns of temporal 
behavior described above are obtainable as specializations of clock. 
Further, programs containing the clock combinator may be equationally 
rewritten into programs not containing the combinator. 
While conceptually simple to understand, hence A requires the execution of 
A at every subsequent real time instant. Such a powerful combinator may 
seem impossible to implement computationally. For example, it may be 
possible to express programs of the form new T in (T=0, hence dot(T)=1, 
hence if rational (T) then A) which require the execution of A at every 
rational q&gt;0. Such programs are not implementable. To make Hybrid cc 
computationally realizable, the basic intuition we exploit is that, in 
general, physical systems change slowly, with points of discontinuous 
change, followed by periods of continuous evolution. This is captured by a 
stability condition on continuous constraint systems that guarantees that 
for every constraint a and b there is a neighborhood around 0 in which a 
either entails or disentails b at every point. This rules out constraints 
such as rational (T) as inadmissible. 
With this restriction, computation in Hybrid cc may be thought of as 
progressing in alternating phases of computation at a time point, and in 
an open interval. Computation at the time point establishes the constraint 
in effect at that instant, and sets up the program to execute 
subsequently. Computation in the succeeding open interval determines the 
length of the interval r and the constraint whose continuous evolution 
over (O,r) describes the state of the system over (0,r). 
3 The Implementation 
We will now present a simple implementation for Hybrid cc built on top of a 
simple continuous constraint system. The interpreter is built on top of 
Prolog, and consideration has been given to simplicity rather than 
efficiency. We have already identified several ways in which performance 
can be significantly enhanced using standard logic programming techniques. 
3.1 The continuous constraint system 
Basic tokens are formulas d, hence d or prev (d), where d is either an 
atomic proposition p or an equation of the form dot(x,m)=r, for x a 
variable, m a non-negative integer and r a real number. Tokens consist of 
basic tokens closed under conjunction and existential quantification. Some 
rudimentary arithmetic can be done using the underlying prolog primitives. 
The inference relations are defined in the obvious way under the 
interpretation that p states that p is true and dot(x,m)=r states that the 
mth derivative of x is r.prev(d) asserts that d was true in the limit from 
the left, and hence d states that for all time t&gt;0 d holds. The inference 
relations are trivially decidable: the functions of time expressible are 
exactly the polynomials. The only non-trivial computation involved is that 
of finding the smallest non-negative root of univariate polynomials (this 
can be done using one of several numerical methods). 
3.2 The basic interpreter 
The interpreter simply implements the formal operational semantics 
discussed in detail in GJSB95!. It operates alternately in point and 
interval phases, passing information from one to the other as one phase 
ends. All discrete change takes place in the point state, which executes a 
simple Default cc program. In a continuous phase computation progresses 
only through the evolution of time. The interval state is exited as soon 
as the status of one of the conditionals changes--one which always fired 
does not fire anymore, or one starts firing. 
The interpreter takes a Hybrid cc program and starts in the point phase 
with time t=0. 
The point phase 
The input to the point phase is a set of Hybrid cc agents and a prev store, 
which carries information from the previous interval phase--the atomic 
propositions and the values of the variables at the right endpoint of the 
interval (initially at time 0 this is empty). The outputs are the store at 
the current instant, which is printed out and passed on to the next 
interval phase as the initial store, and the agent or the continuation, to 
be executed in the interval phase. 
The interpreter takes each agent one by one and processes it. It maintains 
the store as a pair of lists--the first list contains the atomic 
propositions that are known to be true at the point, and the second 
contains a list of variables and the information that is known about the 
values of their derivatives. It also maintains lists of suspended 
conditionals (if . . . then and if . . . else statements whose constraints 
are not yet known to be true or false) and a list of agents to be executed 
at the next interval phase. 
When a tell action (a constraint a) is seen, it is added to the store and a 
check for consistency is made. If the constraint is of the form 
dot(x,m)=r, then it means that all derivatives of x of order &lt;m are 
continuous, and thus their values are copies from the prev store. Any 
conditional agents that have been suspended on a are reactivated and 
placed in the pool of active agents. 
When any conditional agent appears, its constraint is immediately checked 
for validity. If this can be determined, the appropriate action is taken 
on the consequence of the agent--it is discarded or added to the pool of 
active agents. Otherwise it is added to an indexed list of suspended 
conditionals for future processing. A hence action is placed in the list 
of agents to be executed in the next interval. 
When no more active agents are left, the interpreter looks at the suspended 
agents of the form if a else A, the defaults. On successful termination, 
one of two conditions must hold for each such agent: either the final 
store entails a, or else the final store incorporates the effect of 
executing A. Thus all that the interpreter has to do is to 
non-deterministically choose one alternative for each such default. In the 
current implementation, this non-deterministic choice is implemented by 
backtracking, with execution in the current phase terminating with the 
first successful branch. 
The interval phase 
This is quite similar to the point phase, except that it also has to return 
the duration of the phase. The input is a set of agents and an initial 
store which determines the initial values for the differential equations 
true in the store. The output is a set of agents to be executed in the 
next point phase, a store giving the values of the variables at the end of 
the interval phase, and the length of the phase. Initially, we assume that 
the length will be infinite, this is trimmed down during the execution of 
the phase. 
A tell is processed as before--it is added to a similar store, and 
reactivates any suspended conditionals. Conditional agents are added to 
the suspended list if their conditions re not known to be valid or invalid 
yet, otherwise the consequence of the agent is added to the active pool or 
discarded. In addition, if the condition can be decided, then we compute 
the duration for which the status will hold. For example if we have 
dot(x,1)=3 in the store, and x=4 in the initial store, then we know that 
x=3t+4. Now if we ask if (x=10) then A, then we immediately know that this 
is not true in the current interval, so A can be discarded for now. 
However, we also know, by solving the equation 3t+4=10 that this status 
will hold for only 2 seconds, so this interval phase cannot be longer than 
two seconds. (This is where we need to solve the polynomial equations.) 
At the end of the processing, the defaults are processed as before, and are 
used to trim the length of the interval phase further. Also, the remaining 
suspended conditionals if a then . . . are checked to when a could first 
become valid, to reduce the duration of the phase if necessary. Finally a 
computation is done to find the store at the end of the interval, and this 
information is passed to the next point phase. Since all agents are of the 
form hence A in an interval phase, the agent to be executed at the next 
point phase must be A, hence A. 
If any interval phase has no agents to execute, the program terminates. 
3.3 Combinators 
This basic syntax of Hybrid cc has been quite enough for us to write all 
the programs that we have. However, we have noticed several recurrent 
patterns in our programs, and some of these can be written up as definable 
combinators, and make the job of programming considerably easier. Note 
that these are defined combinators, i.e. they are definable in terms of 
the basic combinators. Thus, these defined combinators are merely 
syntactic sugar, and can be compiled away into basic combinators. 
Always 
always A=A, hence A is read logically as .quadrature.A, the necessity 
modality. Parameter less recursion can be mimicked--replace a recursive 
process P::body by always if P then body. Parameters can be handled by 
textual substitution. 
Waiting for a condition 
whenever a do A reduces to A at the first time instant that a becomes 
true--if there is a well-defined notion of first occurrence of a. Note 
that there is no "first" occurrence of a in the situation when the a 
occurs in the interval (0,t), as happens in the agent hence a. In such 
cases, A will not be invoked. whenever can be defined in terms of the 
basic combinators as mentioned in the previous section. 
In the following discussion of definable combinators, and in the rest of 
this paper, we shall not repeat the caveat about the subtlety of the 
well-definedness of the "first" occurrences of events. 
Watchdogs 
do A watching a, read logically as "A until a", is the strong abortion 
interrupt of ESTEREL. The familiar cntrl-C is a construct in this vein. do 
A watching a behaves like A until the first time instant when a is 
entailed: when a is entailed A is killed instantaneously. It can be 
defined using the basic constructs as follows: 
##EQU1## 
Multiform time 
time A on a denotes a process whose notion of time is the occurrence of a-A 
evolves only the store entails a. It can be defined by structural 
induction as above. 
Implementation of the defined constructs 
The laws given above suffice to implement all these constructs in the 
interpreter. However, for the sake of efficiency, we have implemented the 
constructs directly, at the same level as basic constructs. The always 
construct is of course trivial, and has been implemented using the given 
rule. whenever is implemented similarly to an if a then A construct, 
except that if a is not entailed, then it is carried across to the next 
phase. It has no effect in an interval phase for the reason mentioned 
above. 
do A watching a is very similar to an if b else B, and is implemented 
analogously. The only thing to be noted here is that whenever something 
from the A is to be passed on to the next phase, it must be passed inside 
a do . . . watching a, so that the proper termination of all spawned 
agents can be achieved when a becomes true. time A on a is similar--it is 
like an if a then A, remembering the same rule about passing spawned 
agents through phases. 
4 Programming examples 
We illustrate the programming/model description style of Hybrid cc via a 
few examples. In each of these examples, we write each of the conceptually 
distinct components separately. We then exploit the expressive power of 
Hybrid cc to combine the subprograms (submodels) via appropriate 
combinators, to get the complete program/model. We also present the trace 
of the interpreter on some of these examples. 
4.1 Sawtooth function 
We start off with a simple example, the sawtooth function defined as 
f(y)=y-y!, where y! denotes the greatest integer in y. 
As mentioned above, prev(x=1.0) is read as asserting that the left limit of 
x equals 1. 
______________________________________ 
sawtooth:: 
x = 0, 
hence (if prev(x = 1.0) then x = 0), 
hence (if prev(x = 1.0) else dot(x) = 1)). 
______________________________________ 
The trace of this program as executed by our interpreter is seen below. The 
execution in the point and interval phases is displayed separately. For 
both phases of execution, the contents of the store are displayed. In 
addition, for the interval phase, the interval is also displayed, and the 
continuous variables are displayed as polynomials in time. In the 
interval, note that time is always measured from the beginning of the 
interval, not from 0. Also, this program has infinite output, so we 
aborted it after some time. 
Time=0 
Store contains dot (x,0)=0!. 
Time Interval is (0, 1.0) 
Store contains x=1*t+0! 
Time=1.0 
Store contains dot(x,0)=0!. 
Time Interval is (1.0, 2.0) 
Store contains x=1*t+0!. 
Time=2.0. 
Store contains dot(x,0)=0!. 
Time Interval is (2.0, 3.0) 
Store contains x=1*t+0!. 
Time=3.0. 
Store contains dot(x,0)=0!. 
Prolog interruption (h for help)? a {Execution aborted} 
.vertline.?- 
4.2 Temperature Controller 
We model a simple room heating system which consists of a furnace which 
supplies heat, and a controller which turns it on and off. The temperature 
of the furnace is denoted temp. The furnace is either on (modeled by the 
signal furnace.sub.-- on) or off (modeled by the signal furnace.sub.-- 
off). The actual switching is modeled by the signals switch.sub.-- on and 
switch.sub.-- off. When the furnace is on, the temperature rises at a 
given rate, HeatR. When the furnace is off, the temperature falls at a 
given rate, CoolR. The controller detects the temperature of the furnace, 
and switches the furnace on and off as the temperature reaches certain 
pre-specified thresholds; Cut.sub.-- out is the maximum temperature and 
Cut.sub.-- in is the minimum temperature. 
The heating of the furnace is modeled by the following program. The 
multiform time construct ensures that heating occurs only when the signal 
furnace.sub.-- on is present. 
furnace.sub.-- heat(HeatR)::time (always dot(temp)=HeatR) on furnace.sub.-- 
on. 
The cooling of the furnace is modeled by the following program. The 
multiform time construct ensures that heating occurs only when the signal 
furnace.sub.-- off is present. 
furnace.sub.-- cool(CoolR)::time (always dot(temp)=-CoolR) on 
furnace.sub.-- off. 
The furnace itself is the parallel composition of the heating and cooling 
programs. 
furnace (HeatR, CoolR)::furnace.sub.-- heat (HeatR), furnace.sub.-- cool 
(CoolR). 
The controller is modeled by the following program--at any instant, the 
program watches for the thresholds to be exceeded, and turns the 
appropriate switch on or off. 
______________________________________ 
controller(Cut.sub.-- out, Cut.sub.-- in):: 
always (if switch.sub.-- on then do (always furnace.sub.-- on) watching 
switch.sub.-- off, 
if switch.sub.-- off then do (always furnace.sub.-- off) watching 
switch.sub.-- on, 
if prev(temp = Cut.sub.-- out) then switch.sub.-- off, 
if prev(temp = Cut.sub.-- in) then switch.sub.-- on). 
______________________________________ 
The entire assembly is defined by the parallel composition of the furnace 
and the controller. 
controlled.sub.-- furnace (HeatR, CoolR, Cut.sub.-- out, Cut.sub.-- 
in)::(furnace (HeatR, CoolR), controller (Cut.sub.-- out, Cut.sub.-- in)). 
The trace of this program with parameters HeatR=2, CoolR=-0.5, Cut.sub.-- 
Out=30, Cut.sub.-- in=26 and initial conditions temp=26 and the signal 
switch.sub.-- on, as executed by our interpreter is seen below. 
Time=0. 
Store contains furnace.sub.-- on, switch.sub.-- on, dot(temp,1)=2.0, 
dot(temp,0)=26.0!. 
Time Interval is (0, 2.0) 
Store contains furnace.sub.-- on, temp=2.0*t+26.0!. 
Time=2.0. 
Store contains furnace.sub.-- off, switch.sub.-- off, dot(temp,1)=-0.5, 
dot(temp,0)=30.0!. 
Time Interval is (2.0, 10.0) 
Store contains furnace.sub.-- off, temp=-0.5*t+30.0!. 
Time=10.0. 
Store contains furnace.sub.-- on, switch.sub.-- on, dot(temp,1)=2.0, 
dot(temp,0)=26.0!. 
Time Interval is (10.0, 12.0) 
Store contains furnace.sub.-- on, temp=2.0*t+26.0!. 
Prolog interruption (h for help)? a 
{Execution aborted} 
4.3 Cat and Mouse 
Next, we consider the example of a cat chasing a mouse. A mouse starts at 
the origin, running at speed 10 meters/second for a hole 100 meters away. 
After it has traveled 50 meters, a cat is released, that runs at a speed 
20 meters/second after the mouse. The positions of the cat and the mouse 
are modeled by c and m respectively. The cat wins (modeled by the signal 
wincat) if it catches the mouse before the hole, and loses otherwise 
(modeled by the signal winmouse). 
The cat and the mouse are modeled quite simply. The positions of the cat 
and the mouse change according to the respective velocities. Note that 
there is no reference to the cat or the position of the hole in the mouse 
program; similarly for the cat program. This is essential for reuse of 
these models. 
mouse::M=0, always dot(M)=10. 
cat::C=0, always dot(C)=20. 
The entire system is given by the assembly of the components. The mouse 
wins if it reaches the hole m=100; the cat wins if c=100 and the mouse has 
not reached the hole. The combination 
EQU do (. . . ) watching prev (m=100), whenever m=100 do 
is used as an exception handler; it handles the case of the mouse reaching 
the hole. Similarly, the combination 
EQU do (. . . ) watching prev (c=100)), whenever prev (c=100) do 
is used as an exception handler; it handles the case of the cat reaching 
hole. The higher priority of do . . . watching prev (c=100) relative to do 
(. . . ) watching prev (m=100) is captured by lexical nesting--in this 
program the cat catches the mouse if both reach the hole simultaneously. 
______________________________________ 
system.sub.-- configuration :: 
do (do (mouse, 
whenever prev (m = 50) do cat) 
watching prev (m = 100, 
whenever prev (m = 100) do winmouse) 
watching prev (c = 100), 
whenever prev (c = 100) do wincat. 
______________________________________ 
A trace of this program as executed by the interpreter is given below: 
Time=0. 
Store contains dot(m,1)=10, dot(m,0)=0!. 
Time Interval is (0, 5.0) 
Store contains m=10*t+0!. 
Time=5.0. 
Store contains dot(m,1)=10, dot(m,0)=50.0, dot(c,1)-20, dot(c,0)=0!. 
Time Interval is (5.0, 10.0) 
Store contains c=20*t+0, m-10*t+50.0!. 
Time=10.0. 
Store contains wincat!. 
Termination after Time 10.0. 
Initial Conditions: wincat!. 
Store has !. 
yes 
The other alternative, i.e., the mouse wins if the cat and the mouse reach 
the hole simultaneously is captured by reversing the lexical nesting of do 
(. . . ) watching prev (m=100) and do (. . . ) watching prev (c=100). 
Concretely, the program is: 
______________________________________ 
system.sub.-- configuration :: 
do (do (mouse 
whenever prev(m = 60 do cat) 
watching prev(c = 100), 
whenever prev(c = 100) do wincat) 
watching prev(m = 100), 
whenever prev(m = 100) do winmouse. 
______________________________________ 
A trace of this program as executed by the interpreter is given below: 
Time=0. 
Store contains dot(m,1)=10,dot(m,0)=0!. 
Time Interval is (0, 5.0) 
Store contains m=10*t+0!. 
Time=5.0. 
Store contains {dot(m,1)=10,dot(m,0)=50.0,dot(c,1)=20, dot (c,0)=0!. 
Time Interval is (5.0) 10.0) 
Store contains c=20*t+0,m=10*+50.0!. 
Time=10.0. 
Store contains winmouse!. 
Termination after Time 10.0. 
Initial Conditions: winmouse!. 
Store has !. 
yes 
4.4 A simple game of Billiards 
We model a billiards (pool) table with several balls. The balls roll in a 
straight line till a collision with another ball or an edge occurs. When a 
collision occurs the velocity of the balls involved changes discretely. 
When a ball falls into a pocket, it disappears from the game. For 
simplicity, we assume that all balls have equal mass and radius (called 
R). We model only two ball collisions, and assume that there is no 
friction. 
Impulses, denoted I, are assumed to be vectors. Velocities, positions are 
assume to be pairs with an x-component and a y-component. 
The structure of the program is that each ball, each kind of collision, and 
the check for pocketing for each ball are modeled by programs. A ball is 
basically a record with fields for name, position and velocity. 
The agent ball maintains a given ball (Ball) with initial position 
(InitPos) and velocity (InitVel). The program is given here in a syntax 
that allows the declaration of procedures. The syntax p(X.sub.1, . . . 
,X.sub.n)::A is read as asserting that for all X.sub.1, . . . ,X.sub.n 
p(X.sub.1, . . . ,X.sub.n) is equivalent to A. As the game evolves, 
position changes according to velocity (dot(Ball.pos)=Ball.InitVel) and 
velocity changes according to the effect of collisions. A propositional 
constraint Change(Ball), shared between the collision and ball agents, 
communicates occurrences of changes in the velocity of the ball named 
Ball. The ball process is terminated when the ball is removed, e.g. it 
falls in a pocket--as before, the higher priority of do . . . watching 
pocketed(Ball) relative to do (. . . ) watching Change(Ball) is captured 
by lexical nesting. 
______________________________________ 
ball(Ball, InitPos, InitVel):: 
do (Ball.pos = InitPos, 
do hence Ball.vel = InitVel watching Change(Ball), 
whenever Change(Ball) do ball(Ball, Ball.pos, Ball.newvel) 
hence dot(Ball.pos) = Ball.vel) 
watching pocketed(Ball). 
______________________________________ 
The table is assumed to start at (0,0), with length xMax and breadth yMax. 
If a ball hits the edge, one velocity component is reversed in sign and 
the other component is unchanged. 
______________________________________ 
edge.sub.-- collision(B):: 
always (if (B.pos.xl = B.r) or (B.pos.x = xMax -- B.r) 
then (Change(B), B.newvel = (-- B.vel.x, B.vel.y)), 
if (B.pos.y = B.r) or (B.pos.y = yMax -- B.R.) 
then (Change(B), B.newvel = (B.vel.x, -- B.vel.y))). 
______________________________________ 
Ball-ball collisions involve solutions to the quadratic conservation of 
energy equation. "if .vertline.I.vertline.=0 else .vertline.I.vertline.&gt;0" 
chooses the correct solution, I.noteq.0. The solution I=0 makes the balls 
go through each other| We use distance(P1,P2) as short hand for the 
computation of the distance between the P1 and P2. 
##EQU2## 
A ball is pocketed if its center is within distance p from some pocket. 
pocket(Ball)::always if in-pocket(xMax, yMax, Ball.pos) then 
pocketed(Ball). 
in-pocket(xMax, yMax, P)::(distance(P, (0, 0))&lt;p or distance(P, (o, 
yMax))&lt;p or distance(P, (xMax, 0))&lt;p or distance(P, (xMax, yMax))&lt;p or 
distance(P, (xMax/2, 0))&lt;p or distance(P, (xMax/2, yMax))&lt;p). 
4.5 The Copier Paper Path 
We now present a larger example, which utilizes some of the programming 
ideas illustrated by the previous "toy" examples. We model the copier 
paper path that we mentioned in Section 1. As we discussed there, we will 
model each of the components of the paper path in Hybrid cc, and put them 
to produce a model for the entire paper path. This model and the 
underlying intuitions are discussed in detail in Vineet Gupta, Vijay 
Saraswat, and Peter Struss. A model of photocopier paper path. In 
Proceedings of the 2nd IJCAI Workshop on Engineering Problems for 
Qualitative Reasoning, August, 1995--here we present an overview. 
The constraint system we use for this model is richer than the constraint 
system described before--besides simple propositions and first-order 
formulas on them, we can asset arithmetic inequalities between variables, 
their derivatives and real constants. We will also allow the expression of 
attribute-value lists--given a list L we can use L.a to refer to the value 
of a in the list L, if it exists. La=r,b=s, . . . ! adds the attributes 
a,b, . . . to L with value r,s, . . . 
The Intuitions 
Our basic idea is to construct models for each of the individual components 
of the paperpath--the rollers and belts etc. We will also build a model 
for the sheets of paper going through the paperpath. In addition, we need 
to model the local interaction between a sheet of paper and a 
transportation element, i.e. a belt or a roller. 
This interaction results in the transportation elements applying forces to 
the sheet, and the sheet then transmits these forces and moves under their 
influence. The local interactions will naturally induce a partition of the 
sheet into segments, which we view as individual entities, analyzing their 
freebody diagrams. 
We make a number of modeling assumptions to simplify our model. For 
example, we do not model the acceleration of the sheet of paper, instead 
we view its velocity as changing discretely when a change takes place in 
the influences on it. We also assume that the sheet is homogeneous, the 
paperpath is straight, and some other things, these are discussed in 
detail in Vineet Gupta, Vijay Saraswat, and Peter Struss, a model of 
photocopier paper path, Proceedings of the 2nd IJCAI Workshop on 
Engineering Problems for Qualitative Reasoning, August, 1995. 
The Model 
The paperpath is modeled as a segment of the real line, and each component 
occupies a segment of the real line. All forces and velocities are 
oriented with respect to the paperpath. The first model fragment describes 
a basic transportation element--this can be further specialized into 
models for different types of belts and rollers. The properties and 
initial state of the element are specified using an attribute-value list 
Init. Each element has a nominal velocity V.sub.nom, which is the velocity 
along the paperpath supplied by the motor. It also has an actual velocity 
V.sub.act, which may be differ from the nominal velocity, as a sheet of 
paper may be pulling or pushing the element. The force exerted on the 
transportation element is denoted F.sub.act, and the force exerted by the 
motor is denoted F.sub.resist. The freebody equation relates these two. 
F.sub.resist is bounded by F.sub.fast and F.sub.slow. The remaining 
constraints show the relation between the forces and the velocities--they 
assert that if the element is going faster than the nominal velocity 
V.sub.nom, then the force F.sub.act, must be at its maximum value and 
similarly for the minimum value. 
transportationElement(T, Init)::always(transport(T), 
T.Loc=Init.Loc, T.surfacetype=Init.surfacetype, 
T.F.sub.fast =Init.F.sub.fast, T.F.sub.slow =Init.F.sub.slow, 
T.F.sub.normal =Init.F.sub.normal, 
T.F.sub.act +T.F.sub.resist =0, 
-T.F.sub.fast .ltoreq.T.F.sub.resist .ltoreq.T.F..sub.slow, 
if T.V.sub.act &gt;T.V.sub.nom then T.F.sub.act =T.F.sub.fast, 
if T.V.sub.act &lt;T.V.sub.nom then T.F.sub.act =-T.F.sub.slow). 
This model is simply an enumeration of the constraints on the 
transportation element, these are always true. The value of V.sub.nom is 
not set here, this is done during the specialization of this generic 
transportation element description into various particular kinds of 
elements. 
The next "component" of the paperpath is the sheet of paper that travels 
along it. This again has a number of properties, and also an initial 
location. Furthermore, the sheet is partitioned into various segments--the 
contactSegments are those portions of the sheet in contact with some 
transportation element. Between two contact segments is an 
internalSegment, whereas beyond the extreme contact segments are the 
TailSegments. In order to create these segments, we use the new operator 
forall X: CX!.AX!. This is simply a parallel composition of finitely 
many AX!'s, one for each X such that CX! is true. The declarative style 
of programming is particularly useful here--this way of asserting the 
existence of segments is much simpler than the dynamic creation and 
destruction of segments that would have to be done in an imperative 
program. 
______________________________________ 
sheet(S, Init):: 
S.Loc = Init.Loc, 
do always 
sheet(S), 
S.width = Init.width, S.length = Init.length, 
S.thickness = Init.thickness, S.elasticity = Init.elasticity, 
S.surfacetype = Init.surfacetype, S.strength = Init.strength, 
if .E-backward.I.(S.I.condition-tearing) then S.torn, 
forall T:transport(T). if (T.engaged, .vertline.T.Loc.andgate.S.Loc 
.vertline. &gt; 0) 
then contact(S, S.Loc.andgate.T.Loc), 
forall I:contact(S, I). contactSegment(S, I), 
forall I:contact(S, I). forall J:contact(S, J). 
if I &lt; J then if .E-backward.K.(contact(S, K), I &lt; K &lt; J) 
else internalSegment(S, (ub(I), 1b(J))), 
forall I:contact(S, I). if .E-backward.K.(contact(S, K), K &lt; I) 
else leftTailSegment(S, (1b(S.Loc), 1b(I))), 
forall I:contact(S, I). if .E-backward.K.(contact(S, K), I &lt; K) 
else rightTailSegment(S, (ub(I), ub(S.Loc))), 
dot(1b(S.Loc)) = S.vel.1b(S.Loc), 
dot(ub(S.Loc)) = S.vel.ub(S.Loc)) 
watching S.torn. 
______________________________________ 
For brevity, we omit the code for the segments of the sheet. The agent 
interact creates an interaction process sheetTransportation for each 
transportation element overlapping the sheet. The sheet transportation 
process models the interaction between the sheet and the transportation 
element. It asserts that the force exerted by the element on the sheet is 
equal and opposite to the force exerted by the sheet on the element. It 
gives the freebody equation for the contact segment, and then bounds the 
amount of force exerted by the transportation element by the amount of 
friction. Finally, the friction and the velocities are related. 
______________________________________ 
interact(S):: 
always forall T:transport(T). 
if(T.engaged, .vertline.T.Loc.andgate.S.Loc.vertline. &gt; 0) 
then sheetTransportation(S, T, T.Loc.andgate.S.Loc). 
sheetTransportation(S, T, I):: 
new F.sub.friction in 
(I = S.Loc.andgate.T.Loc, 
F.sub.friction = mu(S.surfacetype, T.surfacetype) .times. T.F.sub.normal, 
S.I.F.sub.te + T.F.sub.act = 0, 
S.(1b(I)).F.sub.left + S.(ub(I)).F.sub.right + S.I.F.sub.te = 0, 
.vertline.S.I.F.sub.te .vertline. .ltoreq. F.sub.friction, 
F.sub.friction,) &gt; T.V.sub.act then S.I.F.sub.te = 
if S.vel.(ub(I)) &lt; T.V.sub.act then S.I.F.sub.te = F.sub.friction). 
______________________________________ 
Finally we provide the model for the paperpath shown in FIG. 1. The various 
kinds of transportation elements are modeled first, followed by a typical 
sheet, then these are composed together to give the entire paperpath. 
There is one new combinator used here--wait T do A, which waits for T 
seconds before starting A. This can be expressed in terms of the basic 
combinators. A new sheet is placed at (0,21) every time a signal Sync is 
received from the scheduler. 
______________________________________ 
cvElement(R, Init):: 
transportationElement(R, Init), always (R, V.sub.nom = Init.V.sub.nom, 
R.engaged). 
roller(R, Init):: 
cvElement(R, InitsurfaceType = rubber, F.sub.fast = 1000, F.sub.slow = 
1000, 
F.sub.normal = 300!), 
- F.sub.fast) then R.broken.low v R.F.sub.act = 
clutchedRoller(R, Init):: 
cvElement(R, InitsurfaceType = rubber, F.sub.fast = 3, F.sub.slow = 
1000, 
F.sub.normal = 200!), 
if R.F.sub.act = R.F.sub.slow then R.broken. 
belt(R, Init):: 
cvElement(R, InitsurfaceType = steel, F.sub.fast = 10000, F.sub.slow = 
10000, 
F.sub.normal = 120!). 
fuserRoll(R, Init):: 
cvElement(R, InitsurfaceType = rubber, F.sub.fast = 1000, F.sub.slow = 
1000, 
F.sub.normal = 1000!). 
regClutch(R, Init):: 
transportationElement(R, Init), always R.engaged, 
always (if R.on then do always R.V.sub.nom = Init. V.sub.nom watching 
R.off, 
if R. off then do always R.V.sub.nom = 0 watching R.on). 
a4GlossySheet(S):: 
sheet(S, length = 21, width = 29.7, thickness = 0.015, elasticity = 
15, 
surfaceType = glossy, strength = 500, Loc = (0, 21)!). 
copierModel(Sync) :: new (R1, R2, R3, R4, R5, R6) in 
(roller(R1, (V.sub.nom = 30, Loc = (10, 10.5)!), 
roller(R2, V.sub.nom = 30, Loc = (30, 30.2)!), 
regclutch(R3, V.sub. nom = 30, Loc = (39.9, 40.1), surfaceType = 
rubber, 
F.sub.fast = 1000, F.sub.normal = 1000, F.sub.normal = 300!), 
clutchedRoller(R4, V.sub.nom = 0, Loc = (50, 50.1)!), 
belt(R5, V.sub.nom = 30, Loc = (55, 80)!), 
fuserRoll(R6, V.sub.nom = 35, Loc = (85, 86)!), 
always (f(rubber, glossy) = 0.8, f(steel, glossy) = 0.1), 
always if Sync then (new S in (a4GlossySheet(S), interact(S)), 
R3.off, wait .8 do R3.on)). 
______________________________________ 
The model can now be executed to simulate the photocopier. However, we 
would like to put to the various other uses mentioned in the introduction, 
by exploiting the fact that Hybrid tcc has a well-defined mathematical 
semantics. 
One simple use for our model would be to verify whether some properties are 
true of it. For example we might want to assert that sheets will never 
tear--always forall S:sheet(S). if S.torn then ERROR. Similarly, several 
other properties can be asserted, these can be now proved using various 
theorem-proving and model-checking techniques. We could also want to prove 
that successive sheets never overlap--this proof would give us a condition 
on how far apart the Sync signals must be. Similar techniques may be used 
for control code generation. The other applications mentioned in the 
introduction also make use of such formal models and their semantics. 
4.6 Qualitative simulation 
Abstract interpretation of Hybrid tcc programs might provide an alternate 
conceptual framework for the qualitative modeling approaches. 
Hybrid tcc can be used to model exactly systems with continuous and 
discrete change. For example, here is a model of a bathtub, with the tap 
on, and the drain unplugged. 
______________________________________ 
bathtub(Inflow, F, Capacity) :: new (netflow, outflow, amount) in 
constant(F), monotone(F), F(0) = 0, 
constant(Inflow), 
constant(Capacity), 
do always (netflow = outflow + Inflow, 
outflow = F(amount), 
dot(amount) = netflow) 
watching (amount = Capacity dot(amount &gt; 0). 
______________________________________ 
Here the first three lines assert that the three parameters do not vary 
with time, and that F is a monotone function in its argument, assuming the 
value 0 on input 0. 
Essentially with this information, QSIM produces a graph that shows that 
from the initial state there are only three possible (qualitative) states 
that the program can transit to (for any possible input values of Inflow, 
F, and Capacity): namely those in which the tub overflows, the tub 
equilibrates at a level below Capacity, and the tub equilibrates at 
capacity. To do this reasoning, QSIM employs knowledge about the behavior 
of continuously-varying functions. 
Since Hybrid tcc provides an exact description of the model, it should be 
possible to do an abstract interpretation of the program to get the 
qualitative reasoning of QSIM. This is useful in cases when a precise 
value for the inputs is not known, only a range is given. Abstract 
interpretation could also be useful in verification. For example, in the 
cat-and-mouse example, we may not know the exact velocities of the cat and 
the mouse, only a range of velocities. However it may still be possible to 
prove that the mouse always wins. The ability to run this program 
abstractly for all the possible values of the velocities provides an 
alternative way of verification of this property. 
5 Future work 
This paper presents a simple programming language for hybrid computing, 
extending the untimed computation model of Default cc uniformly over the 
reals. Conceptually, computation is performed at each real time point; 
however, the language is such that it can be compiled into finite 
automata. We have an interpreter for the language by directly extending 
the interpreter for Default cc, with an integrator for computing evolution 
of a set of variables subject to constraints involving differentiation. 
We demonstrate the expressiveness of the language through several 
programming examples, and show that the preemption-based control 
constructs of the (integer-time based) synchronous programming languages 
(such as "do . . . watching . . . ) extend smoothly to the hybrid setting. 
Much remains to be done. What are semantic foundations for higher-order 
hybrid programming, in which programs themselves are representable as 
data-objects? How should such a hybrid modeling methodology be combined 
with the program structuring ideas of object-oriented programming? What is 
the appropriate notion of types in such a setting? How do the frameworks 
for static analysis of programs (data- and control-flow analysis, abstract 
interpretation techniques) generalize to this setting? What are 
appropriate techniques for partial evaluation and program transformation 
of such programs? Besides these language issues, there are a number of 
modeling and implementation issues--What are appropriate continuous 
constraint systems which have fast algorithms for deciding the entailment 
relation? Can boundary value problems be solved in this framework? How 
does stepsize in numerical integration techniques affect execution and 
visualization of results? Some of these will be the subject of future 
papers. 
Computing with continuous change 
1 Introduction and motivation 
The construction of the software to implement, monitor, control and 
diagnose complex systems composed of electro-mechanical and 
computationally realized elements is a complex task. We are investigating 
the application of model-based computing techniques to address this 
complexity. Model-based computing is based on the idea that such 
machine-related software can be produced by applying appropriate reasoning 
techniques to a declarative, veridical model of the electro-mechanical 
system. 
The model-based computing approach places a set of requirements on the 
nature of the modeling language. We motivate these demands by considering 
a concrete example--the paper path of a simple photocopier, see FIG. 7. 
EXAMPLE 
Paper Transportation in a Photocopier 
In the photocopier of FIG. 7, paper is loaded in a paper tray at the left 
of the machine. When a signal is received, the acquisition roll (Acq Roll) 
is lowered onto the paper and pulls the top sheet of paper towards the 
first set of rollers (R1). After the paper is grasped by the first set of 
rollers, the acquisition roll (Acq Roll) is lifted, and the rollers 
(R2,R4) pull the paper forward, till it reaches the registration clutch 
(R3). This starts at a precise moment for perfect alignment, and the image 
is transferred onto the paper by the image transfer mechanism. The vacuum 
belt (5) transports it to the fuser roll (R6), from where it exists. 
Hybrid modeling 
The photocopier of FIG. 7 has a collection of components with continuous 
behavior, for example, the rollers and belts. The control program of the 
photocopier is a discrete event driven system. Therefore, the modeling 
language should be able to describe the interaction of the control program 
and the continuous components--thus, the modeling language has to fall in 
the framework of hybrid systems. 
Executability 
Given a model of the system, it should be possible to predict the behavior 
of the system when inputs are supplied. Thus the model should be 
executable, i.e. it should also be possible to view models as programs. 
This would allow hybrid control programs to be written using the same 
notation as component models. If sensors and actuators coupling the 
language implementation with the physical environment are provided then, 
in fact, it should be possible to use programs in this notation to drive 
physical mechanisms. 
Compositional modeling 
Out of considerations of reuse, it seems clear that models of components 
should reflect their physics, without reflecting any pre-compile knowledge 
of the structure (configurations) in which they will be used (the "no 
function in structure principle,"). Concretely, this implies that the 
modeling language must be expressive enough to modularly describe and 
support extant control architectures and techniques for compositional 
design of hybrid systems. From a programming language standpoint, these 
modularity concerns are addressed by the analysis underlying synchronous 
programming languages, (adapted to dense discrete domains); this analysis 
leads to the following demands on the modeling language. 
The modeling should support the interconnection of difference components, 
and allow for the hiding of these interconnections. For example, the model 
of the copier is the composition of the control program and the model of 
the paper path. The model of the paper path in turn, is the composition of 
the models of the roller, clutches, etc. 
Furthermore, in the photocopier example, if paper jams, the control program 
should cause the rollers to stop. However, the model of the rollers, in 
isolation, does not need to have any knowledge of potential error 
conditions. Thus, the modeling language should support orthogonal 
preemption--any signal can cause preemption. 
Finally, the language should allow the expression of multiple notions of 
logical time--for example, in the photocopier the notion of time relevant 
to the paper tray is (occurrences of) the event of removing paper from the 
tray; the notion of time relevant to the acquisition roll is determined by 
the rotation rate of the roller; the notion of time of the image transfer 
mechanism is the duration of the action of transferring images, etc. 
Thus, we demand that the modeling language be an algebra of processes, that 
includes concurrency, hiding, preemption and multiform time. 
Declarative view 
It must be possible for systems engineers--people quite different in 
training and background from software engineers--to use such a formalism. 
Typically, systems engineers understand the physics of the system being 
designed or analyzed, and are used to mathematical or constraint-based 
formalisms (equational and algebraic models, transfer functions, 
differential equations) for expressing that knowledge. This suggests that 
it must be possible to view a model (fragment) expressed in the language 
as a declaration of facts in a (real-time) (temporal) logic. 
Reasoning 
Given a model of the paper-path, and the control procedures governing it, 
it should be possible to perform a tolerance analysis--establish the 
windows on early/late arrival of sheets of papers at various sensors on 
the paper-path, given that a particular physical component may exhibit any 
behavior within a specified tolerance. This, and other such engineering 
tasks, suggest that the modeling language must be amenable to (adapting) 
the methodology developed in the extensive research on reasoning about 
hybrid and real-time systems--for example, specification and verification 
of properties of hybrid systems, qualitative reasoning about physical 
systems, and envisionment of qualitative states. 
1.1 What have we done? 
This paper describes and studies a modeling language, Hybrid cc--hybrid 
concurrent constraint programming. Intuitively, Hybrid cc is obtained by 
"freely extending" an untimed non-monotonic language default cc over 
continuous time. 
We introduce the notion of a continuous constraint system to describe the 
continuous evolution of system trajectories. 
Hybrid constraint languages--developed generically over continuous 
constraint systems--are obtained by adding a single temporal construct, 
called hence. Intuitively, a formula hence A is read as asserting that A 
holds continuously beyond the current instant. 
We describe operational and denotational semantics and show Full 
Abstraction (for non-Zeno processes). The operational semantics has been 
implemented to yield an interpreter for Hybrid cc. 
We show that continuous variants of preemption-based control constructs and 
multiform timing constructs are definable in Hybrid cc. In particular, we 
show that these combinators arise as instances of a uniform pre-emption 
construct ("clock"). 
We adapt the ideas underlying compilation algorithms of synchronous 
languages to compile Hybrid cc programs to (essentially) hybrid automata. 
This makes the programs amenable to existing verification techniques. 
1.2 The underlying computational intuition 
Hybrid cc is a language in the concurrent constraint programming framework, 
augmented with a notion of continuous time and defaults. The (concurrent) 
constraint (cc) programming paradigm replaces the traditional notion of a 
store as a valuation of variables with the notion of a store as a 
constraint on the possible values of variables. Computation progresses by 
accumulating constraints in the store, and by checking whether the store 
entails constraints. Recently, several concrete general-purpose 
programming language have been implemented in this paradigm. 
A salient aspect of the cc computation model is that programs may be 
thought of as imposing constraints on the evolution of the system. Default 
cc provides five basic constructs: (tell) P (for P a primitive 
constraint), parallel composition (A, B), positive ask (if P then A), 
negative ask (if P else A), and hiding (new X in A). The program P imposes 
the constraint P. The program (A, B) imposes the constraints of both A and 
B--logically, this is the conjunction of A and B. new X in A imposes the 
constraints of A, but hides the variable X from the other 
programs--logically this can be thought of as a form of existential 
quantification. The program if P then A imposes the constraints of A 
provided that the rest of the system imposes the constraints P--logically, 
this can be thought of as intuitionist implication. The program if P else 
A imposes the constraints of A unless the rest of the system imposes the 
constraint P--logically, this can be thought of as a form of defaults 
Rei80!. (Note that if P else A is quite distinct from the program if P 
then A (assuming that the constraint system is closed under negation). The 
former will reduce to A if the final store does not entail P; the latter 
will reduce to A if the final store entails P.) The difference arises 
because, by their very nature, stores can contain partial information; 
they may not be strong enough to entail either P or P. (In the time 
contexts discussed below, the subtlety of the non-monotonic behavior of 
programs--intimately related to the casualty issues in synchronous 
programming languages--arises from this combinator.) To see this, note 
that A may itself cause further information to be added to the store at 
the current time instant; and indeed, several other programs 
simultaneously be active and adding more information to the store. 
Therefore requiring that information P be absent amounts to making a 
demand on "stability" of negative information. 
This declarative way of looking at programs is complemented by an 
operational view. The basic idea in the operational view is that of a 
network of programs interacting with a shared store of primitive 
constraints. The program P is viewed as adding P to the store 
instantaneously. The program (A, B) behaves like the simultaneous 
execution of both A and B. new X in A starts A but creates a new local 
variable X, so no information can be communicated on it outside. The 
program if P then A behaves like A if the current store entails P. The 
program if P else A behaves like A if the current store on quiescence does 
not entail P. 
The cc paradigm has no conception of time execution. For modeling discrete, 
reactive systems, Vijay Saraswat et al., Default Times Concurrent 
Constraint Programming, Proceedings of Twenty Second ACM Symposium on 
Principles of Programming Languages, San Francisco, January, 1995, 
introduced the idea (from synchronous programming) that the environment 
reacts with a system (program) at discrete time ticks. At each time tick, 
the program executes a cc program, outputs the resulting constraint, and 
sets up another program for execution at the next clock tick. Concretely, 
this led to the addition of two control constructs to the language next A 
(execute A at the next time instant), and always A (execute A at every 
time instant). Thus, intuitively, the discrete timed language was obtained 
by uniformly extending the untimed language (Default cc) across (integer) 
time. 
Continuous evolution over time 
We follow a similar intuition in developing Hybrid cc: the continuous time 
language is obtained by uniformly extending Default cc across real 
(continuous) time. This is accomplished by two technical developments. 
First, we enrich the underlying notion of constraint system to make it 
possible to describe the continuous evolution of state. Intuitively, we 
allow constraints expressing initial value (integration) problem, e.g. 
constraints of the form X=0, hence dot(X)=1; from these we can infer at 
time t that X=t. The technical innovation here is the presentation of a 
generic notion of continuous constraint systems (ccs), which builds into 
the very general notion of constraint systems just the extra structure 
needed to enable the definition of continuous control constructs (without 
committing to a particular choice of vocabulary for constraints involving 
continuous time). As a result subsequent development is parametfic on the 
underlying constraint language: for each choice of a ccs we get a hybrid 
programming language. 
Second we add to the untimed Default cc a single temporal control 
construct: hence A. Declaratively, hence A imposes the constraints of A at 
every time instant after the current one. Operationally, if hence A is 
invoked at time t, a new copy of A is invoked at each instant in (t, oo). 
Intuitively, hence might appear to be a very specialized construct, since 
it requires repetition of the same program at every subsequent time 
instant. However, hence can combine in very powerful ways with positive 
and negative ask operations to yield rich patterns of temporal evolution. 
The key idea is that negative asks allow the instantaneous preemption of a 
program--hence, a program hence if P else A will in fact not execute A at 
all those time instants at which P is true. 
Let us consider some concrete examples. First, clearly, one can program 
always A (which executes A at every time instant) by (A, hence A). Second, 
suppose that we require that a program A be executed at every time point 
beyond the current one until the first time instant at which P can be 
expressed as new X in (hence (if X else A, if P then always X)). 
Intuitively, at every time point beyond the current one, the condition X 
is checked. Unless it holds, A is executed. X is local--the only way it 
can be generated is by the other program (if P then always X), which, in 
fact generates X continuously if it generates it at all. Thus, a copy of A 
is executed at each time point beyond the current one upto (and excluding) 
the first time point at which P is detected. 
Similarly, to execute A precisely at the first time instant (assuming there 
is one) at which P holds, execute: new X in hence (if X else if P then A, 
if P then hence X). 
We show that the continuous version of the general preemption control 
construct clock is definable within the model presented here. The patterns 
of temporal behavior described above are obtainable as specializations of 
clock. Further, we show how programs containing the clock combinator may 
be equationally rewritten into programs not containing the combinator. 
While conceptually simple to understand, hence A requires the execution of 
A at every subsequent real time instant. Such a powerful combinator may 
seem impossible to implement computationally. For example, it may be 
possible to express programs of the form new T in (T=0, hence dot(T)=1, 
hence if rational(T) then A) which require the execution of A at every 
rational q&gt;0. Such programs are not implementable. We show that in fact 
Hybrid cc is computationally realizable. The basic intuition we exploit is 
that, in general, physical systems change slowly, with points of 
discontinuous change, followed by periods of continuous evolution. 
Technically, we introduce a stability condition (Condition 5, Section 2.2) 
for continuous constraint systems that guarantees that for every 
constraint P and Q there is a neighborhood around 0 in which P either 
entails of disentails Q at every point. This rules out constraints such as 
rational(T) as inadmissible. 
With this restriction, computation in Hybrid cc may be thought of as 
progressing in alternating phases of computation at a time point, and in 
an open interval. Computation at the time point establishes the constraint 
in effect at that instant, and sets up the program to execute 
subsequently. Computation in the succeeding open interval determines the 
length of the interval r and the constraint whose continuous evolution 
over (0,r) describes the state of the system over (0,r). 
Rest of this paper 
Formally, we proceed as follows. First, we review our earlier work on 
constraint systems and Default cc. Next, we describe the denotational 
model of Hybrid cc as an "extension" of Default cc over continuous time. 
This extension proceeds in two stages. First, we introduce the notion of a 
continuous constraint system--a real-time extension of constraint 
systems--to describe the continuous evolution of system trajectories. 
Next, we extend the Default cc model of processes over continuous time to 
describe Hybrid cc processes. This denotational model formalizes the 
"programs as constraints" idea and associates with each process, the 
collection of its observations. Next, we describe the operational 
semantics, an effective presentation of the operational view alluded to 
earlier. Finally, we establish the connection between the denotational and 
operational semantics. 
The following contains the formal definition of the clock operator, and 
transformation rules for it, and contain a representative programming 
example. In addition, several other examples, including a model of the 
paperpath of the simple photocopier (see "Modeling a paper path," by V. 
Gupta and P. Struss in the proceedings of Qualitative reasoning, 95) have 
been programmed in Hybrid cc. 
What remains to be done? 
A key area of future work is the development of reasoning methodologies for 
Hybrid cc. The good formal properties of Hybrid cc constitute preliminary 
evidence for the potential of adapting extant reasoning methodologies to 
Hybrid cc programs/models. It remains to carry out this program fully. In 
this endeavor, we hope that the denotational framework underlying Hybrid 
cc will facilitate the synthesis of three different traditions of static 
analysis--(1) the tradition of specification/verification; (2) the 
tradition of abstract interpretation, and (3) the tradition of types and 
type inference in functional/object-oriented languages. The integration of 
(2) and (3) in the framework of constraint based program analysis, the 
implicit integration of (1) and (2), via homomorphisms as abstractions, 
and the integration of (1) and (3) in the work on interaction categories 
constitute evidence for the viability of this program. 
2. Hybrid concurrent constraint programming 
2.1 Default cc programming 
We first review Default cc programming. 
Constraint systems 
A constraint system D is a system of partial information, consisting of a 
set of primitive constraints (first-order formulas) or tokens D, closed 
under conjunction and existential quantification, and an inference 
relation (logical entailment) .perp-right. that relates tokens to tokens 
(For technical convenience, the presentation here is a slight variation on 
earlier published presentations.) .perp-right. naturally induces logical 
equivalance, written .apprxeq.. Formally, 
Definition 2.1 
A constraint system is a structure &lt;D.perp-right.,Var,{.E-backward..sub.x 
.vertline.X.di-elect cons.Var}&gt; such that: 
D is closed under conjunction ():.perp-right..OR right.D.times.D satisfies: 
-P.perp-right.P; P.perp-right.Q and QR.perp-right.T implies that 
PR.perp-right.T 
-PQ.perp-right.P and PQ.perp-right.Q; P.perp-right.Q and P.perp-right.R 
implies that P.perp-right.QR 
Var is an infinite set of propositional variables, such that for each 
variable X.di-elect cons.Var,.E-backward..sub.x :D.fwdarw.D is an 
operation satisfying usual laws on existentials: 
P.perp-right..E-backward..sub.X P,.E-backward..sub.X (P.E-backward..sub.X 
Q).apprxeq..E-backward..sub.X P.E-backward..sub.X Q,.E-backward..sub.X 
.E-backward..sub.Y P.apprxeq..E-backward..sub.Y .E-backward..sub.X P and 
P.perp-right.Q.E-backward..sub.X P.perp-right..E-backward..sub.X Q. 
A constraint is an entailment closed subset of D. For any set of tokens, S, 
we let S stand for the set {P.di-elect 
cons.D.vertline..E-backward.{P.sub.1, . . . , P.sub.k }.OR right.S.P.sub.1 
. . . P.sub.k .perp-right.P}. For any token P, P is just the set {P}. 
We use a, c, d, e . . . to range over constraints. The set of constraints, 
written .vertline.D.vertline., ordered by inclusion (.OR right.) form a 
complete algebraic lattice with least upper bounds induced by . Reverse 
inclusion is written .OR left...E-backward.,.perp-right. lift to 
operations on constraints. An example of a constraint system is Herbrand, 
underlying logic programming--tokens are equalities over terms which are 
finite trees with variables ranging over trees. In the rest of this 
subsection we will assume that we are working in some constraint system 
&lt;D,.perp-right.,Var,{.E-backward..sub.x .vertline.X.di-elect cons.Var}&gt;. 
We will let P, Q, R, T , . . . range over D. 
Computability: We demand decidability of .perp-right. to make the 
operational semantics effective. 
Denotational semantics 
Observe for each program A those stores d in which they are quiescent, 
given the guess e about the final result. Note that the guess e must 
always be stronger than d--it must contain at least the information on 
which A is being tested for quiescence. 
Definition 2.2 (Simple Observations) SObs={(d, e).di-elect 
cons..vertline.D.vertline..times..vertline.D.vertline..vertline.e.OR 
left.d}. .quadrature. 
To describe processes and the denotation of combinators, we need some 
notation--for a set S of constraints, and constraint e,(S,e) stands for 
the set {(d,e).vertline.d.di-elect cons.S};S stands for the greatest lower 
bound of S and P.ltoreq.S exactly when each element in S entails P. Given 
a collection of sets (S.sub.i,e.sub.i) we write 
.orgate.(S.sub.i,e.sub.i)for their union. If X is a propositional 
variable, .E-backward..sub.x S={(cX.vertline.c.di-elect 
cons.S}.orgate.{.E-backward..sub.x c.vertline.c.di-elect cons.S}. 
A process is a collection of observations that satisfy two "closure" 
conditions: 1) Local determinacy--the idea is that once a guess is made, 
every process behaves like a determinate and monotone (with respect to the 
partial order on constraints) program; 2) Guess convergence--we will only 
make those guesses under which a process can actually quiesce. 
Definition 2.3 (Process) 
A process Z is a subset of SObs satisfying: (1)(S,e).di-elect cons.Z if 
S.noteq..O slashed. and (S,e).di-elect cons.Z and (2) (e,e).di-elect 
cons.Z if (d,c).di-elect cons.Z. 
The denotational semantics of the combinators can now be described. 
abortd).0. 
A,BdA.andgate.B 
Pd{(d,e).di-elect cons.SObs.vertline.P.di-elect cons.d} 
if P then Ad{(d,e).di-elect cons.SObs.vertline.P.di-elect 
cons.e(e,e.di-elect cons.A,P.di-elect cons.d(d,e).di-elect cons.A} 
if P else Ad{(d,e).di-elect cons.SObs.vertline.Pe(d,e).di-elect cons.A 
new X in Ad new .sub.x A 
where for a process Z 
new .sub.x Z d.orgate.{(.E-backward..sub.x ,e).OR 
right.SObs.vertline.(S,.E-backward..sub.x e).OR right.Z or 
(S,(.E-backward..sub.x e).hoarfrost.{X}).OR right.Z,X.ltoreq.S} 
The two cases in the definition of new.sub.X Z correspond intuitively to 
the following two possibilities: 1) Z quiesces on .E-backward..sub.X e. 
This case corresponds to the situation in which the execution of Z does 
not produce an internal X; 2) Z quiesces on e. In this case, Z must itself 
produce the X, since there is no other program around to produce it. 
Operational semantics 
A configuration is a multiset of programs--to be thought of as the parallel 
composition of the programs. We define binary transition 
relations.fwdarw.p on configurations; thus, the transition relation is 
indexed by the "guessed output token" P that will e used to evaluate 
defaults. .sigma.(.theta.) is the conjunction of the tokens in .theta.. 
##EQU3## 
Execution of a program A corresponds to finding a terminal configuration 
.theta.such that the "guessed output constraint" is actually achieved. 
##EQU4## 
where Y are the (propositional) variables in .GAMMA.' that are not in e; 
these are the variables introduced for new local variables by the 
operational semantics. 
2.2 Continuous constraint systems 
Continuous constraint systems augment constraint systems with the notion of 
a constraint holding continuously over a period of time. This is done via 
two mechanisms: for every token P, we have a token hence P. Intuitively, 
such a token is an activity condition that says that P is in effect at 
every instant r&gt;0. In addition, we require to be given, for every 
r.di-elect cons.R, a relation .perp-right..sub.r .OR right.D.times.D. The 
relation describes what tokens (the r-projection) must follow at time r 
given some initial and activity conditions. Intuitively such a family of 
relations captures the information content of "initial value problems" in 
integration. Formally, we have the following conditions: 
______________________________________ 
hence P .perp-right. hence hence P, 
hence hence P .perp-right. hence P (1) 
P .perp-right. Q hence P .perp-right. hence Q 
hence P .perp-right..sub.r P, if r &gt; 0 
______________________________________ 
A token is instantaneous if it not an activity condition, i.e., for no Q, 
P.OR right..perp-right. hence Q. We use IP, IQ, etc. to range over 
instantaneous tokens. 
It is not necessarily the case that P.perp-right., P, unless of course r=0. 
EQU P.perp-right..sub.0 P (2) 
Transitivity must be preserved on the left and the right, with respect to 
.perp-right.: 
##EQU5## 
The duration of integration is important, not when it was started. 
##EQU6## 
Finally, we demand a neighborhood of 0, where .perp-right..sub.r 
information is "stable." Define P.perp-right..sup.r 
Q(P(.A-inverted.).sup.r Q) exactly if P.sub.t .perp-right..sub.t 
Q(P(.A-inverted.).sub.t Q) for all t.di-elect cons.(0,r). Then we require: 
EQU (.A-inverted.P,Q.di-elect cons.D)(.E-backward.r&gt;0)(P.perp-right..sup.r 
Q)(P(.A-inverted.).sup.r Q)! (5) 
Definition 2.4 (Continuous Constraint System) 
A continuous constraint systems (ccs) is a tuple 
&lt;D,.perp-right.,Var,{.E-backward..sub.x .vertline.X.di-elect 
cons.Var},{.perp-right..sub.r .vertline.r.di-elect cons.R}&gt; satisfying 
&lt;D,.perp-right.,Var{.E-backward..sub.x .vertline.X.di-elect cons.Var}&gt; is a 
constraint system whose tokens are closed under hence 
.perp-right.,.perp-right..sub.r,.perp-right..sup.r,(.A-inverted.).sup.r 
satisfy Eqns 1-5.quadrature. 
A constraint, written a, c, d, e . . . , is a .perp-right. closed subset of 
D. This set of all constraints, .vertline.D.vertline., ordered by 
inclusion, .OR right., form a complete algebraic lattice, with least 
element true. .E-backward., hence and the entailment relations lift to 
operations on constraints. Reverse inclusion is written .OR left.. 
Integration operators .intg..sup.r, for every r.di-elect cons.R are 
generated by .perp-right..sub.r : 
EQU .intg..sup.r c={P.di-elect cons.D.vertline..E-backward.Q.di-elect 
cons.c.Q.perp-right..sub.r P} 
Computability 
The following are required to make the operational semantics effective. 
1. .perp-right.,.perp-right..sub.r, (.A-inverted.).sup.r are decidable. 
2. For all tokens P and for all real numbers r, there exists a token 
Q.sub.r such that {S.vertline.P.perp-right..sub.r 
S}={S.vertline.Q.perp-right..sub.0 S}. This ensures that if c is finite in 
.vertline.D.vertline.then .intg..sup.r c is finite in 
.vertline.D.vertline.. 
EXAMPLE 2.1 
The trivial ccs is defined as follows. Basic tokens are formulas hence d or 
d, where d is of the form dot(X, m)=r, for X a variable, m a non-negative 
integer and r a real number. Tokens consist of basic tokens closed under 
conjunction and existential quantification. The inference relations are 
defined in the obvious way under the interpretation that dot(X, m)=r 
states that the mth derivative of X is r, and that hence dot(X, m=r states 
that for all time t&gt;0 the mth derivative of X is r. The inference 
relations are trivially decidable: the functions of time expressible are 
exactly the polynomials. The .perp-right..sub.r, 
(.A-inverted.).sub.r,.perp-right..sup.r,(.A-inverted.).sup.r relations are 
expressible parameterically in r; the only non-trivial computation 
involved is that of finding the smallest non-negative root of univariate 
polynomials (this can be done using numerical integration). 
2.3 Denotational Model of Hybrid cc 
In the rest of this section we will assume that we are working in some 
continuous constraint system &lt;D,.perp-right.,Var,{.E-backward..sub.x 
.vertline.X.di-elect cons.Var},{.perp-right..sub.r .vertline.r.di-elect 
cons.R}&gt;. 
Notation 
We use standard notation for intervals of real numbers: (t1,t2) for the 
open interval, (t1, t2) for the left closed and right open interval etc. 
We will be working with partial functions on the reals--their domains will 
be initial segments of the real line of the form {0,t,t.di-elect cons.R. 
We use dom(.function.) for the domain of definition of .function.. Given 
.function. with dom(.function.)=0,r) and g with 
dom(g)=0,s),h=.function..multidot.g is defined as 
h(t)=.function.(t),t.di-elect cons.0,r) and h(r+t)=g(t),t.di-elect 
cons.0,s). We use .function..Arrow-up bold.0,t) to denote the 
restriction of the partial function .function. to the interval 0,t). 
Similarly, for .function..Arrow-up bold.0,t). Given two partial functions 
.function.,g, we say .function. is a prefix of g if graph(.function.).OR 
right. graph(g), where graph(.function.) is the representation of 
.function. as a set of pairs (I,.function.(I)). .function.is a proper 
prefix of g if .function. is a prefix of g and .function..noteq.g. If 
.function. is a prefix of g, we define the function g after .function. as: 
(g after.function.)(t)=g(t+r) where dom(.function.)=0,r) or 
dom(.function.)=0,r!. This is extended to sets of partial functions S in 
a natural way: S after .function.={g after 
.function..vertline.(.E-backward.g.OR left..function..di-elect cons.S)}. 
We also define S(0)={g(0).vertline.g.di-elect cons.S}. 
Observations 
An observation, a run of the system, is a tracing of the system trajectory 
over time--pieces of continuous evolution connected by discrete changes. 
Definition 2.5 (Observations) 
Obs consists of functions .function.:R.fwdarw.SObs such that 
dom(.function.)=0,r), for some r and satisfying piecewise continuity. 
EQU (.A-inverted.t.di-elect 
cons.dom(.function.))(.E-backward..epsilon..sub.t)(.E-backward.e.sub.1.sup 
.t,e.sub.2.sup.t .di-elect cons.D)..(.A-inverted.t'.di-elect 
cons.(t,t+.epsilon..sub.t)).function.(t')=(.intg..sup.t'-t 
e.sub.1.sup.t,.intg..sup.t'-t e.sub.2.sup.t).!..quadrature. 
Let .function..di-elect cons.Obs,t .di-elect cons.dom(.function.). Then, 
the Default cc observation executed continuously in some right 
neighborhood of t in .function. is 
.function.(t.sup.+)=(p(e.sub.1),p(e.sub.2)), where p(e)={c.vertline.hence 
c.di-elect cons.e}. The maximal such right neighborhoods are called 
phases. The notation is extended to subsets S of Obs: 
S(0.sup.+)={.function.(0.sup.+).vertline..function..di-elect cons.S}. 
Processes 
A process is a collection of observations that satisfies (1) captures the 
limit closure property of computational systems--if every approximation to 
an observation .function. is a system run, so is .function.(2) 
instantaneous execution at any time instant is modeled by a Default cc 
process and (3) the continuous behavior is generated by Default cc 
processes. 
Definition 2.6 
A process P is a non-empty, prefix-closed subset of Obs satisfying: 1. If 
all proper prefixes of .function..di-elect cons.Obs are in P, then 
.function..di-elect cons.P. 2. (.A-inverted..function..di-elect cons.P) (P 
after .function.)(0) is a Default cc process. 3. 
(.A-inverted..function..di-elect cons.P) (.A-inverted.t.di-elect 
cons.dom(.function.))(P after .function..Arrow-up bold.0,t!)(0.sup.+)! 
is a Default cc process.quadrature. 
Combinators 
P,if P then A, if P else A,(A,B) are inherited from Default cc and their 
denotations are induced by their Default cc definitions. 
Pd{.function..di-elect cons.Obs.vertline..function.(0)=(d,e)P.di-elect 
cons.d} 
if P then Ad{.function..di-elect 
cons.Obs.vertline..function.(0)=(d,e),P.di-elect cons.d.function..di-elect 
cons.A, P.di-elect cons.eg.di-elect cons.Awhere 
g(0)=(e,e),.A-inverted.t&gt;0.g(t)=.function.(t)} 
if P else Ad{.function..di-elect 
cons.Obs.vertline..vertline..function.(0)=(d,e),P.epsilon 
slash.e.function..di-elect cons.A} 
A,BdA.andgate.B 
new X in A imposes the constraints of A, but hides the variable X from the 
other programs. Every observation .function..di-elect cons.new X in A is 
induced by an observation g.di-elect cons.A, i.e. at every time instant t, 
.function.(t) must equal the result of hiding X in the Default cc process 
given by A at time t after history g.Arrow-up bold.0,t). Formally, new X 
in Ad 
{.function..di-elect cons.Obs.vertline..E-backward.g.OR 
right.A.dom(g)=dom(.function.)(.A-inverted.t.di-elect 
cons.dom(.function.)).function.(t).di-elect cons. new .sub.X (A after 
(g.Arrow-up bold.0,t)(0)))!} 
abortd{.di-elect cons.} 
hence Ad{.function..di-elect cons.Obs.vertline.(.A-inverted.t.di-elect 
cons.dom(.function.)).function.after (.function..Arrow-up 
bold.0,t)).di-elect cons.A!} 
2.4 Operational Semantics 
We assume that the program is operating in isolation--interaction with the 
environment can be coded as an observation and run in parallel with the 
program. We use .GAMMA.,.DELTA., . . . for multisets of programs; 
.sigma.(.GAMMA.) is defined as before. 
Configurations can be point or interval configurations. A point 
configuration is a Default cc program that is executed instantaneously (at 
a real time instant)--all discrete changes happen at point states. This 
execution results in two pieces of information: the constraint c on 
quiescence, and the "continuation"--the program to be executed at 
subsequent times. 
Interval configurations are triples (P,.GAMMA.,.DELTA.) and model 
continuous execution. P is the initial token, this is similar to the 
initial conditions in a differential equation. .GAMMA. consists of the 
programs active in the interval configuration. Computation progresses only 
through the (continuous) evolution of the store as captured by the passage 
of time. In particular, the interval state is exited as soon as the status 
of any of the conditionals changes--one which always fired does not fire 
anymore, or one starts firing. .DELTA.accumulates the "continuation." 
First, we describe transitions from point to interval configurations. 
.fwdarw. is the transition relation of Default cc, and .delta.(.GAMMA.) is 
the sub-multiset of programs of the form hence A in .delta.. 
##EQU7## 
In the interval configuration (P,.GAMMA., .DELTA.) we are going to execute 
the program .delta."once," and make sure that the status of the 
conditionals remains constant throughout the interval 0,r). Condition 5 
on continuous constraint systems ensures the existence of such an r&gt;0. The 
derivation relation is indexed by the "guessed output constraint" Q (used 
to evaluate defaults as in the operational semantics of Default cc) and 
the length of the interval r. 
##EQU8## 
The transition from interval to point configurations, 
##EQU9## 
is defined from 
##EQU10## 
e,r--verify that the guessed output constraint is achieved and verify that 
the residual conditionals were not enabled at any intermediate time. 
##EQU11## 
where Y are the (propositional) variables in .GAMMA.' that are not in Q, 
the variables introduced for new local variables by the operational 
semantics. .GAMMA.'.dwnarw..sub.r.sup.Q verifies that the remaining 
conditionals in .GAMMA.' were not enabled at any time during the open 
interval (0,r). 
##EQU12## 
Implementation 
The above operational semantics has been used as the basis of an 
implementation of Hybrid cc on top of the trivial constraint system of 
Section 2.1. The basic workhorse is the interpreter for Default cc, 
modified to work with the new constraint system. The guessing of the 
quiescent point in each phase (instant or interval) is accomplished by 
local backtracking in each phase. Roots of univariate polynomials are 
found in order to obtain bounds on the extent of an interval phase. The 
implementation is in (Sicstus) Prolog, and is available from the authors. 
Full Abstraction 
The operational and denotational semantics are equivalent. The proofs 
follow Default tcc and are omitted here for space reasons. Let U and Z be 
programs. 
Theorem 2.1 (Adequacy) 
U=Z implies U and Z have the same operational input-output behavior. 
The converse of the above theorem does not hold in general because of Zeno 
processes. For example, the above operational semantics run on a Hybrid cc 
program of a typical Zeno system--say, a bouncing ball, with a coefficient 
of restitution e&lt;1--does not progress to and beyond the finite real limit 
point. However, the denotational semantics can potentially have further 
information. 
Theorem 2.2 (Full Abstraction) 
For non-Zeno U,Z U=Z if U and Z have the same operational input-output 
behavior. 
2.5 Compilation to constraint hybrid automata 
Hybrid cc can be compiled into constraint hybrid automata, a variant of 
hybrid automata. A constraint hybrid automaton is a directed bipartite 
graph. The nodes are labeled by Default cc programs--these Default cc 
programs can be compiled to a finite lookup table. The two kinds of nodes 
are point and interval states. The start node is a point state. 
Transitions are labeled by constraints and connect point (resp. interval) 
to interval (resp. point) states. 
Execution is instantaneous in point states--the Default cc program in a 
point state is executed in parallel with any input from the environment. 
The automation makes a transition to an interval state based upon the 
output. Execution in the interval state begins in the succeeding open 
interval, with the output of the preceding point state treated as the 
initial condition. In the interval state, the labeling Default cc program 
is executed continuously in parallel with (continuous) input from the 
environment, until one of the transitions is enabled. When a transition is 
enabled, the automaton makes a transition to the corresponding point 
state. The constraint labeling the transition is treated as environment 
input to the point state. 
We sketch the construction for hence in FIGS. 8a-8f--the other cases are 
straightforward, and omitted for space reasons; e.g. the automaton for A,B 
is (essentially) the product construction. Particularly, FIG. 8a shows 
automation for P; FIG. 8b illustrates Automation for hence P; FIG. 8c 
discloses automation for if Q then hence P; FIG. 8d is a construct of 
powerset automation. FIG. 8e shows minimizing by merging equal states, 
noting that each state has an implicit arrow to itself. Lastly, FIG. 8f 
shows splitting each state into a point state and an interval state. 
Thereafter, a new start state is added and minimizing again takes place. 
Automaton for hence A 
This is essentially a powerset of the automaton for A. Consider the subsets 
of the set of states of the automaton for A containing the start state of 
A. The program at each state is the parallel composition of the programs 
of the component states. The transition table is induced by this view. 
Make two copies of this structure, a copy each for the interval states and 
the point states. The targets of the transitions are relabeled to reach 
the appropriate point or interval state. Add a transition labeled true 
from each point state to its corresponding interval state. Finally, add a 
new start state labeled true, with a single transition labeled true to the 
interval state labeled by singleton set containing the start state of A. 
The determinacy algorithm is used to check that the Default cc program in 
each state is determinate. 
A The Clock construct 
Clock 
clock B do A is a process that executes A only on those instants which are 
quiescent points of B. Note the resemblance to the when(undersampling) 
construct of LUSTRE and SIGNAL, and the integrator variables of integrator 
computation tree logic (ICTL). We show that many common combinators are 
definable from clock. 
Let B be a process. We identify the maximal subsequence .function..sub.B of 
the an observation .function. that is an element of the process B--a 
definition by (transfinite) induction. Limit closure of processes 
(condition (1)) facilitates the induction at limit ordinals. Other 
inductive steps are: 
##EQU13## 
Recognizing that A is executed only at the quiescent points of B: 
EQU clock B do A={.function..di-elect cons.Obs.vertline..function..sub.B 
.di-elect cons.A} 
However, clock B do a may not be a process for arbitrary B. So, we restrict 
the processes B to be generated by the grammar: 
B::=a.vertline.if a then abort.vertline.if a then hence B.vertline.if a 
else hence B.vertline.B,B.vertline.hence B 
For such processes B, clock B do A is indeed a process. The equational laws 
that hold for the clock combinator are summarized in table A, in the 
appendix. These rules allow the elimination of occurrences of clock from 
any program. 
First. first c do A=clock c do A, reduces to A at the first time instant 
that c becomes true--if there is a well-defined notion of the first 
occurrence of c, eg. there is no "first" occurrence of c in observations 
of hence c. In such cases, A will not be invoked. 
In the following discussion on definable combinators, we shall not repeat 
the caveat about the subtlety of the well-definedness of the "first" 
occurrences of events. 
Multiform time. time A on a=clock (always a) do A denotes a process whose 
notion of time is the occurrence of a--A evolves only when the store 
entails a. 
Watchdogs. do a watching a=clock (first a do abort) do A, read logically as 
"A until first a," is the strong abortion interrupt of ESTEREL. do A 
watching a behaves like A until the first time instant when a is entailed; 
when a is entailed A is killed instantaneously. 
Suspension-Activation. This is similar to the familiar (control--Z,fg). 
S.sub.a A.sub.b (A) behaves like A until the first instant when a is 
entailed; when a is entailed A is suspended from then on (thus, the 
S.sub.a). A is reactivated in the first time instant when b is entailed 
(thus, the A.sub.b). 
__________________________________________________________________________ 
S.sub.a A.sub.b (A) = new X in do(always X) watching a, first a do 
(first e do always X), time A on X! 
__________________________________________________________________________ 
hence (A.sub.1, A.sub.2) 
= hence A.sub.1, hence A.sub.2 
clock (B.sub.1, B.sub.2) do A 
= clock B.sub.1 do clock B.sub.2 do A 
clock B do (A.sub.1, A.sub.2) 
= clock B do A.sub.1, clock B do A.sub.2 
clock a do A = new X in (always if X else if c then A, if c then hence 
X!). 
clock (if a then hence B) do 
= if a then clock hence B do A, if a else A. 
clock (if a else hence B) do A 
= if a else clock hence B do A, if a then A. 
clock if a then abort do A 
= if a else A 
clock hence B do a 
= a. 
clock hence B do abort 
= abort. 
clock hence B do if a then A 
= if a then clock hence B do A 
clock hence B do if a else A 
= if a else clock hence B do A 
clock hence a do hence A 
= hence clock hence a do A. 
clock hence (if a then abort) 
= hence clock hence (if a then abort) do A 
do hence A 
clock hence (if a then hence 
= new X in if a then always X, hence clock hence (if X 
B) do hence A then hence B) do A! 
clock hence (if a else hence 
= new X in if a else always X, hence clock hence (if X 
B) do hence A else hence B) do A! 
__________________________________________________________________________ 
B An extended programming example: Billiards 
We model a billiards (pool) table with several balls. The balls roll in a 
straight line till a collision with another ball or an edge occurs. When a 
collision occurs the velocity of the balls involved changes discretely. 
When a ball falls into a pocket, it disappears from the game. For 
simplicity, we assume that all balls have equal mass and radius (called 
R). We model only two ball collisions, and assume that there is no 
friction. 
Impulses, denoted I, are assumed to be vectors. Velocities, positions are 
assumed to be pairs with an x-component and a y-component. 
The structure of the program is that each ball, each kind of collision, and 
the check for pocketing for each ball are modeled by programs. A ball is 
basically a record with fields for name, position and velocity. 
The program ball maintains a given ball (Ball) with initial position 
(InitPos) and velocity (InitVel). The program is given here in a syntax 
that allows the declaration of procedures. The syntax p(X.sub.1, . . . 
,X.sub.2)::A is read as asserting that for all X.sub.1, . . . ,X.sub.2) is 
equivalent to A. As the game evolves, position changes according to 
velocity (dot(Ball.pos)=Bell.InitVel) and velocity changes according to 
the effect of collisions. A propositional constraint Change (Ball), shared 
between the collision and ball programs, communicates occurrences of 
changes in the velocity of the ball named Ball. The combination do (. . . 
) watching pocketed (Ball) relative to do (. . . ) watching Change (Ball) 
is captured by lexical nesting. 
ball(Ball, InitPos, InitVel)::do (Ball.pos=InitPos, 
do Hence Ball.vel=InitVel watching Change(Ball), 
first Change(Ball) do ball(Ball, Ball.pos, Ball.newvel) 
hence dot(Ball.pos)=Ball.vel) watching pocketed(Ball). 
This table is assumed to start at (0,0) with length xMax and breadth yMax. 
If a ball hits the edge, one velocity component is reversed in sign and 
the other component is unchanged. 
edge.collision(B):: always (if(B.pos.x=B.r) or (B.pos.x=xMax-B.r) 
then (Change(B), B.newvel=(-B.vel.x, B.vel.y)), 
if (B.pos.y=B.r) or (B.pos.y=yMax-B.r) 
then (Change(B), B.newvel=(B.vel.x, -B.vel.y))). 
Ball-ball collisions involve solutions to the quadratic conservation of 
energy equation. "if .vertline.I.vertline.=0 else.vertline.I.vertline.&gt;o" 
chooses the correct solution, I.noteq.0. The solution I=0 makes the balls 
go through each other ||| We use distance (P1,P2) as short hand for the 
computation of the distance between the P1 and P2. 
##EQU14## 
A ball is pocketed if its center is within distance p from some pocket. 
pocket(Ball)::always if in pocket (xMax, yMax, Ball.pos) then pocketed 
(Ball). in pocket (xMax, yMax, P):: 
(distance(P, (0,0))&lt;p or distance(P, (0, yMax))&lt;p or 
distance(P, (xMax, 0))&lt;p or distance(P, (xMax, yMax))&lt;p or 
distance(P, (xMax/2, 0))&lt;p or distance(P, (xMax/2, yMax))&lt;p). 
This invention has been described with reference to the preferred 
embodiment. Obviously, modifications and alterations will occur to others 
upon a reading and understanding of the specification. It is intended that 
all such modifications and alterations be included insofar as they come 
within the scope of the appended claims or the equivalents thereof.