Abstract FR:

Concurrent Constraint Programming (CCP) is a formalism for concurrency in which agents (processes) interact with one another by telling (adding) and asking (reading) information represented as constraints in a shared medium (the store). Temporal Concurrent Constraint Programming (tcc) extends CCP by allowing agents to be constrained by time conditions. This dissertation studies temporal CCP as a model of concurrency for mobile, timed reactive systems. The study is conducted by developing a process calculus called utcc, Universal Temporal CCP. The thesis is that utcc is a model for concurrency where behavioral and declarative reasoning techniques coexist coherently, thus allowing for the specification and verification of mobile reactive systems in emergent application areas. The utcc calculus generalizes tcc, a temporal CCP model of reactive synchronous programming, with the ability to express mobility. Here mobility is understood as communication of private names as typically done for mobile systems and security protocols. The utcc calculus introduces parametric ask operations called abstractions that behave as persistent parametric asks during a time-interval but may disappear afterwards. The applicability of the calculus is shown in several domains of Computer Science. Namely, decidability of Pnueli's First-order Temporal Logic, closure-operator semantic characterization of security protocols, semantics of a Service-Oriented Computing language, and modeling of Dynamic Multimedia-Interaction systems. The utcc calculus is endowed with an operational semantics and then with a symbolic semantics to deal with problematic operational aspects involving infinitely many substitutions and divergent internal computations. The novelty of the symbolic semantics is to use temporal constraints to represent finitely infinitely-many substitutions. In the tradition of CCP-based languages, utcc is a declarative model for concurrency. It is shown that utcc processes can be seen, at the same time, as computing agents and as logic formulae in the Pnueli's First-order Linear-time Temporal Logic (FLTL). More precisely, the outputs of a process correspond to the formulae entailed by its FLTL representation. The above-mentioned FLTL characterization is here used to prove an insightful (un)decidability result for Monadic FLTL. To do this it is proven that in contrast to tcc, utcc is Turing-powerful by encoding Minsky machines. The encoding uses a simple decidable constraint system involving only monadic predicates and no equality nor function symbols. The importance of using such a constraint system is that it allows for using the underlying theory of utcc to prove the undecidability of the validity problem for monadic FLTL without function symbols nor equality. In fact, it is shown that this fragment of FLTL is strongly incomplete. This result refutes a decidability conjecture for FLTL from a previous work. It also justifies the restriction imposed in previous decidability results on the quantification of flexible-variables. This dissertation then fills a gap on the decidability study of monadic FLTL. Similarly to tcc, utcc processes can be semantically characterized as partial closure operators. Because of additional technical difficulties posed by utcc, the codomain of the closure operators is more involved than that for tcc. Namely, processes are mapped into sequences of future-free temporal formulae rather than sequences of basic constraints as in tcc. This representation is shown to be fully abstract with respect to the input-output behavior of processes for a meaningful fragment of the calculus. This shows that mobility can be captured as closure operators over an underlying constraint system. As a compelling application of the semantic study of utcc, this dissertation gives a closure operator semantics to a language for security protocols. This language arises as a specialization of utcc with a particular cryptographic constraint systems. This brings new semantic insights into the modeling and verification of security protocols. The utcc calculus is also used in this dissertation to give an alternative interpretation of the pi-based language defined by Honda, Vasconcelos and Kubo (hvk) for structuring communications. The encoding of hvk into utcc is straightforwardly extended to explicitly model information on session duration, allows for declarative preconditions within session establishment constructs, and features a construct for session abortion. Then, a richer language for the analysis of sessions is defined where time can be explicitly modeled. Additionally, relying on the above-mentioned interpretation of utcc processes as FLTL formulae, reachability analysis of sessions can be characterized as FLTL entailment. It is also illustrated that the utcc calculus allows for the modeling of dynamic multimedia interaction systems. The notion of constraints as partial information neatly defines temporal relations between interactive agents or events. Furthermore, mobility in utcc allows for the specification of more flexible and expressive systems in this setting, thus broadening the interaction mechanisms available in previous models. Finally, this dissertation proposes a general semantic framework for the data flow analyses of utcc and tcc programs by abstract interpretation techniques. The concrete and abstract semantics are compositional reducing the complexity of data flow analyses. Furthermore, the abstract semantics is parametric with respect to the abstract domain and allows for reusing the most popular abstract domains previously defined for logic programming. Particularly, a groundness analysis is developed and used in the verification of a simple reactive systems. The abstract semantics allows also to efficiently exhibit a secrecy flaw in a security protocol modeled in utcc.