Skip to Main content Skip to Navigation
Conference papers

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
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.
Document type :
Conference papers
Complete list of metadata

Cited literature [28 references]  Display  Hide  Download
Contributor : Catuscia Palamidessi Connect in order to contact the contributor
Submitted on : Monday, December 29, 2008 - 4:53:08 PM
Last modification on : Thursday, January 20, 2022 - 4:12:41 PM
Long-term archiving on: : Thursday, October 11, 2012 - 2:55:39 PM


Files produced by the author(s)




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⟩



Record views


Files downloads