PhD Thesis.

Universal Temporal Concurrent Constraint Programming

Supervised by Catuscia Palamidessi and Frank D. Valencia.

LIX, Ecole Polytechnique.

- Abstract. - Publications from this Dissertation.   - Proceedings of conferences   - Proceedings of workshops      - Book Chapters   - Abstracts and Short Papers   - Journals (Under preparation)   - Others - Dissertation. - Members of the Jury. -  Logistic Information.  

Final version of the manuscript in PDF: Click here.

Abstract

Concurrent Constraint Programming (CCP) [1] 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 [2], 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 [3]. 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.

REFERENCES

[1] V. Saraswat. Concurrent Constraint Programming. MIT Press, 1993.

[2] V. Saraswat, R. Jagadeesan, and V. Gupta. Foundations of Timed Concurrent Constraint Programming. In Proc. of LICS'94. IEEE CS, 1994.

[3] K. Honda, V. T. Vasconcelos, and M. Kubo. Language primitives and type discipline for structured communication-based programming. In Proc. of ESOP, volume 1381 of LNCS. Springer, 1998.

Publications from this Dissertation.

Proceedings of conferences

• C. Olarte and F. Valencia. The Expressivity of Universal Timed CCP: Undecidability of Monadic FLTL and Closure Operators for Security. PPDP'08: 8-19. ACM Press. 2008.

• C. Olarte and F. Valencia. Universal Concurrent Constraint Programing: Symbolic Semantics and Applications to Security. SAC 2008: 145-150. ACM Press. 2008.

• M. Falaschi, C. Olarte and C. Palamidessi. A Framework for Abstract Interpretation of Timed Concurrent Constraint Programs. In Proc of PPDP09. ACM Press. 2009. 

• M. Falaschi, C. Olarte, C. Palamidessi and F. Valencia. Declarative Diagnosis of Temporal Concurrent Constraint Programs. ICLP 2007: 271-285. Springer. 2007.

• Carlos Olarte and Camilo Rueda. A declarative language for dynamic multimedia interaction systems. In Proc of. MCM'09. Springer, 2009.

Proceedings of workshops

• H. A. Lopez, C. Olarte, and J. A. Perez. Towards a Unified Framework for Declarative Structured Communications. In Programming Language Approaches to Concurrency and Communication-cEntric Software: PLACES'09, February 2009. 

Book Chapters

• C. Olarte, C. Rueda and F. Valencia. Concurrent Constraint Calculi: a Declarative Paradigm for Modeling Music Systems. To appear in Nouveaux paradigmes pour l'informatique musicale. 2009. 

Abstracts and Short Papers

• C. Olarte, C. Palamidessi and F. Valencia. Universal Timed Concurrent Constraint Programming (Abstract). ICLP 2007: 464-465. Springer-Verlag. 2007.

• Jesus Aranda, Gerard Assayag, Carlos Olarte, Jorge A. Perez, Camilo Rueda, Mauricio Toro and Frank D. Valencia. An Overview of FORCES: An INRIA Project on Declarative Formalisms for Emergent Systems. To appear in Proc. of ICLP 2009. 

Journals (Under preparation)

•  C. Olarte and F. Valencia. Undecidability of Monadic First-Order Linear-Time Temporal Logic. 

Others

• C. Olarte. A Process Calculus for Universal Concurrent Constraint Programming: Semantics, Logic and Application. Vol. 20 n. 3/4, December 2007 of the Association for Logic Programming (ALP) Newsletter.

• C. Olarte, C. Rueda and Frank D. Valencia. Concurrent Constraint Programming: Calculi, Languages and Emerging Applications. Vol. 21 n. 2-3, August 2008 of the Association for Logic Programming (ALP) Newsletter.

Dissertation

Final version of the manuscript: Click here.

Slides: Click here.

Members of the Jury

• Rapporteurs:

  • Ugo Montanari.

  • Thomas T. Hildebrandt.

• Examinateurs:

  • Vijay A. Saraswat.

  • François Fages.

  • Marc Pouzet.

  • Moreno Falaschi.

• Directeur de these:

  • Catuscia Palamidessi.

  • Frank D. Valencia.

Logistic Information

• Where: Ecole Polytechnique. Amphitheatre Monge. Jury committee at "Classe 24".

• When: 29-sep-2009. 15:00.

Click here to know how to reach the Ecole Polytechnique and for information about accommodation.

Click here for a list of hotels in Paris.