A Condensed Goal-Independent Bottom-Up Fixpoint Semantics Modeling the Behavior of tccp

Abstract

In this paper, we present a new compositional bottom-up semantics for the Timed Concurrent Constraint Language (tccp in short) which is defined for the full language. In particular, is able to deal with the non- monotonic characteristic of tccp, which constitutes a substantial addi- tional technical difficulty w.r.t. other compositional denotational seman- tics present in literature (which do not tackle the full language). The semantics is proved to be (correct and) fully abstract w.r.t. the full behavior of tccp, including infinite computations. This is particularly important since tccp has been defined to model reactive systems and they may not terminate with a purpose. The overall of these features makes our proposal particularly suitable as the basis for the definition of semantic-based program manipulation tools (like analyzers, debuggers or verifiers), especially in the context of reactive systems.