Abstract
Aiming at a deeper understanding of the essence of spatial logics for concurrency, we study a minimal spatial logic without quantifiers or any operators talking about names. The logic just includes the basic spatial operators void, composition and its adjunct, and the next step modality; for the model we consider a tiny fragment of CCS. We show that this core logic can already encode its own extension with quantifiers, and modalities for actions. From this result, we derive several consequences. Firstly, we establish the intensionality of the logic, we characterize the equivalence it induces on processes, and we derive characteristic formulas. Secondly, we show that, unlike in static spatial logics, the composition adjunct adds to the expressiveness of the logic, so that adjunct elimination is not possible for dynamic spatial logics, even quantifier-free. Finally, we prove that both model-checking and satisfiability problems are undecidable in our logic. We also conclude that our results extend to other calculi, namely the π-calculus and the ambient calculus.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Basu, S., Pollack, R., Roy, M.-F.: On the combinatorial and algebraic complexity of quantifier elimination. In: IEEE Symposium on Foundations of Computer Science (1994)
Caires, L.: Behavioral and Spatial Observations in a Logic for the p-Calculus. In: Walukiewicz, I. (ed.) FOSSACS 2004. LNCS, vol. 2987, pp. 72–89. Springer, Heidelberg (2004)
Caires, L., Cardelli, L.: A Spatial Logic for Concurrency (Part II). In: Brim, L., Jančar, P., Křetínský, M., Kucera, A. (eds.) CONCUR 2002. LNCS, vol. 2421, p. 209. Springer, Heidelberg (2002)
Caires, L., Cardelli, L.: A Spatial Logic for Concurrency (Part I). Information and Computation 186(2), 194–235 (2003)
Caires, L., Lozes, E.: Elimination of Quantifiers and Undecidability in Spatial Logics for Concurrency. Technical report, ENS-Lyon LIP Report (2004)
Calcagno, C., Cardelli, L., Gordon, A.D.: Deciding Validity in a Spatial Logic of Trees. In: ACM Workshop on Types in Language Design and Implementation, New Orleans, USA, pp. 62–73. ACM Press, New York (2003)
Calcagno, C., Yang, H., O’Hearn, P.W.: Computability and complexity results for a spatial assertion language for data structures. In: Hariharan, R., Mukund, M., Vinay, V. (eds.) FSTTCS 2001. LNCS, vol. 2245, p. 108. Springer, Heidelberg (2001)
Cardelli, L., Gardner, P., Ghelli, G.: Manipulating Trees with Hidden Labels. In: Gordon, A.D. (ed.) ETAPS 2003 and FOSSACS 2003. LNCS, vol. 2620, pp. 216–232. Springer, Heidelberg (2003)
Cardelli, L., Ghelli, G.: A Query Language Based on the Ambient Logic. In: Sands, D. (ed.) ESOP 2001 and ETAPS 2001. LNCS, vol. 2028, pp. 1–22. Springer, Heidelberg (2001)
Cardelli, L., Gordon, A.D.: Logical Properties of Name Restriction. In: Abramsky, S. (ed.) TLCA 2001. LNCS, vol. 2044, p. 46. Springer, Heidelberg (2001)
Cardelli, L., Gordon, A.D.: Anytime, Anywhere. Modal Logics for Mobile Ambients. In: 27th ACM Symp. on Principles of Programming Languages, pp. 365–377. ACM Press, New York (2000)
Charatonik, W., Gordon, A.D., Talbot, J.-M.: Finite-control mobile ambients. In: Le Métayer, D. (ed.) ESOP 2002 and ETAPS 2002. LNCS, vol. 2305, pp. 295–313. Springer, Heidelberg (2002)
Charatonik, W., Talbot, J.-M.: The decidability of model checking mobile ambients. In: Proceedings of the 15th Annual Conference of the European Association for Computer Science Logic. LNCS. Springer, Heidelberg (2001)
Conforti, G., Ghelli, G.: Decidability of Freshness, Undecidability of Revelation. In: Walukiewicz, I. (ed.) FOSSACS 2004. LNCS, vol. 2987, pp. 105–120. Springer, Heidelberg (2004)
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)
Hirschkoff, D., Lozes, E., Sangiorgi, D.: Separability, Expressiveness and Decidability in the Ambient Logic. In: Third Annual Symposium on Logic in Computer Science, Copenhagen, Denmark. IEEE Computer Society Press, Los Alamitos (2002)
Hirschkoff, D., Lozes, É., Sangiorgi, D.: Minimality results for the spatial logics. In: Pandya, P.K., Radhakrishnan, J. (eds.) FSTTCS 2003. LNCS, vol. 2914, pp. 252–264. Springer, Heidelberg (2003)
Lozes, E.: Adjunct elimination in the static Ambient Logic. In: Proc. of EXPRESS 2003. Elsevier, Amsterdam (to appear, 2003)
O’Hearn, P.W.: Resources, Concurrency, and Local Reasoning. In: Schmidt, D. (ed.) ESOP 2004. LNCS, vol. 2986, pp. 1–2. Springer, Heidelberg (2004)
Reynolds, J.C.: Separation Logic: A Logic for Shared Mutable Data Structures. In: Seventieth Annual Symposium on Logic in Computer Science, Copenhagen, Denmark. IEEE Computer Society Press, Los Alamitos (2002)
Sangiorgi, D.: Extensionality and Intensionality of the Ambient Logics. In: 28th Annual Symposium on Principles of Programming Languages, pp. 4–13. ACM Press, New York (2001)
Trakhtenbrot, B.A.: The impossibility of an algorithm for the decision problem for finite models. Dokłady Akademii Nauk SSR 70, 569–572 (1950)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Caires, L., Lozes, É. (2004). Elimination of Quantifiers and Undecidability in Spatial Logics for Concurrency. In: Gardner, P., Yoshida, N. (eds) CONCUR 2004 - Concurrency Theory. CONCUR 2004. Lecture Notes in Computer Science, vol 3170. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-28644-8_16
Download citation
DOI: https://doi.org/10.1007/978-3-540-28644-8_16
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-22940-7
Online ISBN: 978-3-540-28644-8
eBook Packages: Springer Book Archive