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
Inria Saclay - Ile de France, LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau]
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

https://hal.inria.fr/inria-00349353
Contributor : Catuscia Palamidessi <>
Submitted on : Monday, December 29, 2008 - 4:53:08 PM
Last modification on : Thursday, March 5, 2020 - 6:23:45 PM
Long-term archiving on: : Thursday, October 11, 2012 - 2:55:39 PM

File

ppdp_08.pdf
Files produced by the author(s)

Identifiers

Collections

Citation

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⟩

Share

Metrics

Record views

528

Files downloads

569