Copenhagen Programming Language Seminar

The Expressivity of Universal Timed CCP:

Undecidability of Monadic FLTL and Closure Operators for Security

Carlos Olarte
INRIA. LIX, ╔cole Polytechnique

Monday, October 27, 2008, 15:00-16:00
The IT University, Rued Langgaards Vej 7, DK-2300, Auditorium 3


The timed concurrent constraint programing model (tcc) is a declarative framework, closely related to First-Order Linear Temporal Logic (FLTL), for modeling reactive systems. The universal tcc formalism (utcc) is an extension of tcc with the ability to express mobility. Here mobility is understood as communication of private names as typically done for mobile systems and security protocols.

This talk is devoted to show a study of 1) the expressiveness of utcc and 2) its semantic foundations. As applications of this study, we also state 3) a noteworthy decidability result forthe well-established framework of FLTL and 4) bring new semantic insights into the modeling of security protocols.

More precisely, we shall show that in contrast to tcc, utcc is Turing-powerful by encoding Minsky machines. The encoding uses a monadic constraint system allowing us to prove a new result for a fragment of FLTL: The undecidability of the validity problem for monadic FLTL without equality and function symbols. This result refutes a decidability conjecture for FLTL from a previous paper. It also justifies the restriction imposed in previous decidability results on the quantification of flexible-variables.

We shall also show that as in tcc, utcc processes can be semantically represented as partial closure operators. The representation is fully abstract wrt the input-output behavior of processes for a meaningful fragment of the utcc. This shows that mobility can be captured as closure operators over an underlying constraint system. As an application we identify a language for security protocols that can be represented as closure operators over a cryptographic constraint system.

Paper presented in PPDP┤08 conference, available at http://www.lix.polytechnique.fr/~colarte/colarte/Publications_files/ppdp46-olarte.pdf
Keywords: Concurrent Constraint Programming, First-order Linear Temporal Logic, Closure Operators, Security Protocols

Scientific host:Thomas Hildebrandt and Hugo A. Lopez Administrative host: Annette Enggaard. All are welcome.
The Copenhagen Programming Language Seminar (COPLAS) is a collaboration between DIKU, ITU, KVL and RUC.
COPLAS is sponsored by the FIRST Graduate School.
To receive information about COPLAS talks by email, send a message to prog-lang-request@mail.it-c.dk with the word 'subscribe' as subject or in the body.

For more information about COPLAS, see http://www.coplas.org