File(s) under permanent embargo
Completeness and logical full abstraction in modal logics for typed mobile processes
chapter
posted on 2023-06-08, 05:05 authored by Martin BergerMartin Berger, Kohei Honda, Nobuko YoshidaWe study an extension of Hennessy-Milner logic for the pi-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.
History
Publication status
- Published
Publisher
Springer VerlagVolume
5126Page range
99-111Pages
13.0Event name
35th International Colloquium on Automata, Languages and Programming (ICALP)Event location
Reykjavik, IcelandEvent type
conferenceBook title
Automata, Languages and ProgrammingISBN
978-3-540-70582-6Series
Lecture Notes in Computer ScienceDepartment affiliated with
- Informatics Publications
Notes
35th International Colloquium, ICALP 2008, Reykjavik, Iceland, July 7-11, 2008, Proceedings, Part IIFull text available
- No
Peer reviewed?
- Yes
Editors
A Luca, M Magnus, D Ivan, I Anna, A LeslieLegacy Posted Date
2012-02-06Usage metrics
Categories
No categories selectedKeywords
Licence
Exports
RefWorks
BibTeX
Ref. manager
Endnote
DataCite
NLM
DC