Publications on Automata
2020
- Transducer Degrees: Atoms, Infima and SupremaJörg Endrullis, Jan Willem Klop, and Rena BakhshiActa 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
- Degrees of Infinite Words, Polynomials and AtomsJörg Endrullis, Juhani Karhumäki, Jan Willem Klop, and Aleksi SaarelaInternational 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.
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
- Undecidability and Finite AutomataJörg Endrullis, Jeffrey Shallit, and Tim SmithIn: 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
- Degrees of Infinite Words, Polynomials and AtomsJörg Endrullis, Juhani Karhumäki, Jan Willem Klop, and Aleksi SaarelaIn: 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.
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
- Regularity Preserving but Not Reflecting EncodingsJörg Endrullis, Clemens Grabmayer, and Dimitri HendriksIn: 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
- Proving Non-Termination by Finite AutomataJörg Endrullis, and Hans ZantemaIn: 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
- Degrees of TransducibilityJörg Endrullis, Jan Willem Klop, Aleksi Saarela, and Markus A. WhitelandIn: 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.
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
- The Degree of Squares Is an AtomJörg Endrullis, Clemens Grabmayer, Dimitri Hendriks, and Hans ZantemaIn: 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
- Streams Are ForeverJörg Endrullis, Dimitri Hendriks, and Jan Willem KlopBulletin 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} }
- Mix-Automatic SequencesJörg Endrullis, Clemens Grabmayer, and Dimitri HendriksIn: 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
- Automatic Sequences and Zip-SpecificationsClemens Grabmayer, Jörg Endrullis, Dimitri Hendriks, Jan Willem Klop, and Lawrence S. MossIn: 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
- On Equal μ-TermsJörg Endrullis, Clemens Grabmayer, Jan Willem Klop, and Vincent van OostromTheoretical 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
- Degrees of StreamsJörg Endrullis, Dimitri Hendriks, and Jan Willem KlopJournal 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} }
2010
- Local Termination: Theory and PracticeJörg Endrullis, Roel C. de Vrijer, and Johannes WaldmannLogical 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
- Transforming Outermost into Context-Sensitive RewritingJörg Endrullis, and Dimitri HendriksLogical 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
- From Outermost to Context-Sensitive RewritingJörg Endrullis, and Dimitri HendriksIn: 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
- Local TerminationJörg Endrullis, Roel C. de Vrijer, and Johannes WaldmannIn: 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
- Proving Infinitary NormalizationJörg Endrullis, Clemens Grabmayer, Dimitri Hendriks, Jan Willem Klop, and Roel C. de VrijerIn: 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
- Matrix Interpretations for Proving Termination of Term RewritingJörg Endrullis, Johannes Waldmann, and Hans ZantemaIn: 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
- Decomposing Terminating Rewrite RelationsJörg Endrullis, Dieter Hofbauer, and Johannes WaldmannIn: 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} }