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

Carlos Olarte 1 Frank D. Valencia 1
1 COMETE - Concurrency, Mobility and Transactions
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France, Polytechnique - X, CNRS - Centre National de la Recherche Scientifique : UMR7161
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. Here mobility is understood as communication of private names as typically done for mobile systems and security protocols. This paper is devoted to the 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 for the well-established framework of FLTL and 4) bring new semantic insights into the modeling of security protocols. More precisely, we 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.
Type de document :
Communication dans un congrès
Sergio Antoy and Elvira Albert. 10th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, Jul 2008, Valencia, Spain. pp.8-19, 2008, Proceedings of the 10th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming. 〈10.1145/1389449.1389452〉
Liste complète des métadonnées

Littérature citée [28 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00349353
Contributeur : Catuscia Palamidessi <>
Soumis le : lundi 29 décembre 2008 - 16:53:08
Dernière modification le : jeudi 11 janvier 2018 - 06:22:14
Document(s) archivé(s) le : jeudi 11 octobre 2012 - 14:55:39

Fichier

ppdp_08.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Carlos Olarte, Frank D. Valencia. The Expressivity of Universal Timed CCP: Undecidability of Monadic FLTL and Closure Operators for Security. Sergio Antoy and Elvira Albert. 10th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, Jul 2008, Valencia, Spain. pp.8-19, 2008, Proceedings of the 10th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming. 〈10.1145/1389449.1389452〉. 〈inria-00349353〉

Partager

Métriques

Consultations de la notice

410

Téléchargements de fichiers

317