NDLI: The expressivity of universal timed CCP: undecidability of Monadic FLTL and closure operators for security

Please wait, while we are loading the content...

The expressivity of universal timed CCP: undecidability of Monadic FLTL and closure operators for security

Comparing tag scheme variations using an abstract machine generator

Call pattern analysis for functional logic programs

Macros for context-free grammars

Towards execution time estimation in abstract machine-based languages

Classifying integrity checking methods with regard to inconsistency tolerance

Global difference constraint propagation for finite domain solvers

Declarative programming for verification: lessons and outlook

Parallel execution of multi-set constraint rewrite rules

'Galculator': functional prototype of a Galois-connection based proof assistant

Characterizations of polynomial complexity classes with a better intensionality

Pattern by example: type-driven visual programming of XML queries

Similarity-based reasoning in qualified logic programming

Comprehending finite maps for algorithmic debugging of higher-order functional programs

Model-driven constraint programming

Declarative Ajax and client side evaluation of workflows using iTasks

Fixed point semantics and partial recursion in Coq

Inferring precise polymorphic type dependencies in logic programs

A rewriting framework for the composition of access control policies

Dynamic variable elimination during propagation solving

Semantically linear programming languages

A type system for safe memory management and its proof of correctness

Cooperation of constraint domains in the TOY system

Order-sorted dependency pairs

Programming with proofs and explicit contexts

The expressivity of universal timed CCP: undecidability of Monadic FLTL and closure operators for security

Content Provider	ACM Digital Library
Author	Olarte, Carlos Valencia, Frank D.
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 wellestablished 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 Turingpowerful 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.
Starting Page	8
Ending Page	19
Page Count	12
File Format	PDF
ISBN	9781605581170
DOI	10.1145/1389449.1389452
Language	English
Publisher	Association for Computing Machinery (ACM)
Publisher Date	2008-07-15
Publisher Place	New York
Access Restriction	Subscribed
Subject Keyword	Concurrent constraint programming First-order linear temporal logic Security protocols Closure operators
Content Type	Text
Resource Type	Article

Central Library (ISO-9001:2015 Certified)
Indian Institute of Technology Kharagpur
Kharagpur, West Bengal, India | PIN - 721302

See location in the Map
03222 282435
Mail: support@ndl.gov.in

Sl.	Authority	Responsibilities	Communication Details
1	Ministry of Education (GoI), Department of Higher Education	Sanctioning Authority	https://www.education.gov.in/ict-initiatives
2	Indian Institute of Technology Kharagpur	Host Institute of the Project: The host institute of the project is responsible for providing infrastructure support and hosting the project	https://www.iitkgp.ac.in
3	National Digital Library of India Office, Indian Institute of Technology Kharagpur	The administrative and infrastructural headquarters of the project	Dr. B. Sutradhar bsutra@ndl.gov.in
4	Project PI / Joint PI	Principal Investigator and Joint Principal Investigators of the project	Dr. B. Sutradhar bsutra@ndl.gov.in Prof. Saswat Chakrabarti will be added soon
5	Website/Portal (Helpdesk)	Queries regarding NDLI and its services	support@ndl.gov.in
6	Contents and Copyright Issues	Queries related to content curation and copyright issues	content@ndl.gov.in
7	National Digital Library of India Club (NDLI Club)	Queries related to NDLI Club formation, support, user awareness program, seminar/symposium, collaboration, social media, promotion, and outreach	clubsupport@ndl.gov.in
8	Digital Preservation Centre (DPC)	Assistance with digitizing and archiving copyright-free printed books	dpc@ndl.gov.in
9	IDR Setup or Support	Queries related to establishment and support of Institutional Digital Repository (IDR) and IDR workshops	idr@ndl.gov.in