zbMATH — the first resource for mathematics

Hybrid logical analyses of the ambient calculus. (English) Zbl 1175.68271
Leivant, Daniel (ed.) et al., Logic, language, information and computation. 14th international workshop, WoLLIC 2007, Rio de Janeiro, Brazil, July 2–5, 2007. Proceedings. Berlin: Springer (ISBN 978-3-540-73443-7/pbk). Lecture Notes in Computer Science 4576, 83-100 (2007).
Summary: In this paper, hybrid logic is used to formulate a rational reconstruction of a previously published control flow analysis for the mobile ambients calculus, and we further show how a more precise flow-sensitive analysis, that takes the ordering of action sequences into account, can be formulated in a natural way. We show that hybrid logic is very well suited to express the semantic structure of the ambient calculus and how features of hybrid logic can be exploited to reduce the “administrative overhead” of the analysis specification and thus simplify it. Finally, we use HyLoTab, a fully automated theorem prover for hybrid logic, both as a convenient platform for a prototype implementation as well as to formally prove the correctness of the analysis.
For the entire collection see [Zbl 1119.03004].

68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
03B62 Combined logics
03B70 Logic in computer science
68Q55 Semantics in the theory of computing
68Q60 Specification and verification (program logics, model checking, etc.)
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
Full Text: DOI