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). Such semantics is defined for the full language. In particular, is able to deal with the non-monotonic characteristic of the language, which constitutes a substantial additional technical difficulty w.r.t. other compositional denotational semantics 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. 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.