×

zbMATH — the first resource for mathematics

Hybrid logical analyses of the ambient calculus. (English) Zbl 1200.68160
Summary: Hybrid logic is used to formulate three control flow analyses for Mobile Ambients, a process calculus designed for modelling mobility. 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.
MSC:
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
68T27 Logic in artificial intelligence
Software:
HyLoTab
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Cardelli, L.; Gordon, A.D., Mobile ambients, Theoretical computer science, 240, 177-213, (2000) · Zbl 0954.68108
[2] Nielson, H.R.; Nielson, F., Flow logic: a multi-paradigmatic approach to static analysis, (), 223-244 · Zbl 1026.68029
[3] Nielson, F.; Hansen, R.R.; Nielson, H.R., Abstract interpretation of mobile ambients, Science of computer programming, 47, 2-3, 145-175, (2003) · Zbl 1047.68080
[4] J. van Eijck, Constraint Tableaux for Hybrid Logics, Manuscript, CWI, Amsterdam, 2002.
[5] Nielson, F.; Nielson, H.R.; Hansen, R.R., Validating firewalls using flow logics, Theoretical computer science, 283, 2, 381-418, (2002) · Zbl 1016.68003
[6] H.R. Nielson, F. Nielson, Shape analysis for mobile ambients, in: Conference Record of the Annual ACM Symposium on Principles of Programming Languages, POPL’00, ACM Press, 2000, pp. 142-154. · Zbl 1323.68414
[7] T. Bolander, R.R. Hansen, Hybrid logical analyses of the ambient calculus, in: D. Leivant, R. de Queiroz (Eds.), Workshop on Logic, Language, Information and Computation (WoLLIC’07), Lecture Notes in Computer Science, vol. 4576, Springer-Verlag, Rio de Janeiro, Brazil, 2007, pp. 83-100, doi: 10.1007/978-3-540-73445-1. · Zbl 1175.68271
[8] Nielson, H.R.; Nielson, F.; Buchholtz, M., Security for mobility, (), 207-265 · Zbl 1202.68173
[9] R.R. Hansen, J.G. Jensen, Flow logics for mobile ambients, Master’s Thesis, Aarhus University, 1999.
[10] Hansen, R.R.; Jensen, J.G.; Nielson, F.; Nielson, H.R., Abstract interpretation of mobile ambients, (), 134-148 · Zbl 0957.68079
[11] F. Nielson, H.R. Nielson, R.R. Hansen, J.G. Jensen, Validating firewalls in mobile ambients, in: International Conference on Concurrency Theory (CONCUR’99), 1999, pp. 463-477Available from: <citeseer.ist.psu.edu/nielson99validating.html>.
[12] Blackburn, P.; de Rijke, M.; Venema, Y., Modal logic, () · Zbl 0988.03006
[13] T. Braüner, Natural deduction for hybrid logic, Journal of Logic and Computation 14 (3) (2004) 329-353. Available from: <http://dx.doi.org/10.1093/logcom/14.3.329>.
[14] Cardelli, L.; Gordon, A.D., Anytime, anywhere: modal logics for mobile ambients, (), 365-377 · Zbl 1323.68405
[15] J. van Eijck, HyLoTab—Tableau-based Theorem Proving for Hybrid Logics, Manuscript, CWI, Amsterdam, 2002.
[16] C. Braghin, Static analysis of security properties in Mobile Ambients, Ph.D. Thesis, Università Ca’ Foscari di Venezia, TD-2005-1, 2005. Available from: <http://www.unive.it/media/dipInformatica/phd/CBraghin_thesis_hyperlinks3.pdf.>.
[17] ten Cate, B.; Franceschet, M., On the complexity of hybrid logics with binders, (), 339-354 · Zbl 1136.03311
[18] T. Bolander, P. Blackburn, Terminating tableau calculi for hybrid logics extending K, in: Proceedings of Methods for Modalities 5 (M4M-5), 2007.
[19] Cardelli, L.; Gordon, A.D., Types for mobile ambients, (), 79-92 · Zbl 0954.68108
[20] T. Amtoft, H. Makholm, J.B. Wells, Polya: true type polymorphism for mobile ambients, in: J.-J. Levy, E.W. Mayr, J.C. Mitchell (Eds.), TCS 2004 (Third IFIP International Conference on Theoretical Computer Science), Toulouse, France, August 2004, Kluwer Academic Publishers, 2004, pp. 591-604. · Zbl 1088.68653
[21] Amtoft, T.; Kfoury, A.J.; Pericas-Geertsen, S.M., What are polymorphically-typed ambients?, (), 206-220 · Zbl 0977.68525
[22] C. Calcagno, P. Gardner, U. Zarfaty, Context logic and tree update, in: Conference Record of the Annual ACM Symposium on Principles of Programming Languages, POPL’05, ACM, 2005, pp. 271-282. · Zbl 1369.68132
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.