Hybrid Logical Analyses of the Ambient Calculus

Publication: Research - peer-reviewConference article – Annual report year: 2010

View graph of relations

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
Publication date2010
Volume208
Journal number5
Pages433-449
ISSN0890-5401
DOIs
StatePublished

Conference

Conference14th Workshop on Logic, Language, Information and Computation (WoLLIC)
Number14
CountryBrazil
CityRio de Janeiro
Period02/07/0705/07/07
CitationsWeb of Science® Times Cited: 0

Keywords

  • Hybrid logic, Static analysis, Mobile Ambients
Download as:
Download as PDF
Select render style:
APAAuthorCBEHarvardMLAStandardVancouverShortLong
PDF
Download as HTML
Select render style:
APAAuthorCBEHarvardMLAStandardVancouverShortLong
HTML
Download as Word
Select render style:
APAAuthorCBEHarvardMLAStandardVancouverShortLong
Word

ID: 5251623