Deciding validity in a spatial logic for trees

ABSTRACT

(MATH) We consider a propositional spatial logic for finite trees. The logic includes A ???? Par B (tree composition), A ???? B (the implication induced by composition), and O (the unit of composition). We show that the satisfaction and validity problems are equivalent, and decidable. The crux of the argument is devising a finite enumeration of trees to consider when deciding whether a spatial implication is satisfied. We introduce a sequent calculus for the logic, and show it to be sound and complete with respect to an interpretation in terms of satisfaction. Finally, we describe a complete proof procedure for the sequent calculus. We envisage applications in the area of logic-based type systems for semistructured data. We describe a small programming language based on this idea.

REFERENCES

• 1: Extensible markup language. http://www.w3.org/XML/.
• 2: Peter Buneman, Semistructured data, Proceedings of the sixteenth ACM SIGACT-SIGMOD-SIGART symposium on Principles of database systems, p.117-121, May 11-15, 1997, Tucson, Arizona, United States [doi>10.1145/263661.263675]
• 3: Luís Caires , Luca Cardelli, A Spatial Logic for Concurrency, Proceedings of the 4th International Symposium on Theoretical Aspects of Computer Software, p.1-37, October 29-31, 2001
• 4: Luís Caires , Luca Cardelli, A Spatial Logic for Concurrency (Part II), Proceedings of the 13th International Conference on Concurrency Theory, p.209-225, August 20-23, 2002
• 5: Luís Caires , Luís Monteiro, Verifiable and Executable Logic Specifications of Concurrent Objects in Lpi, Proceedings of the 7th European Symposium on Programming: Programming Languages and Systems, p.42-56, March 28-April 04, 1998
• 6: C. Calcagno, L. Cardelli, and A. D. Gordon. Deciding validity in a spatial logic for trees. Technical Report MSR--TR--2002--113, Microsoft Research, 2002.
• 7: Cristiano Calcagno , Hongseok Yang , Peter W. O'Hearn, Computability and Complexity Results for a Spatial Assertion Language for Data Structures, Proceedings of the 21st Conference on Foundations of Software Technology and Theoretical Computer Science, p.108-119, December 13-15, 2001
• 8: Luca Cardelli , Philippa Gardner , Giorgio Ghelli, A Spatial Logic for Querying Graphs, Proceedings of the 29th International Colloquium on Automata, Languages and Programming, p.597-610, July 08-13, 2002
• 9: Luca Cardelli , Giorgio Ghelli, A Query Language Based on the Ambient Logic, Proceedings of the 10th European Symposium on Programming Languages and Systems, p.1-22, April 02-06, 2001
• 10: Luca Cardelli , Andrew D. Gordon, Anytime, anywhere: modal logics for mobile ambients, Proceedings of the 27th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.365-377, January 19-21, 2000, Boston, MA, USA [doi>10.1145/325694.325742]
• 11: L. Cardelli and A. D. Gordon. Logical properties of name restriction. In Proceedings of the 5th International Conference on Typed Lambda Calculi and Applications (TLCA'01), volume 2044 of Lecture Notes in Computer Science, pages 46--60. Springer, 2001.
• 12: Witold Charatonik , Silvano Dal-Zilio , Andrew D. Gordon , Supratik Mukhopadhyay , Jean-Marc Talbot, The Complexity of Model Checking Mobile Ambients, Proceedings of the 4th International Conference on Foundations of Software Science and Computation Structures, p.152-167, April 02-06, 2001
• 13: Witold Charatonik , Jean-Marc Talbot, The Decidability of Model Checking Mobile Ambients, Proceedings of the 15th International Workshop on Computer Science Logic, p.339-354, September 10-13, 2001
• 14: E. Cohen. Validity and model checking for logics of finite multisets. Draft, Microsoft Research, 2002.
• 15: Daniel Hirschkoff , Étienne Lozes , Davide Sangiorgi, Separability, Expressiveness, and Decidability in the Ambient Logic, Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science, p.423-432, July 22-25, 2002
• 16: Haruo Hosoya , Benjamin C. Pierce, XDuce: A Typed XML Processing Language (Preliminary Report), Selected papers from the Third International Workshop WebDB 2000 on The World Wide Web and Databases, p.226-244, May 18-19, 2000
• 17: Haruo Hosoya , Benjamin Pierce, Regular expression pattern matching for XML, Proceedings of the 28th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.67-80, January 2001, London, United Kingdom
• 18: Samin S. Ishtiaq , Peter W. O'Hearn, BI as an assertion language for mutable data structures, Proceedings of the 28th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.14-26, January 2001, London, United Kingdom
• 19: P. Lincoln, J. Mitchell, A. Scedrov, and N. Shankar. Decision problems for propositional linear logic. Annals of Pure and Applied Logic, 56:239--311, 1992.
• 20: D. Lugiez and S. Dal Zilio. Multitrees automata, Presburger's constraints and tree logics. Laboratoire d'Informatique Fondamentale, CNRS and Université de Provence, 2002.
• 21: Peter W. O'Hearn , John C. Reynolds , Hongseok Yang, Local Reasoning about Programs that Alter Data Structures, Proceedings of the 15th International Workshop on Computer Science Logic, p.1-19, September 10-13, 2001
• 22: John C. Reynolds, Separation Logic: A Logic for Shared Mutable Data Structures, Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science, p.55-74, July 22-25, 2002
• 23: A. Urquhart. The undecidability of entailment and relevant implication. Journal of Symbolic Logic, 45:1059--1073, 1984.

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.0 General

Additional Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.0 General

General Terms:
Algorithms, Languages, Theory