
AbstractTimed 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 universaltccformalism (utcc) is an extension oftccwith 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 fortcc, and extend it to a “collecting” semantics forutccbased on closure operators over sequences of constraints. Relying on this semantics, we formalize a general framework for data flow analyses oftccandutccprograms by abstract interpretation techniques. The concrete and abstract semantics that 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 fortccprograms. We show the applicability of this analysis in the context of reactive systems. Furthermore, we also make 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 thattccprograms are suspension-free. This can be useful for several purposes, such as for optimizing compilation or for debugging.
FOS: Computer and information sciences, Computer Science - Logic in Computer Science, [INFO.INFO-LO] Computer Science [cs]/Logic in Computer Science [cs.LO], Semantics in the theory of computing, reactive systems, Logic programming, Process calculi, Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.), abstract interpretation, Denotational semantics, F.3.1; D.3.2, process calculi, D.3.2, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], Abstract interpretation, timed concurrent constraint programming, process calculi, abstract interpretation, denotational semantics, reactive systems, 004, Logic in Computer Science (cs.LO), Reactive systems, Timed concurrent constraint programming, timed concurrent constraint programming, F.3.1, denotational semantics
FOS: Computer and information sciences, Computer Science - Logic in Computer Science, [INFO.INFO-LO] Computer Science [cs]/Logic in Computer Science [cs.LO], Semantics in the theory of computing, reactive systems, Logic programming, Process calculi, Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.), abstract interpretation, Denotational semantics, F.3.1; D.3.2, process calculi, D.3.2, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], Abstract interpretation, timed concurrent constraint programming, process calculi, abstract interpretation, denotational semantics, reactive systems, 004, Logic in Computer Science (cs.LO), Reactive systems, Timed concurrent constraint programming, timed concurrent constraint programming, F.3.1, denotational semantics
| selected citations These citations are derived from selected sources. This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | 7 | |
| popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network. | Average | |
| influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | Average | |
| impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network. | Average |
