6 Search Results for "Manuel, Amaldev"

Document
DOI: 10.4230/LIPIcs.MFCS.2016.66
Two-Variable Logic over Countable Linear Orderings

Authors: Amaldev Manuel and A. V. Sreejith

Published in: LIPIcs, Volume 58, 41st International Symposium on Mathematical Foundations of Computer Science (MFCS 2016)

Abstract
We study the class of languages of finitely-labelled countable linear orderings definable in two-variable first-order logic. We give a number of characterisations, in particular an algebraic one in terms of circle monoids, using equations. This generalises the corresponding characterisation, namely variety DA, over finite words to the countable case. A corollary is that the membership in this class is decidable: for instance given an MSO formula it is possible to check if there is an equivalent two-variable logic formula over countable linear orderings. In addition, we prove that the satisfiability problems for two-variable logic over arbitrary, countable, and scattered linear orderings are NEXPTIME-complete.
Cite as

Amaldev Manuel and A. V. Sreejith. Two-Variable Logic over Countable Linear Orderings. In 41st International Symposium on Mathematical Foundations of Computer Science (MFCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 58, pp. 66:1-66:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{manuel_et_al:LIPIcs.MFCS.2016.66,
  author =	{Manuel, Amaldev and Sreejith, A. V.},
  title =	{{Two-Variable Logic over Countable Linear Orderings}},
  booktitle =	{41st International Symposium on Mathematical Foundations of Computer Science (MFCS 2016)},
  pages =	{66:1--66:13},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-016-3},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{58},
  editor =	{Faliszewski, Piotr and Muscholl, Anca and Niedermeier, Rolf},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2016.66},
  URN =		{urn:nbn:de:0030-drops-64788},
  doi =		{10.4230/LIPIcs.MFCS.2016.66},
  annote =	{Keywords: circ-monoids, countable linear orderings, FO^2}
}
Document
DOI: 10.4230/LIPIcs.STACS.2016.29
Cost Functions Definable by Min/Max Automata

Authors: Thomas Colcombet, Denis Kuperberg, Amaldev Manuel, and Szymon Torunczyk

Published in: LIPIcs, Volume 47, 33rd Symposium on Theoretical Aspects of Computer Science (STACS 2016)

Abstract
Regular cost functions form a quantitative extension of regular languages that share the array of characterisations the latter possess. In this theory, functions are treated only up to preservation of boundedness on all subsets of the domain. In this work, we subject the well known distance automata (also called min-automata), and their dual max-automata to this framework, and obtain a number of effective characterisations in terms of logic, expressions and algebra.
Cite as

Thomas Colcombet, Denis Kuperberg, Amaldev Manuel, and Szymon Torunczyk. Cost Functions Definable by Min/Max Automata. In 33rd Symposium on Theoretical Aspects of Computer Science (STACS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 47, pp. 29:1-29:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{colcombet_et_al:LIPIcs.STACS.2016.29,
  author =	{Colcombet, Thomas and Kuperberg, Denis and Manuel, Amaldev and Torunczyk, Szymon},
  title =	{{Cost Functions Definable by Min/Max Automata}},
  booktitle =	{33rd Symposium on Theoretical Aspects of Computer Science (STACS 2016)},
  pages =	{29:1--29:13},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-001-9},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{47},
  editor =	{Ollinger, Nicolas and Vollmer, Heribert},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2016.29},
  URN =		{urn:nbn:de:0030-drops-57305},
  doi =		{10.4230/LIPIcs.STACS.2016.29},
  annote =	{Keywords: distance automata, B-automata, regular cost functions, stabilisation monoids, decidability, min-automata, max-automata}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2015.98
Fragments of Fixpoint Logic on Data Words

Authors: Thomas Colcombet and Amaldev Manuel

Published in: LIPIcs, Volume 45, 35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015)

Abstract
We study fragments of a mu-calculus over data words whose primary modalities are 'go to next position' (X^g), 'go to previous position}' (Y^g), 'go to next position with the same data value' (X^c), 'go to previous position with the same data value (Y^c)'. Our focus is on two fragments that are called the bounded mode alternation fragment (BMA) and the bounded reversal fragment (BR). BMA is the fragment of those formulas that whose unfoldings contain only a bounded number of alternations between global modalities (X^g, Y^g) and class modalities (X^c, Y^c). Similarly BR is the fragment of formulas whose unfoldings contain only a bounded number of alternations between left modalities (Y^g, Y^c) and right modalities (X^g, X^c). We show that these fragments are decidable (by inclusion in Data Automata), enjoy effective Boolean closure, and contain previously defined logics such as the two variable fragment of first-order logic and DataLTL. More precisely the definable language in each formalism obey the following inclusions that are effective. FO^2 subsetneq DataLTL subsetneq BMA BR subsetneq nu subseteq Data Automata. Our main contribution is a method to prove inexpressibility results on the fragment BMA by reducing them to inexpressibility results for combinatorial expressions. More precisely we prove the following hierarchy of definable languages, emptyset=BMA^0 subsetneq BMA^1 subsetneq ... subsetneq BMA subsetneq BR , where BMA^k is the set of all formulas whose unfoldings contain at most k-1 alternations between global modalities (X^g, Y^g) and class modalities (X^c, Y^c). Since the class BMA is a generalization of FO^2 and DataLTL the inexpressibility results carry over to them as well.
Cite as

Thomas Colcombet and Amaldev Manuel. Fragments of Fixpoint Logic on Data Words. In 35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 45, pp. 98-111, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{colcombet_et_al:LIPIcs.FSTTCS.2015.98,
  author =	{Colcombet, Thomas and Manuel, Amaldev},
  title =	{{Fragments of Fixpoint Logic on Data Words}},
  booktitle =	{35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015)},
  pages =	{98--111},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-97-2},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{45},
  editor =	{Harsha, Prahladh and Ramalingam, G.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2015.98},
  URN =		{urn:nbn:de:0030-drops-56289},
  doi =		{10.4230/LIPIcs.FSTTCS.2015.98},
  annote =	{Keywords: Data words, Data automata, Fixpoint logic}
}
Document
DOI: 10.4230/LIPIcs.STACS.2015.249
Combinatorial Expressions and Lower Bounds

Authors: Thomas Colcombet and Amaldev Manuel

Published in: LIPIcs, Volume 30, 32nd International Symposium on Theoretical Aspects of Computer Science (STACS 2015)

Abstract
A new paradigm, called combinatorial expressions, for computing functions expressing properties over infinite domains is introduced. The main result is a generic technique, for showing indefinability of certain functions by the expressions, which uses a result, namely Hales-Jewett theorem, from Ramsey theory. An application of the technique for proving inexpressibility results for logics on metafinite structures is given. Some extensions and normal forms are also presented.
Cite as

Thomas Colcombet and Amaldev Manuel. Combinatorial Expressions and Lower Bounds. In 32nd International Symposium on Theoretical Aspects of Computer Science (STACS 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 30, pp. 249-261, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{colcombet_et_al:LIPIcs.STACS.2015.249,
  author =	{Colcombet, Thomas and Manuel, Amaldev},
  title =	{{Combinatorial Expressions and Lower Bounds}},
  booktitle =	{32nd International Symposium on Theoretical Aspects of Computer Science (STACS 2015)},
  pages =	{249--261},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-78-1},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{30},
  editor =	{Mayr, Ernst W. and Ollinger, Nicolas},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2015.249},
  URN =		{urn:nbn:de:0030-drops-49181},
  doi =		{10.4230/LIPIcs.STACS.2015.249},
  annote =	{Keywords: expressions, lower bound, indefinability}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2014.267
Generalized Data Automata and Fixpoint Logic

Authors: Thomas Colcombet and Amaldev Manuel

Published in: LIPIcs, Volume 29, 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)

Abstract
Data omega-words are omega-words where each position is additionally labelled by a data value from an infinite alphabet. They can be seen as graphs equipped with two sorts of edges: "next position" and "next position with the same data value". Based on this view, an extension of Data Automata called Generalized Data Automata (GDA) is introduced. While the decidability of emptiness of GDA is open, the decidability for a subclass class called Büchi GDA is shown using Multicounter Automata. Next a natural fixpoint logic is defined on the graphs of data omega-words and it is shown that the mu-fragment as well as the alternation-free fragment is undecidable. But the fragment which is defined by limiting the number of alternations between future and past formulas is shown to be decidable, by first converting the formulas to equivalent alternating Büchi automata and then to Büchi GDA.
Cite as

Thomas Colcombet and Amaldev Manuel. Generalized Data Automata and Fixpoint Logic. In 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 29, pp. 267-278, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)

Copy BibTex To Clipboard

@InProceedings{colcombet_et_al:LIPIcs.FSTTCS.2014.267,
  author =	{Colcombet, Thomas and Manuel, Amaldev},
  title =	{{Generalized Data Automata and Fixpoint Logic}},
  booktitle =	{34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)},
  pages =	{267--278},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-77-4},
  ISSN =	{1868-8969},
  year =	{2014},
  volume =	{29},
  editor =	{Raman, Venkatesh and Suresh, S. P.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2014.267},
  URN =		{urn:nbn:de:0030-drops-48483},
  doi =		{10.4230/LIPIcs.FSTTCS.2014.267},
  annote =	{Keywords: Data words, Data Automata, Decidability, Fixpoint Logic}
}
Document
DOI: 10.4230/LIPIcs.CSL.2013.484
Two-Variable Logic on 2-Dimensional Structures

Authors: Amaldev Manuel and Thomas Zeume

Published in: LIPIcs, Volume 23, Computer Science Logic 2013 (CSL 2013)

Abstract
This paper continues the study of the two-variable fragment of first-order logic (FO^2) over two- dimensional structures, more precisely structures with two orders, their induced successor relations and arbitrarily many unary relations. Our main focus is on ordered data words which are finite sequences from the set \Sigma x D where \Sigma is a finite alphabet and D is an ordered domain. These are naturally represented as labelled finite sets with a linear order <=_l and a total preorder <=_p. We introduce ordered data automata, an automaton model for ordered data words. An ordered data automaton is a composition of a finite state transducer and a finite state automaton over the product Boolean algebra of finite and cofinite subsets of N. We show that ordered data automata are equivalent to the closure of FO^2(+1_l,<=_p,+1_p) under existential quantification of unary relations. Using this automaton model we prove that the finite satisfiability problem for this logic is decidable on structures where the <=_p-equivalence classes are of bounded size. As a corollary, we obtain that finite satisfiability of FO^2 is decidable (and it is equivalent to the reachability problem of vector addition systems) on structures with two linear order successors and a linear order corresponding to one of the successors. Further we prove undecidability of FO^2 on several other two-dimensional structures.
Cite as

Amaldev Manuel and Thomas Zeume. Two-Variable Logic on 2-Dimensional Structures. In Computer Science Logic 2013 (CSL 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 23, pp. 484-499, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)

Copy BibTex To Clipboard

@InProceedings{manuel_et_al:LIPIcs.CSL.2013.484,
  author =	{Manuel, Amaldev and Zeume, Thomas},
  title =	{{Two-Variable Logic on 2-Dimensional Structures}},
  booktitle =	{Computer Science Logic 2013 (CSL 2013)},
  pages =	{484--499},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-60-6},
  ISSN =	{1868-8969},
  year =	{2013},
  volume =	{23},
  editor =	{Ronchi Della Rocca, Simona},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2013.484},
  URN =		{urn:nbn:de:0030-drops-42159},
  doi =		{10.4230/LIPIcs.CSL.2013.484},
  annote =	{Keywords: FO2, Data words, Satisfiability, Decidability, Automata}
}
  • Refine by Author
  • 6 Manuel, Amaldev
  • 4 Colcombet, Thomas
  • 1 Kuperberg, Denis
  • 1 Sreejith, A. V.
  • 1 Torunczyk, Szymon
  • Show More...

  • Refine by Classification

  • Refine by Keyword
  • 3 Data words
  • 2 Decidability
  • 1 Automata
  • 1 B-automata
  • 1 Data Automata
  • Show More...

  • Refine by Type
  • 6 document

  • Refine by Publication Year
  • 2 2015
  • 2 2016
  • 1 2013
  • 1 2014

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact