Title
Decidability of Freshness, Undecidability of Revelation.
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.
Year
DOI
Venue
2004
10.1007/978-3-540-24727-2_9
LECTURE NOTES IN COMPUTER SCIENCE
Field
DocType
Volume
Discrete mathematics,Computer science,Decidability,First-order logic,Operator (computer programming),Revelation,Ambient calculus,Software development,Undecidable problem
Conference
2987
ISSN
Citations 
PageRank 
0302-9743
11
0.80
References 
Authors
20
2
Name
Order
Citations
PageRank
Giovanni Conforti1110.80
Giorgio Ghelli21300255.19