2020

  1. Transducer Degrees: Atoms, Infima and Suprema
    Jörg Endrullis, Jan Willem Klop, and Rena Bakhshi
    Acta Informatica , 57 (3-5) , pp. 727–758 (2020)
    paper

    Summary

    Although finite state transducers are very natural and simple devices, surprisingly little is known about the transducibility relation they induce on streams (infinite words). We collect some intriguing problems that have been unsolved since several years. The transducibility relation arising from finite state transduction induces a partial order of stream degrees, which we call Transducer degrees, analogous to the well-known Turing degrees or degrees of unsolvability.

    We show that there are pairs of degrees without supremum and without infimum. The former result is somewhat surprising since every finite set of degrees has a supremum if we strengthen the machine model to Turing machines, but also if we weaken it to Mealy machines.

    Bibtex

    @article{streams:degrees:suprema:2020,
  author = {Endrullis, J{\"{o}}rg and Klop, Jan Willem and Bakhshi, Rena},
  title = {{Transducer Degrees: Atoms, Infima and Suprema}},
  journal = {Acta Informatica},
  volume = {57},
  number = {3-5},
  pages = {727--758},
  year = {2020},
  doi = {10.1007/s00236-019-00353-7},
  keywords = {streams, degrees, automata},
  type = {journal}
}

    Digital Object Identifier

    10.1007/s00236-019-00353-7

2018

  1. Degrees of Infinite Words, Polynomials and Atoms
    Jörg Endrullis, Juhani Karhumäki, Jan Willem Klop, and Aleksi Saarela
    International Journal of Foundations of Computer Science , 29 (5) , pp. 825–843 (2018)
    paper

    Summary

    A finite state transducer is a finite automaton that transforms input words into output words. The transducer reads the input letter by letter, in each step producing an output word and changing its state.

    While finite state transducers are very simple and elegant devices, their power in transforming infinite words is hardly understood.

    In this paper we show that techniques from continuous mathematics can be used to reason about finite state transducers. To be precise, we use the following methods from linear algebra and analysis:

    • continuity,
    • Vandermonde matrices,
    • invertibility of matrices, and
    • the generalised mean inequality.
    We employ these techniques to obtain both positive and negative results on transducibility.

    The main result in this paper is the existance of an infinite number of atoms in the hierarchy of streams arising from finite state transduction.

    This paper is an extended version of Degrees of Infinite Words, Polynomials and Atoms presented at the Conference on Developments in Language Theory (DLT), 2016.

    See research for an introduction to finite state transducers, an overview of my research and many open questions.

    Bibtex

    @article{streams:degrees:polynomials:2018,
  author = {Endrullis, J\"{o}rg and Karhum{\"{a}}ki, Juhani and Klop, Jan Willem and Saarela, Aleksi},
  title = {{Degrees of Infinite Words, Polynomials and Atoms}},
  journal = {International Journal of Foundations of Computer Science},
  volume = {29},
  number = {5},
  pages = {825--843},
  year = {2018},
  doi = {10.1142/S0129054118420066},
  keywords = {streams, degrees, automata},
  type = {journal}
}

    Digital Object Identifier

    10.1142/S0129054118420066

2017

  1. Undecidability and Finite Automata
    Jörg Endrullis, Jeffrey Shallit, and Tim Smith
    In: Proc. Conf. Developments in Language Theory (DLT 2017), pp. 160–172, Springer (2017)
    paper

    Summary

    Using a novel rewriting problem, we show that several natural decision problems about finite automata are undecidable. In contrast, we also prove three related problems are decidable.

    We apply one result to prove the undecidability of a related problem about k-automatic sets of rational numbers.

    Bibtex

    @inproceedings{automata:undecidability:2017,
  author = {Endrullis, J\"{o}rg and Shallit, Jeffrey and Smith, Tim},
  title = {{Undecidability and Finite Automata}},
  booktitle = {Proc.\ Conf.\ Developments in Language Theory (DLT~2017)},
  volume = {10396},
  pages = {160--172},
  publisher = {Springer},
  series = {LNCS},
  year = {2017},
  doi = {10.1007/978-3-319-62809-7\_11},
  keywords = {automata, undecidability},
  type = {conference}
}

    Digital Object Identifier

    10.1007/978-3-319-62809-7_11

2016

  1. Degrees of Infinite Words, Polynomials and Atoms
    Jörg Endrullis, Juhani Karhumäki, Jan Willem Klop, and Aleksi Saarela
    In: Proc. Conf. on Developments in Language Theory (DLT 2016), pp. 164–176, Springer (2016)
    paper

    Summary

    A finite state transducer is a finite automaton that transforms input words into output words. The transducer reads the input letter by letter, in each step producing an output word and changing its state.

    While finite state transducers are very simple and elegant devices, their power in transforming infinite words is hardly understood.

    In this paper we show that techniques from continuous mathematics can be used to reason about finite state transducers. To be precise, we use the following methods from linear algebra and analysis:

    • continuity,
    • Vandermonde matrices,
    • invertibility of matrices, and
    • the generalised mean inequality.
    We employ these techniques to obtain both positive and negative results on transducibility.

    The main result in this paper is the existance of an infinite number of atoms in the hierarchy of streams arising from finite state transduction.

    We have published an extended journal version of this paper in the International Journal of Foundations of Computer Science, 2018.

    See research for an introduction to finite state transducers, an overview of my research and many open questions.

    Bibtex

    @inproceedings{streams:degrees:polynomials:2016,
  author = {Endrullis, J\"{o}rg and Karhum{\"{a}}ki, Juhani and Klop, Jan Willem and Saarela, Aleksi},
  title = {{Degrees of Infinite Words, Polynomials and Atoms}},
  booktitle = {Proc.\ Conf.\ on Developments in Language Theory (DLT~2016)},
  volume = {9840},
  pages = {164--176},
  publisher = {Springer},
  series = {LNCS},
  year = {2016},
  doi = {10.1007/978-3-662-53132-7\_14},
  keywords = {streams, degrees, automata},
  type = {conference}
}

    Digital Object Identifier

    10.1007/978-3-662-53132-7_14

2015

  1. Regularity Preserving but Not Reflecting Encodings
    Jörg Endrullis, Clemens Grabmayer, and Dimitri Hendriks
    In: Proc. Symp. on Logic in Computer Science (LICS 2015), pp. 535–546, IEEE Computer Society (2015)
    paper

    Summary

    Encodings, that is, injective functions from words to words, have been studied extensively in several settings. In computability theory the notion of encoding is crucial for defining computability on arbitrary domains, as well as for comparing the power of models of computation. In language theory much attention has been devoted to regularity preserving functions.

    A natural question arising in these contexts is: Is there a bijective encoding such that its image function preserves regularity of languages, but its pre-image function does not? Our main result answers this question in the affirmative: For every countable class \( C \) of languages there exists a bijective encoding \( f \) such that for every language \( L \in C \) its image \( f[L] \) is regular.

    Our construction of such encodings has several noteworthy consequences. Firstly, anomalies arise when models of computation are compared with respect to a known concept of implementation that is based on encodings which are not required to be computable: Every countable decision model can be implemented, in this sense, by finite-state automata, even via bijective encodings. Hence deterministic finite-state automata would be equally powerful as Turing machine deciders. A second consequence concerns the recognizability of sets of natural numbers via number representations and finite automata. A set of numbers is said to be recognizable with respect to a representation if an automaton accepts the language of representations. Our result entails that there is one number representation with respect to which every recursive set is recognizable.

    Bibtex

    @inproceedings{regularity:reflecting:2015,
  author = {Endrullis, J\"{o}rg and Grabmayer, Clemens and Hendriks, Dimitri},
  title = {{Regularity Preserving but Not Reflecting Encodings}},
  booktitle = {Proc.\ Symp.\ on Logic in Computer Science (LICS~2015)},
  pages = {535--546},
  publisher = {{IEEE} Computer Society},
  year = {2015},
  doi = {10.1109/LICS.2015.56},
  keywords = {automata},
  type = {conference}
}

    Digital Object Identifier

    10.1109/LICS.2015.56
  2. Proving Non-Termination by Finite Automata
    Jörg Endrullis, and Hans Zantema
    In: Proc. Conf. on Rewriting Techniques and Applications (RTA 2015), pp. 160–176, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2015)
    paper

    Summary

    We present a new technique to prove non-termination of term rewriting. The basic idea is tofind a non-empty regular language of terms that is weakly closed under rewriting and does not containnormal forms. It is automated by representing the language by a tree automaton with a fixednumber of states, and expressing the mentioned requirements in a SAT formula. Satisfiabilityof this formula implies non-termination. Our approach succeeds for many examples where allearlier techniques fail, for instance for the S-rule from combinatory logic.

    See research for an overview of my research on termination.

    Bibtex

    @inproceedings{termination:automata:2015,
  author = {Endrullis, J\"{o}rg and Zantema, Hans},
  title = {{Proving Non-termination by Finite Automata}},
  booktitle = {Proc.\ Conf.\ on Rewriting Techniques and Applications (RTA~2015)},
  volume = {36},
  pages = {160--176},
  publisher = {Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik},
  series = {LIPIcs},
  year = {2015},
  doi = {10.4230/LIPIcs.RTA.2015.160},
  keywords = {rewriting, termination, automata},
  type = {conference}
}

    Digital Object Identifier

    10.4230/LIPIcs.RTA.2015.160
  3. Degrees of Transducibility
    Jörg Endrullis, Jan Willem Klop, Aleksi Saarela, and Markus A. Whiteland
    In: Proc. Conf. on Combinatorics on Words (WORDS 2015), pp. 1–13, Springer (2015)
    paper

    Summary

    In this survey paper we compare different hierarchies of degrees of infinite words (streams) arising from transformation (transduction) of these words. As transformational devices we consider

    • Turing machines,
    • finite state transducers, and
    • Mealy machines.
    The stream transformation realised by these machine models induces equivalence classes of streams, called degrees, and a partial order on these degrees. We refer to these hierarchies as Turing degrees, Transducer degrees and Mealy degrees, respectively.

    While Turing degrees have been extensively studied in the 60th and 70th, hardly anything is known about Transducer and Mealy degrees. In this paper, we compare central properties of these hierarchies and mention many open problems.

    See research for an introduction to finite state transducers, an overview of my research and many open questions.

    Bibtex

    @inproceedings{streams:degrees:transducibility:2015,
  author = {Endrullis, J\"{o}rg and Klop, Jan Willem and Saarela, Aleksi and Whiteland, Markus A.},
  title = {{Degrees of Transducibility}},
  booktitle = {Proc.\ Conf.\ on Combinatorics on Words (WORDS~2015)},
  volume = {9304},
  pages = {1--13},
  publisher = {Springer},
  series = {LNCS},
  year = {2015},
  doi = {10.1007/978-3-319-23660-5\_1},
  keywords = {streams, degrees, automata},
  type = {conference}
}

    Digital Object Identifier

    10.1007/978-3-319-23660-5_1
  4. The Degree of Squares Is an Atom
    Jörg Endrullis, Clemens Grabmayer, Dimitri Hendriks, and Hans Zantema
    In: Proc. Conf. on Combinatorics on Words (WORDS 2015), pp. 109–121, Springer (2015)
    paper

    Summary

    A finite state transducer is a finite automaton that transforms input words into output words. The transducer reads the input letter by letter, in each step producing an output word and changing its state.

    While finite state transducers are very simple and elegant devices, their power in transforming infinite words is hardly understood.

    In this paper we show that the degree of the stream \[ \prod_{i = 0}^\infty 1\, 0^{i^2} = 1 \, 0^0 \, 1 \, 0^1 \, 1 \, 0^4 \, 1 \, 0^9 \, 1 \, 0^{16} \, \cdots = 1101000010000000001 \cdots \] is an atom in the hierarchy of streams arising from finite state transduction.

    In the paper Degrees of Infinite Words, Polynomials and Atoms we vastly generalise this result by showing that there is precisely one atom for each polynomial degree. See research for an introduction to finite state transducers, an overview of my research and many open questions.

    Bibtex

    @inproceedings{streams:degrees:squares:2015,
  author = {Endrullis, J\"{o}rg and Grabmayer, Clemens and Hendriks, Dimitri and Zantema, Hans},
  title = {{The Degree of Squares is an Atom}},
  booktitle = {Proc.\ Conf.\ on Combinatorics on Words (WORDS~2015)},
  volume = {9304},
  pages = {109--121},
  publisher = {Springer},
  series = {LNCS},
  year = {2015},
  doi = {10.1007/978-3-319-23660-5\_10},
  keywords = {streams, degrees, automata},
  type = {conference}
}

    Digital Object Identifier

    10.1007/978-3-319-23660-5_10

2013

  1. Streams Are Forever
    Jörg Endrullis, Dimitri Hendriks, and Jan Willem Klop
    Bulletin of the EATCS , 109 , pp. 70–106 (2013)
    paper

    Bibtex

    @article{streams:forever:2013,
  author = {Endrullis, J\"{o}rg and Hendriks, Dimitri and Klop, Jan Willem},
  title = {{Streams are Forever}},
  journal = {Bulletin of the {EATCS}},
  volume = {109},
  pages = {70--106},
  year = {2013},
  keywords = {streams, degrees, automata},
  type = {journal}
}

    Digital Object Identifier

  2. Mix-Automatic Sequences
    Jörg Endrullis, Clemens Grabmayer, and Dimitri Hendriks
    In: Proc. Conf. on Language and Automata Theory and Applications (LATA 2013), pp. 262–274, Springer (2013)
    paper

    Bibtex

    @inproceedings{streams:mix:automatic:2013,
  author = {Endrullis, J\"{o}rg and Grabmayer, Clemens and Hendriks, Dimitri},
  title = {{Mix-Automatic Sequences}},
  booktitle = {Proc.\ Conf.\ on Language and Automata Theory and Applications (LATA~2013)},
  volume = {7810},
  pages = {262--274},
  publisher = {Springer},
  series = {LNCS},
  year = {2013},
  doi = {10.1007/978-3-642-37064-9\_24},
  keywords = {streams, automata},
  type = {conference}
}

    Digital Object Identifier

    10.1007/978-3-642-37064-9_24

2012

  1. Automatic Sequences and Zip-Specifications
    Clemens Grabmayer, Jörg Endrullis, Dimitri Hendriks, Jan Willem Klop, and Lawrence S. Moss
    In: Proc. Symp. on Logic in Computer Science (LICS 2012), pp. 335–344, IEEE Computer Society (2012)
    paper

    Bibtex

    @inproceedings{streams:zip:2012,
  author = {Grabmayer, Clemens and Endrullis, J\"{o}rg and Hendriks, Dimitri and Klop, Jan Willem and Moss, Lawrence S.},
  title = {{Automatic Sequences and Zip-Specifications}},
  booktitle = {Proc.\ Symp.\ on Logic in Computer Science (LICS~2012)},
  pages = {335--344},
  publisher = {{IEEE} Computer Society},
  year = {2012},
  doi = {10.1109/LICS.2012.44},
  keywords = {rewriting, streams, automata},
  type = {conference}
}

    Digital Object Identifier

    10.1109/LICS.2012.44

2011

  1. On Equal μ-Terms
    Jörg Endrullis, Clemens Grabmayer, Jan Willem Klop, and Vincent van Oostrom
    Theoretical Computer Science , 412 (28) , pp. 3175–3202 (2011)
    paper

    Summary

    We consider the rewrite system Rμ with μx.M → μM [x := μx.M ] as its single rewrite rule. This kernel system denoting recursively defined objects occurs in several contexts, e.g. it is the framework of recursive types. For general signatures this rewriting system is widely used to represent and manipulate infinite regular trees.

    The main concern of this paper is the convertibility relation for μ-terms as given by the μ-rule, in particular its decidability. This relation is sometimes called weak μ-equality, in contrast with strong μ-equality, which is given by equality of the possibly infinite tree unwinding of μ-terms. While strong equality has received much attention, the opposite is the case for weak μ-equality.

    We present three alternative proofs for decidability of weak μ-equality.

    Bibtex

    @article{equal:mu:terms:2011,
  author = {Endrullis, J\"{o}rg and Grabmayer, Clemens and Klop, Jan Willem and van~Oostrom, Vincent},
  title = {{On Equal $\mu$-Terms}},
  journal = {Theoretical Computer Science},
  volume = {412},
  number = {28},
  pages = {3175--3202},
  year = {2011},
  doi = {10.1016/j.tcs.2011.04.011},
  keywords = {rewriting,automata},
  type = {journal}
}

    Digital Object Identifier

    10.1016/j.tcs.2011.04.011
  2. Degrees of Streams
    Jörg Endrullis, Dimitri Hendriks, and Jan Willem Klop
    Journal of Integers , 11B (A6) , pp. 1–40 (2011)
    paper

    Bibtex

    @article{streams:degrees:2011,
  author = {Endrullis, J\"{o}rg and Hendriks, Dimitri and Klop, Jan Willem},
  title = {{Degrees of Streams}},
  journal = {Journal of Integers},
  volume = {11B},
  number = {A6},
  pages = {1--40},
  year = {2011},
  note = {Proceedings of the Leiden Numeration Conference 2010},
  keywords = {streams, degrees, automata},
  type = {journal}
}

    Digital Object Identifier

2010

  1. Local Termination: Theory and Practice
    Jörg Endrullis, Roel C. de Vrijer, and Johannes Waldmann
    Logical Methods in Computer Science , 6 (3) (2010)
    paper

    Bibtex

    @article{termination:local:2010,
  author = {Endrullis, J\"{o}rg and de~Vrijer, Roel C. and Waldmann, Johannes},
  title = {{Local Termination: Theory and Practice}},
  journal = {Logical Methods in Computer Science},
  volume = {6},
  number = {3},
  year = {2010},
  doi = {10.2168/LMCS-6(3:20)2010},
  keywords = {rewriting, termination, automata},
  type = {journal}
}

    Digital Object Identifier

    10.2168/LMCS-6(3:20)2010
  2. Transforming Outermost into Context-Sensitive Rewriting
    Jörg Endrullis, and Dimitri Hendriks
    Logical Methods in Computer Science , 6 (2) (2010)
    paper

    Summary

    We define two transformations from term rewriting systems (TRSs) to context-sensitive TRSs in such a way that termination of the target system implies outermost termination of the original system. In the transformation based on `context extension', each outermost rewrite step is modeled by exactly one step in the transformed system. This transformation turns out to be complete for the class of left-linear TRSs. The second transformation is called `dynamic labeling' and results in smaller sized context-sensitive TRSs. Here each modeled step is adjoined with a small number of auxiliary steps. As a result state-of-the-art termination methods for context-sensitive rewriting become available for proving termination of outermost rewriting. Both transformations have been implemented in Jambox, making it the most successful tool in the category of outermost rewriting of the annual termination competition.

    This is an extended version of the paper From Outermost to Context-Sensitive Rewriting (RTA 2009).

    See research for an overview of my research on termination.

    Bibtex

    @article{termination:outermost:2010,
  author = {Endrullis, J\"{o}rg and Hendriks, Dimitri},
  title = {{Transforming Outermost into Context-Sensitive Rewriting}},
  journal = {Logical Methods in Computer Science},
  volume = {6},
  number = {2},
  year = {2010},
  doi = {10.2168/LMCS-6(2:5)2010},
  keywords = {rewriting, termination, automata},
  type = {journal}
}

    Digital Object Identifier

    10.2168/LMCS-6(2:5)2010

2009

  1. From Outermost to Context-Sensitive Rewriting
    Jörg Endrullis, and Dimitri Hendriks
    In: Proc. Conf. on Rewriting Techniques and Applications (RTA 2009), pp. 305–319, Springer (2009)
    paper

    Summary

    We define a transformation from term rewriting systems (TRSs) to context-sensitive TRSs in such a way that termination of the target system implies outermost termination of the original system. For the class of left-linear TRSs the transformation is complete. Thereby state-of-the-art termination methods and automated termination provers for context-sensitive rewriting become available for proving termination of outermost rewriting. The translation has been implemented in Jambox, making it the most successful tool in the category of outermost rewriting of the last edition of the annual termination competition.

    An extended version of this paper is available from Transforming Outermost into Context-Sensitive Rewriting (Logical Methods in Computer Science 2010).

    See research for an overview of my research on termination.

    Bibtex

    @inproceedings{termination:outermost:2009,
  author = {Endrullis, J\"{o}rg and Hendriks, Dimitri},
  title = {{From Outermost to Context-Sensitive Rewriting}},
  booktitle = {Proc.\ Conf.\ on Rewriting Techniques and Applications (RTA~2009)},
  volume = {5595},
  pages = {305--319},
  publisher = {Springer},
  series = {LNCS},
  year = {2009},
  doi = {10.1007/978-3-642-02348-4\_22},
  keywords = {rewriting, termination, automata},
  type = {conference}
}

    Digital Object Identifier

    10.1007/978-3-642-02348-4_22
  2. Local Termination
    Jörg Endrullis, Roel C. de Vrijer, and Johannes Waldmann
    In: Proc. Conf. on Rewriting Techniques and Applications (RTA 2009), pp. 270–284, Springer (2009)
    paper

    Bibtex

    @inproceedings{termination:local:2009,
  author = {Endrullis, J\"{o}rg and de~Vrijer, Roel C. and Waldmann, Johannes},
  title = {{Local Termination}},
  booktitle = {Proc.\ Conf.\ on Rewriting Techniques and Applications (RTA~2009)},
  volume = {5595},
  pages = {270--284},
  publisher = {Springer},
  series = {LNCS},
  year = {2009},
  doi = {10.1007/978-3-642-02348-4\_19},
  keywords = {rewriting, termination, automata},
  type = {conference}
}

    Digital Object Identifier

    10.1007/978-3-642-02348-4_19

2008

  1. Proving Infinitary Normalization
    Jörg Endrullis, Clemens Grabmayer, Dimitri Hendriks, Jan Willem Klop, and Roel C. de Vrijer
    In: Proc. Conf. on Types for Proofs and Programs (TYPES 2008), pp. 64–82, Springer (2008)
    paper

    Bibtex

    @inproceedings{infinitary:normalization:2009,
  author = {Endrullis, J\"{o}rg and Grabmayer, Clemens and Hendriks, Dimitri and Klop, Jan Willem and de~Vrijer, Roel C.},
  title = {{Proving Infinitary Normalization}},
  booktitle = {Proc.\ Conf.\ on Types for Proofs and Programs (TYPES~2008)},
  volume = {5497},
  pages = {64--82},
  publisher = {Springer},
  series = {LNCS},
  year = {2008},
  doi = {10.1007/978-3-642-02444-3\_5},
  keywords = {rewriting, infinitary rewriting, automata},
  type = {conference}
}

    Digital Object Identifier

    10.1007/978-3-642-02444-3_5

2006

  1. Matrix Interpretations for Proving Termination of Term Rewriting
    Jörg Endrullis, Johannes Waldmann, and Hans Zantema
    In: Proc. Int. Joint Conf. on Automated Reasoning (IJCAR 2006), pp. 574–588, Springer (2006)
    paper

    Summary

    We present a new method for automatically proving termination of term rewriting using matrix interpretation (weighted automata with natural numbers as weights). It is based on the well-known idea of interpretation of terms where every rewrite step causes a decrease, but instead of the usual natural numbers we use vectors of natural numbers, ordered by a particular non-total well-founded ordering. Function symbols are interpreted by linear mappings represented by matrices. This method allows to prove termination and relative termination. A modification of the latter in which strict steps are only allowed at the top, turns out to be helpful in combination with the dependency pair transformation.

    By bounding the dimension and the matrix coefficients, the search problem becomes finite. Our implementation transforms it to a Boolean satisfiability problem (SAT), to be solved by a state-of-the-art SAT solver. Our implementation performs well on the Termination Problem Data Base: better than 5 out of 6 tools that participated in the 2005 termination competition in the category of term rewriting.

    An extended journal version of this paper is available from Matrix Interpretations for Proving Termination of Term Rewriting (Journal of Automated Reasoning 2008).

    See research for an overview of my research on termination.

    Bibtex

    @inproceedings{termination:matrix:2006,
  author = {Endrullis, J\"{o}rg and Waldmann, Johannes and Zantema, Hans},
  title = {{Matrix Interpretations for Proving Termination of Term Rewriting}},
  booktitle = {Proc.\ Int.\ Joint Conf.\ on Automated Reasoning (IJCAR~2006)},
  volume = {4130},
  pages = {574--588},
  publisher = {Springer},
  series = {LNCS},
  year = {2006},
  doi = {10.1007/11814771\_47},
  keywords = {rewriting, termination, automata},
  type = {conference}
}

    Digital Object Identifier

    10.1007/11814771_47
  2. Decomposing Terminating Rewrite Relations
    Jörg Endrullis, Dieter Hofbauer, and Johannes Waldmann
    In: Proc. Workshop on Termination (WST 2006), pp. 39–43 (2006)
    paper

    Summary

    In this paper we are concerned with automatically proving termination of string rewriting systems (or word rewriting systems). We introduce an efficient technique for constructing automata that serve as certificates of match-boundedness, and thereby termination. Previously constructions have either been inefficient or incomplete:

    • Match-Bounded String Rewriting Systems by Alfons Geser, Dieter Hofbauer and Johannes Waldmann. The construction in this paper is complete but very inefficient.
    • On tree automata that certify termination of left-linear term rewriting systems by Alfons Geser, Dieter Hofbauer, Johannes Waldmann and Hans Zantema. The construction in this paper is efficient but incomplete.
      • We present the first automata construction for matchbounded string rewriting that is both efficient and complete. Here completenss means that the algorithm always terminates if the system is matchbounded.

    See research for an overview of my research on termination.

    Bibtex

    @inproceedings{termination:matchbounds:2006,
  author = {Endrullis, J\"{o}rg and Hofbauer, Dieter and Waldmann, Johannes},
  title = {{Decomposing Terminating Rewrite Relations}},
  booktitle = {Proc.\ Workshop on Termination (WST~2006)},
  pages = {39--43},
  year = {2006},
  keywords = {rewriting, termination, automata},
  type = {workshop}
}

    Digital Object Identifier