Abstract interpretation of temporal concurrent constraint programs

DOI10.1017/S1471068413000641zbMATH Open1379.68060arXiv1312.2552OpenAlexW2046682249MaRDI QIDQ4592982FDOQ4592982

Authors: Carlos Olarte, Catuscia Palamidessi, M. Falaschi 

Publication date: 9 November 2017

Published in: Theory and Practice of Logic Programming (Search for Journal in Brave)

Abstract: Timed Concurrent Constraint Programming (tcc) is a declarative model for concurrency offering a logic for specifying reactive systems, i.e. systems that continuously interact with the environment. 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. In this paper we consider the denotational semantics for tcc, and we extend it to a "collecting" semantics for utcc based on closure operators over sequences of constraints. Relying on this semantics, we formalize a general framework for data flow analyses of tcc and utcc programs by abstract interpretation techniques. The concrete and abstract semantics we propose are compositional, thus allowing us to reduce the complexity of data flow analyses. We show that our method is sound and parametric with respect to the abstract domain. Thus, different analyses can be performed by instantiating the framework. We illustrate how it is possible to reuse abstract domains previously defined for logic programming to perform, for instance, a groundness analysis for tcc programs. We show the applicability of this analysis in the context of reactive systems. Furthermore, we make also use of the abstract semantics to exhibit a secrecy flaw in a security protocol. We also show how it is possible to make an analysis which may show that tcc programs are suspension free. This can be useful for several purposes, such as for optimizing compilation or for debugging.

Full work available at URL: https://arxiv.org/abs/1312.2552

Recommendations

• A program analysis framework for \textit{tccp} based on abstract interpretation
• Abstract Analysis of Universal Properties for tccp
• A semantic framework for the abstract model checking of tccp programs
• Abstract model checking of \textsf{tccp} programs
• scientific article; zbMATH DE number 1332633

zbMATH Keywords

abstract interpretationreactive systemsdenotational semanticsprocess calculitimed concurrent constraint programming

Mathematics Subject Classification ID

Logic programming (68N17) Semantics in the theory of computing (68Q55) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Cites Work

• The Esterel synchronous programming language: Design, semantics, implementation
• Design, implementation, and evaluation of the constraint language cc(FD)
• Truly concurrent constraint programming
• A calculus of mobile processes. I
• Linear concurrent constraint programming: Operational and phase semantics
• Models and emerging trends of concurrent constraint programming
• Title not available (Why is that?)
• Abstract interpretation and application to logic programs
• Closures and Modules Within Linear Logic Concurrent Constraint Programming
• Two classes of Boolean functions for dependency analysis
• Enumeration of success patterns in logic programs
• Declarative Diagnosis of Temporal Concurrent Constraint Programs
• Title not available (Why is that?)
• Nondeterminism and infinite computations in constraint programming
• On the security of public key protocols
• Confluence in concurrent constraint programming
• A timed concurrent constraint language.
• Abstract diagnosis for timed concurrent constraint programs
• Title not available (Why is that?)
• Title not available (Why is that?)
• Automatic verification of timed concurrent constraint programs
• Constraints in computational logics. 1st international conference, CCL '94, Munich, Germany, September 7--9, 1994. Proceedings
• Types for Secure Pattern Matching with Local Knowledge in Universal Concurrent Constraint Programming
• Automata, languages and programming. 28th international colloquium, ICALP 2001, Crete, Greece, July 8--12, 2001. Proceedings
• Constraint logic programming with dynamic scheduling: A semantics based on closure operators
• Generalized semantics and abstract interpretation for constraint logic programs
• A confluent semantic basis for the analysis of concurrent constraint logic programs

Cited In (7)

• A symbolic model for timed concurrent constraint programming
• A program analysis framework for \textit{tccp} based on abstract interpretation
• Types for Secure Pattern Matching with Local Knowledge in Universal Concurrent Constraint Programming
• Abstract diagnosis for timed concurrent constraint programs
• A logical and graphical framework for reaction systems
• Abstract Analysis of Universal Properties for tccp
• Title not available (Why is that?)

Uses Software

• Esterel

This page was built for publication: Abstract interpretation of temporal concurrent constraint programs

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4592982)