7 Search Results for "Seidl, Helmut"

Document
Invited Talk
DOI: 10.4230/LIPIcs.MFCS.2023.4
Algebraic Reasoning for (Un)Solvable Loops (Invited Talk)

Authors: Laura Kovács

Published in: LIPIcs, Volume 272, 48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023)

Abstract
Loop invariants describe valid program properties that hold before and after every loop iteration. As such, loop invariants are the workhorses in formalizing loop semantics and automating the formal analysis and verification of programs with loops. While automatically synthesizing loop invariants is, in general, an uncomputable problem, when considering only single-path loops with linear updates (linear loops), the strongest polynomial invariant is in fact computable [Michael Karr, 1976; Markus Müller-Olm and Helmut Seidl, 2004; Laura Kovács, 2008; Ehud Hrushovski et al., 2018]. Yet, already for loops with "only" polynomial updates, computing the strongest invariant has been an open challenge since 2004 [Markus Müller-Olm and Helmut Seidl, 2004]. In this invited talk, we first present computability results on polynomial invariant synthesis for restricted polynomial loops, called solvable loops [Rodríguez-Carbonell and Kapur, 2004]. Key to solvable loops is that one can automatically compute invariants from closed-form solutions of algebraic recurrence equations that model the loop behaviour [Laura Kovács, 2008; Andreas Humenberger et al., 2017]. We also establish a technique for invariant synthesis for classes of loops that are not solvable, termed unsolvable loops [Daneshvar Amrollahi et al., 2022]. We next study the limits of computability in deriving the (strongest) polynomial invariants for arbitrary polynomial loops. We prove that computing the strongest polynomial invariant of arbitrary, single-path polynomial loops is very hard [Julian Müllner, 2023] - namely, it is at least as hard as the Skolem problem [Graham Everest et al., 2003; Terrence Tao, 2008], a prominent algebraic problem in the theory of linear recurrences. Going beyond single-path loops, we show that the strongest polynomial invariant is uncomputable already for multi-path polynomial loops with arbitrary quadratic polynomial updates [Laura Kovács and Anton Varonka, 2023].
Cite as

Laura Kovács. Algebraic Reasoning for (Un)Solvable Loops (Invited Talk). In 48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 272, pp. 4:1-4:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{kovacs:LIPIcs.MFCS.2023.4,
  author =	{Kov\'{a}cs, Laura},
  title =	{{Algebraic Reasoning for (Un)Solvable Loops}},
  booktitle =	{48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023)},
  pages =	{4:1--4:2},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-292-1},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{272},
  editor =	{Leroux, J\'{e}r\^{o}me and Lombardy, Sylvain and Peleg, David},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2023.4},
  URN =		{urn:nbn:de:0030-drops-185385},
  doi =		{10.4230/LIPIcs.MFCS.2023.4},
  annote =	{Keywords: Symbolic Computation, Formal Methods, Loop Analysis, Polynomial Invariants}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2020.134
When Is a Bottom-Up Deterministic Tree Translation Top-Down Deterministic?

Authors: Sebastian Maneth and Helmut Seidl

Published in: LIPIcs, Volume 168, 47th International Colloquium on Automata, Languages, and Programming (ICALP 2020)

Abstract
We consider two natural subclasses of deterministic top-down tree-to-tree transducers, namely, linear and uniform-copying transducers. For both classes we show that it is decidable whether the translation of a transducer with look-ahead can be realized by a transducer without look-ahead. The transducers constructed in this way, may still make use of inspection, i.e., have an additional tree automaton restricting the domain. We provide a second procedure which decides whether inspection can be removed and if so, constructs an equivalent transducer without inspection. The construction relies on a fixpoint algorithm that determines inspection requirements and on dedicated earliest normal forms for linear as well as uniform-copying transducers which can be constructed in polynomial time. As a consequence, equivalence of these transducers can be decided in polynomial time. Applying these results to deterministic bottom-up transducers, we obtain that it is decidable whether or not their translations can be realized by deterministic uniform-copying top-down transducers without look-ahead (but with inspection) - or without both look-ahead and inspection.
Cite as

Sebastian Maneth and Helmut Seidl. When Is a Bottom-Up Deterministic Tree Translation Top-Down Deterministic?. In 47th International Colloquium on Automata, Languages, and Programming (ICALP 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 168, pp. 134:1-134:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{maneth_et_al:LIPIcs.ICALP.2020.134,
  author =	{Maneth, Sebastian and Seidl, Helmut},
  title =	{{When Is a Bottom-Up Deterministic Tree Translation Top-Down Deterministic?}},
  booktitle =	{47th International Colloquium on Automata, Languages, and Programming (ICALP 2020)},
  pages =	{134:1--134:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-138-2},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{168},
  editor =	{Czumaj, Artur and Dawar, Anuj and Merelli, Emanuela},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2020.134},
  URN =		{urn:nbn:de:0030-drops-125416},
  doi =		{10.4230/LIPIcs.ICALP.2020.134},
  annote =	{Keywords: Top-Down Tree Transducers, Earliest Transformation, Linear Transducers, Uniform-copying Transucers, Removal of Look-ahead, Removal of Inspection}
}
Document
DOI: 10.4230/LIPIcs.STACS.2018.48
Computing the Longest Common Prefix of a Context-free Language in Polynomial Time

Authors: Michael Luttenberger, Raphaela Palenta, and Helmut Seidl

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

Abstract
We present two structural results concerning the longest common prefixes of non-empty languages. First, we show that the longest common prefix of the language generated by a context-free grammar of size N equals the longest common prefix of the same grammar where the heights of the derivation trees are bounded by 4N. Second, we show that each non-empty language L has a representative subset of at most three elements which behaves like L w.r.t. the longest common prefix as well as w.r.t. longest common prefixes of L after unions or concatenations with arbitrary other languages. From that, we conclude that the longest common prefix, and thus the longest common suffix, of a context-free language can be computed in polynomial time.
Cite as

Michael Luttenberger, Raphaela Palenta, and Helmut Seidl. Computing the Longest Common Prefix of a Context-free Language in Polynomial Time. In 35th Symposium on Theoretical Aspects of Computer Science (STACS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 96, pp. 48:1-48:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{luttenberger_et_al:LIPIcs.STACS.2018.48,
  author =	{Luttenberger, Michael and Palenta, Raphaela and Seidl, Helmut},
  title =	{{Computing the Longest Common Prefix of a Context-free Language in Polynomial Time}},
  booktitle =	{35th Symposium on Theoretical Aspects of Computer Science (STACS 2018)},
  pages =	{48:1--48:13},
  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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2018.48},
  URN =		{urn:nbn:de:0030-drops-84828},
  doi =		{10.4230/LIPIcs.STACS.2018.48},
  annote =	{Keywords: longest common prefix, context-free languages, combinatorics on words}
}
Document
DOI: 10.4230/DagRep.7.4.23
Formal Methods of Transformations (Dagstuhl Seminar 17142)

Authors: Emmanuel Filiot, Sebastian Maneth, and Helmut Seidl

Published in: Dagstuhl Reports, Volume 7, Issue 4 (2018)

Abstract
The goal of this Dagstuhl seminar was to gather researchers working on the theory and practice of transformations (also know as transductions) of word and tree structures, which are realised by transducers (automata with outputs). This seminar was motivated by recent advances and breakthrough results, both in the settings of words and trees.
Cite as

Emmanuel Filiot, Sebastian Maneth, and Helmut Seidl. Formal Methods of Transformations (Dagstuhl Seminar 17142). In Dagstuhl Reports, Volume 7, Issue 4, pp. 23-37, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@Article{filiot_et_al:DagRep.7.4.23,
  author =	{Filiot, Emmanuel and Maneth, Sebastian and Seidl, Helmut},
  title =	{{Formal Methods of Transformations (Dagstuhl Seminar 17142)}},
  pages =	{23--37},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2017},
  volume =	{7},
  number =	{4},
  editor =	{Filiot, Emmanuel and Maneth, Sebastian and Seidl, Helmut},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagRep.7.4.23},
  URN =		{urn:nbn:de:0030-drops-75462},
  doi =		{10.4230/DagRep.7.4.23},
  annote =	{Keywords: string transducers, tree transducers, expressiveness, complexity}
}
Document
DOI: 10.4230/DagRep.3.5.1
Tree Transducers and Formal Methods (Dagstuhl Seminar 13192)

Authors: Sebastian Maneth and Helmut Seidl

Published in: Dagstuhl Reports, Volume 3, Issue 5 (2013)

Abstract
The aim of this Dagstuhl Seminar was to bring together researchers from various research areas related to the theory and application of tree transducers. Recently, interest in tree transducers has been revived due to surprising new applications in areas such as XML databases, security verification, programming language theory, and linguistics. This seminar therefore aimed to inspire the exchange of theoretical results and information regarding the practical requirements related to tree transducers.
Cite as

Sebastian Maneth and Helmut Seidl. Tree Transducers and Formal Methods (Dagstuhl Seminar 13192). In Dagstuhl Reports, Volume 3, Issue 5, pp. 1-18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)

Copy BibTex To Clipboard

@Article{maneth_et_al:DagRep.3.5.1,
  author =	{Maneth, Sebastian and Seidl, Helmut},
  title =	{{Tree Transducers and Formal Methods (Dagstuhl Seminar 13192)}},
  pages =	{1--18},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2013},
  volume =	{3},
  number =	{5},
  editor =	{Maneth, Sebastian and Seidl, Helmut},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagRep.3.5.1},
  URN =		{urn:nbn:de:0030-drops-41769},
  doi =		{10.4230/DagRep.3.5.1},
  annote =	{Keywords: tree transducers, expressiveness, complexity}
}
Document
DOI: 10.4230/DagSemRep.193
Applications of Tree Automata in Rewriting, Logic and Programming (Dagstuhl Seminar 9743)

Authors: Hubert Comon, Dexter Kozen, Helmut Seidl, and Mosche Y. Vardi

Published in: Dagstuhl Seminar Reports. Dagstuhl Seminar Reports, Volume 1 (2021)

Abstract
Cite as

Hubert Comon, Dexter Kozen, Helmut Seidl, and Mosche Y. Vardi. Applications of Tree Automata in Rewriting, Logic and Programming (Dagstuhl Seminar 9743). Dagstuhl Seminar Report 193, pp. 1-34, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (1997)

Copy BibTex To Clipboard

@TechReport{comon_et_al:DagSemRep.193,
  author =	{Comon, Hubert and Kozen, Dexter and Seidl, Helmut and Vardi, Mosche Y.},
  title =	{{Applications of Tree Automata in Rewriting, Logic and Programming (Dagstuhl Seminar 9743)}},
  pages =	{1--34},
  ISSN =	{1619-0203},
  year =	{1997},
  type = 	{Dagstuhl Seminar Report},
  number =	{193},
  institution =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemRep.193},
  URN =		{urn:nbn:de:0030-drops-150792},
  doi =		{10.4230/DagSemRep.193},
}
Document
DOI: 10.4230/DagSemRep.81
Algorithms in Automata Theory (Dagstuhl Seminar 9406)

Authors: André Arnold, Helmut Seidl, and Bernhard Steffen

Published in: Dagstuhl Seminar Reports. Dagstuhl Seminar Reports, Volume 1 (2021)

Abstract
Cite as

André Arnold, Helmut Seidl, and Bernhard Steffen. Algorithms in Automata Theory (Dagstuhl Seminar 9406). Dagstuhl Seminar Report 81, pp. 1-28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (1994)

Copy BibTex To Clipboard

@TechReport{arnold_et_al:DagSemRep.81,
  author =	{Arnold, Andr\'{e} and Seidl, Helmut and Steffen, Bernhard},
  title =	{{Algorithms in Automata Theory (Dagstuhl Seminar 9406)}},
  pages =	{1--28},
  ISSN =	{1619-0203},
  year =	{1994},
  type = 	{Dagstuhl Seminar Report},
  number =	{81},
  institution =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemRep.81},
  URN =		{urn:nbn:de:0030-drops-149691},
  doi =		{10.4230/DagSemRep.81},
}
  • Refine by Author
  • 6 Seidl, Helmut
  • 3 Maneth, Sebastian
  • 1 Arnold, André
  • 1 Comon, Hubert
  • 1 Filiot, Emmanuel
  • Show More...

  • Refine by Classification
  • 1 Theory of computation → Algebraic semantics
  • 1 Theory of computation → Formal languages and automata theory
  • 1 Theory of computation → Invariants
  • 1 Theory of computation → Models of computation
  • 1 Theory of computation → Program verification

  • Refine by Keyword
  • 2 complexity
  • 2 expressiveness
  • 2 tree transducers
  • 1 Earliest Transformation
  • 1 Formal Methods
  • Show More...

  • Refine by Type
  • 7 document

  • Refine by Publication Year
  • 1 1994
  • 1 1997
  • 1 2013
  • 1 2017
  • 1 2018
  • 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