Abstract
Bigraphs are emerging as an interesting model for concurrent calculi, like CCS, pi-calculus, and Petri nets. Bigraphs are built orthogonally on two structures: a hierarchical place graph for locations and a link (hyper-)graph for connections. With the aim of describing bigraphical structures, we introduce a general framework for logics whose terms represent arrows in monoidal categories. We then instantiate the framework to bigraphical structures and obtain a logic that is a natural composition of a place graph logic and a link graph logic. We explore the concepts of separation and sharing in these logics and we prove that they generalise some known spatial logics for trees, graphs and tree contexts.
Research partially supported by the EU projects: IHP ‘Marie Curie DisCo’ HPMT-CT-2001-00290, FET-GC ‘MIKADO’ IST-2001-32222, and FET-GC ‘MyThS’ IST-2001-32617.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Caires, L., Cardelli, L.: A spatial logic for concurrency (Part I). In: Kobayashi, N., Pierce, B.C. (eds.) TACS 2001. LNCS, vol. 2215, pp. 1–37. Springer, Heidelberg (2001)
Calcagno, C., Cardelli, L., Gordon, A.D.: Deciding validity in a spatial logic for trees. In: Proc. of TLDI (2003)
Calcagno, C., Gardner, P., Zarfaty, U.: A context logic for tree update. In: Proc. of LRPP (2004); revised version to appear in POPL, 2005
Cardelli, L., Gardner, P., Ghelli, G.: A spatial logic for querying graphs. In: Widmayer, P., Triguero, F., Morales, R., Hennessy, M., Eidenbenz, S., Conejo, R. (eds.) ICALP 2002. LNCS, vol. 2380, p. 597. Springer, Heidelberg (2002)
Cardelli, L., Gardner, P., Ghelli, G.: Manipulating trees with hidden labels. In: Gordon, A.D. (ed.) FOSSACS 2003. LNCS, vol. 2620, pp. 216–232. Springer, Heidelberg (2003)
Cardelli, L., Gordon, A.D.: Ambient logic. To appear in Mathematical Structures in Computer Science
Cardelli, L., Gordon, A.D.: Anytime, anywhere: Modal logics for mobile ambients. In: Proc. of POPL. ACM Press, New York (2000)
Conforti, G., Macedonio, D., Sassone, V.: Bigraphical logics for XML. In: Proc. of SEBD (2005) (to appear)
Conforti, G., Macedonio, D., Sassone, V.: BiLog: spatial logics for bigraphs. Computer Science Report 2005:02, University of Sussex (2005)
Hildebrandt, T., Winther, J.W.: Bigraphs and (Reactive) XML, an XML-centric model of computation. IT University of Copenhagen Technical Report TR-2005-26 (2005)
Hirschkoff, D.: An extensional spatial logic for mobile processes. In: Gardner, P., Yoshida, N. (eds.) CONCUR 2004. LNCS, vol. 3170, pp. 325–339. Springer, Heidelberg (2004)
Jensen, O.H., Milner, R.: Bigraphs and mobile processes (revised). Technical Report UCAM-CL-TR-580. University of Cambridge (2004)
Leifer, J.J., Milner, R.: Transition systems, link graphs and petri nets. Technical Report UCAM-CL-TR-598. University of Cambridge (2004)
Milner, R.: Bigraphical reactive systems. In: Larsen, K.G., Nielsen, M. (eds.) CONCUR 2001. LNCS, vol. 2154, pp. 16–35. Springer, Heidelberg (2001)
Milner, R.: Axioms for bigraphical structure. Technical Report UCAM-CL-TR-581. University of Cambridge (2004)
Milner, R.: Bigraphs for petri-nets. In: Lectures on Concurrency and Petri Nets: Advances in Petri Nets, pp. 686–701. Springer, Heidelberg (2004)
Milner, R.: Pure bigraphs. Technical Report UCAM-CL-TR-614. University of Cambridge (2005)
O’Hearn, P., Reynolds, J.C., Yang, H.: Local reasoning about programs that alter data structures. In: Fribourg, L. (ed.) CSL 2001 and EACSL 2001. LNCS, vol. 2142, pp. 1–19. Springer, Heidelberg (2001)
Pitts, A.M.: Nominal logic: A first order theory of names and binding. In: Kobayashi, N., Pierce, B.C. (eds.) TACS 2001. LNCS, vol. 2215, pp. 219–242. Springer, Heidelberg (2001)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Conforti, G., Macedonio, D., Sassone, V. (2005). Spatial Logics for Bigraphs. In: Caires, L., Italiano, G.F., Monteiro, L., Palamidessi, C., Yung, M. (eds) Automata, Languages and Programming. ICALP 2005. Lecture Notes in Computer Science, vol 3580. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11523468_62
Download citation
DOI: https://doi.org/10.1007/11523468_62
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-27580-0
Online ISBN: 978-3-540-31691-6
eBook Packages: Computer ScienceComputer Science (R0)