2020

• E. Grädel and M. Otto. Guarded Teams: The Horizontally Guarded Case. In 28th EACSL Annual Conference on Computer Science Logic (CSL 2020) (M. Fernández and A. Muscholl, Eds.), vol. 152 of Leibniz International Proceedings in Informatics (LIPIcs), pp. 22:1–22:17, Dagstuhl, Germany. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, 2020.             
  BibTeX

  @inproceedings{GO20,
       author = {Erich Gr{\"a}del and Martin Otto},
       title = {{Guarded Teams: The Horizontally Guarded Case}},
       booktitle = {28th EACSL Annual Conference on Computer Science Logic (CSL 2020)},
       pages = {22:1--22:17},
       series = {Leibniz International Proceedings in Informatics (LIPIcs)},
       isbn = {978-3-95977-132-0},
       issn = {1868-8969},
       year = {2020},
       volume = {152},
       editor = {Maribel Fern{\'a}ndez and Anca Muscholl},
       publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
       address = {Dagstuhl, Germany},
       url = {https://drops.dagstuhl.de/opus/volltexte/2020/11665},
       urn = {urn:nbn:de:0030-drops-116650},
       doi = {10.4230/LIPIcs.CSL.2020.22},
       annote = {Keywords: Team semantics, guarded logics, bisimulation, characterisation theorems},
  }
  

2014

• E. Grädel and M. Otto. The Freedoms of (Guarded) Bisimulation. In Johan van Benthem on Logic and Information Dynamics (A. Baltag and S. Smets, Eds.), vol. 5 of Outstanding Contributions to Logic, pp. 3-31. Springer, 2014.             
  BibTeX

  @incollection{GO14,
       year = {2014},
       booktitle = {Johan van Benthem on Logic and Information Dynamics},
       volume = {5},
       series = {Outstanding Contributions to Logic},
       editor = {Alexandru Baltag and Sonja Smets},
       doi = {10.1007/978-3-319-06025-5_1},
       title = {The Freedoms of (Guarded) Bisimulation},
       url = {http://logic.rwth-aachen.de/pub/graedel/FreedomBisimulation.pdf},
       publisher = {Springer},
       pages = {3-31},
       author = {Erich Gr{\"a}del and Martin Otto},
       language = {English},
  }
  

2002

• E. Grädel, C. Hirsch, and M. Otto. Back and Forth Between Guarded and Modal Logics. ACM Transactions on Computational Logics, vol. 3(3), pp. 418 – 463, 2002.                                 
  Abstract   BibTeX

  Guarded fixed-point logic $\mu$GF extends the guarded fragment by means of least and greatest fixed points, and thus plays the same role within the domain of guarded logics as the modal $\mu$-calculus plays within the modal domain. We provide a semantic characterization of $\mu$GF within an appropriate fragment of second-order logic, in terms of invariance under guarded bisimulation. The corresponding characterization of the modal $\mu$-calculus, due to Janin and Walukiewicz, is lifted from the modal to the guarded domain by means of model theoretic translations. Guarded second-order logic, the fragment of second-order logic which is introduced in the context of our characterization theorem, captures a natural and robust level of expressiveness with several equivalent characterizations. For a wide range of issues in guarded logics it may take up a role similar to that of monadic second-order in relation to modal logics. At the more general methodological level, the translations between the guarded and modal domains make the intuitive analogy between guarded and modal logics available as a tool in the further analysis of the model theory of guarded logics.

  @article{GrHiOt00a,
       author = {Erich Gr{\"a}del and Colin Hirsch and Martin Otto},
       journal = {ACM Transactions on Computational Logics},
       note = {See also: conference version \cite{GrHiOt00}},
       number = {3},
       pages = {418 -- 463},
       title = {{Back and Forth Between Guarded and Modal Logics}},
       url = {http://www.logic.rwth-aachen.de/pub/graedel/GrHiOt-tocl02.ps},
       volume = {3},
       year = {2002},
  }
  

2000

• E. Grädel, C. Hirsch, and M. Otto. Back and Forth Between Guarded and Modal Logics. In Proceedings of 15th IEEE Symposium on Logic in Computer Science LICS 2000, pp. 217–228, Santa Barbara, 2000.                                 
  Abstract   BibTeX

  We propose a second-order extension for the guarded fragment showing that several canonical extensions are in fact equivalent. Then we ask the question in how far results from the modal world can be brought into the world of guarded logics. We give a transformation from first-order structures to Kripke type transition systems. This is used here to transform a theorem due to Janin and Walukiewicz about the expressive completeness of fixed-point logic in the context of bisimulation invariance.

  @inproceedings{GrHiOt00,
       address = {Santa Barbara},
       author = {Erich Gr{\"a}del and Colin Hirsch and Martin Otto},
       booktitle = {{Proceedings of 15th IEEE Symposium on Logic in Computer Science LICS 2000}},
       note = {See also: journal version \cite{GrHiOt00a}},
       pages = {217--228},
       title = {{Back and Forth Between Guarded and Modal Logics}},
       url = {http://www.logic.rwth-aachen.de/pub/graedel/GrHiOt-lics00.ps},
       year = {2000},
  }
  

1999

• E. Grädel and M. Otto. On Logics with Two Variables. Theoretical Computer Science, vol. 224, pp. 73–113, 1999.                                 
  Abstract   BibTeX

  Logical languages whose leading feature lies in the restriction to just two element variables play an important role in a number of applications, including the specification of processes or of the temporal or causal behaviour of transition systems, as well as the formalization of epistemological or terminological dependencies. The two-variable nature of many important languages may be attributed to the fact that they contain propositional modal logic as an essential core. Diverse mechanisms for extending basic modal logic have been analyzed with great success within the modal framework, and have lead to interesting, manageable languages, that meet the essential expressive needs for certain applications. For many applications, however, first-order closure properties offer an equally desirable direction for extensions. In this case, the extension of basic modal logic to first-order logic with two variables provides the natural starting point. This survey presents an overview of recent results pertaining to logics that lift some of the prominent mechanisms of extension from the modal framework to the framework of two-variable first-order logic. Most strikingly, two-variable first-order logic turns out to be not nearly as robust as modal logic with respect to satisfiability; several seemingly weak extensions of two-variable first-oder in important directions turn out to be highly undecidable. One notable exception is the extension by counting quantifiers, which does provide a decidable common extension of graded modal logic and two-variable first order. Some of the resulting other logics, while being undecidable, do provide natural levels of expressiveness for model checking applications, journal-title their complexity is generally no worse than for the underlying modal variants.

  @article{GraedelOtto98,
       author = {Erich Gr{\"a}del and Martin Otto},
       journal = {Theoretical Computer Science},
       pages = {73--113},
       title = {{On Logics with Two Variables}},
       url = {http://www.logic.rwth-aachen.de/pub/graedel/GrOt-tcs99.ps},
       volume = {224},
       year = {1999},
  }
  

• E. Grädel, M. Otto, and E. Rosen. Undecidability Results on Two-Variable Logics. Archive for Mathematical Logic, vol. 38, pp. 213–354, 1999.                                 
  Abstract   BibTeX

  It is a classical result of Mortimer's that L$^2$, first-order logic with two variables, is decidable for satisfiability. It is shown that going beyond L$^2$ by adding any one of the following leads to an undecidable logic:

  – very weak forms of recursion, viz. transitive closure operations, or (restricted) monadic fixed-point operations

  – weak access to cardinalities, through the Härtig (or equicardinality) quantifier, or

  – a choice construct known as Hilbert's epsilon operator.

  In fact all these extensions of L$^2$ prove to be undecidable both for satisfiability, and for satisfiability in finite models. Moreover most of them are hard for $\Sigma\_1^1$, the first level of the analytical hierachy, and thus have a much higher degree of undecidability than first-order logic.

  @article{GraedelOttoRosen98,
       author = {Erich Gr{\"a}del and Martin Otto and Eric Rosen},
       journal = {Archive for Mathematical Logic},
       note = {See also: conference version \cite{GraedelOttoRosen97a}},
       pages = {213--354},
       title = {{Undecidability Results on Two-Variable Logics}},
       url = {http://www.logic.rwth-aachen.de/pub/graedel/gor.ps},
       volume = {38},
       year = {1999},
  }
  

• E. Hoogland, M. Marx, and M. Otto. Beth Definability for the Guarded Fragment. In Proceedings of LPAR'99, LNAI. Springer, 1999.                                 
  Abstract   BibTeX

  We analyze the question of existence of asymptotic cumulative probabilities for monadic second order definable properties of finite algebras. We focus our attention on the directly representable varieties and on the variety of groups. We prove in a very strong way that some recently proven first-order $0–1$ laws and limit laws for these varieties cannot be extended to monadic second order logic. Namely, if the function (n,A)->$pr\_n[A]$ assigning probabilities to structures is recursive, then the 0-1 law holds according to the sequence pr\_n=$pr\_1$,$pr\_2$,... of probabilities iff asymptotically there exists pr-almost surely precisely one algebra. Similarly, the convergence law holds iff asymptotically there are no large algebras according to pr.

  @inproceedings{HooglandMarxOtto99,
       author = {E. Hoogland and M. Marx and Martin Otto},
       booktitle = {{Proceedings of LPAR'99}},
       publisher = {{Springer}},
       series = {{LNAI}},
       title = {{Beth Definability for the Guarded Fragment}},
       url = {http://www.logic.rwth-aachen.de/pub/otto/beth.ps},
       year = {1999},
  }
  

• F. Neven, M. Otto, J. Tyszkiewicz, and V. den Bussche. Adding FOR-Loops to First-Order Logic. In Proceedings of ICDT'99, vol. 1540 of LNCS, pp. 58–69. Springer, 1999.             
  BibTeX

  @inproceedings{NeOtTyVa99,
       author = {F. Neven and Martin Otto and Jurek Tyszkiewicz and Van den Bussche},
       booktitle = {{Proceedings of ICDT'99}},
       pages = {58--69},
       publisher = {{Springer}},
       series = {{LNCS}},
       title = {{Adding FOR-Loops to First-Order Logic}},
       volume = {1540},
       year = {1999},
  }
  

• M. Otto. Bounded-Variable Logics: Two, Three, and More. Archive for Mathematical Logic, vol. 38, pp. 235–256, 1999.                                 
  Abstract   BibTeX

  This study concerns the bounded variable logics $L^k$ (with $k$ variable symbols), and $C^k$ (with $k$ variables in the presence of first-order counting quantifiers). These fragments of infinitary logic are well known to provide an adequate logical framework for some important issues in finite model theory. This paper deals with a translation that associates equivalence of structures in the $k$-variable fragments with bisimulation equivalence between derived structures. Apart from a uniform and intuitively appealing treatment of these equivalences, this approach relates some interesting issues for the case of an arbitrary number of variables to the case of just three variables. Invertibility of the invariants for $C^3$, in particular, would imply a positive answer to the tempting conjecture that fixed-point logic with counting captures Ptime in the world of bounded variable logic with counting.

  @article{Ot99,
       author = {Martin Otto},
       journal = {Archive for Mathematical Logic},
       pages = {235--256},
       title = {{Bounded-Variable Logics: Two, Three, and More}},
       url = {ftp://ftp.informatik.rwth-aachen.de/pub/FMT/otto/twothree.ps},
       volume = {38},
       year = {1999},
  }
  

• M. Otto. Bisimulation-Invariant Ptime and Higher-Dimensional mu-Calculus. Theoretical Computer Science, vol. 224, pp. 237–265, 1999.                                 
  Abstract   BibTeX

  Let \em bisimilar Ptime be the class of those monadic queries over finite Kripke structures that are in Ptime and closed under bisimulation equivalence. This class \em bisimilar Ptime has a natural logical characterisation: it is captured, in the sense of descriptive complexity, by the straightforward extension of propositional $\mu$-calculus to arbitrary finite dimension. Here $\mu$-calculus in dimension $k$ is based on modal logic with $k$-tuples of worlds as the new $k$-worlds, $k$ different accessibility relations, one for each component, and a $\mu$-operator. It is also shown that even 2-dimensional $\mu$-calculus does not have the finite model property, is undecidable for finite satisfiability, and $\Sigma^1\_1$-hard for satisfiability.

  @article{Otto98b,
       author = {Martin Otto},
       journal = {Theoretical Computer Science},
       pages = {237--265},
       title = {{Bisimulation-Invariant Ptime and Higher-Dimensional mu-Calculus}},
       url = {http://www.logic.rwth-aachen.de/pub/otto/bisimP.ps},
       volume = {224},
       year = {1999},
  }
  

• M. Otto. Eliminating Recursion in the μ-Calculus. In Proceedings of STACS'99, vol. 1563 of LNCS, pp. 531–540. Springer, 1999.                                 
  Abstract   BibTeX

  The following decision problem is analysed: given a formula of the modal mu-calculus, decide whether there is some formula of basic modal logic equivalent to it. It is shown that this problem is decidable, and indeed Exptime complete. The decidability proof can be given through a purely model theoretic reduction to the monadic second-order theory of the binary tree, or through an analysis of suitably adapted tree automata. The latter analysis also yields a decision procedure in deterministic exponential time.

  @inproceedings{Otto98e,
       author = {Martin Otto},
       booktitle = {{Proceedings of STACS'99}},
       pages = {531--540},
       publisher = {{Springer}},
       series = {{LNCS}},
       title = {{Eliminating Recursion in the $\mu$-Calculus}},
       url = {http://www.logic.rwth-aachen.de/pub/otto/mllmu.ps},
       volume = {1563},
       year = {1999},
  }
  

1998

• P. Kolaitis and M. Otto. On the Boundedness Problem for Two-Variable First-Order Logic. In Proceedings of IEEE Symposium on Logic in Computer Science LICS `98, 1998.                                 
  Abstract   BibTeX

  A positive first-order formula is bounded if the sequence of its stages converges to the least fixed point of the formula within a fixed finite number of steps independent of the input structure. The boundedness problem for a fragment of first-order logic asks: given a positive formula in the fragment, is it bounded? \par We investigate the boundedness problem for two-variable first-order logic, an otherwise very well-behaved and, in particular, decidable fragment of first-order logic. Our main result asserts that the boundedness problem for two-variable first-order logic is undecidable, even when restricted to negation-free and equality-free formulae with a single monadic predicate variable that occurs within the scopes of universal quantifiers only. This contrasts sharply with earlier decidability results for monadic Datalog programs, which amount to the decidability of boundedness for negation-free and equality-free existential first-order formulae with a single monadic predicate variable. \ par Our main result has certain applications to circumscription, the most well-developed formalism of nonmonotonic reasoning. Specifically, we show that it is an undecidable problem to tell whether the circumscription of a given two-variable first-order formula is equivalent to a first-order formula.

  @inproceedings{KolaitisOtto98,
       author = {Phonion Kolaitis and Martin Otto},
       booktitle = {{Proceedings of IEEE Symposium on Logic in Computer Science LICS `98}},
       title = {{{O}n the {B}oundedness {P}roblem for {T}wo-{V}ariable {F}irst-{O}rder {L}ogic}},
       url = {http://www.logic.rwth-aachen.de/pub/jurek/kaufmann.ps},
       year = {1998},
  }
  

• M. Otto. Two-Variable First-Order Logic over Ordered Domains. 1998.                                 
  Abstract   BibTeX

  The satisfiability problem for the two-variable fragment FO$^2$ of first-order logic is investigated over finite and infinite linearly ordered, respectively wellordered domains, as well as over finite and infinite domains in which one or several designated binary predicates are interpreted as arbitrary wellfounded relations. It is shown that FO$^2$ over ordered, respectively wellordered, domains or in the presence of one wellfounded relation, is decidable for satisfiability as well as for finite satisfiability. Actually the complexity of these decision problems is essentially the same as for plain unconstrained FO$^2$, namely non-deterministic exponential time. In contrast FO$^2$ becomes undecidable for satisfiability and for finite satisfiability, if a sufficiently large number of predicates are required to be interpreted as (even partial) orderings, wellorderings, or as arbitrary wellfounded relations. This undecidability result also entails the undecidability of the natural common extension of FO$^2$ and computation tree logic.

  @unpublished{Otto98c,
       author = {Martin Otto},
       title = {{Two-Variable First-Order Logic over Ordered Domains}},
       url = {http://www.logic.rwth-aachen.de/pub/otto/fotord.ps},
       year = {1998},
  }
  

• M. Otto. Epsilon-Logic is More Expressive Than First-Order Logic over Finite Structures. 1998.                                 
  Abstract   BibTeX

  It is shown that there are properties of finite structures that are expressible with the use of Hilbert's epsilon-operator in a manner that does not depend on the actual interpretation for epsilon-terms, but not expressible in plain first-order. This observation strengthens a corresponding result of Gurevich, concerning the invariant use of an auxiliary ordering in first-order logic over finite structures. The present result also implies that certain non-deterministic choice constructs, which have been considered in database theory, properly enhance the expressive power of first-order logic even as far as deterministic queries are concerned, thereby answering a question raised by Abiteboul and Vianu.

  @unpublished{Otto98d,
       author = {Martin Otto},
       title = {{Epsilon-Logic is More Expressive Than First-Order Logic over Finite Structures}},
       url = {http://www.logic.rwth-aachen.de/pub/otto/epsilon.ps},
       year = {1998},
  }
  

• M. Otto. An interpolation theorem. 1998.                                 
  Abstract   BibTeX

  A relativized variant of Lyndons's Interpolation Theorem is proved, which gives a tool to focus on existential and universal quantification over designated subdomains – through positive and negative occurrences of predicates denoting these subdomains in relativized quantifications. It is shown how this single new interpolation theorem unifies a number of related results: namely, the classical preservation theorems concerning extensions/substructures with those concerning monotonicity, as well as a many-sorted interpolation theorem focusing on existentially/universally quantified sorts.

  @unpublished{Otto98f,
       author = {Martin Otto},
       note = {Preprint, unpublished},
       title = {{An interpolation theorem}},
       url = {http://www.logic.rwth-aachen.de/pub/otto/int.ps},
       year = {1998},
  }
  

1997

• E. Grädel, M. Otto, and E. Rosen. Two-Variable Logic with Counting is Decidable. In Proceedings of 12th IEEE Symposium on Logic in Computer Science LICS `97, Warschau, 1997.                                 
  Abstract   BibTeX

  The satisfiability problem for C2 is shown to be decidable. \par C$^2$ is first-order logic with only two variables in the presence of arbitrary counting quantifiers of the form ''there exist at least m''. It considerably extends L$^2$, plain first-order with only two variables, which is known to be decidable by a result of Mortimer. Unlike L$^2$, C$^2$ does not have the finite model property. As C$^2$ extends L$^2$ by expressive means for counting, significant applications arise from the fact that C$^2$ embeds corresponding counting extensions of modal logics.

  @inproceedings{GraedelOttoRosen97,
       author = {Erich Gr{\"a}del and Martin Otto and Eric Rosen},
       booktitle = {{Proceedings of 12th IEEE Symposium on Logic in Computer Science LICS `97, Warschau}},
       title = {{Two-Variable Logic with Counting is Decidable}},
       url = {http://www.logic.rwth-aachen.de/pub/graedel/gorc2.ps},
       year = {1997},
  }
  

• E. Grädel, M. Otto, and E. Rosen. Undecidability Results on Two-Variable Logics. In Proceedings of 14th Symposium on Theoretical Aspects of Computer Science STACS`97, vol. 1200 of Lecture Notes in Computer Science, pp. 249–260, 1997.             
  BibTeX

  @inproceedings{GraedelOttoRosen97a,
       author = {Erich Gr{\"a}del and Martin Otto and Eric Rosen},
       booktitle = {{Proceedings of 14th Symposium on Theoretical Aspects of Computer Science STACS`97}},
       note = {See also: journal version \cite{GraedelOttoRosen98}},
       pages = {249--260},
       series = {{Lecture Notes in Computer Science}},
       title = {{Undecidability Results on Two-Variable Logics}},
       volume = {1200},
       year = {1997},
  }
  

• M. Otto. Canonization for Two Variables and Puzzles on the Square. Annals of Pure and Applied Logic, vol. 85, pp. 243–282, 1997.                                 
  Abstract   BibTeX

  We consider infinitary logic with only two variable symbols, both with and without counting quantifiers, $L^2$ and $C^2$. The main result is that finite relational structures admit PTIME canonization with respect to $L^2$ and $C^2$: there are polynomial time computable functors mapping finite relational structures to unique representatives of their equivalence class with respect to indistinguishability in either of these logics. In fact Ptime inverses are constructed for the natural Ptime invariants that characterize structures up to $L^2$- or $C^2$-equivalence, respectively. This yields a recursive representations of the classes of all Ptime boolean queries that are closed with respect to $L^2$–or $C^2$–equivalence.

  @article{Ot97,
       author = {Martin Otto},
       journal = {Annals of Pure and Applied Logic},
       pages = {243--282},
       title = {{{C}anonization for {T}wo {V}ariables and {P}uzzles on the {S}quare}},
       volume = {85},
       year = {1997},
  }
  

• M. Otto. Capturing Bisimulation-Invariant Ptime. In Proceedings of 4th Symposium on Logical Foundations of Computer Science, LFCS `97, vol. 1234 of LNCS, pp. 294–305. Springer, 1997.             
  BibTeX

  @inproceedings{Ot97c,
       author = {Martin Otto},
       booktitle = {{Proceedings of 4th Symposium on Logical Foundations of Computer Science, LFCS `97}},
       pages = {294--305},
       publisher = {{Springer}},
       series = {{LNCS}},
       title = {{Capturing Bisimulation-Invariant Ptime}},
       volume = {1234},
       year = {1997},
  }
  

• M. Otto. Bounded variable logics and counting — A study in finite models. Springer, 1997.                                 
  Abstract   BibTeX

  This is a comprehensive treatment of a variety of results on infinitary logics with a bounded number of variables, both with and without counting quantifiers, as well as on related fixed-point logics. The emphasis is on central issues in finite model theory and in particular on descriptive complexity. Despite its character as a research monograph the exposition is largely self-contained. Much room is given to connections with the existing body of work in this area. From the contents:

  – An introduction to the relevant notions from logic, model theory, and to the programme of descriptive complexity.

  – A systematic treatment of the relevant games and game-theoretic structural invariants.

  – The analysis of fixed-point logics, both with and without counting.

  – Canonization and inversion problems as an approach to capturing fragments of PTIME.

  – Capturing results for the two-variable fragments of PTIME.

  @book{Otto95b,
       author = {Martin Otto},
       booktitle = {{Lecture Notes in Logic}},
       publisher = {{Springer}},
       title = {{Bounded variable logics and counting --- A study in finite models}},
       volume = {9},
       year = {1997},
  }
  

• M. Otto. The Logic of Explicitly Representation-Invariant Circuits. Selected Papers of CSL `96, vol. 1258, pp. 369–384, 1997.             
  BibTeX

  @article{Ot97b,
       author = {Martin Otto},
       editor = {D.~van~Dalen and M.~Bezem},
       journal = {Selected Papers of CSL `96},
       pages = {369--384},
       publisher = {{Springer}},
       series = {{LNCS}},
       title = {{The Logic of Explicitly Representation-Invariant Circuits}},
       volume = {1258},
       year = {1997},
  }
  

1996

• M. Otto. The Expressive Power of Fixed-Point Logic with Counting. Journal of Symbolic Logic, vol. 61, pp. 147–176, 1996.                                 
  Abstract   BibTeX

  This is an investigation in finite model theory concerning the expressive power of the logic FP+Counting, the extension of first-order logic which is obtained through adding both the fixed-point constructor and the ability to count. The analysis is carried out in parallel along two entirely different lines. One employs an isomorphism preserving (`generic') model of computation, whose PTIME restriction exactly corresponds to FP+Counting, while its PSPACE restriction corresponds to WHILE+Counting. A normal form gives a clear separation of the relational vs. the arithmetical side of the algorithms involved. The other one uses the connection with the infinitary logics Cr, r-variable infinitary logic with counting quantifiers, to apply the corresponding pebble games in the analysis. \par The main result involves the concept of an arithmetical invariant. This is a functor taking every finite relational structure to an expansion of (an initial segment of) the standard arithmetical structure. A family of arithmetical invariants Ir with the following properties is introduced:

  – each $I^r$ can be evaluated in polynomial time.

  – a class of finite relational structures is definable in FP+Counting if and only if membership can be decided in polynomial time on the basis of the values of one of the invariants.

  – $I^r$ classifies all finite relational structures exactly up to equivalence with respect to the logic $C^r$.

  Further issues concern a characterization of FP+Counting in terms of those sequences of finitary formulae in the $C^r$ that are polynomial time computable, and a positive assessment of the expressive power of FP+Counting in comparison with related extensions of fixed-point logic by Lindström quantifiers. The extesnsion by all Lindström quantifiers, which capture PTIME computable properties of cardinalities of definable predicates, remains strictly weaker than FP+Counting. In particular, every extension of fixed-point logic by monadic Lindström quantifiers, which stays within PTIME, is strictly contained in FP+Counting.

  @article{Ot96,
       author = {Martin Otto},
       journal = {Journal of Symbolic Logic},
       pages = {147--176},
       title = {{The {E}xpressive {P}ower of {F}ixed-{P}oint {L}ogic with {C}ounting}},
       volume = {61},
       year = {1996},
  }
  

• M. Otto and J. V. den Bussche. First-Order Queries on Databases Embedded in an Infinite Structure. Information Processing Letters, vol. 60, pp. 37–41, 1996.             
  BibTeX

  @article{OtVa96,
       author = {Martin Otto and J. Van den Bussche},
       journal = {Information Processing Letters},
       pages = {37--41},
       title = {{First-{O}rder {Q}ueries on {D}atabases {E}mbedded in an {I}nfinite {S}tructure}},
       volume = {60},
       year = {1996},
  }
  

1995

• M. Otto. Bounded variable logics and counting — A study in finite models. 1995.             
  BibTeX

  @misc{Ot95,
       author = {Martin Otto},
       note = {Habilitationsschrift RWTH Aachen, 190 pages. See also: monograph \cite{Otto95b}},
       title = {{Bounded variable logics and counting --- A study in finite models}},
       year = {1995},
  }
  

• M. Otto. A note on the number of monadic quantifiers in monadic Σ^1_1. Information Processing Letters, vol. 53(6), pp. 337–339, 1995.                                 
  Abstract   BibTeX

  A simple proof is given, that the number of monadic quantifiers in existential monadic second-order logic gives rise to a strict hierarchy over finite structures. This resolves a problem put forward by R.Fagin.

  @article{Ot95c,
       author = {Martin Otto},
       day = {24},
       journal = {Information Processing Letters},
       month = {March},
       number = {6},
       pages = {337--339},
       title = {{A note on the number of monadic quantifiers in monadic {$\Sigma^1\_1$}}},
       volume = {53},
       year = {1995},
  }
  

• M. Otto. Ptime canonization for two variables with counting. In Proceedings of 10th IEEE Symposium on Logic in Computer Science LICS `95, pp. 342–352, 1995.                                 
  Abstract   BibTeX

  Infinitary logic with two variable symbols and counting quantifiers $C^2$ and its intersection with PTIME are considered on finite relational structures. A PTIME canonization procedure is presented which provides unique representatives up to equivalence in $C^2$ for finite relational structures. As a consequence there is a recursive presentation for the class of all those queries on arbitrary finite relational structures which are both PTIME and definable in $C^2$. The proof renders a succinct normal form representation of this non-trivial semantically defined fragment of PTIME. Through specializations of the proof techniques similar results apply with respect to the logic L2, infinitary logic with two variable symbols, itself.

  @inproceedings{Ot95d,
       author = {Martin Otto},
       booktitle = {{Proceedings of 10th IEEE Symposium on Logic in Computer Science LICS `95}},
       pages = {342--352},
       title = {{Ptime canonization for two variables with counting}},
       url = {http://www.logic.rwth-aachen.de/pub/otto/LICS95.ps},
       year = {1995},
  }
  

1994

• M. Otto. Generalized quantifiers for simple properties. In Proceedings of 9th IEEE Symposium on Logic in Computer Science LICS `94, pp. 30–39, 1994.                                 
  Abstract   BibTeX

  Extensions of fixed-point logic by means of generalized quantifiers are considered in the context of descriptive complexity. By the well-known theorem of Immerman and Vardi, fixed-point logic captures PTIME over linearly ordered structures. It fails, however, to express even most fundamental structural properties, like simple cardinality properties, in the absence of order. The present investigation concentrates on extensions by generalized quantifiers which serve to adjoin \em simple or \em basic structural properties. An abstract notion of simplicity is put forward which isolates those structural properties, that can be characterized in terms of a concise \em structural invariant. The key examples are provided by all monadic and cardinality properties in a very general sense. The main theorem establishes that no extension by any family of such simple quantifiers can cover all of PTIME. These limitations are proved on the basis of the semantically motivated notion of simplicity; in particular there is no implicit bound on the arities of the generalized quantifiers involved. Quite to the contrary, the natural applications concern infinite families of quantifiers adjoining certain structural properties across all arities in a uniform way.

  @inproceedings{Ot94,
       author = {Martin Otto},
       booktitle = {{Proceedings of 9th IEEE Symposium on Logic in Computer Science LICS `94}},
       pages = {30--39},
       title = {{Generalized quantifiers for simple properties}},
       url = {http://www.logic.rwth-aachen.de/pub/otto/LICS94.ps},
       year = {1994},
  }
  

• M. Otto. Symmetry and First-Order: Explicitly Representation-Invariant Circuits. 1994.                                 
  Abstract   BibTeX

  Circuit complexity is considered under the additional assumption of full combinatorial symmetry with respect to permutations of the input representation. This approach leads to a very natural and simple characterization of first-order logic and its infinitary variant with bounded numbers of variables over finite structures. Extensions to not necessarily acyclic boolean networks provide corresponding characterizations of partial fixed-point logic (or the relational query language WHILE) and ordinary fixed-point logic.

  @unpublished{Ot94b,
       author = {Martin Otto},
       note = {See also: journal version \cite{Ot97b}},
       title = {{Symmetry and First-Order: Explicitly Representation-Invariant Circuits}},
       url = {http://www.logic.rwth-aachen.de/pub/otto/Circ.ps},
       year = {1994},
  }
  

1993

• E. Grädel and M. Otto. Inductive Definability with Counting on Finite Structures. In Computer Science Logic, 6th Workshop, CSL `92, San Miniato 1992, Selected Papers (E. Börger, G. Jäger, H. K. Büning, S. Martini, and M. M. Richter, Eds.), vol. 702 of LNCS, pp. 231–247. Springer, 1993.                                 
  Abstract   BibTeX

  The properties and the expressive power of logical languages that include both a mechanism for inductive definitions and the ability to count are studied. The most important of these languages is fixed-point logic with counting terms, denoted FP+C. It is shown that in the presence of counting terms inductive definability on arbitrary finite structures has nice properties that it retains without counting only in the case of ordered structures. Main issues of the investigation concern:

  – equivalent charcterizations and robustness of FP+C: e.g. FP+C is equivalent with DATALOG+C and offers intuitive functional as well as machine theoretic characterizations.

  – relations with infinitary logic with bounded number of variables and counting quantifiers.

  – relations with partial fixed-point logic with counting, PFP+C.

  @inproceedings{GrOt93,
       author = {Erich Gr{\"a}del and Martin Otto},
       booktitle = {{Computer Science Logic, 6th Workshop, CSL `92, San Miniato 1992, Selected Papers}},
       editor = {E. B{\"o}rger and G. J{\"a}ger and H. Kleine B{\"u}ning and S. Martini and M. M. Richter},
       pages = {231--247},
       publisher = {{Springer}},
       series = {{LNCS}},
       title = {{Inductive Definability with Counting on Finite Structures}},
       url = {http://www.logic.rwth-aachen.de/pub/otto/CSL92.ps},
       volume = {702},
       year = {1993},
  }
  

1992

• M. Otto. Automorphism Properties of Stationary Logic. Journal of Symbolic Logic, vol. 57, pp. 231–237, 1992.             
  BibTeX

  @article{Ot92,
       author = {Martin Otto},
       journal = {Journal of Symbolic Logic},
       pages = {231--237},
       title = {{Automorphism Properties of Stationary Logic}},
       volume = {57},
       year = {1992},
  }
  

• M. Otto. EM Functors for a Class of Generalized Quantifiers. Archive for Mathematical Logic, vol. 31, pp. 355–371, 1992.             
  BibTeX

  @article{Ot92b,
       author = {Martin Otto},
       journal = {Archive for Mathematical Logic},
       pages = {355--371},
       title = {{EM Functors for a Class of Generalized Quantifiers}},
       volume = {31},
       year = {1992},
  }
  

1990

• M. Otto. Ehrenfeucht-Mostowski Konstruktionen in Erweiterungslogiken. PhD thesis, Freiburg University, 1990.             
  BibTeX

  @phdthesis{Ot90,
       author = {Martin Otto},
       school = {Freiburg University},
       title = {{Ehrenfeucht-Mostowski Konstruktionen in Erweiterungslogiken}},
       year = {1990},
  }
  

1987

• M. Otto. A Reduction Scheme for Phase Spaces with Almost-Kähler Symmetry – Regularity Results for Momentum Level Sets. Journal of Geometry and Physics, vol. 4, pp. 101–118, 1987.             
  BibTeX

  @article{Ot87,
       author = {Martin Otto},
       journal = {Journal of Geometry and Physics},
       pages = {101--118},
       title = {{A Reduction Scheme for Phase Spaces with Almost-K{\"a}hler Symmetry -- Regularity Results for Momentum Level Sets}},
       volume = {4},
       year = {1987},
  }