Thumbnail
Access Restriction
Subscribed

Author Eiter, Thomas ♦ Gottlob, Georg ♦ Gurevich, Yuri
Source ACM Digital Library
Content type Text
Publisher Association for Computing Machinery (ACM)
File Format PDF
Copyright Year ©2000
Language English
Subject Domain (in DDC) Computer science, information & general works ♦ Data processing & computer science
Subject Keyword NP ♦ S1S ♦ Decision problem ♦ Descriptive complexity ♦ Existential fragment ♦ Finite model theory ♦ Finite satisfiability ♦ Finite words ♦ Model checking ♦ Prefix classes ♦ Regular languages ♦ Second-order logic ♦ Strings
Abstract Existential second-order logic (ESO) and monadic second-order logic(MSO) have attracted much interest in logic and computer science. ESO is a much expressive logic over successor structures than MSO. However, little was known about the relationship between MSOand syntatic 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 successor structures). Moreover, we determine the complexity of model checking over strings, for all ESO-prefix classes. Let ESO( Q ) are the maximal standard ESO-prefix classes contained in MSO, thus expressing only regular languages. We further prove the following dichotomy theorem: An ESO prefix-class either expresses only regular languages (and is thus in MSO), or it expresses some NP-complete languages. We also give a precise characterization of those ESO-prefix classes that are $\textit{equivalent}$ to MSO over strings, and of the ESO-prefix classes which are closed under complementation on strings.
ISSN 00045411
Age Range 18 to 22 years ♦ above 22 year
Educational Use Research
Education Level UG and PG
Learning Resource Type Article
Publisher Date 2000-01-01
Publisher Place New York
e-ISSN 1557735X
Journal Journal of the ACM (JACM)
Volume Number 47
Issue Number 1
Page Count 55
Starting Page 77
Ending Page 131


Open content in new tab

   Open content in new tab
Source: ACM Digital Library