30 Result(s)
-
Chapter and Conference Paper
DFAs and PFAs with Long Shortest Synchronizing Word Length
It was conjectured by Černý in 1964, that a synchronizing DFA on n states always has a synchronizing word of length at most $$...
-
Chapter and Conference Paper
Finding DFAs with Maximal Shortest Synchronizing Word Length
It was conjectured by Černý in 1964 that a synchronizing DFA on n states always has a shortest synchronizing word of length at most ...
-
Chapter and Conference Paper
Classifying Non-periodic Sequences by Permutation Transducers
Transducers order infinite sequences into natural classes, but permutation transducers provide a finer classification, respecting certain changes to finite segments. We investigate this hierarchy for non-perio...
-
Chapter and Conference Paper
Using SMT for Solving Fragments of Parameterised Boolean Equation Systems
Fixpoint logics such as parameterised Boolean equation systems (PBESs) provide a unifying framework in which a number of practical decision problems can be encoded. Efficient evaluation methods (solving methods i...
-
Chapter and Conference Paper
Proving Termination of Graph Transformation Systems Using Weighted Type Graphs over Semirings
We introduce techniques for proving uniform termination of graph transformation systems, based on matrix interpretations for string rewriting. We generalize this technique by adapting it to graph rewriting ins...
-
Chapter and Conference Paper
The Degree of Squares is an Atom
We answer an open question in the theory of degrees of infinite sequences with respect to transducibilityby finite-state transducers. An initial study of this partial order of degrees was carried out in [1], but ...
-
Chapter and Conference Paper
Termination Analysis for Graph Transformation Systems
We introduce two techniques for proving termination of graph transformation systems. We do not fix a single initial graph, but consider arbitrary initial graphs (uniform termination), but also certain sets of ...
-
Chapter and Conference Paper
Termination of Cycle Rewriting
String rewriting can not only be applied on strings, but also on cycles and even on general graphs. In this paper we investigate termination of string rewriting applied on cycles, shortly denoted as cycle rewr...
-
Chapter and Conference Paper
Erratum: Cinderella versus the Wicked Stepmother
The name of the first author of the paper starting on page 57 of this volume has been printed incorrectly. It should read: Marijke H.L. Bodlaender
-
Chapter and Conference Paper
Cinderella versus the Wicked Stepmother
We investigate a combinatorial two-player game, in which one player wants to keep the behavior of an underlying water-bucket system stable whereas the other player wants to cause overflows. This game is motiva...
-
Chapter and Conference Paper
Well-Definedness of Streams by Termination
Streams are infinite sequences over a given data type. A stream specification is a set of equations intended to define a stream. We propose a transformation from such a stream specification to a TRS in such a ...
-
Chapter and Conference Paper
A Tool Proving Well-Definedness of Streams Using Termination Tools
A stream specification is a set of equations intended to define a stream, that is, an infinite sequence over a given data type. In [5] a transformation from such a stream specification to a TRS is defined in s...
-
Chapter and Conference Paper
Degrees of Undecidability in Term Rewriting
Undecidability of various properties of first order term rewriting systems is well-known. An undecidable property can be classified by the complexity of the formula defining it. This gives rise to a hierarchy ...
-
Article
Matrix Interpretations for Proving Termination of Term Rewriting
We present a new method for automatically proving termination of term rewriting. It is based on the well-known idea of interpretation of terms where every rewrite step causes a decrease, but instead of the usu...
-
Chapter and Conference Paper
Normalization of Infinite Terms
We investigate the property SN ∞ being the natural concept related to termination when considering term rewriting applied to infinite terms. It turns out that this property can be fully characteri...
-
Chapter and Conference Paper
The Termination Competition
Since 2004, a Termination Competition is organized every year. This competition boosted a lot the development of automatic termination tools, but also the design of new techniques for proving termination. We p...
-
Chapter and Conference Paper
Termination by Quasi-periodic Interpretations
We present a new method for automatically proving termination of term rewriting and string rewriting. It is based on the well-known idea of interpretation of terms in natural numbers where every rewrite step c...
-
Chapter and Conference Paper
Automation of Recursive Path Ordering for Infinite Labelled Rewrite Systems
Semantic labelling is a transformational technique for proving termination of Term Rewriting Systems (TRSs). Only its variant with finite sets of labels was used so far in tools for automatic termination provi...
-
Chapter and Conference Paper
Matrix Interpretations for Proving Termination of Term Rewriting
We present a new method for automatically proving termination of term rewriting. It is based on the well-known idea of interpretation of terms where every rewrite step causes a decrease, but instead of the usu...
-
Chapter and Conference Paper
Finding Finite Automata That Certify Termination of String Rewriting
We present a technique based on the construction of finite automata to prove termination of string rewriting systems. Using this technique the tools Matchbox and TORPA are able to prove termination of particular ...
