 |
 |
Mikolaj Bojanczyk - Two-Way Unary Temporal Logic over Trees
lmcs:917 - Logical Methods in Computer Science, August 5, 2009, Volume 5, Issue 3 - https://doi.org/10.2168/LMCS-5(3:5)2009Two-Way Unary Temporal Logic over TreesArticle
We consider a temporal logic EF+F^-1 for unranked, unordered finite trees.
The logic has two operators: EF\phi, which says "in some proper descendant \phi holds", and F^-1\phi, which says "in some proper ancestor \phi holds". We present an algorithm for deciding if a regular language of unranked finite trees can be expressed in EF+F^-1. The algorithm uses a characterization expressed in terms of forest algebras.
Comment: 29 pages. Journal version of a LICS 07 paper
Source: arXiv.org:0904.4119
Volume: Volume 5, Issue 3
Secondary volumes: Selected Papers of the 22nd IEEE Symposium on Logic in Computer Science (LICS 2007)
Published on: August 5, 2009
Imported on: January 8, 2008
Keywords: Computer Science - Logic in Computer Science, F.4.1
Classifications
Mathematics Subject Classification 20201
- 03B44 - Temporal logic
- 03C07 - Basic properties of first-order languages and structures
- 03C13 - Model theory of finite structures
- 03D05 - Automata and formal grammars in connection with logical questions
- 68Q17 - Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.)
- 68Q19 - Descriptive complexity and finite models
1 Document citing this article
Consultation statistics
This page has been seen 3039 times.
This article's PDF has been downloaded 362 times.