Temporal Concurrent Constraint Programming

Autor: Valencia, Frank Dan
Jazyk: angličtina
Rok vydání: 2003
Zdroj: Valencia, F D 2003, Temporal Concurrent Constraint Programming . BRICS Dissertation Series DS-03-2 edn, Århus Universitetsforlag, Århus .
Popis: Concurrent constraint programming (ccp) is a formalism for concurrency in which agents interact with one another by telling (adding) and asking (reading) information in a shared medium. Temporal ccp extends ccp by allowing agents to be constrained by time conditions. This dissertation studies temporal ccp by developing a process calculus called ntcc.The ntcc calculus generalizes the tcc model, the latter being a temporal ccp model for deterministic and synchronouss timed reactive systems. The calculus is built upon few basic ideas but it captures several aspects of timed systems. As tcc, ntcc can model unit delays, time-outs, pre-emption and synchrony. Additionally, it can model unbounded but finit delays, bounded eventuality, asynchrony and nondeterminism. The applicability of the calculus is illustrated with several interesting examples of discrete-timed systems involving mutable data structures, robotic devises, multi-agent systems and music applications.The calculus is provided with a denotational semantics that captures the reactive computations of processes in the presence of arbitrary environments. The denotation is proven to be fully-abstract for a substantial fragment of the calculus. This dissertation identifies the exact technical problems (arising mainly from allowing nondeterminism, locality and time-outs in the calculus) that makes it impossible to obtain a fully abstract result for the full language of ntcc.Also, the calculus is provided with a process logic for expressing temporal specifications of ntcc processes. This dissertation introduces a (relatively) complete inference system to prove that a given ntcc process satisfies a given formula in this logic.The denotation, process logic and inference system presented in this dissertation significantly extend and strengthen similar developments for tcc and (untimed) ccp.This dissertation addresses the decidability of various behavioral equivalences for the calculus and characterizes their corresponding induced congruence. The equivalences (and their associated congruences) are proven to be decidable for a significant fragment of the calculus. The decidability results involve a systematic translation of processes into finite state Büchi automata. To the author's best knowledge the study of decidability for ccp equivalences is original to this work.Furthermore, this dissertation deepens the understanding of previous ccp work by establishing an expressive power hierarchy of several temporal ccp languages which were proposed in the literature by other authors. These languages, represented in this dissertation as variants of ntcc, differ in their way of defining infinite behavior (i.e., replication or recursion) and the scope of variables (i.e., static or dynamic scope). In particular, it is shown that (1) recursive procedures with parameters can be encode into parameterless recursive procedures with dynamic scoping, and vice-versa; (2) replication can be encoded into parameterless recursive procedures with static scoping, and vice-versa; (3) the languages for (1) are strictly more expressive than the languages from (2). (Thus, in this family of languages recursion is more expressive than replication and dynamic scope is more expressive than static scope.) Moreover, it is shown that behavioral equivalence is undecidable for the language from (1), but decidable for the languages from (2). Interestingly, the undecidability result holds even if the process variables take values from a fixed finite domain whilst the decidability holds for arbitrary domains.Both the expressive prower hierarchy and decidability/undecidability results give a clear distinction among the various temporal ccp languages. Also, the distinction between static and dynamic scoping helps to clarify the situation in thee (untimed) ccp family of languages. Moreover, the methods used in the decidability results may provide a framework to perform further systematic investigations of temporal ccp languages.
Databáze: OpenAIRE
načítá se...