  Hybrid Communicating Sequential Processes (HCSP) is a powerful formal
modeling language for hybrid systems, which is an extension of CSP by
introducing differential equations for modeling continuous evolution and
interrupts for modeling interaction between continuous and discrete dynamics.
In this paper, we investigate the semantic foundation for HCSP from an
operational point of view by proposing notion of approximate bisimulation,
which provides an appropriate criterion to characterize the equivalence between
HCSP processes with continuous and discrete behaviour. We give an algorithm to
determine whether two HCSP processes are approximately bisimilar. In addition,
based on that, we propose an approach on how to discretize HCSP, i.e., given an
HCSP process A, we construct another HCSP process B which does not contain any
continuous dynamics such that A and B are approximately bisimilar with given
precisions. This provides a rigorous way to transform a verified control model
to a correct program model, which fills the gap in the design of embedded
systems.
