License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.FSCD.2018.16
URN: urn:nbn:de:0030-drops-91868
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2018/9186/
Go to the corresponding LIPIcs Volume Portal

Genet, Thomas

Completeness of Tree Automata Completion

pdf-format:
LIPIcs-FSCD-2018-16.pdf (0.6 MB)

Abstract

We consider rewriting of a regular language with a left-linear term rewriting system. We show a completeness theorem on equational tree automata completion stating that, if there exists a regular over-approximation of the set of reachable terms, then equational completion can compute it (or safely under-approximate it). A nice corollary of this theorem is that, if the set of reachable terms is regular, then equational completion can also compute it. This was known to be true for some term rewriting system classes preserving regularity, but was still an open question in the general case. The proof is not constructive because it depends on the regularity of the set of reachable terms, which is undecidable. To carry out those proofs we generalize and improve two results of completion: the Termination and the Upper-Bound theorems. Those theoretical results provide an algorithmic way to safely explore regular approximations with completion. This has been implemented in Timbuk and used to verify safety properties, automatically and efficiently, on first-order and higher-order functional programs.

BibTeX - Entry

@InProceedings{genet:LIPIcs:2018:9186,
  author =	{Thomas Genet},
  title =	{{Completeness of Tree Automata Completion}},
  booktitle =	{3rd International Conference on Formal Structures for  Computation and Deduction (FSCD 2018)},
  pages =	{16:1--16:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-077-4},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{108},
  editor =	{H{\'e}l{\`e}ne Kirchner},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2018/9186},
  URN =		{urn:nbn:de:0030-drops-91868},
  doi =		{10.4230/LIPIcs.FSCD.2018.16},
  annote =	{Keywords: term rewriting systems, regularity preservation, over-approximation, completeness, tree automata, tree automata completion}
}

Keywords: term rewriting systems, regularity preservation, over-approximation, completeness, tree automata, tree automata completion
Collection: 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)
Issue Date: 2018
Date of publication: 04.07.2018

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI