Paper Info
Title
Completeness and Logical Full Abstraction in Modal Logics for Typed Mobile Processes
Abstract
We study an extension of Hennessy-Milner logic for the 茂戮驴-calculus which gives a sound and complete characterisation of representative behavioural preorders and equivalences over typed processes. New connectives are introduced representing actual and hypothetical typed parallel composition and hiding. We study three compositional proof systems, characterising the May/Must testing preorders and bisimilarity. The proof systems are uniformly applicable to different type disciplines. Logical axioms distill proof rules for parallel composition studied by Amadio and Dam. We demonstrate the expressiveness of our logic through verification of state transfer in multiparty interactions and fully abstract embeddings of program logics for higher-order functions.
Year
DOI
Venue
2008
10.1007/978-3-540-70583-3_9
ICALP (2)
Keywords
Field
DocType
modal logics,distill proof rule,complete characterisation,parallel composition,abstract embeddings,representative behavioural preorders,compositional proof system,typed mobile processes,testing preorders,program logic,hennessy-milner logic,logical full abstraction,proof system,higher order functions,modal logic
Discrete mathematics,Abstraction,Axiom,Computer science,Program logic,Modal logic,Completeness (statistics),Modal,Expressivity
Conference
Volume
ISSN
Citations 
5126
0302-9743
12
PageRank 
References 
Authors
0.64
18
3
Name
Order
Citations
PageRank
Martin Berger118113.40
Kohei Honda269829.60
Nobuko Yoshida32607153.29