Publications

2011

• V. Bárány, E. Grädel, and S. Rubin. Automata-Based Presentations of Infinite Structures. In Finite and Algorithmic Model Theory (J. Esparza, C. Michaux, and C. Steinhorn, Eds.), pp. 1–76, 2011.             
  BibTeX

  @incollection{BGR10,
       author = {Vince B{\'a}r{\'a}ny and Erich Gr{\"a}del and Sasha Rubin},
       booktitle = {{Finite and Algorithmic Model Theory}},
       editor = {Javier Esparza and Christian Michaux and Charles Steinhorn},
       isbn = {9780521718202},
       month = {March},
       pages = {1--76},
       title = {{Automata-Based Presentations of Infinite Structures}},
       url = {http://logic.rwth-aachen.de/pub/graedel/surveyBGR.pdf},
       year = {2011},
  }
  

• V. Bárány, Ł. Kaiser, and A. Rabinovich. Expressing Cardinality Quantifiers in Monadic Second-Order Logic over Chains. J. Symb. Logic, vol. 76(2), pp. 603-619, 2011.                                 
  Abstract   BibTeX

  We investigate the extension of monadic second-order logic of order with cardinality quantifiers “there exists uncountably many sets such that ...'' and “there exists continuum many sets such that ...''. We prove that over the class of countable linear orders the two quantifiers are equivalent and can be effectively and uniformly eliminated. Weaker or partial elimination results are obtained for certain wider classes of chains. In particular, we show that over the class of ordinals the uncountability quantifier can be effectively and uniformly eliminated. Our argument makes use of Shelah's composition method and Ramsey-like theorem for dense linear orders.

  @article{BKRJSL,
       author = {Vince B{\'a}r{\'a}ny and {\L}ukasz Kaiser and Alexander Rabinovich},
       journal = {J. Symb. Logic},
       volume = {76},
       number = {2},
       year = {2011},
       pages = {603-619},
       title = {{Expressing Cardinality Quantifiers in Monadic Second-Order Logic over Chains}},
       url = {http://logic.rwth-aachen.de/~kaiser/msoc_chains.pdf},
  }
  

2010

• V. Bárány, Ł. Kaiser, and A. Rabinovich. Expressing Cardinality Quantifiers in Monadic Second-Order Logic over Trees. Fundamenta Informaticae, vol. 100, pp. 1–18, 2010.                                 
  Abstract   BibTeX

  We study an extension of monadic second-order logic of order with the uncountability quantifier “there exist uncountably many sets''. We prove that, over the class of finitely branching trees, this extension is equally expressive to plain monadic second-order logic of order. Additionally we find that the continuum hypothesis holds for classes of sets definable in monadic second-order logic over finitely branching trees, which is notable for not all of these classes are analytic. Our approach is based on Shelah's composition method and uses basic results from descriptive set theory. The elimination result is constructive, yielding a decision procedure for the extended logic.

  @article{BKR10,
       author = {Vince B{\'a}r{\'a}ny and {\L}ukasz Kaiser and Alexander Rabinovich},
       journal = {Fundamenta Informaticae},
       pages = {1--18},
       title = {{Expressing Cardinality Quantifiers in Monadic Second-Order Logic over Trees}},
       url = {http://logic.rwth-aachen.de/~kaiser/msoc_trees_fi.pdf},
       volume = {100},
       year = {2010},
  }
  

2009

• V. Bárány, Ł. Kaiser, and A. Rabinovich. Cardinality quantifiers in MLO over trees. In Proceedings of the 18th EACSL Annual Conference on Computer Science Logic, CSL '09 (E. Grädel and R. Kahle, Eds.), vol. 5771 of LNCS, pp. 117–132. Springer, 2009.                                 
  Abstract   BibTeX

  We study an extension of monadic second-order logic of order with the uncountability quantifier “there exist uncountably many sets''. We prove that, over the class of finitely branching trees, this extension is equally expressive to plain monadic second-order logic of order. Additionally we find that the continuum hypothesis holds for classes of sets definable in monadic second-order logic over finitely branching trees, which is notable for not all of these classes are analytic. Our approach is based on Shelah's composition method and uses basic results from descriptive set theory. The elimination result is constructive, yielding a decision procedure for the extended logic. Furthermore, by the well-known correspondence between monadic second-order logic and tree automata, our findings translate to analogous results on the extension of first-order logic by cardinality quantifiers over injectively presentable Rabin-automatic structures, generalizing the work of Kuske and Lohrey.

  @inproceedings{BKR09,
       author = {Vince B{\'a}r{\'a}ny and {\L}ukasz Kaiser and Alexander Rabinovich},
       booktitle = {{Proceedings of the 18th EACSL Annual Conference on Computer Science Logic, CSL~'09}},
       editor = {Erich Gr{\"a}del and Reinhard Kahle},
       pages = {117--132},
       publisher = {{Springer}},
       series = {{LNCS}},
       title = {{Cardinality quantifiers in MLO over trees}},
       url = {http://logic.rwth-aachen.de/~kaiser/msoc_trees.pdf},
       volume = {5771},
       year = {2009},
  }
  

2008

• V. Bárány. A Hierarchy of Automatic ω-Words having a Decidable MSO Theory. RAIRO - Theor. Inf. Appl., vol. 42, pp. 417–450, 2008.                                 
  Abstract   BibTeX

  We investigate automatic presentations of omega-words. Starting points of our study are the works of Rigo and Maes, Caucal, and Carton and Thomas concerning lexicographic presentation, MSO-interpretability in algebraic trees, and the decidability of the MSO theory of morphic words. Refining their techniques we observe that the lexicographic presentation of a (morphic) word is in a certain sense canonical. We then generalize our techniques to a hierarchy of classes of omega-words enjoying the above mentioned definability and decidability properties. We introduce k-lexicographic presentations, and morphisms of level k stacks and show that these are inter-translatable, thus giving rise to the same classes of k-lexicographic or level k morphic words. We prove that these presentations are also canonical, which implies decidability of the MSO theory of every k-lexicographic word as well as closure of these classes under MSO-definable recolorings, e.g. closure under deterministic sequential mappings. The classes of k-lexicographic words are shown to constitute an infinite hierarchy.

  @article{Bar08ITA,
       author = {Vince B{\'a}r{\'a}ny},
       doi = {10.1051/ita:2008008},
       journal = {RAIRO - Theor. Inf. Appl.},
       pages = {417--450},
       title = {{A Hierarchy of Automatic $\omega$-Words having a Decidable MSO Theory}},
       url = {http://www.logic.rwth-aachen.de/~vbarany/hom_ITA.pdf},
       volume = {42},
       year = {2008},
  }
  

• Ł. Kaiser, S. Rubin, and V. Bárány. Cardinality and counting quantifiers on omega-automatic structures. In Proceedings of the 25th International Symposium on Theoretical Aspects of Computer Science, STACS 2008 (S. Albers and P. Weil, Eds.), pp. 385–396, 2008.                                 
  Abstract   BibTeX

  We investigate structures that can be represented by omega-automata, so called omega-automatic structures, and prove that relations defined over such structures in first-order logic expanded by the first-order quantifiers `there exist at most $\aleph\_0$ many', 'there exist finitely many' and 'there exist $k$ modulo $m$ many' are omega-regular. The proof identifies certain algebraic properties of omega-semigroups. As a consequence an omega-regular equivalence relation of countable index has an omega-regular set of representatives. This implies Blumensath's conjecture that a countable structure with an $\omega$-automatic presentation can be represented using automata on finite words. This also complements a very recent result of Hjörth, Khoussainov, Montalban and Nies showing that there is an omega-automatic structure which has no injective presentation.

  @inproceedings{BKR08,
       author = {{\L}ukasz Kaiser and Sasha Rubin and Vince B{\'a}r{\'a}ny},
       booktitle = {{Proceedings of the 25th International Symposium on Theoretical Aspects of Computer Science, STACS~2008}},
       editor = {Susanne Albers and Pascal Weil},
       pages = {385--396},
       title = {{Cardinality and counting quantifiers on omega-automatic structures}},
       url = {http://www.logic.rwth-aachen.de/~kaiser/cardinality_automatic.pdf},
       year = {2008},
  }
  

2007

• V. Bárány. Automatic Presentations of Infinite Structures. PhD thesis, RWTH Aachen, 2007.             
  BibTeX

  @phdthesis{Bar07diss,
       author = {Vince B{\'a}r{\'a}ny},
       school = {RWTH Aachen},
       title = {{Automatic Presentations of Infinite Structures}},
       type = {Dissertation},
       url = {http://www.logic.rwth-aachen.de/~vbarany/diss.pdf},
       year = {2007},
  }
  

2006

• V. Bárány. A Hierarchy of Automatic Words having a Decidable MSO Theory. In Online Proceedings of the 11th Journées Montoises, Rennes (D. Caucal, Ed.), 2006.                                 
  Abstract   BibTeX

  We investigate automatic presentations of infinite words. Starting points of our study are the works of Rigo and Maes, and Carton and Thomas concerning the lexicographic presentation, respectively the decidability of the MSO theory of morphic words. Refining their techniques we observe that the lexicographic presentation of a (morphic) word is canonical in a certain sense. We then go on to generalize our techniques to a hierarchy of classes of infinite words enjoying the above mentioned properties. We introduce $k$-lexicographic presentations, and morphisms of level $k$ stacks and show that these are inter-translatable, thus giving rise to the same classes of $k$-lexicographic or level $k$ morphic words. We prove that these presentations are also canonical, which implies decidability of the MSO theory of every $k$-lexicographic word as well as closure of these classes under restricted MSO interpretations, e.g. closure under deterministic sequential mappings. The classes of $k$-lexicographic words are shown to form an infinite hierarchy.

  @inproceedings{Bar06JM,
       author = {Vince B{\'a}r{\'a}ny},
       booktitle = {{Online Proceedings of the 11th Journ{\'e}es Montoises, Rennes}},
       editor = {D. Caucal},
       title = {{A Hierarchy of Automatic Words having a Decidable MSO Theory}},
       url = {http://www.logic.rwth-aachen.de/~vbarany/jm06.pdf},
       year = {2006},
  }
  

• V. Bárány, C. Löding, and O. Serre. Regularity Problems for Visibly Pushdown Languages. In Proceedings of the 23rd Annual Symposium on Theoretical Aspects of Computer Science, STACS 2006 (B. Durand and W. Thomas, Eds.), vol. 3884 of LNCS, pp. 420–431. Springer, 2006.                                 
  Abstract   BibTeX

  Visibly pushdown automata are special pushdown automata whose stack behavior is driven by the input symbols according to a partition of the alphabet. We show that it is decidable for a given visibly pushdown automaton whether it is equivalent to a visibly counter automaton, i.e. an automaton that uses its stack only as counter. In particular, this allows to decide whether a given visibly pushdown language is a regular restriction of the set of well-matched words, meaning that the language can be accepted by a finite automaton if only well-matched words are considered as input.

  @inproceedings{BLS06STACS,
       author = {Vince B{\'a}r{\'a}ny and Christof L{\"o}ding and Olivier Serre},
       booktitle = {{Proceedings of the 23rd Annual Symposium on Theoretical Aspects of Computer Science, STACS 2006}},
       editor = {B. Durand and W. Thomas},
       pages = {420--431},
       publisher = {Springer},
       series = {{LNCS}},
       title = {{Regularity Problems for Visibly Pushdown Languages}},
       url = {http://www.logic.rwth-aachen.de/~vbarany/BLS_stacs06_withAppendix.pdf},
       volume = {3884},
       year = {2006},
  }
  

• V. Bárány. Invariants of Automatic Presentations and Semi-Synchronous Transductions. In Proceedings of the 23rd Annual Symposium on Theoretical Aspects of Computer Science, STACS 2006 (B. Durand and W. Thomas, Eds.), vol. 3884 of LNCS, pp. 289–300. Springer, 2006.                                 
  Abstract   BibTeX

  Automatic structures are countable structures finitely presentable by a collection of automata. We study questions related to properties invariant with respect to the choice of an automatic presentation. We give a negative answer to a question of Rubin concerning definability of intrinsically regular relations by showing that order-invariant first-order logic can be stronger than first-order logic with counting on automatic structures. We introduce a notion of equivalence of automatic presentations, define semi-synchronous transductions, and show how these concepts correspond. Our main result is that a one-to-one function on words preserves regularity as well as non-regularity of all relations iff it is a semi-synchronous transduction. We also characterize automatic presentations of the complete structures of Blumensath and Grädel.

  @inproceedings{Bar06STACS,
       author = {Vince B{\'a}r{\'a}ny},
       booktitle = {{Proceedings of the 23rd Annual Symposium on Theoretical Aspects of Computer Science, STACS 2006}},
       editor = {B. Durand and W. Thomas},
       pages = {289--300},
       publisher = {Springer},
       series = {{LNCS}},
       title = {{Invariants of Automatic Presentations and Semi-Synchronous Transductions}},
       url = {http://www.logic.rwth-aachen.de/~vbarany/stacs06_88_appendix.pdf},
       volume = {3884},
       year = {2006},
  }