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.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Full version of this paper as a DoC technical report, Imperial College London (to appear, 2008) www.dcs.qmul.ac.uk/~kohei/processlogic
Amadio, R., Dam, M.: A modal theory of types for the π-calculus. In: Jonsson, B., Parrow, J. (eds.) FTRTFT 1996. LNCS, vol. 1135, pp. 347–365. Springer, Heidelberg (1996)
Berger, M.: A program logic for sequential higher-order control (1): stateless case. Typescript, 36 pages (October 2007)
Berger, M., Honda, K., Yoshida, N.: Sequentiality and the π-calculus. In: Abramsky, S. (ed.) TLCA 2001. LNCS, vol. 2044, pp. 29–45. Springer, Heidelberg (2001)
Bonsangue, M., Kurz, A.: Pi-calculus in logical form. In: LICS 2007, pp. 303–312. IEEE, Los Alamitos (2007)
Caires, L., Cardelli, L.: A spatial logic for concurrency. I& C 186(2), 194–235 (2003)
Cardelli, L., Gordon, A.D.: Anytime, anywhere: Modal logics for mobile ambients. In: POPL, pp. 365–377 (2000)
Dam, M.: Proof systems for pi-calculus logics. In: Logic for Concurrency and Synchronisation. Trends in Logic, Studia Logica Library, pp. 145–212. Kluwer, Dordrecht (2003)
Honda, K.: From process logic to program logic. In: ICFP 2004, pp. 163–174. ACM, New York (2004)
Honda, K., Berger, M., Yoshida, N.: Descriptive and relative completeness for logics for higher-order functions. In: Bugliesi, M., Preneel, B., Sassone, V., Wegener, I. (eds.) ICALP 2006. LNCS, vol. 4052, pp. 360–371. Springer, Heidelberg (2006)
Honda, K., Vasconcelos, V.T., Kubo, M.: Language Primitives and Type Disciplines for Structured Communication-based Programming. In: Hankin, C. (ed.) ESOP 1998 and ETAPS 1998. LNCS, vol. 1381, pp. 22–138. Springer, Heidelberg (1998)
Jones, C.B.: Specification and design of (parallel) programs. In: IFIP Congress, pp. 321–332 (1983)
Larsen, K.G.: Proof systems for satisfiability in Hennessy-Milner logic with recursion. Theor. Comput. Sci. 72(2&3), 265–288 (1990)
Longley, J., Plotkin, G.: Logical full abstraction and PCF. In: Tbilisi Symposium on Logic, Language and Information, CLSI (1998)
Miller, D., Tiu, A.: A proof theory for generic judgments. ACM Transactions on Computational Logic 6(4), 749–783 (2005)
Milner, R.: The polyadic π-calculus: A tutorial. In: Proceedings of the International Summer School on Logic Algebra of Specification, Marktoberdorf (1992)
Milner, R., Parrow, J., Walker, D.: A Calculus of Mobile Processes, Parts I and II. Info.& Comp. 100(1) (1992)
Milner, R., Parrow, J., Walker, D.: Modal logics for mobile processes. TCS 114, 149–171 (1993)
Simpson, A.: Sequent calculi for process verification: Hennessy-Milner logic for an arbitrary GSOS. J. Log. Algebr. Program. 60-61, 287–322 (2004)
Stirling, C.: A complete compositional model proof system for a subset of CCS. In: Brauer, W. (ed.) ICALP 1985. LNCS, vol. 194, pp. 475–486. Springer, Heidelberg (1985)
Stirling, C.: Modal logics for communicating systems. TCS 49, 311–347 (1987)
Takeuchi, K., Honda, K., Kubo, M.: An Interaction-based Language and its Typing System. In: Halatsis, C., Philokyprou, G., Maritsas, D., Theodoridis, S. (eds.) PARLE 1994. LNCS, vol. 817, pp. 398–413. Springer, Heidelberg (1994)
Tiu, A.F.: Model checking for pi-calculus using proof search. In: Abadi, M., de Alfaro, L. (eds.) CONCUR 2005. LNCS, vol. 3653, pp. 36–50. Springer, Heidelberg (2005)
Yoshida, N., Berger, M., Honda, K.: Strong Normalisation in the π-Calculus. Information and Computation 191, 145–202 (2004)
Yoshida, N., Honda, K., Berger, M.: Logical reasoning for higher-order functions with local state. In: Seidl, H. (ed.) FOSSACS 2007. LNCS, vol. 4423, pp. 361–377. Springer, Heidelberg (2007)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Berger, M., Honda, K., Yoshida, N. (2008). Completeness and Logical Full Abstraction in Modal Logics for Typed Mobile Processes . In: Aceto, L., Damgård, I., Goldberg, L.A., Halldórsson, M.M., Ingólfsdóttir, A., Walukiewicz, I. (eds) Automata, Languages and Programming. ICALP 2008. Lecture Notes in Computer Science, vol 5126. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-70583-3_9
Download citation
DOI: https://doi.org/10.1007/978-3-540-70583-3_9
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-70582-6
Online ISBN: 978-3-540-70583-3
eBook Packages: Computer ScienceComputer Science (R0)