Existential second-order logic over strings
Loading...
Date
Advisors/Reviewers
Further Contributors
Contributing Institutions
Publisher
Journal Title
Journal ISSN
Volume Title
Publisher
License
Quotable link
Abstract
Existential secondorder logic (ESO) and monadic secondorder logic (MSO) have attracted much interest in logic and computer science. ESO is a much more expressive logic over word structures than MSO. However, little was known about the relationship between MSO and syntactic fragments of ESO. We shed light on this issue by completely characterizing this relationship for the prefix classes of ESO over strings, (i.e., finite word structures). Moreover, we determine the complexity of model checking over strings, for all ESOprefix classes. Let ESO(Q) denote the prefix class containing all sentences of the shape 9RQ' where R is a list of predicate variables, Q is a firstorder quantifier prefix from the prefix set Q, and ' is quantifier free. We show that ESO(9 \Lambda 89 \Lambda ) and ESO(9 \Lambda 88) are the maximal standard ESOprefix classes contained in MSO, thus expressing only regular languages. We further prove the following dichotomy theorem: An ESO prefixclass either expresses only regular languages (and is thus in MSO), or it expresses some NPcomplete languages. We also give a precise characterization of those ESOprefix classes which are equivalent to MSO over strings, and of the ESOprefix classes which are closed under complementation on strings.Link to publications or other datasets
Description
Notes
Original publication in
Original publication in
Anthology
Collections
URI of original publication
Forschungsdaten
Series
IFIG Research Report; 9702 / 1997