Arrow Research search

Author name cluster

Thomas Schwentick

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

30 papers
2 author rows

Possible papers

30

MFCS Conference 2023 Conference Paper

Dynamic Constant Time Parallel Graph Algorithms with Sub-Linear Work

  • Jonas Schmidt 0001
  • Thomas Schwentick

The paper proposes dynamic parallel algorithms for connectivity and bipartiteness of undirected graphs that require constant time and 𝒪(n^{1/2+ε}) work on the CRCW PRAM model. The work of these algorithms almost matches the work of the 𝒪(log n) time algorithm for connectivity by Kopelowitz et al. (2018) on the EREW PRAM model and the time of the sequential algorithm for bipartiteness by Eppstein et al. (1997). In particular, we show that the sparsification technique, which has been used in both mentioned papers, can in principle also be used for constant time algorithms in the CRCW PRAM model, despite the logarithmic depth of sparsification trees.

MFCS Conference 2023 Conference Paper

On the Work of Dynamic Constant-Time Parallel Algorithms for Regular Tree Languages and Context-Free Languages

  • Jonas Schmidt 0001
  • Thomas Schwentick
  • Jennifer Todtenhoefer

Previous work on Dynamic Complexity has established that there exist dynamic constant-time parallel algorithms for regular tree languages and context-free languages under label or symbol changes. However, these algorithms were not developed with the goal to minimise work (or, equivalently, the number of processors). In fact, their inspection yields the work bounds 𝒪(n²) and 𝒪(n⁷) per change operation, respectively. In this paper, dynamic algorithms for regular tree languages are proposed that generalise the previous algorithms in that they allow unbounded node rank and leaf insertions, while improving the work bound from 𝒪(n²) to 𝒪(n^ε), for arbitrary ε > 0. For context-free languages, algorithms with better work bounds (compared with 𝒪(n⁷)) for restricted classes are proposed: for every ε > 0 there are such algorithms for deterministic context-free languages with work bound 𝒪(n^{3+ε}) and for visibly pushdown languages with work bound 𝒪(n^{2+ε}).

CSL Conference 2020 Conference Paper

Dynamic Complexity Meets Parameterised Algorithms

  • Jonas Schmidt 0001
  • Thomas Schwentick
  • Nils Vortmeier
  • Thomas Zeume
  • Ioannis Kokkinis

Dynamic Complexity studies the maintainability of queries with logical formulas in a setting where the underlying structure or database changes over time. Most often, these formulas are from first-order logic, giving rise to the dynamic complexity class DynFO. This paper investigates extensions of DynFO in the spirit of parameterised algorithms. In this setting structures come with a parameter k and the extensions allow additional "space" of size f(k) (in the form of an additional structure of this size) or additional time f(k) (in the form of iterations of formulas) or both. The resulting classes are compared with their non-dynamic counterparts and other classes. The main part of the paper explores the applicability of methods for parameterised algorithms to this setting through case studies for various well-known parameterised problems.

CSL Conference 2018 Conference Paper

The Ackermann Award 2018

  • Dexter Kozen
  • Thomas Schwentick

The Ackermann Award is the EACSL Outstanding Dissertation Award for Logic in Computer Science. It is presented during the annual conference of the EACSL (CSL'xx). This contribution reports on the 2018 edition of the award.

Highlights Conference 2016 Conference Abstract

Containment for Conjunctive Queries with Negation

  • With Bas Ketsman
  • Frank Neven
  • Thomas Schwentick

A query Q is contained in a query Q’ if, for every database D, the result Q(D) is contained in Q'(D). Deciding containment is an interesting and often used sub-problem for minimisation of queries, verification of dependencies and other tasks. It was shown that the containment of conjunctive queries is intimately related to the existence of a homomorphism between the queries and that deciding containment in this case is NP-complete [1]. We have shown that deciding containment for conjunctive queries _with negation_ is coNEXPTIME-complete in general [2]. Previously the problem seems only to have been studied for queries over schemas of bounded arity, where it was known to be Pi^p_2-complete [3]. PUBLICATION: This result has been published in [2] for the 19th International Conference on Database Theory, ICDT 2016, Bordeaux, France, March 15-18, 2016. REFERENCES [1] Ashok K. Chandra, Philip M. Merlin: Optimal Implementation of Conjunctive Queries in Relational Data Bases. STOC 1977: 77-90 [2] Gaetano Geck, Bas Ketsman, Frank Neven, Thomas Schwentick: Parallel-Correctness and Containment for Conjunctive Queries with Union and Negation. ICDT 2016: 9: 1-9: 17 [3] Marie-Laure Mugnier, Geneviève Simonet, Michaël Thomazo: On the complexity of entailment in existential conjunctive first-order logic with atomic negation. Inf. Comput. 215: 8-31 (2012)

Highlights Conference 2016 Conference Abstract

Dynamic descriptive complexity of FO-definable modifications

  • Thomas Schwentick
  • Nils Vortmeier
  • Thomas Zeume

A dynamic program, as introduced by Dong, Su and Topor and Patnaik and Immerman, maintains the result of a fixed query for an input database which is subject to modifications. It can use an auxiliary database whose relations are updated via first-order formulas upon modifications of the input database. In the original setting, only insertions and deletions of single tuples are considered. In this talk, which is based on joint work with Thomas Schwentick and Thomas Zeume, we will allow modifications defined by (restricted) first-order formulas and review which queries can still be maintained. This talk is based on so far unpublished work.

I&C Journal 2015 Journal Article

On the quantifier-free dynamic complexity of Reachability

  • Thomas Zeume
  • Thomas Schwentick

The dynamic complexity of the reachability query is studied in the dynamic complexity framework of Patnaik and Immerman, restricted to quantifier-free update formulas. It is shown that, with this restriction, the reachability query cannot be dynamically maintained, neither with binary auxiliary relations nor with unary auxiliary functions, and that ternary auxiliary relations are more powerful with respect to graph queries than binary auxiliary relations. Further inexpressibility results are given for the reachability query in a different setting as well as for a syntactical restriction of quantifier-free update formulas. Moreover inexpressibility results for some other queries are presented.

CSL Conference 2015 Conference Paper

Static Analysis for Logic-based Dynamic Programs

  • Thomas Schwentick
  • Nils Vortmeier
  • Thomas Zeume

The goal of dynamic programs as introduced by Patnaik and Immerman (1994) is to maintain the result of a fixed query for an input database which is subject to tuple insertions and deletions. To this end such programs store an auxiliary database whose relations are updated via first-order formulas upon modifications of the input database. One of those auxiliary relations is supposed to store the answer to the query. Several static analysis problems can be associated to such dynamic programs. Is the answer relation of a given dynamic program always empty? Does a program actually maintain a query? That is, is the answer given of the program the same when an input database was reached by two different modification sequences? Even more, is the content of auxiliary relations independent of the modification sequence that lead to an input database? We study the algorithmic properties of those and similar static analysis problems. Since all these problems can easily be seen to be undecidable for full first-order programs, we examine the exact borderline for decidability for restricted programs. Our focus is on restricting the arity of the input databases as well as the auxiliary databases, and to restrict the use of quantifiers.

Highlights Conference 2014 Conference Abstract

Invited talk: Aspects of Dynamic Complexity

  • Thomas Schwentick

In most real-life databases data changes frequently and thus makes efficient query answering challenging. Auxiliary data might help to avoid computing query answers from scratch all the time. One way to study this incremental maintenance scenario is from the perspective of dynamic algorithms with the goal to reduce (re-)computation time. Another option is to investigate it from the perspective of low-level parallel computational complexity [1] or parallelizable database queries [2]. As the lowest complexity class AC 0 (with a suitable unifomity condition) and the core of the standard database query language SQL both coincide with first-order predicate logic, one naturally arrives at the question which queries can be answered/maintained dynamically with first-order predicate logic (DynFO). The most prominent open question in Dynamic Complexity is whether the reachability query on graphs (arguably the simplest recursive query) can be maintained in DynFO. It has been shown that it can be maintained in DynFO on undirected [1] or acyclic directed graphs [2] and on directed embedded planar graphs [3], but the general case remains open. Further results in [3] indicate that reachability on graphs might be maintainable in DynFO, after all. Despite considerable effort in recent years, showing that a given query can not be maintained in DynFO is a very challenging problem, for which currently no methods are available. Furthermore, even though AC 0 is a small complexity class in the static setting, first-order logic is already quite powerful in the dynamic world. These two observations have recently led to the study of fragments of DynFO, e. g. , by restricting or forbidding quantification, with the idea to start developing inexpressibility tools there. The talk will give an introduction into dynamic complexity, survey some of itsmost important results, and report about recent work on fragments of DynFO. Sushant Patnaik and Neil Immerman. Dyn-FO: A parallel, dynamic complexity class. J. Comput. Syst. Sci. , 55(2): 199--209, 1997. Guozhu Dong and Jianwen Su. Incremental and decremental evaluation of transitive closure by first-order queries. Inf. Comput. , 120(1): 101--106, 1995. Samir Datta, William Hesse and Raghav Kulkarni. Dynamic Complexity of Directed Reachability and Other Problems. ICALP 2014. 15: 30 15: 45 Coffee Break

AIJ Journal 2014 Journal Article

The price of query rewriting in ontology-based data access

  • Georg Gottlob
  • Stanislav Kikot
  • Roman Kontchakov
  • Vladimir Podolskii
  • Thomas Schwentick
  • Michael Zakharyaschev

We give a solution to the succinctness problem for the size of first-order rewritings of conjunctive queries in ontology-based data access with ontology languages such as OWL 2 QL, linear Datalog ± and sticky Datalog ±. We show that positive existential and nonrecursive datalog rewritings, which do not use extra non-logical symbols (except for intensional predicates in the case of datalog rewritings), suffer an exponential blowup in the worst case, while first-order rewritings can grow superpolynomially unless NP ⊆ P / poly. We also prove that nonrecursive datalog rewritings are in general exponentially more succinct than positive existential rewritings, while first-order rewritings can be superpolynomially more succinct than positive existential rewritings. On the other hand, we construct polynomial-size positive existential and nonrecursive datalog rewritings under the assumption that any data instance contains two fixed constants.

MFCS Conference 2013 Conference Paper

On the Quantifier-Free Dynamic Complexity of Reachability

  • Thomas Zeume
  • Thomas Schwentick

Abstract The dynamic complexity of the reachability query is studied in the dynamic complexity framework of Patnaik and Immerman, restricted to quantifier-free update formulas. It is shown that, with this restriction, the reachability query cannot be dynamically maintained, neither with binary auxiliary relations nor with unary auxiliary functions, and that ternary auxiliary relations are more powerful with respect to graph queries than binary auxiliary relations. Further results are obtained including more inexpressibility results for reachability in a different setting, inexpressibility results for some other queries and normal forms for quantifier-free update programs.

MFCS Conference 2013 Conference Paper

Validity of Tree Pattern Queries with Respect to Schema Information

  • Henrik Björklund
  • Wim Martens
  • Thomas Schwentick

Abstract We prove that various containment and validity problems for tree pattern queries with respect to a schema are EXPTIME-complete. When one does not require the root of a tree pattern query to match the root of a tree, validity of a non-branching tree pattern query with respect to a Relax NG schema or W3C XML Schema is already EXPTIME-hard when the query does not branch and uses only child axes. These hardness results already hold when the alphabet size is fixed. Validity with respect to a DTD is proved to be EXPTIME-hard already when the query only uses child axes and is allowed to branch only once.

KR Conference 2012 Conference Paper

Rewriting Ontological Queries into Small Nonrecursive Datalog Programs

  • Georg Gottlob
  • Thomas Schwentick

with tractable query-answering have been designed, including OWL 2 QL (Grau et al. 2008; Pérez-Urbina, Horrocks, and Motik 2009), which is an OWL-based equivalent of the description logic DL-LiteR (Calvanese et al. 2007). While experimental and commercial ontological database management systems have existed and have been used for a number of years (e. g. (Chong et al. 2005; Acciarri et al. 2005; Virgilio et al. 2011)), they have been problematic with respect to performance, and there is an agreement that ontological query optimization methods have not yet been developed to their full potential. In fact, there is a general feeling that many issues of ontology querying are still not well understood, and that deep theoretical research is necessary to better understand some fundamental issues of query rewriting. In this spirit, the present paper tries to shed light on a relevant problem in this context: Is it at all possible to translate an ontological conjunctive query into a polynomially sized SQL (or SQL-DDL) query? We consider the setting of ontological database access, where an A-box is given in form of a relational database D and where a Boolean conjunctive query q has to be evaluated against D modulo a T -box Σ formulated in DL-Lite or Linear Datalog±. It is well-known that (Σ, q) can be rewritten into an equivalent nonrecursive Datalog program P that can be directly evaluated over D. However, for Linear Datalog± or for DL-Lite versions that allow for role inclusion, the rewriting methods described so far result in a nonrecursive Datalog program P of size exponential in the joint size of Σ and q. This gives rise to the interesting question of whether such a rewriting necessarily needs to be of exponential size. In this paper we show that it is actually possible to translate (Σ, q) into a polynomially sized equivalent nonrecursive Datalog program P. 1 1. 1

TCS Journal 2010 Journal Article

On notions of regularity for data languages

  • Henrik Björklund
  • Thomas Schwentick

With motivation from considerations in XML database theory and model checking, data strings have been introduced as an extension of finite alphabet strings which carry, at each position, a symbol and a data value from an infinite domain. Previous work has shown that it is difficult to come up with an expressive yet decidable automaton model for data languages. Recently, such a model, data automata, was introduced. This paper introduces a simpler but equivalent model and investigates its expressive power, algorithmic and closure properties, and some extensions.

CSL Conference 2010 Conference Paper

Two-Variable Logic with Two Order Relations - (Extended Abstract)

  • Thomas Schwentick
  • Thomas Zeume

Abstract The finite satisfiability problem for two-variable logic over structures with unary relations and two order relations is investigated. Firstly, decidability is shown for structures with one total preorder relation and one linear order relation. More specifically, we show that this problem is complete for EXPSPACE. As a consequence, the same upper bound applies to the case of two linear orders. Secondly, we prove undecidability for structures with two total preorder relations as well as for structures with one total preorder and two linear order relations. Further, we point out connections to other logics. Decidability is shown for two-variable logic on data words with orders on both positions and data values, but without a successor relation. We also study ”partial models” of compass and interval temporal logic and prove decidability for some of their fragments.

MFCS Conference 2009 Conference Paper

On the Hybrid Extension of CTL and CTL +

  • Ahmet Kara 0002
  • Volker Weber
  • Martin Lange 0001
  • Thomas Schwentick

Abstract The paper studies the expressivity, relative succinctness and complexity of satisfiability for hybrid extensions of the branching-time logics CTL and CTL + by variables. Previous complexity results show that only fragments with one variable do have elementary complexity. It is shown that H 1 CTL + and H 1 CTL, the hybrid extensions with one variable of CTL + and CTL, respectively, are expressively equivalent but H 1 CTL + is exponentially more succinct than H 1 CTL. On the other hand, HCTL +, the hybrid extension of CTL with arbitrarily many variables does not capture CTL ⋆, as it even cannot express the simple CTL ⋆ property EGF p. The satisfiability problem for H 1 CTL + is complete for triply exponential time, this remains true for quite weak fragments and quite strong extensions of the logic.

MFCS Conference 2008 Conference Paper

Optimizing Conjunctive Queries over Trees Using Schema Information

  • Henrik Björklund
  • Wim Martens
  • Thomas Schwentick

Abstract We study the containment, satisfiability, and validity problems for conjunctive queries over trees with respect to a schema. We show that conjunctive query containment and validity are 2EXPTIME-complete w. r. t. a schema (DTD or Relax NG). Furthermore, we show that satisfiability for conjunctive queries w. r. t. a schema can be decided in NP. The problem is NP-hard already for queries using only one kind of axis. Finally, we consider conjunctive queries that can test for equalities and inequalities of data values. Here, satisfiability and validity are decidable, but containment is undecidable, even without schema information. On the other hand, containment w. r. t. a schema becomes decidable again if the “larger” query is not allowed to use both equalities and inequalities.

MFCS Conference 2004 Conference Paper

Complexity of Decision Problems for Simple Regular Expressions

  • Wim Martens
  • Frank Neven
  • Thomas Schwentick

Abstract We study the complexity of the inclusion, equivalence, and intersection problem for simple regular expressions arising in practical XML schemas. These basically consist of the concatenation of factors where each factor is a disjunction of strings possibly extended with ‘*’ or ‘? ’. We obtain lower and upper bounds for various fragments of simple regular expressions. Although we show that inclusion and intersection are already intractable for very weak expressions, we also identify some tractable cases. For equivalence, we only prove an initial tractability result leaving the complexity of more general cases open. The main motivation for this research comes from database theory, or more specifically XML and semi-structured data. We namely show that all lower and upper bounds for inclusion and equivalence, carry over to the corresponding decision problems for extended context-free grammars and single-type tree grammars, which are abstractions of DTDs and XML Schemas, respectively. For intersection, we show that the complexity only carries over for DTDs.

I&C Journal 2003 Journal Article

On the power of tree-walking automata

  • Frank Neven
  • Thomas Schwentick

Tree-walking automata (TWAs) recently received new attention in the fields of formal languages and databases. To achieve a better understanding of their expressiveness, we characterize them in terms of transitive closure logic formulas in normal form. It is conjectured by Engelfriet and Hoogeboom that TWAs cannot define all regular tree languages, or equivalently, all of monadic second-order logic. We prove this conjecture for a restricted, but powerful, class of TWAs. In particular, we show that 1-bounded TWAs, that is TWAs that are only allowed to traverse every edge of the input tree at most once in every direction, cannot define all regular languages. We then extend this result to a class of TWAs that can simulate first-order logic (FO) and is capable of expressing properties not definable in FO extended with regular path expressions; the latter logic being a valid abstraction of current query languages for XML and semistructured data.

TCS Journal 2002 Journal Article

Query automata over finite trees

  • Frank Neven
  • Thomas Schwentick

A main task in document transformation and information retrieval is locating subtrees satisfying some pattern. Therefore, unary queries, i. e. , queries that map a tree to a set of its nodes, play an important role in the context of structured document databases. The motivation of this work is to understand how the natural and well-studied computation model of tree automata can be used to compute such queries. We define a query automaton (QA) as a deterministic two-way finite automaton over trees that has the ability to select nodes depending on the state and the label at those nodes. We study QAs over ranked as well as over unranked trees. Unranked trees differ from ranked ones in that there is no bound on the number of children of nodes. We characterize the expressiveness of the different formalisms as the unary queries definable in monadic second-order logic (MSO). In contrast to the ranked case, special stay transitions had to be added to QAs over unranked trees to capture MSO. We establish the complexity of the non-emptiness, containment, and equivalence of QAs to be complete for EXPTIME.

MFCS Conference 2001 Conference Paper

Towards Regular Languages over Infinite Alphabets

  • Frank Neven
  • Thomas Schwentick
  • Victor Vianu

Abstract Motivated by formal models recently proposed in the context of XML, we study automata and logics on strings over infinite alphabets. These are conservative extensions of classical automata and logics defining the regular languages on finite alphabets. Specifically, we consider register and pebble automata, and extensions of first-order logic and monadic second-order logic. For each type of automaton we consider oneway and two-way variants, as well as deterministic, non-deterministic, and alternating control. We investigate the expressiveness and complexity of the automata, their connection to the logics, as well as standard decision problems.

STOC Conference 2001 Conference Paper

When is the evaluation of conjunctive queries tractable?

  • Martin Grohe
  • Thomas Schwentick
  • Luc Segoufin

The evaluation of conjunctive queries is hard both with respect to its combined complexity (NP-complete) and its parameterized complexity (W[1]-complete). It becomes tractable (PTIME for combined complexity, FPT for parameterized complexity), when the underlying graphs of the conjunctive queries have bounded tree-width [2]. We show that, in some sense, this is optimal both with respect to combined and parameterized complexity: For every class C of graphs, the evaluation of all conjunctive queries whose underlying graph is in C is tractable if, and only if, C has bounded tree-width. A technical result of independent interest is that the colored grid homomorphism problem is NP-complete and, if parameterized by the grid size, W[1]-complete.

FOCS Conference 2000 Conference Paper

Existential Second-Order Logic over Graphs: Charting the Tractability Frontier

  • Georg Gottlob
  • Phokion G. Kolaitis
  • Thomas Schwentick

Fagin's (1974) theorem, the first important result of descriptive complexity, asserts that a property of graphs is in NP if and only if it is definable by an existential second-order formula. We study the complexity of evaluating existential second-order formulas that belong to prefix classes of existential second-order logic, where a prefix class is the collection of all existential second-order and the first-order quantifiers obey a certain quantifier pattern. We completely characterize the computation complexity of prefix classes of existential second-order logic in three different contexts: over directed graphs; over undirected graphs with self-loops; and over undirected graphs without self-loops. Our main result is that in each of these three contexts a dichotomy holds, i. e. , each prefix class of existential second-order logic either contains sentences that can express NP-complete problems or each of its sentences expresses a polynomial-time solvable problem. Although the boundary of the dichotomy coincides for the first two cases, it changes, as one move to undirected graphs without self-loops.

MFCS Conference 2000 Conference Paper

On Diving in Trees

  • Thomas Schwentick

Abstract The paper is concerned with queries on tree-structured data. It defines fragments of first-order logic (FO) and FO extended by regular expressions along paths. These fragments have the same expressive power as the full logics themselves. On the other hand, they can be evaluated reasonably efficient, even if the formula which represents the query is considered as part of the input.

CSL Conference 1999 Invited Paper

Descriptive Complexity, Lower Bounds and Linear Time

  • Thomas Schwentick

Abstract This paper surveys two related lines of research: Logical characterizations of (non-deterministic) linear time complexity classes, and non-expressibility results concerning sublogics of existential second-order logic. Starting from Fagin’s fundamental work there has been steady progress in both fields with the effect that the weakest logics that are used in characterizations of linear time complexity classes are closely related to the strongest logics for which inexpressibility proofs for concrete problems have been obtained. The paper sketches these developments and highlights their connections as well as the obstacles that prevent us from closing the remaining gap between both kinds of logics.

MFCS Conference 1998 Conference Paper

Locality of Order-Invariant First-Order Formulas

  • Martin Grohe
  • Thomas Schwentick

Abstract A query is local if the decision of whether a tuple in a structure satisfies this query only depends on a small neighborhood of the tuple. We prove that all queries expressible by order-invariant first-order formulas are local.

CSL Conference 1998 Conference Paper

Padding and the Expressive Power of Existential Second-Order Logics

  • Thomas Schwentick

Abstract Padding techniques are well-known from Computational Complexity Theory. Here, an analogous concept is considered in the context of existential second-order logics. Informally, a graph H is a padded version of a graph G, if H consists of an isomorphic copy of G and some isolated vertices. A set A of graphs is called weakly expressible by a formula ϕ in the presence of padding, if ϕ is able to distinguish between (sufficiently) padded versions of graphs from A and padded versions of graphs that are not in A. From results of Lynch [Lyn82, Lyn92] it can be easily concluded that (essentially) every NP -set of graphs is weakly expressible by an existential monadic second-order (Monσ 1 1 ) sentence with polynomial padding and built-in addition. In particular, NP ≠ coNP if and only if there is a coNP -set of graphs that is not weakly expressible by a Monσ 1 1 -formula in the presence of addition, even if polynomial padding is allowed. In some sense, this implies that Monσ 1 1 is well suited to investigate the NP vs. coNP question. In this paper, it is shown, that - in the above statements, addition can be replaced by two unary functions, by built-in relations of degree O(n ε ), for every ε > 0, and by built-in relations with at most (1 + ε) n edges, respectively; - on the other hand, Monσ 1 1 with built-in relations of degree n° (l) or with n + n° (l) edges is weak, in the sense that not every P -set of graphs is weakly expressible with polynomial padding in this logic; - Monσ 1 1 with a built-in linear order or built-in coloured trees is very weak, in the sense that they are weak and padding does not increase their expressive power at all. Corresponding results are shown for several sublogics of binary σ 1 1.

CSL Conference 1995 Conference Paper

Logics For Context-Free Languages

  • Clemens Lautemann
  • Thomas Schwentick
  • Denis Thérien

Abstract We define matchings, and show that they capture the essence of context-freeness. More precisely, we show that the class of context-free languages coincides with the class of those sets of strings which can be defined by sentences of the form ∃ bϕ, where ϕ is first order, b is a binary predicate symbol, and the range of the second order quantifier is restricted to the class of matchings. Several variations and extensions are discussed.

FOCS Conference 1994 Conference Paper

Graph Connectivity and Monadic NP

  • Thomas Schwentick

Ehrenfeucht games are a useful tool in proving that certain properties of finite structures are not expressible by formulas of a certain type. In this paper a new method is introduced that allows the extension of a local winning strategy for Duplicator, one of the two players in Ehrenfeucht games, to a global winning strategy. As an application it is shown that graph connectivity cannot be expressed by existential second-order formulas, where the second-order quantification is restricted to unary relations (monadic NP), even, in the presence of a built-in linear order. As a second application it is stated, that, on the other hand, the presence of a linear order increases the power of monadic NP more than the presence of a successor relation. >

v2026.09.13