Berger, Martin, Honda, Kohei and Yoshida, Nobuko (2008) Completeness and logical full abstraction in modal logics for typed mobile processes. In: Luca, A, Ivan, D, Leslie, A, Magnus, M and Anna, I (eds.) Automata, Languages and Programming. Lecture Notes in Computer Science, 5126 . Springer Verlag, pp. 99-111. ISBN 978-3-540-70582-6

PDF Restricted to SRO admin only Download (200kB)

Abstract

We 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.

Item Type:	Book Section
Additional Information:	35th International Colloquium, ICALP 2008, Reykjavik, Iceland, July 7-11, 2008, Proceedings, Part II
Schools and Departments:	School of Engineering and Informatics > Informatics
Depositing User:	Martin Berger
Date Deposited:	06 Feb 2012 20:07
Last Modified:	13 Nov 2013 14:56
URI:	http://sro.sussex.ac.uk/id/eprint/24190

View download statistics for this item

📧 Request an update