Counting in trees for free

Helmut Seidl; Thomas Schwentick; Anca Muscholl; Peter Habermehl

doi:10.1007/978-3-540-27836-8_94

Counting in trees for free

Helmut Seidl, Thomas Schwentick, Anca Muscholl, Peter Habermehl

Informatics 2 - Chair of Formal Languages, Compiler Construction, Software Construction

Research output: Chapter in Book/Report/Conference proceeding › Chapter › peer-review

70 Scopus citations

Abstract

It is known that MSO logic for ordered unranked trees is undecidable if Presburger constraints are allowed at children of nodes. We show here that a decidable logic is obtained if we use a modal fixpoint logic instead. We present a characterization of this logic by means of deterministic Presburger tree automata and show how it can be used to express numerical document queries. Surprisingly, the complexity of satisfiability for the extended logic is asymptotically the same as for the original fixpoint logic. The non-emptiness for Presburger tree automata (PTA) is PSPACE-complete, which is moderate given that it is already PSPACE-hard to test whether the complement of a regular expression is non-empty. We also identify a subclass of PTAs with a tractable non-emptiness problem. Further, to decide whether a tree t satisfies a formula φ is polynomial in the size of φ and linear in the size of t. A technical construction of independent interest is a linear time construction of a Presburger formula for the Parikh image of a regular language.

Original language	English
Title of host publication	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Editors	Josep Díaz, Juhani Karhumäki, Arto Lepistö, Donald Sannella
Publisher	Springer Verlag
Pages	1136-1149
Number of pages	14
ISBN (Print)	3540228497
DOIs	https://doi.org/10.1007/978-3-540-27836-8_94
State	Published - 2004

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	3142
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Access to Document

10.1007/978-3-540-27836-8_94

Cite this

Seidl, H., Schwentick, T., Muscholl, A., & Habermehl, P. (2004). Counting in trees for free. In J. Díaz, J. Karhumäki, A. Lepistö, & D. Sannella (Eds.), Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (pp. 1136-1149). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 3142). Springer Verlag. https://doi.org/10.1007/978-3-540-27836-8_94

Seidl, Helmut ; Schwentick, Thomas ; Muscholl, Anca et al. / Counting in trees for free. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). editor / Josep Díaz ; Juhani Karhumäki ; Arto Lepistö ; Donald Sannella. Springer Verlag, 2004. pp. 1136-1149 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inbook{30413a3ab6e244cb968c50d5782e0c42,

title = "Counting in trees for free",

abstract = "It is known that MSO logic for ordered unranked trees is undecidable if Presburger constraints are allowed at children of nodes. We show here that a decidable logic is obtained if we use a modal fixpoint logic instead. We present a characterization of this logic by means of deterministic Presburger tree automata and show how it can be used to express numerical document queries. Surprisingly, the complexity of satisfiability for the extended logic is asymptotically the same as for the original fixpoint logic. The non-emptiness for Presburger tree automata (PTA) is PSPACE-complete, which is moderate given that it is already PSPACE-hard to test whether the complement of a regular expression is non-empty. We also identify a subclass of PTAs with a tractable non-emptiness problem. Further, to decide whether a tree t satisfies a formula φ is polynomial in the size of φ and linear in the size of t. A technical construction of independent interest is a linear time construction of a Presburger formula for the Parikh image of a regular language.",

author = "Helmut Seidl and Thomas Schwentick and Anca Muscholl and Peter Habermehl",

year = "2004",

doi = "10.1007/978-3-540-27836-8_94",

language = "English",

isbn = "3540228497",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

pages = "1136--1149",

editor = "Josep D{\'i}az and Juhani Karhum{\"a}ki and Arto Lepist{\"o} and Donald Sannella",

booktitle = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

}

Seidl, H, Schwentick, T, Muscholl, A & Habermehl, P 2004, Counting in trees for free. in J Díaz, J Karhumäki, A Lepistö & D Sannella (eds), Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 3142, Springer Verlag, pp. 1136-1149. https://doi.org/10.1007/978-3-540-27836-8_94

Counting in trees for free. / Seidl, Helmut; Schwentick, Thomas; Muscholl, Anca et al.
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). ed. / Josep Díaz; Juhani Karhumäki; Arto Lepistö; Donald Sannella. Springer Verlag, 2004. p. 1136-1149 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 3142).

Research output: Chapter in Book/Report/Conference proceeding › Chapter › peer-review

TY - CHAP

T1 - Counting in trees for free

AU - Seidl, Helmut

AU - Schwentick, Thomas

AU - Muscholl, Anca

AU - Habermehl, Peter

PY - 2004

Y1 - 2004

N2 - It is known that MSO logic for ordered unranked trees is undecidable if Presburger constraints are allowed at children of nodes. We show here that a decidable logic is obtained if we use a modal fixpoint logic instead. We present a characterization of this logic by means of deterministic Presburger tree automata and show how it can be used to express numerical document queries. Surprisingly, the complexity of satisfiability for the extended logic is asymptotically the same as for the original fixpoint logic. The non-emptiness for Presburger tree automata (PTA) is PSPACE-complete, which is moderate given that it is already PSPACE-hard to test whether the complement of a regular expression is non-empty. We also identify a subclass of PTAs with a tractable non-emptiness problem. Further, to decide whether a tree t satisfies a formula φ is polynomial in the size of φ and linear in the size of t. A technical construction of independent interest is a linear time construction of a Presburger formula for the Parikh image of a regular language.

AB - It is known that MSO logic for ordered unranked trees is undecidable if Presburger constraints are allowed at children of nodes. We show here that a decidable logic is obtained if we use a modal fixpoint logic instead. We present a characterization of this logic by means of deterministic Presburger tree automata and show how it can be used to express numerical document queries. Surprisingly, the complexity of satisfiability for the extended logic is asymptotically the same as for the original fixpoint logic. The non-emptiness for Presburger tree automata (PTA) is PSPACE-complete, which is moderate given that it is already PSPACE-hard to test whether the complement of a regular expression is non-empty. We also identify a subclass of PTAs with a tractable non-emptiness problem. Further, to decide whether a tree t satisfies a formula φ is polynomial in the size of φ and linear in the size of t. A technical construction of independent interest is a linear time construction of a Presburger formula for the Parikh image of a regular language.

UR - http://www.scopus.com/inward/record.url?scp=35048830938&partnerID=8YFLogxK

U2 - 10.1007/978-3-540-27836-8_94

DO - 10.1007/978-3-540-27836-8_94

M3 - Chapter

AN - SCOPUS:35048830938

SN - 3540228497

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 1136

EP - 1149

BT - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

A2 - Díaz, Josep

A2 - Karhumäki, Juhani

A2 - Lepistö, Arto

A2 - Sannella, Donald

PB - Springer Verlag

ER -

Seidl H, Schwentick T, Muscholl A, Habermehl P. Counting in trees for free. In Díaz J, Karhumäki J, Lepistö A, Sannella D, editors, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Springer Verlag. 2004. p. 1136-1149. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-540-27836-8_94

Counting in trees for free

Abstract

Publication series

Access to Document

Other files and links

Fingerprint

Cite this