Search Results

Documents authored by Waldmann, Johannes

Document
DOI: 10.4230/LIPIcs.FSCD.2019.21
Sparse Tiling Through Overlap Closures for Termination of String Rewriting

Authors: Alfons Geser, Dieter Hofbauer, and Johannes Waldmann

Published in: LIPIcs, Volume 131, 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)

Abstract
A strictly locally testable language is characterized by its set of admissible factors, prefixes and suffixes, called tiles. We over-approximate reachability sets in string rewriting by languages defined by sparse sets of tiles, containing only those that are reachable in derivations. Using the partial algebra defined by a tiling for semantic labeling, we obtain a transformational method for proving local termination. These algebras can be represented efficiently as finite automata of a certain shape. Using a known result on forward closures, and a new characterisation of overlap closures, we can automatically prove termination and relative termination, respectively. We report on experiments showing the strength of the method.
Cite as

Alfons Geser, Dieter Hofbauer, and Johannes Waldmann. Sparse Tiling Through Overlap Closures for Termination of String Rewriting. In 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 131, pp. 21:1-21:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{geser_et_al:LIPIcs.FSCD.2019.21,
  author =	{Geser, Alfons and Hofbauer, Dieter and Waldmann, Johannes},
  title =	{{Sparse Tiling Through Overlap Closures for Termination of String Rewriting}},
  booktitle =	{4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)},
  pages =	{21:1--21:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-107-8},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{131},
  editor =	{Geuvers, Herman},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2019.21},
  URN =		{urn:nbn:de:0030-drops-105282},
  doi =		{10.4230/LIPIcs.FSCD.2019.21},
  annote =	{Keywords: relative termination, semantic labeling, locally testable language, overlap closure}
}
Document
DOI: 10.4230/LIPIcs.RTA.2015.318
Matrix Interpretations on Polyhedral Domains

Authors: Johannes Waldmann

Published in: LIPIcs, Volume 36, 26th International Conference on Rewriting Techniques and Applications (RTA 2015)

Abstract
We refine matrix interpretations for proving termination and complexity bounds of term rewrite systems we restricting them to domains that satisfy a system of linear inequalities. Admissibility of such a restriction is shown by certificates whose validity can be expressed as a constraint program. This refinement is orthogonal to other features of matrix interpretations (complexity bounds, dependency pairs), but can be used to improve complexity bounds, and we discuss its relation with the usable rules criterion. We present an implementation and experiments.
Cite as

Johannes Waldmann. Matrix Interpretations on Polyhedral Domains. In 26th International Conference on Rewriting Techniques and Applications (RTA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 36, pp. 318-333, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{waldmann:LIPIcs.RTA.2015.318,
  author =	{Waldmann, Johannes},
  title =	{{Matrix Interpretations on Polyhedral Domains}},
  booktitle =	{26th International Conference on Rewriting Techniques and Applications (RTA 2015)},
  pages =	{318--333},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-85-9},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{36},
  editor =	{Fern\'{a}ndez, Maribel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2015.318},
  URN =		{urn:nbn:de:0030-drops-52059},
  doi =		{10.4230/LIPIcs.RTA.2015.318},
  annote =	{Keywords: termination of term rewriting, matrix interpretations, constraint programming, linear inequalities}
}
Document
DOI: 10.4230/LIPIcs.RTA.2013.97
Compression of Rewriting Systems for Termination Analysis

Authors: Alexander Bau, Markus Lohrey, Eric Nöth, and Johannes Waldmann

Published in: LIPIcs, Volume 21, 24th International Conference on Rewriting Techniques and Applications (RTA 2013)

Abstract
We adapt the TreeRePair tree compression algorithm and use it as an intermediate step in proving termination of term rewriting systems. We introduce a cost function that approximates the size of constraint systems that specify compatibility of matrix interpretations. We show how to integrate the compression algorithm with the Dependency Pairs transformation. Experiments show that compression reduces running times of constraint solvers, and thus improves the power of automated termination provers.
Cite as

Alexander Bau, Markus Lohrey, Eric Nöth, and Johannes Waldmann. Compression of Rewriting Systems for Termination Analysis. In 24th International Conference on Rewriting Techniques and Applications (RTA 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 21, pp. 97-112, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)

Copy BibTex To Clipboard

@InProceedings{bau_et_al:LIPIcs.RTA.2013.97,
  author =	{Bau, Alexander and Lohrey, Markus and N\"{o}th, Eric and Waldmann, Johannes},
  title =	{{Compression of Rewriting Systems for Termination Analysis}},
  booktitle =	{24th International Conference on Rewriting Techniques and Applications (RTA 2013)},
  pages =	{97--112},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-53-8},
  ISSN =	{1868-8969},
  year =	{2013},
  volume =	{21},
  editor =	{van Raamsdonk, Femke},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2013.97},
  URN =		{urn:nbn:de:0030-drops-40561},
  doi =		{10.4230/LIPIcs.RTA.2013.97},
  annote =	{Keywords: termination of rewriting, matrix interpretations, constraint solving, tree compression}
}
Document
DOI: 10.4230/LIPIcs.RTA.2010.357
Polynomially Bounded Matrix Interpretations

Authors: Johannes Waldmann

Published in: LIPIcs, Volume 6, Proceedings of the 21st International Conference on Rewriting Techniques and Applications (2010)

Abstract
Matrix interpretations can be used to bound the derivational complexity of rewrite systems. We present a criterion that completely characterizes matrix interpretations that are polynomially bounded. It includes the method of upper triangular interpretations as a special case, and we prove that the inclusion is strict. The criterion can be expressed as a finite domain constraint system. It translates to a Boolean constraint system with a size that is polynomial in the dimension of the interpretation. We report on performance of an implementation.
Cite as

Johannes Waldmann. Polynomially Bounded Matrix Interpretations. In Proceedings of the 21st International Conference on Rewriting Techniques and Applications. Leibniz International Proceedings in Informatics (LIPIcs), Volume 6, pp. 357-372, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{waldmann:LIPIcs.RTA.2010.357,
  author =	{Waldmann, Johannes},
  title =	{{Polynomially Bounded Matrix Interpretations}},
  booktitle =	{Proceedings of the 21st International Conference on Rewriting Techniques and Applications},
  pages =	{357--372},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-18-7},
  ISSN =	{1868-8969},
  year =	{2010},
  volume =	{6},
  editor =	{Lynch, Christopher},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2010.357},
  URN =		{urn:nbn:de:0030-drops-26637},
  doi =		{10.4230/LIPIcs.RTA.2010.357},
  annote =	{Keywords: Derivational complexity of rewriting, matrix interpretation, weighted automata, ambiguity of automata, finite domain constraints}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2008.1762
Complexity Analysis of Term Rewriting Based on Matrix and Context Dependent Interpretations

Authors: Georg Moser, Andreas Schnabl, and Johannes Waldmann

Published in: LIPIcs, Volume 2, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (2008)

Abstract
For a given (terminating) term rewriting system one can often estimate its \emph{derivational complexity} indirectly by looking at the proof method that established termination. In this spirit we investigate two instances of the interpretation method: \emph{matrix interpretations} and \emph{context dependent interpretations}. We introduce a subclass of matrix interpretations, denoted as \emph{triangular matrix interpretations}, which induce polynomial derivational complexity and establish tight correspondence results between a subclass of context dependent interpretations and restricted triangular matrix interpretations. The thus obtained new results are easy to implement and considerably extend the analytic power of existing results. We provide ample numerical data for assessing the viability of the method.
Cite as

Georg Moser, Andreas Schnabl, and Johannes Waldmann. Complexity Analysis of Term Rewriting Based on Matrix and Context Dependent Interpretations. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science. Leibniz International Proceedings in Informatics (LIPIcs), Volume 2, pp. 304-315, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2008)

Copy BibTex To Clipboard

@InProceedings{moser_et_al:LIPIcs.FSTTCS.2008.1762,
  author =	{Moser, Georg and Schnabl, Andreas and Waldmann, Johannes},
  title =	{{Complexity Analysis of Term Rewriting Based on  Matrix and Context Dependent Interpretations}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science},
  pages =	{304--315},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-08-8},
  ISSN =	{1868-8969},
  year =	{2008},
  volume =	{2},
  editor =	{Hariharan, Ramesh and Mukund, Madhavan and Vinay, V},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2008.1762},
  URN =		{urn:nbn:de:0030-drops-17626},
  doi =		{10.4230/LIPIcs.FSTTCS.2008.1762},
  annote =	{Keywords: Term Rewriting, Derivational Complexity, Termination, Automation}
}
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