FB 07 - Mathematik und Informatik, Physik, Geographie

Dauerhafte URI für den Bereich

jlupub.ub.uni-giessen.de/handle/jlupub/1037

Stöbern nach

Auflistung FB 07 - Mathematik und Informatik, Physik, Geographie nach Autor:in "Gottlob, Georg"

Gerade angezeigt 1 - 2 von 2
  • Vorschaubild
    Item
    Enhancing symbolic model checking by AI techniques
    (1997) Buccafurri, Francesco; Eiter, Thomas; Gottlob, Georg; Leone, Nicola
    Comparisons of different cellular devices and the investigation of their computing power can be made in terms of their capabilities to time­construct and time­compute functions. Time­construction means that a distinguished cell has to enter distinguished states exactly at the time steps f(1); f(2); : : :, whereas time­computation requires the distinguished cell to enter a distinguished state firstly at time step f(n), where n is the length of the input. Here the family of functions which are time­constructible by a two­way unbounded cellular space (F(CS)) is characterized in terms of functions which are time­computable by one of the simplest cellular devices, a one­way bounded cellular automaton (C (OCA)). Conceptually, time­constructible functions have to be strictly increasing. Regarding that restriction the reverse characterization is shown, too. Some results concerning the structure of F(CS) and C(OCA) and their relation to formal language recognition are established.
  • Vorschaubild
    Item
    Existential second-order logic over strings
    (1997) Eiter, Thomas; Gottlob, Georg; Gurevich, Yuri
    Existential second­order logic (ESO) and monadic second­order 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 ESO­prefix 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 first­order 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 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 which are equivalent to MSO over strings, and of the ESO­prefix classes which are closed under complementation on strings.