26 Search Results for "Kov�cs, Andr�s"

Document
DOI: 10.4230/LIPIcs.STACS.2024.41
Linear Loop Synthesis for Quadratic Invariants

Authors: S. Hitarth, George Kenison, Laura Kovács, and Anton Varonka

Published in: LIPIcs, Volume 289, 41st International Symposium on Theoretical Aspects of Computer Science (STACS 2024)

Abstract
Invariants are key to formal loop verification as they capture loop properties that are valid before and after each loop iteration. Yet, generating invariants is a notorious task already for syntactically restricted classes of loops. Rather than generating invariants for given loops, in this paper we synthesise loops that exhibit a predefined behaviour given by an invariant. From the perspective of formal loop verification, the synthesised loops are thus correct by design and no longer need to be verified. To overcome the hardness of reasoning with arbitrarily strong invariants, in this paper we construct simple (non-nested) while loops with linear updates that exhibit polynomial equality invariants. Rather than solving arbitrary polynomial equations, we consider loop properties defined by a single quadratic invariant in any number of variables. We present a procedure that, given a quadratic equation, decides whether a loop with affine updates satisfying this equation exists. Furthermore, if the answer is positive, the procedure synthesises a loop and ensures its variables achieve infinitely many different values.
Cite as

S. Hitarth, George Kenison, Laura Kovács, and Anton Varonka. Linear Loop Synthesis for Quadratic Invariants. In 41st International Symposium on Theoretical Aspects of Computer Science (STACS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 289, pp. 41:1-41:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{hitarth_et_al:LIPIcs.STACS.2024.41,
  author =	{Hitarth, S. and Kenison, George and Kov\'{a}cs, Laura and Varonka, Anton},
  title =	{{Linear Loop Synthesis for Quadratic Invariants}},
  booktitle =	{41st International Symposium on Theoretical Aspects of Computer Science (STACS 2024)},
  pages =	{41:1--41:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-311-9},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{289},
  editor =	{Beyersdorff, Olaf and Kant\'{e}, Mamadou Moustapha and Kupferman, Orna and Lokshtanov, Daniel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2024.41},
  URN =		{urn:nbn:de:0030-drops-197512},
  doi =		{10.4230/LIPIcs.STACS.2024.41},
  annote =	{Keywords: program synthesis, loop invariants, verification, Diophantine equations}
}
Document
DOI: 10.4230/LIPIcs.ESA.2023.47
Correlating Theory and Practice in Finding Clubs and Plexes

Authors: Aleksander Figiel, Tomohiro Koana, André Nichterlein, and Niklas Wünsche

Published in: LIPIcs, Volume 274, 31st Annual European Symposium on Algorithms (ESA 2023)

Abstract
For solving NP-hard problems there is often a huge gap between theoretical guarantees and observed running times on real-world instances. As a first step towards tackling this issue, we propose an approach to quantify the correlation between theoretical and observed running times. We use two NP-hard problems related to finding large "cliquish" subgraphs in a given graph as demonstration of this measure. More precisely, we focus on finding maximum s-clubs and s-plexes, i. e., graphs of diameter s and graphs where each vertex is adjacent to all but s vertices. Preprocessing based on Turing kernelization is a standard tool to tackle these problems, especially on sparse graphs. We provide a parameterized analysis for the Turing kernelization and demonstrate their usefulness in practice. Moreover, we demonstrate that our measure indeed captures the correlation between these new theoretical and the observed running times.
Cite as

Aleksander Figiel, Tomohiro Koana, André Nichterlein, and Niklas Wünsche. Correlating Theory and Practice in Finding Clubs and Plexes. In 31st Annual European Symposium on Algorithms (ESA 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 274, pp. 47:1-47:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{figiel_et_al:LIPIcs.ESA.2023.47,
  author =	{Figiel, Aleksander and Koana, Tomohiro and Nichterlein, Andr\'{e} and W\"{u}nsche, Niklas},
  title =	{{Correlating Theory and Practice in Finding Clubs and Plexes}},
  booktitle =	{31st Annual European Symposium on Algorithms (ESA 2023)},
  pages =	{47:1--47:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-295-2},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{274},
  editor =	{G{\o}rtz, Inge Li and Farach-Colton, Martin and Puglisi, Simon J. and Herman, Grzegorz},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ESA.2023.47},
  URN =		{urn:nbn:de:0030-drops-187000},
  doi =		{10.4230/LIPIcs.ESA.2023.47},
  annote =	{Keywords: Preprocessing, Turing kernelization, Pearson correlation coefficient}
}
Document
Track A: Algorithms, Complexity and Games
DOI: 10.4230/LIPIcs.ICALP.2022.21
Fast Sampling via Spectral Independence Beyond Bounded-Degree Graphs

Authors: Ivona Bezáková, Andreas Galanis, Leslie Ann Goldberg, and Daniel Štefankovič

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

Abstract
Spectral independence is a recently-developed framework for obtaining sharp bounds on the convergence time of the classical Glauber dynamics. This new framework has yielded optimal O(n log n) sampling algorithms on bounded-degree graphs for a large class of problems throughout the so-called uniqueness regime, including, for example, the problems of sampling independent sets, matchings, and Ising-model configurations. Our main contribution is to relax the bounded-degree assumption that has so far been important in establishing and applying spectral independence. Previous methods for avoiding degree bounds rely on using L^p-norms to analyse contraction on graphs with bounded connective constant (Sinclair, Srivastava, Yin; FOCS'13). The non-linearity of L^p-norms is an obstacle to applying these results to bound spectral independence. Our solution is to capture the L^p-analysis recursively by amortising over the subtrees of the recurrence used to analyse contraction. Our method generalises previous analyses that applied only to bounded-degree graphs. As a main application of our techniques, we consider the random graph G(n,d/n), where the previously known algorithms run in time n^O(log d) or applied only to large d. We refine these algorithmic bounds significantly, and develop fast nearly linear algorithms based on Glauber dynamics that apply to all constant d, throughout the uniqueness regime.
Cite as

Ivona Bezáková, Andreas Galanis, Leslie Ann Goldberg, and Daniel Štefankovič. Fast Sampling via Spectral Independence Beyond Bounded-Degree Graphs. In 49th International Colloquium on Automata, Languages, and Programming (ICALP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 229, pp. 21:1-21:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{bezakova_et_al:LIPIcs.ICALP.2022.21,
  author =	{Bez\'{a}kov\'{a}, Ivona and Galanis, Andreas and Goldberg, Leslie Ann and \v{S}tefankovi\v{c}, Daniel},
  title =	{{Fast Sampling via Spectral Independence Beyond Bounded-Degree Graphs}},
  booktitle =	{49th International Colloquium on Automata, Languages, and Programming (ICALP 2022)},
  pages =	{21:1--21:16},
  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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2022.21},
  URN =		{urn:nbn:de:0030-drops-163622},
  doi =		{10.4230/LIPIcs.ICALP.2022.21},
  annote =	{Keywords: Hard-core model, Random graphs, Markov chains}
}
Document
DOI: 10.4230/LIPIcs.CSL.2022.28
Generalized Universe Hierarchies and First-Class Universe Levels

Authors: András Kovács

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

Abstract
In type theories, universe hierarchies are commonly used to increase the expressive power of the theory while avoiding inconsistencies arising from size issues. There are numerous ways to specify universe hierarchies, and theories may differ in details of cumulativity, choice of universe levels, specification of type formers and eliminators, and available internal operations on levels. In the current work, we aim to provide a framework which covers a large part of the design space. First, we develop syntax and semantics for cumulative universe hierarchies, where levels may come from any set equipped with a transitive well-founded ordering. In the semantics, we show that induction-recursion can be used to model transfinite hierarchies, and also support lifting operations on type codes which strictly preserve type formers. Then, we consider a setup where universe levels are first-class types and subject to arbitrary internal reasoning. This generalizes the bounded polymorphism features of Coq and at the same time the internal level computations in Agda.
Cite as

András Kovács. Generalized Universe Hierarchies and First-Class Universe Levels. In 30th EACSL Annual Conference on Computer Science Logic (CSL 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 216, pp. 28:1-28:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{kovacs:LIPIcs.CSL.2022.28,
  author =	{Kov\'{a}cs, Andr\'{a}s},
  title =	{{Generalized Universe Hierarchies and First-Class Universe Levels}},
  booktitle =	{30th EACSL Annual Conference on Computer Science Logic (CSL 2022)},
  pages =	{28:1--28:17},
  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.28},
  URN =		{urn:nbn:de:0030-drops-157485},
  doi =		{10.4230/LIPIcs.CSL.2022.28},
  annote =	{Keywords: type theory, universes}
}
Document
DOI: 10.4230/LIPIcs.TYPES.2019.6
For Finitary Induction-Induction, Induction Is Enough

Authors: Ambrus Kaposi, András Kovács, and Ambroise Lafont

Published in: LIPIcs, Volume 175, 25th International Conference on Types for Proofs and Programs (TYPES 2019)

Abstract
Inductive-inductive types (IITs) are a generalisation of inductive types in type theory. They allow the mutual definition of types with multiple sorts where later sorts can be indexed by previous ones. An example is the Chapman-style syntax of type theory with conversion relations for each sort where e.g. the sort of types is indexed by contexts. In this paper we show that if a model of extensional type theory (ETT) supports indexed W-types, then it supports finitely branching IITs. We use a small internal type theory called the theory of signatures to specify IITs. We show that if a model of ETT supports the syntax for the theory of signatures, then it supports all IITs. We construct this syntax from indexed W-types using preterms and typing relations and prove its initiality following Streicher. The construction of the syntax and its initiality proof were formalised in Agda.
Cite as

Ambrus Kaposi, András Kovács, and Ambroise Lafont. For Finitary Induction-Induction, Induction Is Enough. In 25th International Conference on Types for Proofs and Programs (TYPES 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 175, pp. 6:1-6:30, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{kaposi_et_al:LIPIcs.TYPES.2019.6,
  author =	{Kaposi, Ambrus and Kov\'{a}cs, Andr\'{a}s and Lafont, Ambroise},
  title =	{{For Finitary Induction-Induction, Induction Is Enough}},
  booktitle =	{25th International Conference on Types for Proofs and Programs (TYPES 2019)},
  pages =	{6:1--6:30},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-158-0},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{175},
  editor =	{Bezem, Marc and Mahboubi, Assia},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2019.6},
  URN =		{urn:nbn:de:0030-drops-130707},
  doi =		{10.4230/LIPIcs.TYPES.2019.6},
  annote =	{Keywords: type theory, inductive types, inductive-inductive types}
}
Document
Invited Paper
DOI: 10.4230/LIPIcs.CONCUR.2020.1
On Privacy and Accuracy in Data Releases (Invited Paper)

Authors: Mário S. Alvim, Natasha Fernandes, Annabelle McIver, and Gabriel H. Nunes

Published in: LIPIcs, Volume 171, 31st International Conference on Concurrency Theory (CONCUR 2020)

Abstract
In this paper we study the relationship between privacy and accuracy in the context of correlated datasets. We use a model of quantitative information flow to describe the the trade-off between privacy of individuals' data and and the utility of queries to that data by modelling the effectiveness of adversaries attempting to make inferences after a data release. We show that, where correlations exist in datasets, it is not possible to implement optimal noise-adding mechanisms that give the best possible accuracy or the best possible privacy in all situations. Finally we illustrate the trade-off between accuracy and privacy for local and oblivious differentially private mechanisms in terms of inference attacks on medium-scale datasets.
Cite as

Mário S. Alvim, Natasha Fernandes, Annabelle McIver, and Gabriel H. Nunes. On Privacy and Accuracy in Data Releases (Invited Paper). In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 1:1-1:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{alvim_et_al:LIPIcs.CONCUR.2020.1,
  author =	{Alvim, M\'{a}rio S. and Fernandes, Natasha and McIver, Annabelle and Nunes, Gabriel H.},
  title =	{{On Privacy and Accuracy in Data Releases}},
  booktitle =	{31st International Conference on Concurrency Theory (CONCUR 2020)},
  pages =	{1:1--1:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-160-3},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{171},
  editor =	{Konnov, Igor and Kov\'{a}cs, Laura},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2020.1},
  URN =		{urn:nbn:de:0030-drops-128130},
  doi =		{10.4230/LIPIcs.CONCUR.2020.1},
  annote =	{Keywords: Privacy/utility trade-off, Quantitative Information Flow, inference attacks}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2020.16
On the Separability Problem of String Constraints

Authors: Parosh Aziz Abdulla, Mohamed Faouzi Atig, Vrunda Dave, and Shankara Narayanan Krishna

Published in: LIPIcs, Volume 171, 31st International Conference on Concurrency Theory (CONCUR 2020)

Abstract
We address the separability problem for straight-line string constraints. The separability problem for languages of a class C by a class S asks: given two languages A and B in C, does there exist a language I in S separating A and B (i.e., I is a superset of A and disjoint from B)? The separability of string constraints is the same as the fundamental problem of interpolation for string constraints. We first show that regular separability of straight line string constraints is undecidable. Our second result is the decidability of the separability problem for straight-line string constraints by piece-wise testable languages, though the precise complexity is open. In our third result, we consider the positive fragment of piece-wise testable languages as a separator, and obtain an ExpSpace algorithm for the separability of a useful class of straight-line string constraints, and a Pspace-hardness result.
Cite as

Parosh Aziz Abdulla, Mohamed Faouzi Atig, Vrunda Dave, and Shankara Narayanan Krishna. On the Separability Problem of String Constraints. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 16:1-16:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{abdulla_et_al:LIPIcs.CONCUR.2020.16,
  author =	{Abdulla, Parosh Aziz and Atig, Mohamed Faouzi and Dave, Vrunda and Krishna, Shankara Narayanan},
  title =	{{On the Separability Problem of String Constraints}},
  booktitle =	{31st International Conference on Concurrency Theory (CONCUR 2020)},
  pages =	{16:1--16:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-160-3},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{171},
  editor =	{Konnov, Igor and Kov\'{a}cs, Laura},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2020.16},
  URN =		{urn:nbn:de:0030-drops-128286},
  doi =		{10.4230/LIPIcs.CONCUR.2020.16},
  annote =	{Keywords: string constraints, separability, interpolants}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2020.39
Strategy Complexity of Parity Objectives in Countable MDPs

Authors: Stefan Kiefer, Richard Mayr, Mahsa Shirmohammadi, and Patrick Totzke

Published in: LIPIcs, Volume 171, 31st International Conference on Concurrency Theory (CONCUR 2020)

Abstract
We study countably infinite MDPs with parity objectives. Unlike in finite MDPs, optimal strategies need not exist, and may require infinite memory if they do. We provide a complete picture of the exact strategy complexity of ε-optimal strategies (and optimal strategies, where they exist) for all subclasses of parity objectives in the Mostowski hierarchy. Either MD-strategies, Markov strategies, or 1-bit Markov strategies are necessary and sufficient, depending on the number of colors, the branching degree of the MDP, and whether one considers ε-optimal or optimal strategies. In particular, 1-bit Markov strategies are necessary and sufficient for ε-optimal (resp. optimal) strategies for general parity objectives.
Cite as

Stefan Kiefer, Richard Mayr, Mahsa Shirmohammadi, and Patrick Totzke. Strategy Complexity of Parity Objectives in Countable MDPs. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 39:1-39:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{kiefer_et_al:LIPIcs.CONCUR.2020.39,
  author =	{Kiefer, Stefan and Mayr, Richard and Shirmohammadi, Mahsa and Totzke, Patrick},
  title =	{{Strategy Complexity of Parity Objectives in Countable MDPs}},
  booktitle =	{31st International Conference on Concurrency Theory (CONCUR 2020)},
  pages =	{39:1--39:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-160-3},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{171},
  editor =	{Konnov, Igor and Kov\'{a}cs, Laura},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2020.39},
  URN =		{urn:nbn:de:0030-drops-128513},
  doi =		{10.4230/LIPIcs.CONCUR.2020.39},
  annote =	{Keywords: Markov decision processes, Parity objectives, Levy’s zero-one law}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2020.41
The Big-O Problem for Labelled Markov Chains and Weighted Automata

Authors: Dmitry Chistikov, Stefan Kiefer, Andrzej S. Murawski, and David Purser

Published in: LIPIcs, Volume 171, 31st International Conference on Concurrency Theory (CONCUR 2020)

Abstract
Given two weighted automata, we consider the problem of whether one is big-O of the other, i.e., if the weight of every finite word in the first is not greater than some constant multiple of the weight in the second. We show that the problem is undecidable, even for the instantiation of weighted automata as labelled Markov chains. Moreover, even when it is known that one weighted automaton is big-O of another, the problem of finding or approximating the associated constant is also undecidable. Our positive results show that the big-O problem is polynomial-time solvable for unambiguous automata, coNP-complete for unlabelled weighted automata (i.e., when the alphabet is a single character) and decidable, subject to Schanuel’s conjecture, when the language is bounded (i.e., a subset of w_1^* … w_m^* for some finite words w_1,… ,w_m). On labelled Markov chains, the problem can be restated as a ratio total variation distance, which, instead of finding the maximum difference between the probabilities of any two events, finds the maximum ratio between the probabilities of any two events. The problem is related to ε-differential privacy, for which the optimal constant of the big-O notation is exactly exp(ε).
Cite as

Dmitry Chistikov, Stefan Kiefer, Andrzej S. Murawski, and David Purser. The Big-O Problem for Labelled Markov Chains and Weighted Automata. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 41:1-41:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{chistikov_et_al:LIPIcs.CONCUR.2020.41,
  author =	{Chistikov, Dmitry and Kiefer, Stefan and Murawski, Andrzej S. and Purser, David},
  title =	{{The Big-O Problem for Labelled Markov Chains and Weighted Automata}},
  booktitle =	{31st International Conference on Concurrency Theory (CONCUR 2020)},
  pages =	{41:1--41:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-160-3},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{171},
  editor =	{Konnov, Igor and Kov\'{a}cs, Laura},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2020.41},
  URN =		{urn:nbn:de:0030-drops-128534},
  doi =		{10.4230/LIPIcs.CONCUR.2020.41},
  annote =	{Keywords: weighted automata, labelled Markov chains, probabilistic systems}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2020.42
Determinisability of One-Clock Timed Automata

Authors: Lorenzo Clemente, Sławomir Lasota, and Radosław Piórkowski

Published in: LIPIcs, Volume 171, 31st International Conference on Concurrency Theory (CONCUR 2020)

Abstract
The deterministic membership problem for timed automata asks whether the timed language recognised by a nondeterministic timed automaton can be recognised by a deterministic timed automaton. We show that the problem is decidable when the input automaton is a one-clock nondeterministic timed automaton without epsilon transitions and the number of clocks of the deterministic timed automaton is fixed. We show that the problem in all the other cases is undecidable, i.e., when either 1) the input nondeterministic timed automaton has two clocks or more, or 2) it uses epsilon transitions, or 3) the number of clocks of the output deterministic automaton is not fixed.
Cite as

Lorenzo Clemente, Sławomir Lasota, and Radosław Piórkowski. Determinisability of One-Clock Timed Automata. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 42:1-42:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{clemente_et_al:LIPIcs.CONCUR.2020.42,
  author =	{Clemente, Lorenzo and Lasota, S{\l}awomir and Pi\'{o}rkowski, Rados{\l}aw},
  title =	{{Determinisability of One-Clock Timed Automata}},
  booktitle =	{31st International Conference on Concurrency Theory (CONCUR 2020)},
  pages =	{42:1--42:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-160-3},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{171},
  editor =	{Konnov, Igor and Kov\'{a}cs, Laura},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2020.42},
  URN =		{urn:nbn:de:0030-drops-128542},
  doi =		{10.4230/LIPIcs.CONCUR.2020.42},
  annote =	{Keywords: Timed automata, determinisation, deterministic membership problem}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2020.48
Reachability in Fixed Dimension Vector Addition Systems with States

Authors: Wojciech Czerwiński, Sławomir Lasota, Ranko Lazić, Jérôme Leroux, and Filip Mazowiecki

Published in: LIPIcs, Volume 171, 31st International Conference on Concurrency Theory (CONCUR 2020)

Abstract
The reachability problem is a central decision problem in verification of vector addition systems with states (VASS). In spite of recent progress, the complexity of the reachability problem remains unsettled, and it is closely related to the lengths of shortest VASS runs that witness reachability. We obtain three main results for VASS of fixed dimension. For the first two, we assume that the integers in the input are given in unary, and that the control graph of the given VASS is flat (i.e., without nested cycles). We obtain a family of VASS in dimension 3 whose shortest runs are exponential, and we show that the reachability problem is NP-hard in dimension 7. These results resolve negatively questions that had been posed by the works of Blondin et al. in LICS 2015 and Englert et al. in LICS 2016, and contribute a first construction that distinguishes 3-dimensional flat VASS from 2-dimensional ones. Our third result, by means of a novel family of products of integer fractions, shows that 4-dimensional VASS can have doubly exponentially long shortest runs. The smallest dimension for which this was previously known is 14.
Cite as

Wojciech Czerwiński, Sławomir Lasota, Ranko Lazić, Jérôme Leroux, and Filip Mazowiecki. Reachability in Fixed Dimension Vector Addition Systems with States. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 48:1-48:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{czerwinski_et_al:LIPIcs.CONCUR.2020.48,
  author =	{Czerwi\'{n}ski, Wojciech and Lasota, S{\l}awomir and Lazi\'{c}, Ranko and Leroux, J\'{e}r\^{o}me and Mazowiecki, Filip},
  title =	{{Reachability in Fixed Dimension Vector Addition Systems with States}},
  booktitle =	{31st International Conference on Concurrency Theory (CONCUR 2020)},
  pages =	{48:1--48:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-160-3},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{171},
  editor =	{Konnov, Igor and Kov\'{a}cs, Laura},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2020.48},
  URN =		{urn:nbn:de:0030-drops-128605},
  doi =		{10.4230/LIPIcs.CONCUR.2020.48},
  annote =	{Keywords: reachability problem, vector addition systems, Petri nets}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2020.20
List Homomorphism Problems for Signed Graphs

Authors: Jan Bok, Richard Brewster, Tomás Feder, Pavol Hell, and Nikola Jedličková

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

Abstract
We consider homomorphisms of signed graphs from a computational perspective. In particular, we study the list homomorphism problem seeking a homomorphism of an input signed graph (G,σ), equipped with lists L(v) ⊆ V(H), v ∈ V(G), of allowed images, to a fixed target signed graph (H,π). The complexity of the similar homomorphism problem without lists (corresponding to all lists being L(v) = V(H)) has been previously classified by Brewster and Siggers, but the list version remains open and appears difficult. Both versions (with lists or without lists) can be formulated as constraint satisfaction problems, and hence enjoy the algebraic dichotomy classification recently verified by Bulatov and Zhuk. By contrast, we seek a combinatorial classification for the list version, akin to the combinatorial classification for the version without lists completed by Brewster and Siggers. We illustrate the possible complications by classifying the complexity of the list homomorphism problem when H is a (reflexive or irreflexive) signed tree. It turns out that the problems are polynomial-time solvable for certain caterpillar-like trees, and are NP-complete otherwise. The tools we develop will be useful for classifications of other classes of signed graphs, and we mention some follow-up research of this kind; those classifications are surprisingly complex.
Cite as

Jan Bok, Richard Brewster, Tomás Feder, Pavol Hell, and Nikola Jedličková. List Homomorphism Problems for Signed Graphs. In 45th International Symposium on Mathematical Foundations of Computer Science (MFCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 170, pp. 20:1-20:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{bok_et_al:LIPIcs.MFCS.2020.20,
  author =	{Bok, Jan and Brewster, Richard and Feder, Tom\'{a}s and Hell, Pavol and Jedli\v{c}kov\'{a}, Nikola},
  title =	{{List Homomorphism Problems for Signed Graphs}},
  booktitle =	{45th International Symposium on Mathematical Foundations of Computer Science (MFCS 2020)},
  pages =	{20:1--20: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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2020.20},
  URN =		{urn:nbn:de:0030-drops-126886},
  doi =		{10.4230/LIPIcs.MFCS.2020.20},
  annote =	{Keywords: complexity, dichotomy, graph homomorphism, signed graph}
}
Document
DOI: 10.4230/LIPIcs.CCC.2020.23
A Super-Quadratic Lower Bound for Depth Four Arithmetic Circuits

Authors: Nikhil Gupta, Chandan Saha, and Bhargav Thankey

Published in: LIPIcs, Volume 169, 35th Computational Complexity Conference (CCC 2020)

Abstract
We show an Ω̃(n^2.5) lower bound for general depth four arithmetic circuits computing an explicit n-variate degree-Θ(n) multilinear polynomial over any field of characteristic zero. To our knowledge, and as stated in the survey [Amir Shpilka and Amir Yehudayoff, 2010], no super-quadratic lower bound was known for depth four circuits over fields of characteristic ≠ 2 before this work. The previous best lower bound is Ω̃(n^1.5) [Abhijat Sharma, 2017], which is a slight quantitative improvement over the roughly Ω(n^1.33) bound obtained by invoking the super-linear lower bound for constant depth circuits in [Ran Raz, 2010; Victor Shoup and Roman Smolensky, 1997]. Our lower bound proof follows the approach of the almost cubic lower bound for depth three circuits in [Neeraj Kayal et al., 2016] by replacing the shifted partials measure with a suitable variant of the projected shifted partials measure, but it differs from [Neeraj Kayal et al., 2016]’s proof at a crucial step - namely, the way "heavy" product gates are handled. Loosely speaking, a heavy product gate has a relatively high fan-in. Product gates of a depth three circuit compute products of affine forms, and so, it is easy to prune Θ(n) many heavy product gates by projecting the circuit to a low-dimensional affine subspace [Neeraj Kayal et al., 2016; Amir Shpilka and Avi Wigderson, 2001]. However, in a depth four circuit, the second (from the top) layer of product gates compute products of polynomials having arbitrary degree, and hence it was not clear how to prune such heavy product gates from the circuit. We show that heavy product gates can also be eliminated from a depth four circuit by projecting the circuit to a low-dimensional affine subspace, unless the heavy gates together account for Ω̃(n^2.5) size. This part of our argument is inspired by a well-known greedy approximation algorithm for the weighted set-cover problem.
Cite as

Nikhil Gupta, Chandan Saha, and Bhargav Thankey. A Super-Quadratic Lower Bound for Depth Four Arithmetic Circuits. In 35th Computational Complexity Conference (CCC 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 169, pp. 23:1-23:31, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{gupta_et_al:LIPIcs.CCC.2020.23,
  author =	{Gupta, Nikhil and Saha, Chandan and Thankey, Bhargav},
  title =	{{A Super-Quadratic Lower Bound for Depth Four Arithmetic Circuits}},
  booktitle =	{35th Computational Complexity Conference (CCC 2020)},
  pages =	{23:1--23:31},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-156-6},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{169},
  editor =	{Saraf, Shubhangi},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CCC.2020.23},
  URN =		{urn:nbn:de:0030-drops-125757},
  doi =		{10.4230/LIPIcs.CCC.2020.23},
  annote =	{Keywords: depth four arithmetic circuits, Projected Shifted Partials, super-quadratic lower bound}
}
Document
DOI: 10.4230/LIPIcs.SoCG.2020.61
Bounding Radon Number via Betti Numbers

Authors: Zuzana Patáková

Published in: LIPIcs, Volume 164, 36th International Symposium on Computational Geometry (SoCG 2020)

Abstract
We prove general topological Radon-type theorems for sets in ℝ^d, smooth real manifolds or finite dimensional simplicial complexes. Combined with a recent result of Holmsen and Lee, it gives fractional Helly theorem, and consequently the existence of weak ε-nets as well as a (p,q)-theorem. More precisely: Let X be either ℝ^d, smooth real d-manifold, or a finite d-dimensional simplicial complex. Then if F is a finite, intersection-closed family of sets in X such that the ith reduced Betti number (with ℤ₂ coefficients) of any set in F is at most b for every non-negative integer i less or equal to k, then the Radon number of F is bounded in terms of b and X. Here k is the smallest integer larger or equal to d/2 - 1 if X = ℝ^d; k=d-1 if X is a smooth real d-manifold and not a surface, k=0 if X is a surface and k=d if X is a d-dimensional simplicial complex. Using the recent result of the author and Kalai, we manage to prove the following optimal bound on fractional Helly number for families of open sets in a surface: Let F be a finite family of open sets in a surface S such that the intersection of any subfamily of F is either empty, or path-connected. Then the fractional Helly number of F is at most three. This also settles a conjecture of Holmsen, Kim, and Lee about an existence of a (p,q)-theorem for open subsets of a surface.
Cite as

Zuzana Patáková. Bounding Radon Number via Betti Numbers. In 36th International Symposium on Computational Geometry (SoCG 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 164, pp. 61:1-61:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{patakova:LIPIcs.SoCG.2020.61,
  author =	{Pat\'{a}kov\'{a}, Zuzana},
  title =	{{Bounding Radon Number via Betti Numbers}},
  booktitle =	{36th International Symposium on Computational Geometry (SoCG 2020)},
  pages =	{61:1--61:13},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-143-6},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{164},
  editor =	{Cabello, Sergio and Chen, Danny Z.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.SoCG.2020.61},
  URN =		{urn:nbn:de:0030-drops-122198},
  doi =		{10.4230/LIPIcs.SoCG.2020.61},
  annote =	{Keywords: Radon number, topological complexity, constrained chain maps, fractional Helly theorem, convexity spaces}
}
Document
DOI: 10.4230/LIPIcs.ITCS.2020.3
Approximately Strategyproof Tournament Rules: On Large Manipulating Sets and Cover-Consistence

Authors: Ariel Schvartzman, S. Matthew Weinberg, Eitan Zlatin, and Albert Zuo

Published in: LIPIcs, Volume 151, 11th Innovations in Theoretical Computer Science Conference (ITCS 2020)

Abstract
We consider the manipulability of tournament rules, in which n teams play a round robin tournament and a winner is (possibly randomly) selected based on the outcome of all binom{n}{2} matches. Prior work defines a tournament rule to be k-SNM-α if no set of ≤ k teams can fix the ≤ binom{k}{2} matches among them to increase their probability of winning by >α and asks: for each k, what is the minimum α(k) such that a Condorcet-consistent (i.e. always selects a Condorcet winner when one exists) k-SNM-α(k) tournament rule exists? A simple example witnesses that α(k) ≥ (k-1)/(2k-1) for all k, and [Jon Schneider et al., 2017] conjectures that this is tight (and prove it is tight for k=2). Our first result refutes this conjecture: there exists a sufficiently large k such that no Condorcet-consistent tournament rule is k-SNM-1/2. Our second result leverages similar machinery to design a new tournament rule which is k-SNM-2/3 for all k (and this is the first tournament rule which is k-SNM-(<1) for all k). Our final result extends prior work, which proves that single-elimination bracket with random seeding is 2-SNM-1/3 [Jon Schneider et al., 2017], in a different direction by seeking a stronger notion of fairness than Condorcet-consistence. We design a new tournament rule, which we call Randomized-King-of-the-Hill, which is 2-SNM-1/3 and cover-consistent (the winner is an uncovered team with probability 1).
Cite as

Ariel Schvartzman, S. Matthew Weinberg, Eitan Zlatin, and Albert Zuo. Approximately Strategyproof Tournament Rules: On Large Manipulating Sets and Cover-Consistence. In 11th Innovations in Theoretical Computer Science Conference (ITCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 151, pp. 3:1-3:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{schvartzman_et_al:LIPIcs.ITCS.2020.3,
  author =	{Schvartzman, Ariel and Weinberg, S. Matthew and Zlatin, Eitan and Zuo, Albert},
  title =	{{Approximately Strategyproof Tournament Rules: On Large Manipulating Sets and Cover-Consistence}},
  booktitle =	{11th Innovations in Theoretical Computer Science Conference (ITCS 2020)},
  pages =	{3:1--3:25},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-134-4},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{151},
  editor =	{Vidick, Thomas},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ITCS.2020.3},
  URN =		{urn:nbn:de:0030-drops-116881},
  doi =		{10.4230/LIPIcs.ITCS.2020.3},
  annote =	{Keywords: Tournament design, Non-manipulability, Cover-consistence, Strategyproofness}
}
  • Refine by Author
  • 4 Bezáková, Ivona
  • 3 Kovács, András
  • 2 Galanis, Andreas
  • 2 Goldberg, Leslie Ann
  • 2 Kaposi, Ambrus
  • Show More...

  • Refine by Classification
  • 3 Theory of computation → Graph algorithms analysis
  • 3 Theory of computation → Type theory
  • 2 Mathematics of computing → Graph theory
  • 2 Theory of computation → Random walks and Markov chains
  • 2 Theory of computation → Verification by model checking
  • Show More...

  • Refine by Keyword
  • 2 inductive-inductive types
  • 2 type theory
  • 1 #P-hard problem
  • 1 Counting oracle
  • 1 Cover-consistence
  • Show More...

  • Refine by Type
  • 26 document

  • Refine by Publication Year
  • 11 2020
  • 4 2018
  • 3 2019
  • 2 2017
  • 2 2022
  • Show More...

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