2026-08-11T02:58:16Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:3869 2024-03-06T10:34:33Z ddc:004 open_access

Accelerating tree-automatic relations Lin, Anthony Widjaja Semi-algorithm Model Checking Infinite Systems Automata We study the problem of computing the transitive closure of tree-automatic (binary) relations, which are represented by tree automata. Such relations include classes of infinite systems generated by pushdown systems (PDS), ground tree rewrite systems (GTRS), PA-processes, and Turing machines, to name a few. Although this problem is unsolvable in general, we provide a semi-algorithm for the problem and prove completeness guarantee for PDS, GTRS, and PA-processes. The semi-algorithm is an extension of a known semi-algorithm for structure-preserving tree-automatic relations, for which completeness is guaranteed for several interesting parameterized systems over tree topology. Hence, there is a single generic procedure that solves reachability for PDS, GTRS, PA-processes, and several parameterized systems in a uniform way. As an application, we provide a single generic semi-algorithm for checking repeated reachability over tree-automatic relations, for which completeness is guaranteed for the aforementioned classes. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Anthony Widjaja Lin 2012 Is Part Of LIPIcs, Volume 18, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2012) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSTTCS.2012.313 urn:nbn:de:0030-drops-38691 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2012.313 eng https://creativecommons.org/licenses/by-nc-nd/3.0/legalcode