Abstract
We study decidability of a logic for describing processes with restricted names. We choose a minimal fragment of the Ambient Logic, but the techniques we present should apply to every logic which uses Cardelli and Gordon revelation and hiding operators, and Gabbay and Pitts freshness quantifier. We start from the static fragment of ambient logic that Calcagno, Cardelli and Gordon proved to be decidable. We prove that the addition of a hiding quantifier makes the logic undecidable. Hiding can be decomposed as freshness plus revelation. Quite surprisingly, freshness alone is decidable, but revelation alone is not.
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
Abadi, M., Gordon, A.D.: A calculus for cryptographic protocols: The spi calculus. Information and Computation 148(1), 1–70 (1999)
Börger, E., Grädel, E., Gurevich, Y.: The Classical Decision Problem. Springer, Heidelberg (1997)
Caires, L., Cardelli, L.: A spatial logic for concurrency (part 1). In: Kobayashi, N., Pierce, B.C. (eds.) TACS 2001. LNCS, vol. 2215, pp. 1–37. Springer, Heidelberg (2001)
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., Monteiro, L.: Verifiable and executable logic specifications of concurrent objects in L π . In: Hankin, C. (ed.) ESOP 1998. LNCS, vol. 1381, pp. 42–56. Springer, Heidelberg (1998)
Calcagno, C., Cardelli, L., Gordon, A.D.: Deciding validity in a spatial logic for trees. In: Proc. of ACM SIGPLAN Workshop on Types in Language Design and Implementation, TLDI 2003 (2003)
Cardelli, L.: Describing semistructured data. SIGMOD Record, Database Principles Column 30(4) (2001)
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., Ghelli, G.: A query language based on the ambient logic. In: Sands, D. (ed.) ESOP 2001. LNCS, vol. 2028, pp. 1–22. Springer, Heidelberg (2001)
Cardelli, L., Gordon, A.D.: Anytime, anywhere: Modal logics for mobile ambients. In: Proc. of POPL, ACM Press, New York (2000)
Cardelli, L., Gordon, A.D.: Logical properties of name restriction. In: Abramsky, S. (ed.) TLCA 2001. LNCS, vol. 2044, pp. 46–60. Springer, Heidelberg (2001)
Cardelli, L., Gordon, A.D.: Ambient logic. Submitted for publication, available from the authors (2002)
Charatonik, W., Talbot, J.-M.: The decidability of model checking mobile ambients. In: Fribourg, L. (ed.) CSL 2001 and EACSL 2001. LNCS, vol. 2142, p. 339. Springer, Heidelberg (2001)
Conforti, G., Ghelli, G.: Spatial logics to reason about semistructured data. In: Rubettino (ed.) Proc. of SEBD 2003 (2003)
Gabbay, M., Pitts, A.M.: A new approach to abstract syntax involving binders. In: Proc. of LICS 1999, pp. 214–224. IEEE Computer Society Press, Los Alamitos (1999)
Ghelli, G., Conforti, G.: Decidability of freshness, undecidability of revelation. Technical Report TR-03-11. Dipartimento di Informatica, Università di Pisa (2003)
Lozes, É.: Adjuncts elimination in the static ambient logic. In: Proc. of EXPRESS, 2003 (2003) (to appear)
O’Hearn, P.W., 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, M.: Nominal logic: A first order theory of names and binding. In: Proc. of it TACS 2001. LNCS, vol. 2215, pp. 219–242. Springer, Heidelberg (2001)
Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: Proc. LICS 2002, pp. 55–74. IEEE Computer Society, Los Alamitos (2002)
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
Conforti, G., Ghelli, G. (2004). Decidability of Freshness, Undecidability of Revelation. In: Walukiewicz, I. (eds) Foundations of Software Science and Computation Structures. FoSSaCS 2004. Lecture Notes in Computer Science, vol 2987. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-24727-2_9
Download citation
DOI: https://doi.org/10.1007/978-3-540-24727-2_9
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-21298-0
Online ISBN: 978-3-540-24727-2
eBook Packages: Springer Book Archive