Developments in Language Theory

A survey of applications of factorization forests.

While a mature theory around logics such as MSO, LTL, and CTL has been developed in the pure boolean setting of finite automata, weighted automata lack such a natural connection with (temporal) logic and related verification algorithms. In this paper, we will identify weighted versions of MSO and CTL that generalize the classical logics and even other quantitative extensions such as probabilistic CTL. We establish expressiveness results on our logics giving translations from weighted and probabilistic CTL into weighted MSO.

This is a survey on some undecidable problems on integer matrices. The proofs of these results employ special instances, called Claus instances, of the Post Correspondence Problem. The presentation is based on the article Halava et al. “Undecidability bounds for integer matrices using Claus instances” (Internat. J. Foundations of Comput. Sci. 18, 2007, 931–948).

This is a talk on the size complexity of two-way finite automata. We present the central open problem in the area, explain a motivation behind it, recall its early history, and introduce some of the concepts used in its study. We then sketch a possible future, describe a natural systematic way of pursuing it, and record some of the progress that has been achieved. We add little to what is already known—only exposition, terminology, and questions.

In this paper, we establish the Černý-Pin conjecture for automata with the property that their transition monoid cannot recognize the language {

a

,

b

}

*

ab

{

a

,

b

}

*

. For the subclass of automata whose transition monoids have the property that each regular

-class is a subsemigroup, we give a tight bound on lengths of reset words for synchronizing automata thereby answering a question of Volkov.

Černý’s conjecture asserts the existence of a synchronizing word of length at most (

n

 − 1)

2

for any synchronized

n

-state deterministic automaton. We prove a quadratic upper bound on the length of a synchronizing word for any synchronized

n

-state deterministic automaton satisfying the following additional property: there is a letter

a

such that for any pair of states

p

,

q

, one has

p

·

a

r

 = 

q

·

a

s

for some integers

r

,

s

(for a state

p

and a word

w

, we denote by

p

·

w

the state reached from

p

by the path labeled

w

). As a consequence, we show that for any finite synchronized prefix code with an

n

-state decoder, there is a synchronizing word of length

O

(

n

2

). This applies in particular to Huffman codes.

In this paper we consider the class of all regular languages definable by the extended majority quantifier and the order predicate but using only two variables. The main part of the paper is the presentation of a geometric method which is used to show that a given regular language cannot be defined by such formulas. Applying this method we can give a necessary condition in terms of an equation as well as an upper and a lower bound for the corresponding class of monoids. As a consequence we obtain that FO + MAJ

2

[ < ] does not contain FO + MOD

2

[ < ].

We study the problem of testing whether a context-free language is included in a fixed set

L

0

, where

L

0

is the language of words reducing to the empty word in the monoid defined by a complete string rewrite system. We prove that, if the monoid is cancellative, then our inclusion problem is polynomially reducible to the problem of testing equivalence of straight-line programs in the same monoid. As an application, we obtain a polynomial time algorithm for testing if a context-free language is included in a Dyck language (the best previous algorithm for this problem was doubly exponential).

Blanchet-Sadri et al. have shown that

Avoidability

, or the problem of deciding the avoidability of a finite set of partial words over an alphabet of size

k

 ≥ 2, is

${\mathcal{NP}}$

-hard [Theoret. Comput. Sci.

410

(2009) 968–972]. Building on their work, we analyze in this paper the complexity of natural variations on the problem. While some of them are

${\mathcal{NP}}$

-hard, others are shown to be efficiently decidable. Using some combinatorial properties of de Bruijn graphs, we establish a correspondence between lengths of cycles in such graphs and periods of avoiding words, resulting in a tight bound for periods of avoiding words. We also prove that

Avoidability

can be solved in polynomial space, and reduces in polynomial time to the problem of deciding the avoidability of a finite set of partial words of equal length over the binary alphabet. We give a polynomial bound on the period of an infinite avoiding word, in the case of sets of full words, in terms of two parameters: the length and the number of words in the set. We give a polynomial space algorithm to decide if a finite set of partial words is avoided by a non-ultimately periodic infinite word. The same algorithm also decides if the number of finite words of length

n

avoiding a given finite set of partial words grows polynomially or exponentially with

n

.

A famous theorem of Kuratowski states that, in a topological space, at most 14 distinct sets can be produced by repeatedly applying the operations of closure and complement to a given set. We re-examine this theorem in the setting of formal languages, where closure is either Kleene closure or positive closure. We classify languages according to the structure of the algebra they generate under iterations of complement and closure. There are precisely 9 such algebras in the case of positive closure, and 12 in the case of Kleene closure. We study how the properties of being open and closed are preserved under concatenation. We investigate analogues, in formal languages, of the separation axioms in topological spaces; one of our main results is that there is a clopen partition separating two words if and only if the words do not commute. We can decide in quadratic time if the language specified by a DFA is closed, but if the language is specified by an NFA, the problem is PSPACE-complete.

In this paper we investigate the periodic structure of

rich words

(i.e., words having the highest possible number of palindromic factors), giving new results relating them with

periodic-like

words. In particular, some new characterizations of rich words and rich palindromes are given. We also prove that a periodic-like word is rich if and only if the square of its fractional root is also rich.

This is a new applied development of trace theory to compilation. Trace theory allows to commute independent program instructions, but overlooks the differences between control and data dependencies. Control(C)-dependences, unlike data-dependences, are determined by the Control Flow Graph, modelled as a local DFA. To ensure semantic equivalence, partial commutation must preserve C-dependences. New properties are proved for C-dependences and corresponding traces. Any local language is star-connected with respect to C-dependences, hence this trace language family is recognizable. Local languages unambiguously represent traces. Within the family of local languages with the same C-dependences, we construct the language such that instructions are maximally anticipated. This language differs from the Foata-Cartier normal form. Future directions for application of trace theory to program optimization are outlined.

In this paper, we study rational relations that are both left and right synchronous. We show that these relations are boolean combinations of almost length preserving relations, length comparing relations and recognizable relations.

One of the particularities of information encoded as DNA strands is that a string

u

contains basically the same information as its Watson-Crick complement, denoted here as

θ

(

u

). Thus, any expression consisting of repetitions of

u

and

θ

(

u

) can be considered in some sense periodic. In this paper we give a generalization of Lyndon and Schützenberger’s classical result about equations of the form

u

l

 = 

v

n

w

m

, to cases where both sides involve repetitions of words as well as their complements. Our main results show that, for such extended equations, if

l

 ≥ 5,

n

,

m

 ≥ 3, then all three words involved can be expressed in terms of a common word

t

and its complement

θ

(

t

). Moreover, if

l

 ≥ 5, then

n

 = 

m

 = 3 is an optimal bound. We also obtain a complete characterization of all possible overlaps between two expressions that involve only some word

u

and its complement

θ

(

u

).

We show here how to construct a cellular automaton whose asymptotic set (the set of configurations it converges to) is maximally complex: it contains only configurations of maximal Kolmogorov complexity. This cellular automaton hence exhibits the most complex possible asymptotic behavior.

We consider algorithms for approximating context–free grammars by regular grammars, making use of Chomsky’s characterization of non–self–embedding grammars as generating regular languages and a transformation by Mohri and Nederhof on sets of mutually recursive nonterminals. We give an exposition of strongly regular grammars and this transformation, and use it as a subprocedure to obtain tighter regular approximations to a given context-free grammar. In another direction, the generalization by a 1–lookahead extends Mohri and Nederhof’s transformation by incorporating more context into the regular approximation at the expense of a larger grammar.

In this paper we prove that it is decidable whether the set pow(

L

), which we get by taking all the powers of all the words in some regular language

L

, is regular or not. The problem was originally posed by Calbrix and Nivat in 1995. Partial solutions have been given by Cachat for unary languages and by Horváth et al. for various kinds of exponent sets for the powers and regular languages which have primitive roots satisfying certain properties. We show that the regular languages which have a regular power are the ones which are ’almost’ equal to their Kleene-closure.

In the present paper, we study the existence of descriptive patterns, i. e. patterns that cover all words in a given set through morphisms and that are optimal in terms of revealing commonalities of these words. Our main result shows that if patterns may be mapped onto words by arbitrary morphisms, then there exist infinite sets of words that do not have a descriptive pattern. This answers a question posed by Jiang, Kinber, Salomaa, Salomaa and Yu (

International Journal of Computer Mathematics

50, 1994). Since the problem of whether a pattern is descriptive depends on the inclusion relation of so-called pattern languages, our technical considerations lead to a number of deep insights into the inclusion problem for and the topology of the class of terminal-free E-pattern languages.

A stateless

k

-head two-way deterministic finite automaton (

k

-head 2DFA), has only one state, hence the designation stateless. Its transitions depends solely on the symbols currently scanned by its

k

heads, and in every such transition each head can move one cell left, right, or remain stationary. An input, which is delimited by end markers, is accepted if the machine, when started with all heads on the left end marker, reaches the configuration where all the heads are on the right end marker. The nondeterministic version is denoted by

k

-head 2NFA.

We prove that stateless (

k

 + 1)-head 2DFAs (resp., 2NFAs) are computationally more powerful than

k

-head 2DFAs (resp., 2NFAs), improving a recent result where it was shown that (

k

 + 4) heads are better than

k

heads.

We also study stateless multihead pushdown automata in their two-way and one-way, deterministic and nondeterministic variations and show that for all these varieties,

k

 + 1 heads allow more computational power than

k

heads. Finally, we give some characterizations of stateless multihead finite and multihead pushdown automata.

We study expansions in non-integer negative base − 

β

introduced by Ito and Sadahiro [7]. Using countable automata associated with ( − 

β

)-expansions, we characterize the case where the ( − 

β

)-shift is a system of finite type. We prove that, if

β

is a Pisot number, then the ( − 

β

)-shift is a sofic system. In that case, addition (and more generally normalization on any alphabet) is realizable by a finite transducer.

Let

k

 ≥ 2 be an integer. An

abelian k

-th power

is a word of the form

X

1

X

2

 ⋯ 

X

k

where

X

i

is a permutation of

X

1

for 2 ≤ 

i

 ≤ 

k

. In this paper, we consider

crucial words

for abelian

k

-th powers, i.e., finite words that avoid abelian

k

-th powers, but which cannot be extended to the right by any letter of their own alphabets without creating an abelian

k

-th power. More specifically, we consider the problem of determining the minimal length of a crucial word avoiding abelian

k

-th powers. This problem has already been solved for abelian squares by Evdokimov and Kitaev [6], who showed that a

minimal crucial word

over an

n

-letter alphabet

${\mathcal{A}}_n = \{1,2,\ldots, n\}$

avoiding

abelian squares

has length 4

n

 − 7 for

n

 ≥ 3. Extending this result, we prove that a minimal crucial word over

${\mathcal{A}}_n$

avoiding abelian cubes has length 9

n

 − 13 for

n

 ≥ 5, and it has length 2, 5, 11, and 20 for

n

 = 1,2,3, and 4, respectively. Moreover, for

n

 ≥ 4 and

k

 ≥ 2, we give a construction of length

k

2

(

n

 − 1) − 

k

 − 1 of a crucial word over

${\mathcal{A}}_n$

avoiding abelian

k

-th powers. This construction gives the minimal length for

k

 = 2 and

k

 = 3.

We improve on some recent results on lower bounds for conversion problems for regular expressions. In particular we consider the conversion of planar deterministic finite automata to regular expressions, study the effect of the complementation operation on the descriptional complexity of regular expressions, and the conversion of regular expressions extended by adding intersection or interleaving to ordinary regular expressions. Almost all obtained lower bounds are optimal, and the presented examples are over a binary alphabet, which is best possible.

We study the Monadic Second Order (MSO) Hierarchy over infinite pictures, that is tilings. We give a characterization of existential MSO in terms of tilings and projections of tilings. Conversely, we characterise logic fragments corresponding to various classes of infinite pictures (subshifts of finite type, sofic subshifts).

A number

α

, in the range from

n

to 2

n

, is magic for

n

with respect to a given alphabet size

s

, if there is no minimal nondeterministic finite automaton of

n

states and

s

input letters whose equivalent minimal deterministic finite automaton has

α

states. We show that in the case of a ternary alphabet, there are no magic numbers. For all

n

and

α

satisfying that

$n \leqslant \alpha \leqslant 2^n$

, we describe an

n

-state nondeterministic automaton with a three-letter input alphabet that needs

α

deterministic states.

Seki et al. (1991) proved a rather weak pumping lemma for multiple context-free languages, which says that any infinite

m

-multiple context-free language contains a string that is pumpable at some 2

m

substrings. We prove a pumping lemma of the usual universal form for the subclass consisting of

well-nested

multiple context-free languages. This is the same class of languages generated by non-duplicating macro grammars and by coupled-context-free grammars.

We show that the support of a recognizable series over a zero-sum free, commutative semiring is a recognizable language. We also give a sufficient and necessary condition for the existence of an effective transformation of a weighted automaton recognizing a series

S

over a zero-sum free, commutative semiring into an automaton recognizing the support of

S

.

We obtain a simple, purely game-theoretic characterization of Boolean grammars [

A. Okhotin, Information and Computation, 194 (2004) 19-48

]. In particular, we propose a two-player infinite game of perfect information for Boolean grammars, which is equivalent to their well-founded semantics. The game is directly applicable to the simpler classes of conjunctive and context-free grammars, and it offers a promising new connection between game theory and formal languages.

We consider properties of the solution set of a word equation with one unknown. We prove that the solution set of a word equation possessing infinite number of solutions is of the form (

pq

)

*

p

where

pq

is primitive. Next, we prove that a word equation with at most four occurrences of the unknown possesses either infinitely many solutions or at most two solutions. We show that there are equations with at most four occurrences of the unknown possessing exactly two solutions. Finally, we prove that a word equation with at most 2

k

occurrences of the unknown possesses either infinitely many solutions or at most 8log

k

 + 

O

(1) solutions. Hence, if we consider a class

${\cal E}_k$

of equations with at most 2

k

occurrences of the unknown, then each equation in this class possesses either infinitely many solutions or a constant number of solutions. Our considerations allow to construct the first truly linear time algorithm for computing the solution set of an equation in a nontrivial class of equations.

Systems of equations of the form

X

 = 

Y

 + 

Z

and

X

 = 

C

, in which the unknowns are sets of natural numbers, “+” denotes elementwise sum of sets

S

 + 

T

 = 

m

 + 

n

 ∣ 

m

 ∈ 

S

,

n

 ∈ 

T

, and

C

is an ultimately periodic constant, have recently been proved to be computationally universal (Jeż, Okhotin, “Equations over sets of natural numbers with addition only”, STACS 2009). This paper establishes some limitations of such systems. A class of sets of numbers that cannot be represented by unique, least or greatest solutions of systems of this form is defined, and a particular set in this class is constructed.

In this note we solve a problem left open in [2]: namely, we show that the iterated superposition of a regular language is regular. The proof of this result is based on two facts: (i) the iterated superposition of a language equals the restricted iterated superposition of the same language, (ii) the sequence formed by iteratively applying the restricted superposition can be precisely defined. We then define the restricted superposition distance between a word and a language and prove that this distance can be computed in time

${\mathcal O}(n^2f(n))$

, where the language is accepted in time

${\mathcal O}(f(n))$

in the RAM model. Finally, we briefly discuss the necessity of the

n

2

factor for the classes of regular and context-free languages.

We define a weighted

μ

-calculus on finite and infinite words. Hereby, the

μ

-calculus does not use conjunction and the weights are taken from semirings satisfying certain completeness and continuity properties. For important semirings like distributive complete lattices, the tropical and the probabilistic semiring, we show that the formulas of the conjunction-free weighted

μ

-calculus define exactly the class of omega-rational formal power series.

Temporal logics are a well investigated formalism for the specification and verification of reactive systems. Using formal verification techniques, we can ensure the correctness of a system with respect to its desired behavior (specification), by verifying whether a model of the system satisfies a temporal logic formula modeling the specification.

From a practical point of view, a very challenging issue in using temporal logic in formal verification is to come out with techniques that automatically allow to select small critical parts of the system to be successively verified. Another challenging issue is to extend the expressiveness of classical temporal logics, in order to model more complex specifications.

In this paper, we address both issues by extending the classical branching-time temporal logic C

tl

* with minimal model quantifiers (MC

tl

*). These quantifiers allow to extract, from a model, minimal submodels on which we check the specification (also given by an MC

tl

* formula).We show that

MCtl

* is strictly more expressive than C

tl

*. Nevertheless, we prove that the model checking problem for MC

tl

. remains decidable and in particular in

PSpace

. Moreover, differently from C

tl

*, we show that

MCtl

* does not have the tree model property, is not bisimulation-invariant and is sensible to unwinding. As far as the satisfiability concerns, we prove that MC

tl

* is highly undecidable. We further investigate the model checking and satisfiability problems for

MCtl

* sublogics, such as MP

ml

,

MCtl

, and

MCtl

+, for which we obtain interesting results. Among the others, we show that MP

ml

retains the finite model property and the decidability of the satisfiability problem.

We investigate the efficiency of simulations of storages by several counters. A simulation of a pushdown store is described which is optimal in the sense that reducing the number of counters of a simulator leads to an increase in time complexity. The lower bound also establishes a tight counter hierarchy in exponential time. Then we turn to simulations of a set of counters by a different number of counters. We improve and generalize a known simulation in polynomial time and we show a tight hierarchy result for machines working in the same polynomial bound with an increasing number of counters. We also prove hierarchies for machines with a fixed number of counters and with growing polynomial time bounds.

We aim to generalize Büchi’s fundamental theorem on the coincidence of recognizable and MSO-definable languages to a weighted timed setting. For this, we investigate subclasses of weighted timed automata and show how we can extend existing timed MSO logics with weights. Here, we focus on the class of weighted event-recording automata and define a weighted extension of the full logic MSO

$_{\rm er}{(\it \Sigma)}$

introduced by D’Souza. We show that every weighted event-recording automaton can effectively be transformed into a corresponding sentence of our logic and vice versa. The methods presented in the paper can be adopted to weighted versions of timed automata and Wilke’s logic of relative distance. The results indicate the robustness of weighted timed automata models and may be used for specification purposes.

The investigation of the “clustering effect” of the Burrows-Wheeler transform (BWT) leads to study the words having

simple BWT

, i.e. words

w

over an ordered alphabet

A

 = {

a

1

,

a

2

,...,

a

k

}, with

a

1

 < 

a

2

 < ... < 

a

k

, such that

bwt

(

w

) is of the form

$a_k^{n_k} a_{k-1}^{n_{k-1}} \cdots a_1^{n_1}$

, for some non-negative integers

n

1

,

n

2

, ...,

n

k

. We remark that, in the case of binary alphabets, there is an equivalence between words having simple BWT, the family of (circular) balanced words and the conjugates of standard words. In the case of alphabets of size greater than two, there is no more equivalence between these notions. As a main result of this paper we prove that, under assumption of balancing, the following three conditions on a word

w

are equivalent:

i)

w

has simple BWT,

ii)

w

is a circularly rich word, and

iii)

w

is a conjugate of a finite epistandard word.

We analyze Hmelevskii’s theorem, which states that the general solutions of constant-free equations on three unknowns are expressible by a finite collection of formulas of word and numerical parameters. We prove that the size of the finite representation is bounded by an exponential function on the size of the equation. We also prove that the shortest nontrivial solution of the equation, if it exists, is exponential, and that its existence can be solved in nondeterministic polynomial time.

We develop a theory of (first-order) definability in the infix partial order on words in parallel with a similar theory for the

h

-quasiorder of finite

k

-labeled forests. In particular, any element is definable (provided that words of length 1 or 2 are taken as parameters), the first-order theory of the structure is atomic and computably isomorphic to the first-order arithmetic. We also characterize the automorphism group of the structure and show that any arithmetical predicate invariant under the automorphisms of the structure is definable in the structure.

The growth properties of power-free languages over finite alphabets are studied. A method to obtain sharp two-sided bounds of the growth rate of

β

-power-free languages for arbitrary rational number

β

 ≥ 2 is obtained. A table of the growth rates, calculated with the absolute error less than 10

− 5

for different particular power-free languages, is presented.

We give a new proof for the decidability of the equivalence for bounded length-degree transducers, a result established by Weber in 1992. Our proof relies on structural constructions that we have recently introduced to decompose such transducers. The complexity of our procedure is of triple exponential order, whereas the known bound is a tower of exponentials of exponential height. Furthermore, our proof deals with the more general family of transducers whose morphic image by some nonerasing morphism is a

k

-valued transducer.

It is shown that applying linear erasing to a Petri net language yields a language generated by a non-erasing matrix grammar. The proof uses Petri net controlled grammars. These are context-free grammars, where the application of productions has to comply with a firing sequence in a Petri net. Petri net controlled grammars are equivalent to arbitrary matrix grammars (without appearance checking), but a certain restriction on them (linear Petri net controlled grammars) leads to the class of languages generated by non-erasing matrix grammars.

It is also shown that in Petri net controlled grammars (with final markings and arbitrary labeling), erasing rules can be eliminated, which yields a reformulation of the problem of whether erasing rules in matrix grammars can be eliminated.