4 Search Results for "Leiss, Hans"


Document
On the Complexity of Language Membership for Probabilistic Words

Authors: Antoine Amarilli, Mikaël Monet, Paul Raphaël, and Sylvain Salvati

Published in: LIPIcs, Volume 364, 43rd International Symposium on Theoretical Aspects of Computer Science (STACS 2026)


Abstract
We study the membership problem to context-free languages L (CFLs) on probabilistic words, that specify for each position a probability distribution on the letters (assuming independence across positions). Our task is to compute, given a probabilistic word, what is the probability that a word drawn according to the distribution belongs to L. This problem generalizes the problem of counting how many words of length n belong to L, or of counting how many completions of a partial word belong to L. We show that this problem is in polynomial time for unambiguous context-free languages (uCFLs), but can be #P-hard already for unions of two linear uCFLs. More generally, we show that the problem is in polynomial time for so-called poly-slicewise-unambiguous languages, where given a length n we can tractably compute an uCFL for the words of length n in the language. This class includes some inherently ambiguous languages, and implies the tractability of bounded CFLs and of languages recognized by unambiguous polynomial-time counter automata; but we show that the problem can be #P-hard for nondeterministic counter automata, even for Parikh automata with a single counter. We then introduce classes of circuits from knowledge compilation which we use for tractable counting, and show that this covers the tractability of poly-slicewise-unambiguous languages and of some CFLs that are not poly-slicewise-unambiguous. Extending these circuits with negation further allows us to show tractability for the language of primitive words, and for the language of concatenations of two palindromes. We finally show the conditional undecidability of the meta-problem that asks, given a CFG, whether the probabilistic membership problem for that CFG is tractable or #P-hard.

Cite as

Antoine Amarilli, Mikaël Monet, Paul Raphaël, and Sylvain Salvati. On the Complexity of Language Membership for Probabilistic Words. In 43rd International Symposium on Theoretical Aspects of Computer Science (STACS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 364, pp. 5:1-5:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)


Copy BibTex To Clipboard

@InProceedings{amarilli_et_al:LIPIcs.STACS.2026.5,
  author =	{Amarilli, Antoine and Monet, Mika\"{e}l and Rapha\"{e}l, Paul and Salvati, Sylvain},
  title =	{{On the Complexity of Language Membership for Probabilistic Words}},
  booktitle =	{43rd International Symposium on Theoretical Aspects of Computer Science (STACS 2026)},
  pages =	{5:1--5:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-412-3},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{364},
  editor =	{Mahajan, Meena and Manea, Florin and McIver, Annabelle and Thắng, Nguy\~{ê}n Kim},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2026.5},
  URN =		{urn:nbn:de:0030-drops-254943},
  doi =		{10.4230/LIPIcs.STACS.2026.5},
  annote =	{Keywords: Automaton, probabilistic words, context-free grammar, membership problem}
}
Document
On the I/O Complexity of the Cocke-Younger-Kasami Algorithm and of a Family of Related Dynamic Programming Algorithms

Authors: Lorenzo De Stefani and Vedant Gupta

Published in: LIPIcs, Volume 349, 19th International Symposium on Algorithms and Data Structures (WADS 2025)


Abstract
Asymptotically tight lower bounds are derived for the Input/Output (I/O) complexity of a class of dynamic programming algorithms, including matrix chain multiplication, optimal polygon triangulation, and the construction of optimal binary search trees. Assuming no recomputation of intermediate values, we establish an Ω(n³/(√M B)) I/O lower bound, where n denotes the size of the input and M denotes the size of the available fast memory (cache). When recomputation is allowed, we show that the same bound holds for M < cn, where c is a positive constant. In the case where M ≥ 2n, we show an Ω(n/B) I/O lower bound. We also discuss algorithms for which the number of executed I/O operations matches asymptotically each of the presented lower bounds, which are thus asymptotically tight. Additionally, we refine our general method to obtain a lower bound for the I/O complexity of the Cocke-Younger-Kasami algorithm, where the size of the grammar impacts the I/O complexity. An upper bound with asymptotically matching performance in many cases is also provided.

Cite as

Lorenzo De Stefani and Vedant Gupta. On the I/O Complexity of the Cocke-Younger-Kasami Algorithm and of a Family of Related Dynamic Programming Algorithms. In 19th International Symposium on Algorithms and Data Structures (WADS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 349, pp. 49:1-49:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)


Copy BibTex To Clipboard

@InProceedings{destefani_et_al:LIPIcs.WADS.2025.49,
  author =	{De Stefani, Lorenzo and Gupta, Vedant},
  title =	{{On the I/O Complexity of the Cocke-Younger-Kasami Algorithm and of a Family of Related Dynamic Programming Algorithms}},
  booktitle =	{19th International Symposium on Algorithms and Data Structures (WADS 2025)},
  pages =	{49:1--49:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-398-0},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{349},
  editor =	{Morin, Pat and Oh, Eunjin},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.WADS.2025.49},
  URN =		{urn:nbn:de:0030-drops-242800},
  doi =		{10.4230/LIPIcs.WADS.2025.49},
  annote =	{Keywords: I/O complexity, Dynamic Programming Algorithms, Lower Bounds, Recomputation, Cocke-Younger-Kasami}
}
Document
Model Checking as Program Verification by Abstract Interpretation

Authors: Paolo Baldan, Roberto Bruni, Francesco Ranzato, and Diletta Rigo

Published in: LIPIcs, Volume 348, 36th International Conference on Concurrency Theory (CONCUR 2025)


Abstract
Abstract interpretation offers a powerful toolset for static analysis, tackling precision, complexity and state-explosion issues. In the literature, state partitioning abstractions based on (bi)simulation and property-preserving state relations have been successfully applied to abstract model checking. Here, we pursue a different track in which model checking is seen as an instance of program verification. To this purpose, we introduce a suitable language - called MOKA (for MOdel checking as abstract interpretation of 𝖪leene 𝖠lgebras) - which is used to encode temporal formulae as programs. In particular, we show that (universal fragments of) temporal logics, such as ACTL or, more generally, universal μ-calculus can be transformed into MOKA programs. Such programs return all and only the initial states which violate the formula. By applying abstract interpretation to MOKA programs, we pave the way for reusing more general abstractions than partitions as well as for tuning the precision of the abstraction to remove or avoid false alarms. We show how to perform model checking via a program logic that combines under-approximation and abstract interpretation analysis to avoid false alarms. The notion of locally complete abstraction is used to dynamically improve the analysis precision via counterexample-guided domain refinement.

Cite as

Paolo Baldan, Roberto Bruni, Francesco Ranzato, and Diletta Rigo. Model Checking as Program Verification by Abstract Interpretation. In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 8:1-8:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)


Copy BibTex To Clipboard

@InProceedings{baldan_et_al:LIPIcs.CONCUR.2025.8,
  author =	{Baldan, Paolo and Bruni, Roberto and Ranzato, Francesco and Rigo, Diletta},
  title =	{{Model Checking as Program Verification by Abstract Interpretation}},
  booktitle =	{36th International Conference on Concurrency Theory (CONCUR 2025)},
  pages =	{8:1--8:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-389-8},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{348},
  editor =	{Bouyer, Patricia and van de Pol, Jaco},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2025.8},
  URN =		{urn:nbn:de:0030-drops-239583},
  doi =		{10.4230/LIPIcs.CONCUR.2025.8},
  annote =	{Keywords: ACTL, \mu-calculus, model checking, abstract interpretation, program analysis, local completeness, abstract interpretation repair, domain refinement, Kleene algebra with tests}
}
Document
The Matrix Ring of a mu-Continuous Chomsky Algebra is mu-Continuous

Authors: Hans Leiss

Published in: LIPIcs, Volume 62, 25th EACSL Annual Conference on Computer Science Logic (CSL 2016)


Abstract
In the course of providing an (infinitary) axiomatization of the equational theory of the class of context-free languages, Grathwohl, Kozen and Henglein (2013) have introduced the class of mu-continuous Chomsky algebras. These are idempotent semirings where least solutions for systems of polynomial inequations (i.e. context-free grammars) can be computed iteratively and where multiplication is continuous with respect to the least fixed point operator mu. We prove that the matrix ring of a mu-continuous Chomsky algebra also is a mu-continuous Chomsky algebra.

Cite as

Hans Leiss. The Matrix Ring of a mu-Continuous Chomsky Algebra is mu-Continuous. In 25th EACSL Annual Conference on Computer Science Logic (CSL 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 62, pp. 6:1-6:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)


Copy BibTex To Clipboard

@InProceedings{leiss:LIPIcs.CSL.2016.6,
  author =	{Leiss, Hans},
  title =	{{The Matrix Ring of a mu-Continuous Chomsky Algebra is mu-Continuous}},
  booktitle =	{25th EACSL Annual Conference on Computer Science Logic (CSL 2016)},
  pages =	{6:1--6:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-022-4},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{62},
  editor =	{Talbot, Jean-Marc and Regnier, Laurent},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.6},
  URN =		{urn:nbn:de:0030-drops-65467},
  doi =		{10.4230/LIPIcs.CSL.2016.6},
  annote =	{Keywords: context-free language, fixed point operator, idempotent semiring, matrix ring, Chomsky algebra}
}
  • Refine by Type
  • 4 Document/PDF
  • 3 Document/HTML

  • Refine by Publication Year
  • 1 2026
  • 2 2025
  • 1 2016

  • Refine by Author
  • 1 Amarilli, Antoine
  • 1 Baldan, Paolo
  • 1 Bruni, Roberto
  • 1 De Stefani, Lorenzo
  • 1 Gupta, Vedant
  • Show More...

  • Refine by Series/Journal
  • 4 LIPIcs

  • Refine by Classification
  • 1 Theory of computation → Abstraction
  • 1 Theory of computation → Design and analysis of algorithms
  • 1 Theory of computation → Modal and temporal logics
  • 1 Theory of computation → Program verification
  • 1 Theory of computation → Programming logic
  • Show More...

  • Refine by Keyword
  • 1 ACTL
  • 1 Automaton
  • 1 Chomsky algebra
  • 1 Cocke-Younger-Kasami
  • 1 Dynamic Programming Algorithms
  • Show More...

Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail