22 Search Results for "Kuperberg, Denis"

Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2024.124
Lookahead Games and Efficient Determinisation of History-Deterministic Büchi Automata

Authors: Rohan Acharya, Marcin Jurdziński, and Aditya Prakash

Published in: LIPIcs, Volume 297, 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024)

Abstract
Our main technical contribution is a polynomial-time determinisation procedure for history-deterministic Büchi automata, which settles an open question of Kuperberg and Skrzypczak, 2015. A key conceptual contribution is the lookahead game, which is a variant of Bagnol and Kuperberg’s token game, in which Adam is given a fixed lookahead. We prove that the lookahead game is equivalent to the 1-token game. This allows us to show that the 1-token game characterises history-determinism for semantically-deterministic Büchi automata, which paves the way to our polynomial-time determinisation procedure.
Cite as

Rohan Acharya, Marcin Jurdziński, and Aditya Prakash. Lookahead Games and Efficient Determinisation of History-Deterministic Büchi Automata. In 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 297, pp. 124:1-124:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{acharya_et_al:LIPIcs.ICALP.2024.124,
  author =	{Acharya, Rohan and Jurdzi\'{n}ski, Marcin and Prakash, Aditya},
  title =	{{Lookahead Games and Efficient Determinisation of History-Deterministic B\"{u}chi Automata}},
  booktitle =	{51st International Colloquium on Automata, Languages, and Programming (ICALP 2024)},
  pages =	{124:1--124:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-322-5},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{297},
  editor =	{Bringmann, Karl and Grohe, Martin and Puppis, Gabriele and Svensson, Ola},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2024.124},
  URN =		{urn:nbn:de:0030-drops-202672},
  doi =		{10.4230/LIPIcs.ICALP.2024.124},
  annote =	{Keywords: History determinism, Good-for-games, Automata over infinite words, Games}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2024.125
Edit Distance of Finite State Transducers

Authors: C. Aiswarya, Amaldev Manuel, and Saina Sunny

Published in: LIPIcs, Volume 297, 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024)

Abstract
We lift metrics over words to metrics over word-to-word transductions, by defining the distance between two transductions as the supremum of the distances of their respective outputs over all inputs. This allows to compare transducers beyond equivalence. Two transducers are close (resp. k-close) with respect to a metric if their distance is finite (resp. at most k). Over integer-valued metrics computing the distance between transducers is equivalent to deciding the closeness and k-closeness problems. For common integer-valued edit distances such as, Hamming, transposition, conjugacy and Levenshtein family of distances, we show that the closeness and the k-closeness problems are decidable for functional transducers. Hence, the distance with respect to these metrics is also computable. Finally, we relate the notion of distance between functions to the notions of diameter of a relation and index of a relation in another. We show that computing edit distance between functional transducers is equivalent to computing diameter of a rational relation and both are a specific instance of the index problem of rational relations.
Cite as

C. Aiswarya, Amaldev Manuel, and Saina Sunny. Edit Distance of Finite State Transducers. In 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 297, pp. 125:1-125:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{aiswarya_et_al:LIPIcs.ICALP.2024.125,
  author =	{Aiswarya, C. and Manuel, Amaldev and Sunny, Saina},
  title =	{{Edit Distance of Finite State Transducers}},
  booktitle =	{51st International Colloquium on Automata, Languages, and Programming (ICALP 2024)},
  pages =	{125:1--125:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-322-5},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{297},
  editor =	{Bringmann, Karl and Grohe, Martin and Puppis, Gabriele and Svensson, Ola},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2024.125},
  URN =		{urn:nbn:de:0030-drops-202682},
  doi =		{10.4230/LIPIcs.ICALP.2024.125},
  annote =	{Keywords: transducers, edit distance, conjugacy}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2024.157
Domain Reasoning in TopKAT

Authors: Cheng Zhang, Arthur Azevedo de Amorim, and Marco Gaboardi

Published in: LIPIcs, Volume 297, 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024)

Abstract
TopKAT is the algebraic theory of Kleene algebra with tests (KAT) extended with a top element. Compared to KAT, one pleasant feature of TopKAT is that, in relational models, the top element allows us to express the domain and codomain of a relation. This enables several applications in program logics, such as proving under-approximate specifications or reachability properties of imperative programs. However, while TopKAT inherits many pleasant features of KATs, such as having a decidable equational theory, it is incomplete with respect to relational models. In other words, there are properties that hold true of all relational TopKATs but cannot be proved with the axioms of TopKAT. This issue is potentially worrisome for program-logic applications, in which relational models play a key role. In this paper, we further investigate the completeness properties of TopKAT with respect to relational models. We show that TopKAT is complete with respect to (co)domain comparison of KAT terms, but incomplete when comparing the (co)domain of arbitrary TopKAT terms. Since the encoding of under-approximate specifications in TopKAT hinges on this type of formula, the aforementioned incompleteness results have a limited impact when using TopKAT to reason about such specifications.
Cite as

Cheng Zhang, Arthur Azevedo de Amorim, and Marco Gaboardi. Domain Reasoning in TopKAT. In 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 297, pp. 157:1-157:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{zhang_et_al:LIPIcs.ICALP.2024.157,
  author =	{Zhang, Cheng and de Amorim, Arthur Azevedo and Gaboardi, Marco},
  title =	{{Domain Reasoning in TopKAT}},
  booktitle =	{51st International Colloquium on Automata, Languages, and Programming (ICALP 2024)},
  pages =	{157:1--157:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-322-5},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{297},
  editor =	{Bringmann, Karl and Grohe, Martin and Puppis, Gabriele and Svensson, Ola},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2024.157},
  URN =		{urn:nbn:de:0030-drops-203003},
  doi =		{10.4230/LIPIcs.ICALP.2024.157},
  annote =	{Keywords: Kleene algebra, Kleene Algebra With Tests, Kleene Algebra With Domain, Kleene Algebra With Top and Tests, Completeness, Decidability}
}
Document
DOI: 10.4230/LIPIcs.CCC.2023.29
Constant-Depth Circuits vs. Monotone Circuits

Authors: Bruno P. Cavalar and Igor C. Oliveira

Published in: LIPIcs, Volume 264, 38th Computational Complexity Conference (CCC 2023)

Abstract
We establish new separations between the power of monotone and general (non-monotone) Boolean circuits: - For every k ≥ 1, there is a monotone function in AC⁰ (constant-depth poly-size circuits) that requires monotone circuits of depth Ω(log^k n). This significantly extends a classical result of Okol'nishnikova [Okol'nishnikova, 1982] and Ajtai and Gurevich [Ajtai and Gurevich, 1987]. In addition, our separation holds for a monotone graph property, which was unknown even in the context of AC⁰ versus mAC⁰. - For every k ≥ 1, there is a monotone function in AC⁰[⊕] (constant-depth poly-size circuits extended with parity gates) that requires monotone circuits of size exp(Ω(log^k n)). This makes progress towards a question posed by Grigni and Sipser [Grigni and Sipser, 1992]. These results show that constant-depth circuits can be more efficient than monotone formulas and monotone circuits when computing monotone functions. In the opposite direction, we observe that non-trivial simulations are possible in the absence of parity gates: every monotone function computed by an AC⁰ circuit of size s and depth d can be computed by a monotone circuit of size 2^{n - n/O(log s)^{d-1}}. We show that the existence of significantly faster monotone simulations would lead to breakthrough circuit lower bounds. In particular, if every monotone function in AC⁰ admits a polynomial size monotone circuit, then NC² is not contained in NC¹. Finally, we revisit our separation result against monotone circuit size and investigate the limits of our approach, which is based on a monotone lower bound for constraint satisfaction problems (CSPs) established by Göös, Kamath, Robere and Sokolov [Göös et al., 2019] via lifting techniques. Adapting results of Schaefer [Thomas J. Schaefer, 1978] and Allender, Bauland, Immerman, Schnoor and Vollmer [Eric Allender et al., 2009], we obtain an unconditional classification of the monotone circuit complexity of Boolean-valued CSPs via their polymorphisms. This result and the consequences we derive from it might be of independent interest.
Cite as

Bruno P. Cavalar and Igor C. Oliveira. Constant-Depth Circuits vs. Monotone Circuits. In 38th Computational Complexity Conference (CCC 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 264, pp. 29:1-29:37, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{cavalar_et_al:LIPIcs.CCC.2023.29,
  author =	{Cavalar, Bruno P. and Oliveira, Igor C.},
  title =	{{Constant-Depth Circuits vs. Monotone Circuits}},
  booktitle =	{38th Computational Complexity Conference (CCC 2023)},
  pages =	{29:1--29:37},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-282-2},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{264},
  editor =	{Ta-Shma, Amnon},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CCC.2023.29},
  URN =		{urn:nbn:de:0030-drops-182998},
  doi =		{10.4230/LIPIcs.CCC.2023.29},
  annote =	{Keywords: circuit complexity, monotone circuit complexity, bounded-depth circuis, constraint-satisfaction problems}
}
Document
DOI: 10.4230/LIPIcs.CSL.2023.24
Explorable Automata

Authors: Emile Hazard and Denis Kuperberg

Published in: LIPIcs, Volume 252, 31st EACSL Annual Conference on Computer Science Logic (CSL 2023)

Abstract
We define the class of explorable automata on finite or infinite words. This is a generalization of History-Deterministic (HD) automata, where this time non-deterministic choices can be resolved by building finitely many simultaneous runs instead of just one. We show that recognizing HD parity automata of fixed index among explorable ones is in PTime, thereby giving a strong link between the two notions. We then show that recognizing explorable automata is ExpTime-complete, in the case of finite words or Büchi automata. Additionally, we define the notion of ω-explorable automata on infinite words, where countably many runs can be used to resolve the non-deterministic choices. We show that all reachability automata are ω-explorable, but this is not the case for safety ones. We finally show ExpTime-completeness for ω-explorability of automata on infinite words for the safety and co-Büchi acceptance conditions.
Cite as

Emile Hazard and Denis Kuperberg. Explorable Automata. In 31st EACSL Annual Conference on Computer Science Logic (CSL 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 252, pp. 24:1-24:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{hazard_et_al:LIPIcs.CSL.2023.24,
  author =	{Hazard, Emile and Kuperberg, Denis},
  title =	{{Explorable Automata}},
  booktitle =	{31st EACSL Annual Conference on Computer Science Logic (CSL 2023)},
  pages =	{24:1--24:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-264-8},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{252},
  editor =	{Klin, Bartek and Pimentel, Elaine},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2023.24},
  URN =		{urn:nbn:de:0030-drops-174852},
  doi =		{10.4230/LIPIcs.CSL.2023.24},
  annote =	{Keywords: Nondeterminism, automata, complexity}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2022.121
Regular Expressions for Tree-Width 2 Graphs

Authors: Amina Doumane

Published in: LIPIcs, Volume 229, 49th International Colloquium on Automata, Languages, and Programming (ICALP 2022)

Abstract
We propose a syntax of regular expressions, which describes languages of tree-width 2 graphs. We show that these languages correspond exactly to those languages of tree-width 2 graphs, definable in the counting monadic second-order logic (CMSO).
Cite as

Amina Doumane. Regular Expressions for Tree-Width 2 Graphs. In 49th International Colloquium on Automata, Languages, and Programming (ICALP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 229, pp. 121:1-121:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{doumane:LIPIcs.ICALP.2022.121,
  author =	{Doumane, Amina},
  title =	{{Regular Expressions for Tree-Width 2 Graphs}},
  booktitle =	{49th International Colloquium on Automata, Languages, and Programming (ICALP 2022)},
  pages =	{121:1--121:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-235-8},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{229},
  editor =	{Boja\'{n}czyk, Miko{\l}aj and Merelli, Emanuela and Woodruff, David P.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2022.121},
  URN =		{urn:nbn:de:0030-drops-164627},
  doi =		{10.4230/LIPIcs.ICALP.2022.121},
  annote =	{Keywords: Tree width, MSO, Regular expressions}
}
Document
DOI: 10.4230/LIPIcs.CSL.2022.23
Cyclic Proofs for Transfinite Expressions

Authors: Emile Hazard and Denis Kuperberg

Published in: LIPIcs, Volume 216, 30th EACSL Annual Conference on Computer Science Logic (CSL 2022)

Abstract
We introduce a cyclic proof system for proving inclusions of transfinite expressions, describing languages of words of ordinal length. We show that recognising valid cyclic proofs is decidable, that our system is sound and complete, and well-behaved with respect to cuts. Moreover, cyclic proofs can be effectively computed from expressions inclusions. We show how to use this to obtain a Pspace algorithm for transfinite expression inclusion.
Cite as

Emile Hazard and Denis Kuperberg. Cyclic Proofs for Transfinite Expressions. In 30th EACSL Annual Conference on Computer Science Logic (CSL 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 216, pp. 23:1-23:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{hazard_et_al:LIPIcs.CSL.2022.23,
  author =	{Hazard, Emile and Kuperberg, Denis},
  title =	{{Cyclic Proofs for Transfinite Expressions}},
  booktitle =	{30th EACSL Annual Conference on Computer Science Logic (CSL 2022)},
  pages =	{23:1--23:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-218-1},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{216},
  editor =	{Manea, Florin and Simpson, Alex},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2022.23},
  URN =		{urn:nbn:de:0030-drops-157433},
  doi =		{10.4230/LIPIcs.CSL.2022.23},
  annote =	{Keywords: transfinite expressions, transfinite automata, cyclic proofs}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2021.41
Graph Characterization of the Universal Theory of Relations

Authors: Amina Doumane

Published in: LIPIcs, Volume 202, 46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021)

Abstract
The equational theory of relations can be characterized using graphs and homomorphisms. This result, found independently by Freyd and Scedrov and by Andréka and Bredikhin, shows that the equational theory of relations is decidable. In this paper, we extend this characterization to the whole universal first-order theory of relations. Using our characterization, we show that the positive universal fragment is also decidable.
Cite as

Amina Doumane. Graph Characterization of the Universal Theory of Relations. In 46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 202, pp. 41:1-41:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{doumane:LIPIcs.MFCS.2021.41,
  author =	{Doumane, Amina},
  title =	{{Graph Characterization of the Universal Theory of Relations}},
  booktitle =	{46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021)},
  pages =	{41:1--41:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-201-3},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{202},
  editor =	{Bonchi, Filippo and Puglisi, Simon J.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2021.41},
  URN =		{urn:nbn:de:0030-drops-144815},
  doi =		{10.4230/LIPIcs.MFCS.2021.41},
  annote =	{Keywords: Relation algebra, Graph homomorphism, Equational theories, First-order logic}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2021.29
On the Logical Strength of Confluence and Normalisation for Cyclic Proofs

Authors: Anupam Das

Published in: LIPIcs, Volume 195, 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)

Abstract
In this work we address the logical strength of confluence and normalisation for non-wellfounded typing derivations, in the tradition of "cyclic proof theory". We present a circular version CT of Gödel's system T, with the aim of comparing the relative expressivity of the theories CT and T. We approach this problem by formalising rewriting-theoretic results such as confluence and normalisation for the underlying "coterm" rewriting system of CT within fragments of second-order arithmetic. We establish confluence of CT within the theory RCA₀, a conservative extension of primitive recursive arithmetic and IΣ1. This allows us to recast type structures of hereditarily recursive operations as "coterm" models of T. We show that these also form models of CT, by formalising a totality argument for circular typing derivations within suitable fragments of second-order arithmetic. Relying on well-known proof mining results, we thus obtain an interpretation of CT into T; in fact, more precisely, we interpret level-n-CT into level-(n+1)-T, an optimum result in terms of abstraction complexity. A direct consequence of these model-theoretic results is weak normalisation for CT. As further results, we also show strong normalisation for CT and continuity of functionals computed by its type 2 coterms.
Cite as

Anupam Das. On the Logical Strength of Confluence and Normalisation for Cyclic Proofs. In 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 195, pp. 29:1-29:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{das:LIPIcs.FSCD.2021.29,
  author =	{Das, Anupam},
  title =	{{On the Logical Strength of Confluence and Normalisation for Cyclic Proofs}},
  booktitle =	{6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)},
  pages =	{29:1--29:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-191-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{195},
  editor =	{Kobayashi, Naoki},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2021.29},
  URN =		{urn:nbn:de:0030-drops-142678},
  doi =		{10.4230/LIPIcs.FSCD.2021.29},
  annote =	{Keywords: confluence, normalisation, system T, circular proofs, reverse mathematics, type structures}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2020.41
On the Succinctness of Alternating Parity Good-For-Games Automata

Authors: Udi Boker, Denis Kuperberg, Karoliina Lehtinen, and Michał Skrzypczak

Published in: LIPIcs, Volume 182, 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020)

Abstract
We study alternating parity good-for-games (GFG) automata, i.e., alternating parity automata where both conjunctive and disjunctive choices can be resolved in an online manner, without knowledge of the suffix of the input word still to be read. We show that they can be exponentially more succinct than both their nondeterministic and universal counterparts. Furthermore, we present a single exponential determinisation procedure and an Exptime upper bound to the problem of recognising whether an alternating automaton is GFG. We also study the complexity of deciding "half-GFGness", a property specific to alternating automata that only requires nondeterministic choices to be resolved in an online manner. We show that this problem is PSpace-hard already for alternating automata on finite words.
Cite as

Udi Boker, Denis Kuperberg, Karoliina Lehtinen, and Michał Skrzypczak. On the Succinctness of Alternating Parity Good-For-Games Automata. In 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 182, pp. 41:1-41:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{boker_et_al:LIPIcs.FSTTCS.2020.41,
  author =	{Boker, Udi and Kuperberg, Denis and Lehtinen, Karoliina and Skrzypczak, Micha{\l}},
  title =	{{On the Succinctness of Alternating Parity Good-For-Games Automata}},
  booktitle =	{40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020)},
  pages =	{41:1--41:13},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-174-0},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{182},
  editor =	{Saxena, Nitin and Simon, Sunil},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2020.41},
  URN =		{urn:nbn:de:0030-drops-132825},
  doi =		{10.4230/LIPIcs.FSTTCS.2020.41},
  annote =	{Keywords: Good for games, history-determinism, alternation}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2020.58
Regular Resynchronizability of Origin Transducers Is Undecidable

Authors: Denis Kuperberg and Jan Martens

Published in: LIPIcs, Volume 170, 45th International Symposium on Mathematical Foundations of Computer Science (MFCS 2020)

Abstract
We study the relation of containment up to unknown regular resynchronization between two-way non-deterministic transducers. We show that it constitutes a preorder, and that the corresponding equivalence relation is properly intermediate between origin equivalence and classical equivalence. We give a syntactical characterization for containment of two transducers up to resynchronization, and use it to show that this containment relation is undecidable already for one-way non-deterministic transducers, and for simple classes of resynchronizations. This answers the open problem stated in recent works, asking whether this relation is decidable for two-way non-deterministic transducers.
Cite as

Denis Kuperberg and Jan Martens. Regular Resynchronizability of Origin Transducers Is Undecidable. In 45th International Symposium on Mathematical Foundations of Computer Science (MFCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 170, pp. 58:1-58:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{kuperberg_et_al:LIPIcs.MFCS.2020.58,
  author =	{Kuperberg, Denis and Martens, Jan},
  title =	{{Regular Resynchronizability of Origin Transducers Is Undecidable}},
  booktitle =	{45th International Symposium on Mathematical Foundations of Computer Science (MFCS 2020)},
  pages =	{58:1--58:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-159-7},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{170},
  editor =	{Esparza, Javier and Kr\'{a}l', Daniel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2020.58},
  URN =		{urn:nbn:de:0030-drops-127255},
  doi =		{10.4230/LIPIcs.MFCS.2020.58},
  annote =	{Keywords: transducers, origin, resynchronisation, MSO, one-way, two-way, undecidability}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2019.45
Cyclic Proofs and Jumping Automata

Authors: Denis Kuperberg, Laureline Pinault, and Damien Pous

Published in: LIPIcs, Volume 150, 39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2019)

Abstract
We consider a fragment of a cyclic sequent proof system for Kleene algebra, and we see it as a computational device for recognising languages of words. The starting proof system is linear and we show that it captures precisely the regular languages. When adding the standard contraction rule, the expressivity raises significantly; we characterise the corresponding class of languages using a new notion of multi-head finite automata, where heads can jump.
Cite as

Denis Kuperberg, Laureline Pinault, and Damien Pous. Cyclic Proofs and Jumping Automata. In 39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 150, pp. 45:1-45:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{kuperberg_et_al:LIPIcs.FSTTCS.2019.45,
  author =	{Kuperberg, Denis and Pinault, Laureline and Pous, Damien},
  title =	{{Cyclic Proofs and Jumping Automata}},
  booktitle =	{39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2019)},
  pages =	{45:1--45:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-131-3},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{150},
  editor =	{Chattopadhyay, Arkadev and Gastin, Paul},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2019.45},
  URN =		{urn:nbn:de:0030-drops-116071},
  doi =		{10.4230/LIPIcs.FSTTCS.2019.45},
  annote =	{Keywords: Cyclic proofs, regular languages, multi-head automata, transducers}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2018.16
Büchi Good-for-Games Automata Are Efficiently Recognizable

Authors: Marc Bagnol and Denis Kuperberg

Published in: LIPIcs, Volume 122, 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018)

Abstract
Good-for-Games (GFG) automata offer a compromise between deterministic and nondeterministic automata. They can resolve nondeterministic choices in a step-by-step fashion, without needing any information about the remaining suffix of the word. These automata can be used to solve games with omega-regular conditions, and in particular were introduced as a tool to solve Church's synthesis problem. We focus here on the problem of recognizing Büchi GFG automata, that we call Büchi GFGness problem: given a nondeterministic Büchi automaton, is it GFG? We show that this problem can be decided in P, and more precisely in O(n^4m^2|Sigma|^2), where n is the number of states, m the number of transitions and |Sigma| is the size of the alphabet. We conjecture that a very similar algorithm solves the problem in polynomial time for any fixed parity acceptance condition.
Cite as

Marc Bagnol and Denis Kuperberg. Büchi Good-for-Games Automata Are Efficiently Recognizable. In 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 122, pp. 16:1-16:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{bagnol_et_al:LIPIcs.FSTTCS.2018.16,
  author =	{Bagnol, Marc and Kuperberg, Denis},
  title =	{{B\"{u}chi Good-for-Games Automata Are Efficiently Recognizable}},
  booktitle =	{38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018)},
  pages =	{16:1--16:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-093-4},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{122},
  editor =	{Ganguly, Sumit and Pandya, Paritosh},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2018.16},
  URN =		{urn:nbn:de:0030-drops-99157},
  doi =		{10.4230/LIPIcs.FSTTCS.2018.16},
  annote =	{Keywords: B\"{u}chi, automata, games, polynomial time, nondeterminism}
}
Document
DOI: 10.4230/LIPIcs.STACS.2018.47
Width of Non-deterministic Automata

Authors: Denis Kuperberg and Anirban Majumdar

Published in: LIPIcs, Volume 96, 35th Symposium on Theoretical Aspects of Computer Science (STACS 2018)

Abstract
We introduce a measure called width, quantifying the amount of nondeterminism in automata. Width generalises the notion of good-for-games (GFG) automata, that correspond to NFAs of width 1, and where an accepting run can be built on-the-fly on any accepted input. We describe an incremental determinisation construction on NFAs, which can be more efficient than the full powerset determinisation, depending on the width of the input NFA. This construction can be generalised to infinite words, and is particularly well-suited to coBüchi automata in this context. For coBüchi automata, this procedure can be used to compute either a deterministic automaton or a GFG one, and it is algorithmically more efficient in this last case. We show this fact by proving that checking whether a coBüchi automaton is determinisable by pruning is NP-complete. On finite or infinite words, we show that computing the width of an automaton is PSPACE-hard.
Cite as

Denis Kuperberg and Anirban Majumdar. Width of Non-deterministic Automata. In 35th Symposium on Theoretical Aspects of Computer Science (STACS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 96, pp. 47:1-47:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{kuperberg_et_al:LIPIcs.STACS.2018.47,
  author =	{Kuperberg, Denis and Majumdar, Anirban},
  title =	{{Width of Non-deterministic Automata}},
  booktitle =	{35th Symposium on Theoretical Aspects of Computer Science (STACS 2018)},
  pages =	{47:1--47:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-062-0},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{96},
  editor =	{Niedermeier, Rolf and Vall\'{e}e, Brigitte},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2018.47},
  URN =		{urn:nbn:de:0030-drops-84963},
  doi =		{10.4230/LIPIcs.STACS.2018.47},
  annote =	{Keywords: width, non-deterministic automata, determinisation, good-for-games, complexity}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2016.12
Soundness in Negotiations

Authors: Javier Esparza, Denis Kuperberg, Anca Muscholl, and Igor Walukiewicz

Published in: LIPIcs, Volume 59, 27th International Conference on Concurrency Theory (CONCUR 2016)

Abstract
Negotiations are a formalism for describing multiparty distributed cooperation. Alternatively, they can be seen as a model of concurrency with synchronized choice as communication primitive. Well-designed negotiations must be sound, meaning that, whatever its current state, the negotiation can still be completed. In a former paper, Esparza and Desel have shown that deciding soundness of a negotiation is PSPACE-complete, and in PTIME if the negotiation is deterministic. They have also provided an algorithm for an intermediate class of acyclic, non-deterministic negotiations, but left the complexity of the soundness problem open. In the first part of this paper we study two further analysis problems for sound acyclic deterministic negotiations, called the race and the omission problem, and give polynomial algorithms. We use these results to provide the first polynomial algorithm for some analysis problems of workflow nets with data previously studied by Trcka, van der Aalst, and Sidorova. In the second part we solve the open question of Esparza and Desel's paper. We show that soundness of acyclic, weakly non-deterministic negotiations is in PTIME, and that checking soundness is already NP-complete for slightly more general classes.
Cite as

Javier Esparza, Denis Kuperberg, Anca Muscholl, and Igor Walukiewicz. Soundness in Negotiations. In 27th International Conference on Concurrency Theory (CONCUR 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 59, pp. 12:1-12:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{esparza_et_al:LIPIcs.CONCUR.2016.12,
  author =	{Esparza, Javier and Kuperberg, Denis and Muscholl, Anca and Walukiewicz, Igor},
  title =	{{Soundness in Negotiations}},
  booktitle =	{27th International Conference on Concurrency Theory (CONCUR 2016)},
  pages =	{12:1--12:13},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-017-0},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{59},
  editor =	{Desharnais, Jos\'{e}e and Jagadeesan, Radha},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2016.12},
  URN =		{urn:nbn:de:0030-drops-61636},
  doi =		{10.4230/LIPIcs.CONCUR.2016.12},
  annote =	{Keywords: Negotiations, workflows, soundness, verification, concurrency}
}
  • Refine by Author
  • 15 Kuperberg, Denis
  • 2 Almagor, Shaull
  • 2 Colcombet, Thomas
  • 2 Doumane, Amina
  • 2 Hazard, Emile
  • Show More...

  • Refine by Classification
  • 3 Theory of computation → Formal languages and automata theory
  • 2 Mathematics of computing → Discrete mathematics
  • 2 Theory of computation → Automata over infinite objects
  • 2 Theory of computation → Logic and verification
  • 2 Theory of computation → Proof theory
  • Show More...

  • Refine by Keyword
  • 4 complexity
  • 4 regular languages
  • 3 Automata
  • 3 transducers
  • 2 MSO
  • Show More...

  • Refine by Type
  • 22 document

  • Refine by Publication Year
  • 3 2016
  • 3 2024
  • 2 2011
  • 2 2018
  • 2 2020
  • Show More...

© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact