2008.11.13 | Karl Klose

Title: The Expressivity of Universal Timed CCP:Undecidability of Monadic FLTL and Closure operators for Security

Abstract:
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. In this talk we shall show a study of 1) theexpressiveness
of utcc and 2) its semantic foundations. As applications of this
study, we also state 3) a noteworthy decidability result for the 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 usesa
monadic constraint system allowing us to prove a newresult for a
fragment of FLTL: The undecidability of the validity problem for
monadic FLTL without equality andfunction 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.

Joint work with Frank Valencia.

Biosketch: I'm an INRIA funded PhD student at Laboratoire
d'Informatique de l'Ecole Polytechnique (LiX), under supervision of
Catuscia Palamidessi and Frank Valencia. My research interests are
concurrent constraint programming (CCP), process calculi and abstract
interpretation of concurrent languages. I have been working mostly in
the definition of universal timed CCP (utcc), an extension of temporal
CCP to model mobile behavior. The main application of utcc is the
modeling and verification of security protocols. I have also worked in
the expressivity of utcc and its relation with first-order linear-time
temporal logic (FLTL) which allowed us to prove the undecidability of
the validity problem for monadic FLTL.

Host: Olivier Danvy