Search

Automatic sequences can be defined by DFAs with output (DFAO) in two natural ways. We propose to consider the minimal size of a corresponding DFAO as the complexity measure of the automatic sequence, for both variants. This paper compares these complexity measures and investigates their properties like the relationships with kernel and morphic sequences. There exist automatic sequences for which the one complexity is exponentially greater than the other one, in both directions. For both complexity measures we investigate the effect of taking basic operations on sequences like removing or adding an element in front, and observe that these operations may increase the complexity by at most a quadratic factor.

It was conjectured by Černý in 1964 that a synchronizing DFA on n states always has a shortest synchronizing word of length at most (n−1) 2 (n−1)2, and he gave a sequence of DFAs for which this bound is reached. In 2006 Trahtman conjectured that apart from Černý’s sequence only 8 DFAs exist attaining the bound. He gave an investigation of all DFAs up to certain size for which the bound is reached, and which do not contain other synchronizing DFAs. Here we extend this analysis in two ways: we drop this latter condition, and we drop limits on alphabet size. For n≤4 n≤4 we do the full analysis yielding 19 new DFAs with smallest synchronizing word length (n−1) 2 (n−1)2, refuting Trahtman’s conjecture. All these new DFAs are extensions of DFAs that were known before. For n≥5 n≥5 we prove that none of the DFAs in Trahtman’s analysis can be extended similarly. In particular, as a main result we prove that the Černý examples C n Cn do not admit non-trivial extensions keeping the same smallest synchronizing word length (n−1) 2 (n−1)2.

We present new techniques to prove termination of cycle rewriting, that is, string rewriting on cycles, which are strings in which the start and end are connected. Our main technique is to transform cycle rewriting into string rewriting and then apply state of the art techniques to prove termination of the string rewrite system. We present three such transformations, and prove for all of them that they are sound and complete. Apart from this transformational approach, we extend the use of matrix interpretations as was studied before. We present several experiments showing that often our new techniques succeed where earlier techniques fail.

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 many basic questions remain unanswered.One of the central questions concerns the existence of atom degrees, other than the degree of the ‘identity sequence’ 100101102103⋯ . A degree is called an ‘atom’ if below it there is only the bottom degree 00 , which consists of the ultimately periodic sequences. We show that also the degree of the ‘squares sequence’ 1001011041091016⋯ is an atom.As the main tool for this result we characterise the transducts of ‘spiralling’ sequences and their degrees. We use this to show that every transduct of a ‘polynomial sequence’ either is in 00 or can be transduced back to a polynomial sequence for a polynomial of the same order.

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-periodic sequences over \(\{0,1\}\) in which the groups of 0s and 1s grow according to simple functions like polynomials. In this hierarchy we find infinite strictly ascending chains of sequences, all being equivalent with respect to ordinary transducers.

It was conjectured by \v{C}ern\'y in 1964, that a synchronizing DFA on $n$ states always has a shortest synchronizing word of length at most $(n-1)^2$, and he gave a sequence of DFAs for which this bound is reached. Until now a full analysis of all DFAs reaching this bound was only given for $n \leq 4$, and with bounds on the number of symbols for $n \leq 10$. Here we give the full analysis for $n \leq 6$, without bounds on the number of symbols. For PFAs the bound is much higher. For $n \leq 6$ we do a similar analysis as for DFAs and find the maximal shortest synchronizing word lengths, exceeding $(n-1)^2$ for $n =4,5,6$. For arbitrary n we give a construction of a PFA on three symbols with exponential shortest synchronizing word length, giving significantly better bounds than earlier exponential constructions. We give a transformation of this PFA to a PFA on two symbols keeping exponential shortest synchronizing word length, yielding a better bound than applying a similar known transformation., Comment: 16 pages, 2 figures source code added

Streams are infinite sequences over a given data type. A stream specification is a set of equations intended to define a stream. A core property is productivity: unfolding the equations produces the intended stream in the limit. In this paper we show that productivity is equivalent to termination with respect to the balanced outermost strategy of a TRS obtained by adding an additional rule. For specifications not involving branching symbols balancedness is obtained for free, by which tools for proving outermost termination can be used to prove productivity fully automatically.

Haken proved that every resolution refutation of the pigeonhole formula has at least exponential size. Groote and Zantema proved that a particular OBDD computation of the pigeonhole formula has an exponential size. Here we show that any arbitrary OBDD refutation of the pigeonhole formula has an exponential size, too: we prove that the size of one of the intermediate OBDDs is at least $\Omega(1.025^n)$.

Item does not contain fulltext Algebra and Coalgebra in Computer Science, Third International Conference, CALCO 2009, 07 september 2009

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 way that termination of the resulting TRS implies that the stream specification admits a unique solution. As a consequence, proving such well-definedness of several interesting stream specifications can be done fully automatically using present powerful tools for proving TRS termination.

We develop a Coq formalization of the matrix interpretation method, which is a recently developed, powerful approach to proving termination of term rewriting. Our formalization is a contribution to the CoLoR project and allows to automatically certify matrix interpretation proofs produced by tools for proving termination. Thanks to this development the combination of CoLoR and our tool, TPA, was the winner in 2007 in the new certified category of the annual Termination Competition.

Item does not contain fulltext 62 p.

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 present the background, results, and conclusions of the three first editions, and discuss perspectives and challenges for the future.

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 proving and variants with infinite sets of labels were considered not to be suitable for automation. We show that such automation can be achieved for semantic labelling with natural numbers, in combination with recursive path ordering (RPO). In order to do so we developed algorithms to deal with recursive path ordering for these infinite labelled systems. Using these techniques TPA, a tool developed by the first author, is the only current tool that can prove termination of the SUBST system automatically.