The Expressivity of Universal Timed CCP: Undecidability of Monadic FLTL and Closure Operators for Security - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2008

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

Carlos Olarte
  • Fonction : Auteur
  • PersonId : 845696
Frank D. Valencia
  • Fonction : Auteur
  • PersonId : 845697

Résumé

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.
Fichier principal
Vignette du fichier
ppdp_08.pdf (272.47 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

inria-00349353 , version 1 (29-12-2008)

Identifiants

Citer

Carlos Olarte, Frank D. Valencia. The Expressivity of Universal Timed CCP: Undecidability of Monadic FLTL and Closure Operators for Security. 10th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, ACM, Jul 2008, Valencia, Spain. pp.8-19, ⟨10.1145/1389449.1389452⟩. ⟨inria-00349353⟩
202 Consultations
372 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More