Arrow Research search

Author name cluster

Wolfgang Thomas

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.

19 papers
2 author rows

Possible papers

19

Highlights Conference 2024 Conference Abstract

On the Finiteness of Infinite Regular Games

  • Wolfgang Thomas

Starting with McNaughton’s pioneering technical report of 1965 in which he initiated the automata theoretic study of infinite games, we pursue his view that plays of an infinite game should terminate in finite time with the correct declaration of the winner. Such a reduction of regular infinite games to reachability games or safety games is well-known, for example, in the study of parity games. We focus on this reduction for Muller games (reporting on work of D. Neider, R. Rabinovich, M. Zimmermann, Aachen) which offers a so far unexploited player-dependent approach for solving Muller games, based on a new kind of memory structure and avoiding the step through parity games. We conclude with a more general discussion of determinacy proofs for infinite games, motivated by Büchi’s difficult last paper that has not received attention since it appeared in 1983.

Details

CSL Conference 2017 Conference Paper

Determinacy of Infinite Games: Perspectives of the Algorithmic Approach (Invited Talk)

  • Wolfgang Thomas

Determinacy of infinite two-player games is a topic of descriptive set theory that has triggered intensive research in theoretical computer science since 1957 when A. Church formulated his "synthesis problem" (regarding the construction of circuits with infinite behavior from logical specifications). In the first part of the lecture we review the fascinating development of the algorithmic theory of infinite games that was started by Church's problem, that enriched automata theory and related fields, and that led to interesting applications in verification and program synthesis. In the second part we turn to the question how to lift this theory from the case of the Cantor space (where a play is a sequence of bits) to the case of the Baire space (where a play is a sequence of natural numbers). While this step does not involve difficulties in classical descriptive set theory, the algorithmic approach raises non-trivial questions since it requires to consider automata that work over infinite alphabets. We present recent results (joint work with B. Brütsch) that provide a solution of Church's synthesis problem in this context, and we point to numerous questions that are still open.

Details

Highlights Conference 2016 Conference Abstract

Playing Games in the Baire Space

  • Benedikt Brütsch
  • Wolfgang Thomas

We solve a generalized version of Church’s synthesis problem where the alphabet is not a finite set like {0, 1} but the set of natural numbers. This amounts to solving a Gale-Stewart game where a play is a sequence of natural numbers (chosen in alternation by two players Input and Output) rather than a sequence of bits; so a play is an element of the Baire space rather than of the Cantor space. To represent the winning condition L ⊆ ℕ^ω for player Output, we present a natural model of automata (“ℕ-memory automata”) equipped with the parity acceptance condition, and we introduce also the corresponding model of “ℕ-memory transducers”. We show that for games specified by ℕ-memory automata, it is decidable whether player Output has a winning strategy, and that in this case an ℕ-memory transducer can be constructed that implements a winning strategy for player Output. This talk is based on the following paper: Benedikt Brütsch and Wolfgang Thomas: Playing Games in the Baire Space. To appear in Proceedings of the Cassting Workshop on Games for the Synthesis of Complex Systems (Cassting 2016).

Details

TCS Journal 2013 Journal Article

Connectivity games over dynamic networks

  • Sten Grüner
  • Frank G. Radmacher
  • Wolfgang Thomas

A game-theoretic model for the study of dynamic networks is proposed and analyzed. The model is motivated by communication networks that are subject to failure of nodes and where the restoration needs resources. The corresponding two-player game is played between “Destructor” (who can delete nodes) and “Constructor” (who can restore or even create nodes under certain conditions). We also include the feature of information flow by allowing Constructor to change labels of adjacent nodes. As an objective for Constructor the network property to be connected is considered, either as a safety condition or as a reachability condition (in the latter case starting from a non-connected network). We show under which conditions the solvability of the corresponding games for Constructor is decidable, and in this case obtain upper and lower complexity bounds, as well as algorithms derived from winning strategies. Due to the asymmetry between the players, safety and reachability objectives are not dual to each other and are treated separately.

Details DOI

GandALF Workshop 2011 Workshop Paper

Connectivity Games over Dynamic Networks

  • Sten Grüner
  • Frank G. Radmacher
  • Wolfgang Thomas

A game-theoretic model for the study of dynamic networks is analyzed. The model is motivated by communication networks that are subject to failure of nodes and where the restoration needs resources. The corresponding two-player game is played between "Destructor" (who can delete nodes) and "Constructor" (who can restore or even create nodes under certain conditions). We also include the feature of information flow by allowing Constructor to change labels of adjacent nodes. As objective for Constructor the network property to be connected is considered, either as a safety condition or as a reachability condition (in the latter case starting from a non-connected network). We show under which conditions the solvability of the corresponding games for Constructor is decidable, and in this case obtain upper and lower complexity bounds, as well as algorithms derived from winning strategies. Due to the asymmetry between the players, safety and reachability objectives are not dual to each other and are treated separately.

PDF Details DOI

GandALF Workshop 2010 Invited Paper

Infinite Games: Tema con Due Variazioni

  • Wolfgang Thomas

RWTH Aachen, Lehrstuhl für Informatik 7, D-52056 Aachen thomas@automata. rwth-aachen. de The original setting of Church's Problem on the solvability of regular infinite games has been varied in a great number of ways. In this talk we discuss two variations that were touched already in early research on Church's problem and have been revived in recent work. The first variation is concerned with the relation between game specifications and winning strategies, starting from the observation that regular (or: MSO-definable) infinite games are solvable with "regular" (or again MSO-definable) winning strategies. Such a close connection can be established also for other notions of definability, either in terms of logics or in terms of types of automata. We present recent results and some perspectives. The second variation addresses a widening of the concept of strategy, taking up the classical view that a strategy in an infinite game defines a special kind of continuous function over omega-sequences. We study the question of solvability of games with strategies that represent different degrees of continuity. This discussion leads naturally to generalized versions of concurrent games. We present basic results and indicate applications in discrete control. (The first part reports on joint work with A. Rabinovich, J. Olschewski, and W. Fridman, the second part on joint work with M. Holtmann, L. Kaiser, and F. Pöttgen. )

Details DOI

CSL Conference 2008 Invited Paper

Model Transformations in Decidability Proofs for Monadic Theories

  • Wolfgang Thomas

Abstract We survey two basic techniques for showing that the monadic second-order theory of a structure is decidable. In the first approach, one deals with finite fragments of the theory (given for example by the restriction to formulas of a certain quantifier rank) and – depending on the fragment – reduces the model under consideration to a simpler one. In the second approach, one applies a global transformation of models while preserving decidability of the theory. We suggest a combination of these two methods.

Details

CSL Conference 2007 Conference Paper

Logical Refinements of Church's Problem

  • Alexander Rabinovich
  • Wolfgang Thomas

Abstract Church’s Problem (1962) asks for the construction of a procedure which, given a logical specification ϕ on sequence pairs, realizes for any input sequence X an output sequence Y such that ( X, Y ) satisfies ϕ. Büchi and Landweber (1969) gave a solution for MSO specifications in terms of finite-state automata. We address the problem in a more general logical setting where not only the specification but also the solution is presented in a logical system. Extending the result of Büchi and Landweber, we present several logics \({\cal L}\) such that Church’s Problem with respect to \({\cal L}\) has also a solution in \({\cal L}\), and we discuss some perspectives of this approach.

Details

CSL Conference 2006 Conference Paper

Decidable Theories of the Ordering of Natural Numbers with Unary Predicates

  • Alexander Rabinovich
  • Wolfgang Thomas

Abstract Expansions of the natural number ordering by unary predicates are studied, using logics which in expressive power are located between first-order and monadic second-order logic. Building on the model-theoretic composition method of Shelah, we give two characterizations of the decidable theories of this form, in terms of effectiveness conditions on two types of “homogeneous sets”. We discuss the significance of these characterizations, show that the first-order theory of successor with extra predicates is not covered by this approach, and indicate how analogous results are obtained in the semigroup theoretic and the automata theoretic framework.

Details

MFCS Conference 2003 Invited Paper

Constructing Infinite Graphs with a Decidable MSO-Theory

  • Wolfgang Thomas

Abstract This introductory paper reports on recent progress in the search for classes of infinite graphs where interesting model-checking problems are decidable. We consider properties expressible in monadic second-order logic (MSO-logic), a formalism which encompasses standard temporal logics and the modal μ -calculus. We discuss a class of infinite graphs proposed by D. Caucal (in MFCS 2002) which can be generated from the infinite binary tree by applying the two processes of MSO-interpretation and of unfolding. The main purpose of the paper is to give a feeling for the rich landscape of infinite structures in this class and to point to some questions which deserve further study.

Details

TCS Journal 2003 Journal Article

Uniform and nonuniform recognizability

  • Wolfgang Thomas

Deterministic and nondeterministic finite-state recognizability over finite structures are introduced in an algebraic setting, avoiding detailed computational conventions as needed in the definition of finite-state acceptors. For deterministic recognizability, the classical approach is adopted, using a “uniform” homomorphism from the input domain (consisting of terms) into a finite algebra. For the nondeterministic case, we refer to relational input structures and to an acceptance via relational homomorphisms (which are applied “nonuniformly” since they depend on the input structures). We show how this approach encompasses known models of nondeterministic automata over finite words, trees, pictures, and graphs, and present some elementary metaresults connecting uniform recognizability, nonuniform recognizability, and monadic second-order logic.

Details DOI

CSL Conference 2002 Conference Paper

Solving Pushdown Games with a Sigma 3 Winning Condition

  • Thierry Cachat
  • Jacques Duparc
  • Wolfgang Thomas

Abstract We study infinite two-player games over pushdown graphs with a winning condition that refers explicitly to the infinity of the game graph: A play is won by player 0 if some vertex is visited infinity often during the play. We show that the set of winning plays is a proper ∑ 3 -set in the Borel hierarchy, thus transcending the Boolean closure of ∑ 2 -sets which arises with the standard automata theoretic winning conditions (such as the Muller, Rabin, or parity condition). We also show that this ∑ 3 -game over pushdown graphs can be solved effectively (by a computation of the winning region of player 0 and his memoryless winning strategy). This seems to be a first example of an effectively solvable game beyond the second level of the Borel hierarchy.

Details

I&C Journal 2002 Journal Article

The Monadic Quantifier Alternation Hierarchy over Grids and Graphs

  • Oliver Matz
  • Nicole Schweikardt
  • Wolfgang Thomas

The monadic second-order quantifier alternation hierarchy over the class of finite graphs is shown to be strict. The proof is based on automata theoretic ideas and starts from a restricted class of graph-like structures, namely finite two-dimensional grids. Considering grids where the width is a function of the height, we prove that the difference between the levels k+1 and k of the monadic hierarchy is witnessed by a set of grids where this function is (k+1)-fold exponential. We then transfer the hierarchy result to the class of directed (or undirected) graphs, using an encoding technique called strong reduction. It is notable that one can obtain sets of graphs which occur arbitrarily high in the monadic hierarchy but are already definable in the first-order closure of existential monadic second-order logic. We also verify that these graph properties even belong to the complexity class NLOG, which indicates a profound difference between the monadic hierarchy and the polynomial hierarchy.

Details DOI

I&C Journal 2002 Journal Article

The Monadic Theory of Morphic Infinite Words and Generalizations

  • Olivier Carton
  • Wolfgang Thomas

We present new examples of infinite words which have a decidable monadic theory. Formally, we consider structures 〈N, <, P〉 which expand the ordering 〈N, <〉 of the natural numbers by a unary predicate P; the corresponding infinite word is the characteristic 0-1-sequence x P of P. We show that for a morphic predicate P the associated monadic second-order theory MTh〈N, <, P〉 is decidable, thus extending results of Elgot and Rabin (1966) and Maes (1999). The solution is obtained in the framework of semigroup theory, which is then connected to the known automata theoretic approach of Elgot and Rabin. Finally, a large class of predicates P is exhibited such that the monadic theory MTh〈N, <, P〉 is decidable, which unifies and extends the previously known examples.

Details DOI

MFCS Conference 2000 Conference Paper

The Monadic Theory of Morphic Infinite Words and Generalizations

  • Olivier Carton
  • Wolfgang Thomas

Abstract We present new examples of infinite words which have a decidable monadic theory. Formally, we consider structures 〈ℕ, < P 〉 which expand the ordering 〈ℕ, <〉 of the natural numbers by a unary predicate P; the corresponding infinite word is the characteristic 0-1-sequence xP of P. We show that for a morphic predicate P the associated monadic second-order theory MThhℕ, < P 〉 is decidable, thus extending results of Elgot and Rabin (1966) and Maes (1999). The solution is obtained in the framework of semigroup theory, which is then connected to the known automata theoretic approach of Elgot and Rabin. Finally, a large class of predicates P is exhibited such that the monadic theory MTh〈ℕ〈, P 〉 is decidable, which unifies and extends the previously known examples.

Details

I&C Journal 1996 Journal Article

Monadic Second-Order Logic over Rectangular Pictures and Recognizability by Tiling Systems

  • Dora Giammarresi
  • Antonio Restivo
  • Sebastian Seibert
  • Wolfgang Thomas

It is shown that a set of pictures (rectangular arrays of symbols) is recognized by a finite tiling system iff it is definable in existential monadic second-order logic. As a consequence, finite tiling systems constitute a notion of recognizability over two-dimensional inputs which at the same time generalizes finite-state recognizability over strings and also matches a natural logic. The proof is based on the Ehrenfeucht–Fraı̈ssé technique for first-order logic and an implementation of “threshold counting” within tiling systems.

Details DOI

TCS Journal 1992 Journal Article

Infinite trees and automaton- definable relations over ω-words

  • Wolfgang Thomas

We study relations over ω-words using a representation by tree languages. An ω-word over an alphabet with k letters is considered as a path through the k-ary tree, an n-tuple of ω-words as an n-tuple of paths (coded by an appropriate valuation of the k-ary tree using values in {0, 1} n ), and a relation over ω-words as a tree language. In the first part of the paper we give a logical characterization of the “Rabin-recognizable relations” (whose associated tree languages are recognized by Rabin tree automata) in terms of “weak chain logic”, a restriction of monadic second-order logic over trees. In the second part of the paper an extended logic is considered, obtained by adjoining the “equal-level predicate” over trees. We describe the class of relations over ω-words which (in the tree language representation) are definable in this logic, and show that the theory of the k-ary tree in this logic is decidable. It covers tree properties which are not expressible in the monadic second-order logic SkS.

Details DOI

TCS Journal 1981 Journal Article

Remark on the star-height-problem

  • Wolfgang Thomas

A method is presented which allows to construct general regular expressions of star-height 1 for a class of rather ‘complicated’ regular events. (General regular expressions include an operation symbol for complement.) If events of greater general star-height exist (which is still open), they must be more complex than those accessible by this method. An event which seems to be of this kind is suggested at the end of the paper.

Details DOI
v2026.09.13