Hybrid Logical Analyses of the Ambient Calculus

Thomas Bolander, Rene Rydhof Hansen

    Research output: Contribution to journalConference articleResearchpeer-review

    Abstract

    In this paper, 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. (C) 2009 Elsevier Inc. All rights reserved.
    Original languageEnglish
    JournalInformation and Computation
    Volume208
    Issue number5
    Pages (from-to)433-449
    ISSN0890-5401
    DOIs
    Publication statusPublished - 2010
    Event14th Workshop on Logic, Language, Information and Computation (WoLLIC) - Rio de Janeiro, Brazil
    Duration: 2 Jul 20075 Jul 2007
    Conference number: 14

    Conference

    Conference14th Workshop on Logic, Language, Information and Computation (WoLLIC)
    Number14
    CountryBrazil
    CityRio de Janeiro
    Period02/07/200705/07/2007

    Keywords

    • Hybrid logic
    • Static analysis
    • Mobile Ambients

    Fingerprint Dive into the research topics of 'Hybrid Logical Analyses of the Ambient Calculus'. Together they form a unique fingerprint.

    Cite this