05196498

a

05196498 Conforti, Giovanni Ghelli, Giorgio Decidability of freshness, undecidability of revelation (extended abstract). Walukiewicz, Igor (ed.), Foundations of software science and computation structures. 7th international conference, FOSSACS 2004, held as part of the joint European conferences on theory and practice of software, ETAPS 2004, Barcelona, Spain, March 29 -- April 2, 2004. Procedings. Berlin: Springer (ISBN 3-540-21298-1/pbk). Lecture Notes in Computer Science 2987, 105-120 (2004). 2004 Berlin: Springer EN

doi:10.1007/b95995

Summary: 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.