↓Skip to main content

A Logic you Can Count On

XML Automata Mobile Ambients
Table of Contents

Silvano Dal Zilio, Denis Lugiez, Charles Meyssonnier
In POPL 2004 — 31st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, jan 2004.

conference paper

 PDF  DOI〈10.1145/982962.964013〉

Abstract
#

We prove the decidability of the quantifier-free, static fragment of ambient logic, with composition adjunct and iteration, which corresponds to a kind of regular expression language for semistructured data. The essence of this result is a surprising connection between formulas of the ambient logic and counting constraints on (nested) vectors of integers.

Our proof method is based on a new class of tree automata for unranked, unordered trees, which may result in practical algorithms for deciding the satisfiability of a formula. A benefit of our approach is to naturally lead to an extension of the logic with recursive definitions, which is also decidable. Finally, we identify a simple syntactic restriction on formulas that improves the effectiveness of our algorithms on large examples.

References
#

  • An extended version of this paper appears as Research Report 5022, INRIA, November 2003.  PDF

Citation
#


@InProceedings{DalzilioS:logiccount,
   author    = {{Dal Zilio}, Silvano and Lugiez, Denis and Meyssonnier, Charles},
   title     = {{A Logic you Can Count On}},
   booktitle = {POPL 2004 -- 31st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
   publisher = {ACM Press},
   doi = {10.1145/982962.964013},
   month     = jan, 
   year      = 2004
}