4 Search Results for "Kucera, Anton�n"

Document
DOI: 10.4230/LIPIcs.CP.2023.22
Binary Constraint Trees and Structured Decomposability

Authors: Petr Kučera

Published in: LIPIcs, Volume 280, 29th International Conference on Principles and Practice of Constraint Programming (CP 2023)

Abstract
A binary constraint tree (BCT, Wang and Yap 2022) is a normalized binary CSP whose constraint graph is a tree. A BCT constraint is a constraint represented with a BCT where some of the variables may be hidden (i.e. existentially quantified and used only for internal representation). Structured decomposable negation normal forms (SDNNF) were introduced by Pipatsrisawat and Darwiche (2008) as a restriction of decomposable negation normal forms (DNNF). Both DNNFs and SDNNFs were studied in the area of knowledge compilation. In this paper we show that the BCT constraints are polynomially equivalent to SDNNFs. In particular, a BCT constraint can be represented with an SDNNF of polynomial size and, on the other hand, a constraint that can be represented with an SDNNF, can be represented as a BCT constraint of polynomial size. This generalizes the result of Wang and Yap (2022) that shows that a multivalued decision diagram (MDD) can be represented with a BCT . Moreover, our result provides a full characterization of binary constraint trees using a language that is well studied in the area of knowledge compilation. It was shown by Wang and Yap (2023) that a CSP on n variables of domain sizes bounded by d that has treewidth k can be encoded as a BCT on O(n) variables with domain sizes O(d^{k+1}). We provide an alternative reduction for the case of binary CSPs. This allows us to compile any binary CSP to an SDNNF of size that is parameterized by d and k.
Cite as

Petr Kučera. Binary Constraint Trees and Structured Decomposability. In 29th International Conference on Principles and Practice of Constraint Programming (CP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 280, pp. 22:1-22:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{kucera:LIPIcs.CP.2023.22,
  author =	{Ku\v{c}era, Petr},
  title =	{{Binary Constraint Trees and Structured Decomposability}},
  booktitle =	{29th International Conference on Principles and Practice of Constraint Programming (CP 2023)},
  pages =	{22:1--22:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-300-3},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{280},
  editor =	{Yap, Roland H. C.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2023.22},
  URN =		{urn:nbn:de:0030-drops-190595},
  doi =		{10.4230/LIPIcs.CP.2023.22},
  annote =	{Keywords: Binary CSP, Binary Constraint Tree, Structured Decomposability, Strucured DNNF, Polynomial Equivalence}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2023.12
Asymptotic Complexity Estimates for Probabilistic Programs and Their VASS Abstractions

Authors: Michal Ajdarów and Antonín Kučera

Published in: LIPIcs, Volume 279, 34th International Conference on Concurrency Theory (CONCUR 2023)

Abstract
The standard approach to analyzing the asymptotic complexity of probabilistic programs is based on studying the asymptotic growth of certain expected values (such as the expected termination time) for increasing input size. We argue that this approach is not sufficiently robust, especially in situations when the expectations are infinite. We propose new estimates for the asymptotic analysis of probabilistic programs with non-deterministic choice that overcome this deficiency. Furthermore, we show how to efficiently compute/analyze these estimates for selected classes of programs represented as Markov decision processes over vector addition systems with states.
Cite as

Michal Ajdarów and Antonín Kučera. Asymptotic Complexity Estimates for Probabilistic Programs and Their VASS Abstractions. In 34th International Conference on Concurrency Theory (CONCUR 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 279, pp. 12:1-12:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{ajdarow_et_al:LIPIcs.CONCUR.2023.12,
  author =	{Ajdar\'{o}w, Michal and Ku\v{c}era, Anton{\'\i}n},
  title =	{{Asymptotic Complexity Estimates for Probabilistic Programs and Their VASS Abstractions}},
  booktitle =	{34th International Conference on Concurrency Theory (CONCUR 2023)},
  pages =	{12:1--12:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-299-0},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{279},
  editor =	{P\'{e}rez, Guillermo A. and Raskin, Jean-Fran\c{c}ois},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2023.12},
  URN =		{urn:nbn:de:0030-drops-190065},
  doi =		{10.4230/LIPIcs.CONCUR.2023.12},
  annote =	{Keywords: Probabilistic programs, asymptotic complexity, vector addition systems}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2021.30
Deciding Polynomial Termination Complexity for VASS Programs

Authors: Michal Ajdarów and Antonín Kučera

Published in: LIPIcs, Volume 203, 32nd International Conference on Concurrency Theory (CONCUR 2021)

Abstract
We show that for every fixed degree k ≥ 3, the problem whether the termination/counter complexity of a given demonic VASS is O(n^k), Ω(n^k), and Θ(n^k) is coNP-complete, NP-complete, and DP-complete, respectively. We also classify the complexity of these problems for k ≤ 2. This shows that the polynomial-time algorithm designed for strongly connected demonic VASS in previous works cannot be extended to the general case. Then, we prove that the same problems for VASS games are PSPACE-complete. Again, we classify the complexity also for k ≤ 2. Tractable subclasses of demonic VASS and VASS games are obtained by bounding certain structural parameters, which opens the way to applications in program analysis despite the presented lower complexity bounds.
Cite as

Michal Ajdarów and Antonín Kučera. Deciding Polynomial Termination Complexity for VASS Programs. In 32nd International Conference on Concurrency Theory (CONCUR 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 203, pp. 30:1-30:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{ajdarow_et_al:LIPIcs.CONCUR.2021.30,
  author =	{Ajdar\'{o}w, Michal and Ku\v{c}era, Anton{\'\i}n},
  title =	{{Deciding Polynomial Termination Complexity for VASS Programs}},
  booktitle =	{32nd International Conference on Concurrency Theory (CONCUR 2021)},
  pages =	{30:1--30:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-203-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{203},
  editor =	{Haddad, Serge and Varacca, Daniele},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2021.30},
  URN =		{urn:nbn:de:0030-drops-144076},
  doi =		{10.4230/LIPIcs.CONCUR.2021.30},
  annote =	{Keywords: Termination complexity, vector addition systems}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2018.33
Automatic Analysis of Expected Termination Time for Population Protocols

Authors: Michael Blondin, Javier Esparza, and Antonín Kucera

Published in: LIPIcs, Volume 118, 29th International Conference on Concurrency Theory (CONCUR 2018)

Abstract
Population protocols are a formal model of sensor networks consisting of identical mobile devices. Two devices can interact and thereby change their states. Computations are infinite sequences of interactions in which the interacting devices are chosen uniformly at random. In well designed population protocols, for every initial configuration of devices, and for every computation starting at this configuration, all devices eventually agree on a consensus value. We address the problem of automatically computing a parametric bound on the expected time the protocol needs to reach this consensus. We present the first algorithm that, when successful, outputs a function f(n) such that the expected time to consensus is bound by O(f(n)), where n is the number of devices executing the protocol. We experimentally show that our algorithm terminates and provides good bounds for many of the protocols found in the literature.
Cite as

Michael Blondin, Javier Esparza, and Antonín Kucera. Automatic Analysis of Expected Termination Time for Population Protocols. In 29th International Conference on Concurrency Theory (CONCUR 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 118, pp. 33:1-33:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{blondin_et_al:LIPIcs.CONCUR.2018.33,
  author =	{Blondin, Michael and Esparza, Javier and Kucera, Anton{\'\i}n},
  title =	{{Automatic Analysis of Expected Termination Time for Population Protocols}},
  booktitle =	{29th International Conference on Concurrency Theory (CONCUR 2018)},
  pages =	{33:1--33:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-087-3},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{118},
  editor =	{Schewe, Sven and Zhang, Lijun},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2018.33},
  URN =		{urn:nbn:de:0030-drops-95711},
  doi =		{10.4230/LIPIcs.CONCUR.2018.33},
  annote =	{Keywords: population protocols, performance analysis, expected termination time}
}
  • Refine by Author
  • 2 Ajdarów, Michal
  • 2 Kučera, Antonín
  • 1 Blondin, Michael
  • 1 Esparza, Javier
  • 1 Kucera, Antonín
  • Show More...

  • Refine by Classification
  • 2 Theory of computation → Models of computation
  • 1 Theory of computation → Automated reasoning
  • 1 Theory of computation → Constraint and logic programming
  • 1 Theory of computation → Distributed computing models
  • 1 Theory of computation → Logic and verification
  • Show More...

  • Refine by Keyword
  • 2 vector addition systems
  • 1 Binary CSP
  • 1 Binary Constraint Tree
  • 1 Polynomial Equivalence
  • 1 Probabilistic programs
  • Show More...

  • Refine by Type
  • 4 document

  • Refine by Publication Year
  • 2 2023
  • 1 2018
  • 1 2021

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