Language and Automata Theory and Applications

The heterogeneity characterizing the systems populating the Ubiquitous Computing environment prevents their seamless interoperability. Heterogeneous protocols may be willing to cooperate in order to reach some common goal even though they meet dynamically and do not have a priori knowledge of each other. Despite numerous efforts have been done in the literature, the automated and run-time interoperability is still an open challenge for such environment. We consider interoperability as the ability for two Networked Systems (NSs) to communicate and correctly coordinate to achieve their goal(s).

In this paper, we report the main outcomes of our past and recent research on automatically achieving protocol interoperability via connector synthesis. We consider application-layer connectors by referring to two conceptually distinct notions of connector:

coordinator

and

mediator

. The former is used when the NSs to be connected are already able to communicate but they need to be specifically coordinated in order to reach their goal(s). The latter goes a step forward representing a solution for both achieving correct coordination and enabling communication between highly heterogeneous NSs.

In the past, most of the works in the literature described efforts to the automatic synthesis of coordinators while, in recent years the focus moved also to the automatic synthesis of mediators. By considering our past experience on the automatic synthesis of coordinators and mediators as a baseline, we conclude by overviewing a formal method for the automated synthesis of mediators that allows to relax some assumptions state-of-the-art approaches rely on, and characterize the necessary and sufficient interoperability conditions that ensure the mediator existence and correctness.

A new approach to program verification is based on automata. The notion of automaton depends on the verification problem at hand (nested word automata for recursion, Büchi automata for termination, a form of data automata for parametrized programs, etc.). The approach is to first construct an automaton for the candidate proof and then check its validity via automata inclusion. The originality of the approach lies in the construction of an automaton from a correctness proof of a given sequence of statements. A sequence of statements is at the same time a word over a finite alphabet and it is (a very simple case of) a program. Just as we ask whether a word has an accepting run, we can ask whether a sequence of statements has a correctness proof (of a certain form). The automaton accepts exactly the sequences that do.

We survey recent work on the use of Hankel matrices

$$H(f, \Box )$$

for real-valued graph parameters

$$f$$

and a binary sum-like operation

$$\Box $$

on labeled graphs such as the disjoint union and various gluing operations of pairs of laeled graphs. Special cases deal with real-valued word functions. We start with graph parameters definable in Monadic Second Order Logic

$$\mathrm {MSOL}$$

and show how

$$\mathrm {MSOL}$$

-definability can be replaced by the assumption that

$$H(f, \Box )$$

has finite rank. In contrast to

$$\mathrm {MSOL}$$

-definable graph parameters, there are uncountably many graph parameters

$$f$$

with Hankel matrices of finite rank. We also discuss how real-valued graph parameters can be replaced by graph parameters with values in commutative semirings.

The computational power of membrane systems, in their different variants, can be studied by defining classes of problems that can be solved within given bounds on computation time or space, and comparing them with usual computational complexity classes related to the Turing Machine model. Here we will consider in particular membrane systems with active membranes (where new membranes can be created by division of existing membranes). The problems related to the definition of time/space complexity classes for membrane systems will be discussed, and the resulting hierarchy will be compared with the usual hierarchy of complexity classes, mainly through simulations of Turing Machines by (uniform families of) membrane systems with active membranes.

In this paper we survey some recent researches concerning the shuffle operation that arise both in Formal Languages and in Combinatorics on Words.

Approximate string matching is the problem of finding all factors of a text

$$t$$

of length

$$n$$

that are at a distance at most

$$k$$

from a pattern

$$x$$

of length

$$m$$

. Approximate circular string matching is the problem of finding all factors of

$$t$$

that are at a distance at most

$$k$$

from

$$x$$

or

from any of its rotations. In this article, we present a new algorithm for approximate circular string matching under the edit distance model with optimal average-case search time

$$\mathcal {O}(n(k + \log m) /m)$$

. Optimal average-case search time can also be achieved by the algorithms for multiple approximate string matching (Fredriksson and Navarro, 2004) using

$$x$$

and its rotations as the set of multiple patterns. Here we reduce the preprocessing time and space requirements compared to that approach.

We generalise a search algorithm by Mohri and Riley from strings to trees. The original algorithm takes as input a weighted automaton

$$M$$

over the tropical semiring, together with an integer

$$N$$

, and outputs

$$N$$

strings of minimal weight with respect to

$$M$$

. In our setting,

$$M$$

defines a weighted tree language, again over the tropical semiring, and the output is a set of

$$N$$

trees with minimal weight. We prove that the algorithm is correct, and that its time complexity is a low polynomial in

$$N$$

and the relevant size parameters of

$$M$$

.

In the life sciences, determining the sequence of bio-molecules is essential step towards the understanding of their functions and interactions inside an organism. Powerful technologies allows to get huge quantities of short sequencing reads that need to be assemble to infer the complete target sequence. These constraints favour the use of a version de Bruijn Graph (DBG) dedicated to assembly. The de Bruijn Graph is usually built directly from the reads, which is time and space consuming. Given a set

$$R$$

of input words, well-known data structures, like the generalised suffix tree, can index all the substrings of words in

$$R$$

. In the context of DBG assembly, only substrings of length

$$k+1$$

and some of length

$$k$$

are useful. A truncated version of the suffix tree can index those efficiently. As indexes are exploited for numerous purposes in bioinformatics, as read cleaning, filtering, or even analysis, it is important to enable the community to reuse an existing index to build the DBG directly from it. In an earlier work we provided the first algorithms when starting from a suffix tree or suffix array. Here, we exhibit an algorithm that exploits a reduced version of the truncated suffix tree and computes the DBG from it. Importantly, a variation of this algorithm is also shown to compute the contracted DBG, which offers great benefits in practice. Both algorithms are linear in time and space in the size of the output.

Frequent pattern mining is widely used in bioinformatics since frequent patterns in bio sequences often correspond to residues conserved during evolution. In bio sequence analysis, non-overlapping inversions are well-studied because of their practical properties for local sequence comparisons. We consider the problem of finding frequent patterns in a bio sequence with respect to non-overlapping inversions, and design efficient algorithms.

A maximum(-sum) contiguous subsequence of a real-valued sequence is a contiguous subsequence with the maximum cumulative sum. A minimal maximum contiguous subsequence is a minimal contiguous subsequence among all maximum ones of the sequence. We have designed and implemented a domain-decomposed parallel algorithm on cluster systems with Message Passing Interface that finds all successive minimal maximum subsequences of a random sample sequence from a normal distribution with negative mean. Our study employs the theory of random walk to derive an approximate probabilistic length bound for minimal maximum subsequences in an appropriate probabilistic setting, which is incorporated in the algorithm to facilitate the concurrent computation of all minimal maximum subsequences in hosting processors. We also present a preliminary empirical study of the speedup and efficiency achieved by the parallel algorithm with synthetic random data.

Partial orders are a fundamental mathematical structure capable of representing true concurrency and causality on a set of atomic events. In this paper we study two mathematical formalisms capable of the compressed representation of sets of partial orders: Labeled Event Structures (LESs) and Conditional Partial Order Graphs (CPOGs). We demonstrate their advantages and disadvantages and propose efficient algorithms for transforming a set of partial orders from a given compressed representation in one formalism into an equivalent representation in another formalism without the explicit enumeration of each scenario. These transformations reveal the superior expressive power of CPOGs as well as the cost of this expressive power. The proposed algorithms make use of an intermediate mathematical formalism, called Conditional Labeled Event Structures (CLESs), which combines the advantages of LESs and CPOGs. All three formalisms are compared on a number of benchmarks.

We study counting monadic second-order logics (CMso) for unordered data trees. Our objective is to enhance this logic with data constraints for comparing string data values attached to sibling edges of a data tree. We show that CMso satisfiability becomes undecidable when adding data constraints between siblings that can check the equality of factors of data values. For more restricted data constraints that can only check the equality of prefixes, we show that it becomes decidable, and propose a related automaton model with good complexities. This restricted logic is relevant to applications such as checking well-formedness properties of semi-structured databases and file trees. Our decidability results are obtained by compilation of CMso to automata for unordered trees, where both are enhanced with data constraints in a novel manner.

Automata over infinite alphabets have recently come to be studied extensively as potentially useful tools for solving problems in verification and database theory. One popular model of automata studied is the Class Memory Automata (CMA), for which the emptiness problem is equivalent to Petri Net Reachability. We identify a restriction – which we call weakness – of CMA, and show that they are equivalent to three existing forms of automata over data languages. Further, we show that in the deterministic case they are closed under all Boolean operations, and hence have an

ExpSpace

-complete equivalence problem. We also extend CMA to operate over multiple levels of nested data values, and show that while these have undecidable emptiness in general, adding the weakness constraint recovers decidability of emptiness, via reduction to coverability in well-structured transition systems. We also examine connections with existing automata over nested data.

Several insertion operations are studied applied to languages accepted by one-way and two-way deterministic reversal-bounded multicounter machines. These operations are defined by the ideals obtained from relations such as the prefix, infix, suffix and outfix relations. The insertion of regular languages and other languages into deterministic reversal-bounded multicounter languages is also studied. The question of whether the resulting languages can always be accepted by deterministic machines with the same number of turns on the input tape, the same number of counters, and reversals on the counters is investigated. In addition, the question of whether they can always be accepted by increasing either the number of input tape turns, counters, or counter reversals is addressed. The results in this paper form a complete characterization based on these parameters. Towards these new results, we use a technique for simultaneously showing a language cannot be accepted by both one-way deterministic reversal-bounded multicounter machines, and by two-way deterministic machines with one reversal-bounded counter.

We push further a recently proposed approach for studying synchronizing automata and Černý’s conjecture, namely, the

synchronizing probability function

. In this approach, the synchronizing phenomenon is reinterpreted as a Two-Player game, in which the optimal strategies of the players can be obtained through a Linear Program. Our analysis mainly focuses on the concept of

triple rendezvous time

, the length of the shortest word mapping three states onto a single one. It represents an intermediate step in the synchronizing process, and is a good proxy of its overall length. Our contribution is twofold. First, using the synchronizing probability function and properties of linear programming, we provide a new upper bound on the triple rendezvous time. Second, we disprove a conjecture on the synchronizing probability function by exhibiting a family of counterexamples. We discuss the game theoretic approach and possible further work in the light of our results.

Robot Game is a two player vector addition game played in integer lattice

$$\mathbb {Z}^n$$

. In a degree

$$k$$

case both players have

$$k$$

vectors and in each turn the vector chosen by a player is added to the current configuration vector of the game. One of the players, called Attacker, tries to play the game from the initial configuration to the origin while the other player, Defender, tries to avoid origin. The decision problem is to decide whether or not Attacker has a winning strategy. We prove that the problem is decidable in

polynomial time

for the degree two games in any dimension

$$n$$

.

Motivated by the success of bounded model checking framework for finite state machines, Ouaknine and Worrell proposed a time-bounded theory of real-time verification by claiming that restriction to bounded-time recovers decidability for several key decision problem related to real-time verification. In support of this theory, the list of undecidable problems recently shown decidable under time-bounded restriction is rather impressive: language inclusion for timed automata, emptiness problem for alternating timed automata, and emptiness problem for rectangular hybrid automata. The objective of our study was to recover decidability for general recursive timed automata(RTA)—and perhaps for recursive hybrid automata—under time-bounded restriction in order to provide an appealing verification framework for powerful modeling environments such as Stateflow/Simulink. Unfortunately, however, we answer this question in negative by showing that time-bounded reachability problem stays undecidable for RTA with 5 clocks.

Automata networks have been successfully used as abstract modeling schemes in many different fields. This paper deals with the observability of automata networks, which describes the ability to uniquely infer the network’s initial configuration by measuring its output sequence. Simple necessary and sufficient conditions for observability are given. The results employ techniques from symbolic computation and can be easily implemented within the computer algebra environments. Two examples are worked out to illustrate the application of the results.

We present a new proof procedure for reasoning on schemas of formulas defined over various (decidable) base logics (e.g. propositional logic, Presburger arithmetic etc.). Such schemas are useful to model sequences of formulas defined by induction on some parameter. The approach works by computing an automaton accepting exactly the values of the parameter for which the formula is satisfiable. Its main advantage is that it is completely modular, in the sense that external tools are used as “black boxes” both to reason on base formulas and to detect cycles in the proof search. This makes the approach more efficient and scalable than previous attempts. Experimental results are presented, showing evidence of the practical interest of the proposed method.

There is a rich variety of shuffling operations ranging from asynchronous interleaving to various forms of synchronizations. We introduce a general shuffling operation which subsumes earlier forms of shuffling. We further extend the notion of a Brzozowski derivative to the general shuffling operation and thus to many earlier forms of shuffling. This extension enables the direct construction of automata from regular expressions involving shuffles that appear in specifications of concurrent systems.

We extend Brzozowski derivatives and partial derivatives from regular expressions to

$$\omega $$

-regular expressions and establish their basic properties. We observe that the existing derivative-based automaton constructions do not scale to

$$\omega $$

-regular expressions. We define a new variant of the partial derivative that operates on linear factors and prove that this variant gives rise to a translation from

$$\omega $$

-regular expressions to nondeterministic Büchi automata.

The quotient operation, which is dual to the composition, is crucial in specification theories as it allows the synthesis of missing specifications and thus enables incremental design. In this paper, we consider a specification theory based on marked acceptance specifications (MAS) which are automata enriched with variability information encoded by acceptance sets and with reachability constraints on states. We define a sound and complete quotient for MAS hence ensuring reachability properties by construction.

A two-dimensional code is defined as a set

$$X\subseteq \Sigma ^{**}$$

such that any picture over

$$\Sigma $$

is tilable in at most one way with pictures in

$$X$$

. It is in general undecidable whether a set

$$X$$

of pictures is a code also in the finite case. Very recently in [

3

] strong prefix picture codes were defined as a decidable subclass that generalizes prefix string codes. Here a characterization for strong prefix codes that results in an effective procedure to construct them is presented. As a consequence there are also proved interesting results on the measure of strong prefix codes and a connection with the family of string prefix codes.

This paper addresses the torsion problem for a class of automaton semigroups, defined as semigroups of transformations induced by Mealy automata, aka letter-by-letter transducers with the same input and output alphabet. The torsion problem is undecidable for automaton semigroups in general, but is known to be solvable within the well-studied class of (semi)groups generated by invertible bounded Mealy automata. We focus on the somehow antipodal class of invertible reversible Mealy automata and prove that for a wide subclass the generated semigroup is torsion-free.

Surface laminations are classic closed sets of disjoint curves in surfaces. We give here a full description of how to obtain codings of such laminations when they are non-orientable by using lamination languages, i.e. specific linear complexity languages of two-way infinite words. We also compare lamination languages with symbolic laminations, i.e. the coding counterparts of algebraic laminations.

We investigate the length

$$\ell (n,k)$$

of a shortest preset distinguishing sequence (PDS) in the worst case for a

$$k$$

-element subset of an

$$n$$

-state Mealy automaton. It was mentioned by Sokolovskii [

18

] that this problem is closely related to the problem of finding the maximal subsemigroup diameter

$$\ell (\mathbf {T}_n)$$

for the full transformation semigroup

$$\mathbf {T}_n$$

of an

$$n$$

-element set. We prove that

$$\ell (\mathbf {T}_n)=2^n\exp \{\sqrt{\frac{n}{2}\ln n}(1+ o(1))\}$$

as

$$n\rightarrow \infty $$

and, using approach of Sokolovskii, find the asymptotics of

$$\log _2 \ell (n,k)$$

as

$$n,k\rightarrow \infty $$

and

$$k/n\rightarrow a\in (0,1)$$

.

We present a hierarchical construction of 2D subshifts of finite type with a unique direction of non-expansiveness. Our construction combines various techniques that were developed in previous self-similar constructions of SFTs and cellular automata.

Given a word

$$w$$

and a Parikh vector

$$\mathcal {P}$$

, an abelian run of period

$$\mathcal {P}$$

in

$$w$$

is a maximal occurrence of a substring of

$$w$$

having abelian period

$$\mathcal {P}$$

. We give an algorithm that finds all the abelian runs of period

$$\mathcal {P}$$

in a word of length

$$n$$

in time

$$O(n\times |\mathcal {P}|)$$

and space

$$O(\sigma +|\mathcal {P}|)$$

.

A word is

quasiperiodic

(or

coverable

) if it can be covered by occurrences of another finite word, called its

quasiperiod

. This notion was previously studied in the domains of text algorithms and combinatorics of right infinite words. We extend several results to two dimensions. We also characterize all rectangular words that cover non-periodic two-dimensional infinite words. Then we focus on two-dimensional words with infinitely many quasiperiods. We show that such words have zero entropy. However, contrarily to the one-dimensional case, they may not be uniformly recurrent.

We will prove that the word

$$a^ib^ja^k$$

is periodicity forcing if

$$j \ge 3$$

and

$$i+k \ge 3$$

, where

$$i$$

and

$$k$$

are positive integers. Also we will give examples showing that both bounds are optimal.

There exist many constructions of infinite words over three-letter alphabet avoiding squares. However, the characterization of the lexicographically minimal square-free word is an open problem. Efficient construction of this word is not known. We show that the situation changes when some letters commute with each other. We give two characterizations (morphic and recursive) of the lexicographically minimal square-free word

$$\widetilde{\mathbf {v}}$$

in the case of a partially commutative alphabet

$$\Theta $$

of size three. We consider the only non-trivial relation of partial commutativity, for which

$$\widetilde{\mathbf {v}}$$

exists: there are two commuting letters, while the third one is blocking (does not commute at all). We also show that the

$$n$$

-th letter of

$$\widetilde{\mathbf {v}}$$

can be computed in time logarithmic with respect to

$$n$$

.

A partial word is a word which contains some holes known as

do not know

symbols and such places can be replaced by any letter from the underlying alphabet. We study the relation between language of primitive partial words with the conventional language classes viz. regular, linear and deterministic context-free in Chomsky hierarchy. We give proofs to show that the language of primitive partial words over an alphabet having at least two letters is not regular, not linear and not deterministic context free language. Also we give a 2DPDA automaton that recognizes the language of primitive partial words.

We give complexity bounds for various classes of functions computed by cost register automata.

Recently, Williams [STOC ’14] proved a separation between

$$\mathsf {NEXP}$$

and

$$\mathsf {ACC}\circ \mathsf {THR}$$

, where an

$$\mathsf {ACC}\circ \mathsf {THR}$$

circuit has a single layer of threshold gates at the bottom and an

$$\mathsf {ACC}$$

circuit at the top. Two main ideas of his strategy are a closure property of circuit class and an algorithm for counting satisfying assignments of circuits.

In this paper, we show that this general scheme based on these two ideas can be applied for a certain class of circuits with

multi layer

of threshold gates. The circuit class we give has the symmetric gate at the top and poly-log layers of threshold gates to which an extra condition on the

dependency

is imposed. Two gates in a circuit are dependent, if the output of the one is always greater than or equal to the other one. An independent gate set is a set of gates in which two arbitrary gates are

$$not$$

dependent. We show that, if the size of a maximum independent gate set of each layer of threshold gates is at most

$$n^{\gamma }$$

for sufficiently small

$$\gamma >0$$

, then two key ingredients needed to apply his strategy can be established. Namely, (i) we can efficiently find a circuit in our class being equivalent to the AND of two input circuits in our class, and (ii) we can construct a faster than brute-force algorithm for counting satisfying assignments for this class by introducing a partial order to represent the dependency of gates. As a result, we give super quasi-polynomial size lower bounds for our class against

$$\mathsf {NEXP}$$

.

We answer two open questions by (Gruber, Holzer, Kutrib, 2009) on the state-complexity of representing sub- or superword closures of context-free grammars (CFGs): (1) We prove a (tight) upper bound of

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

on the size of nondeterministic finite automata (NFAs) representing the subword closure of a CFG of size

$$n$$

. (2) We present a family of CFGs for which the minimal deterministic finite automata representing their subword closure matches the upper-bound of

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

following from (1). Furthermore, we prove that the inequivalence problem for NFAs representing sub- or superword-closed languages is only NP-complete as opposed to PSPACE-complete for general NFAs. Finally, we extend our results into an approximation method to attack inequivalence problems for CFGs.

We provide a characterisation for the size of proofs in tree-like Q-Resolution by a Prover-Delayer game, which is inspired by a similar characterisation for the proof size in classical tree-like Resolution [

10

]. This gives the first successful transfer of one of the lower bound techniques for classical proof systems to QBF proof systems. We confirm our technique with two previously known hard examples. In particular, we give a proof of the hardness of the formulas of Kleine Büning et al. [

20

] for tree-like Q-Resolution.

In this paper we present a method which can be used to investigate on the positivity of a number sequence defined by a recurrence relation having constant coefficients (in short, a

$$C$$

-recurrence).

Interval temporal logics provide a natural framework for temporal reasoning about interval structures over linearly ordered domains, where intervals are taken as the primitive ontological entities. Their computational behaviour and expressive power mainly depend on two parameters: the set of modalities they feature and the linear orders over which they are interpreted. In this paper, we consider all fragments of Halpern and Shoham’s interval temporal logic HS with a decidable satisfiability problem over the class of all dense linear orders, and we provide a complete classification of them in terms of their complexity and expressiveness by solving the last two open cases.

Recently the class

$$DelayFPT$$

has been introduced into parameterized complexity in order to capture the notion of efficiently solvable parameterized enumeration problems. In this paper we propose a framework for parameterized

ordered

enumeration and will show how to obtain

$$DelayFPT$$

enumeration algorithms in the context of graph modification problems. We study these problems considering two different orders of solutions, lexicographic and by size. We present generic algorithmic strategies: The first one is based on the well-known principle of self-reducibility in the context of lexicographic order. The second one shows that the existence of some neighborhood structure among the solutions implies the existence of a

$$DelayFPT$$

algorithm which outputs all solutions ordered non-decreasingly by their size.

We investigate the computational complexity of some problems related to preimages and ancestors of states of reaction systems. In particular, we prove that finding a minimum-cardinality preimage or ancestor, computing their size, or counting them are all intractable problems, with complexity ranging from

$$\mathbf{FP}^{\mathbf{NP}[\log n]}$$

to

$$\mathbf{FPSPACE}(\mathrm{poly})$$

.

We present an almost complete classification of the parameterized complexity of all operator fragments of the satisfiability problem in computation tree logic CTL. The investigated parameterization is the sum of temporal depth and structural pathwidth. The classification shows a dichotomy between W[1]-hard and fixed-parameter tractable fragments. The only real operator fragment which is confirmed to be in FPT is the fragment containing solely AX. Also we prove a generalization of Courcelle’s theorem to infinite signatures which will be used to proof the FPT-membership case.

Testing Automaton

(TA) is a new kind of

$$\omega $$

-automaton introduced by Hansen et al. [

6

] as an alternative to the standard Büchi Automata (BA) for the verification of stutter-invariant LTL properties. Geldenhuys and Hansen [

5

] shown later how to use TA in the automata-theoretic approach to LTL model checking. They propose a TA-based approach using a verification algorithm that requires two searches (two passes) and compare its performance against the BA approach.

This paper improves their work by proposing a transformation of TA into a normal form (STA) that only requires a single one-pass verification algorithm. The resulting automaton is called

Single-pass Testing Automaton

(STA). We have implemented the STA approach in Spot model checking library. We are thus able to compare it with the BA and TA approaches. These experiments show that STA compete well on our examples.

We study the orthogonal range searching problem on points that have a significant number of

geometric repetitions

, that is, subsets of points that are identical under translation. Such repetitions occur in scenarios such as image compression, GIS applications and in compactly representing sparse matrices and web graphs. Our contribution is twofold. First, we show how to compress geometric repetitions that may appear in standard range searching data structures (such as K-D trees, Quad trees, Range trees, R-trees, Priority R-trees, and K-D-B trees), and how to implement subsequent range queries on the compressed representation with only a constant factor overhead. Secondly, we present a compression scheme that efficiently identifies geometric repetitions in point sets, and produces a hierarchical clustering of the point sets, which combined with the first result leads to a compressed representation that supports range searching.

The Burrows-Wheeler Transform is a text permutation that has revolutionized the fields of pattern matching and text compression, bridging the gap existing between the two. In this paper we approach the BWT-construction problem generalizing a well-known algorithm—based on backward search and dynamic strings manipulation—to work in a context-wise fashion, using automata on words. Let

$$n$$

,

$$\sigma $$

, and

$$H_k$$

be the text length, the alphabet size, and the

$$k$$

-th order empirical entropy of the text, respectively. Moreover, let

$$H_k^*=\min \{H_k+1,\lceil \log \sigma \rceil \}$$

. Under the word RAM model with word size

$$w\in \Theta (\log n)$$

, our algorithm builds the BWT in average

$$\mathcal {O}(nH_k^*)$$

time using

$$nH_k^* + o(nH_k^*)$$

bits of space, where

$$k=\log _\sigma (n/\log ^2 n)-1$$

. We experimentally show that our algorithm has very good performances (essentially linear time) on DNA sequences, using about 2.6 bits per input symbol in RAM.

We present a new backward tree pattern matching algorithm for ordered trees. The algorithm finds all occurrences of a single given tree pattern which match an input tree. It makes use of linearisations of both the given pattern and the input tree. The algorithm preserves the properties and advantages of standard backward string pattern matching approaches. The number of symbol comparisons in the backward tree pattern matching can be sublinear in the size of the input tree. As in the case of backward string pattern matching, the size of the bad character shift table used by the algorithm is linear in the size of the alphabet. We compare the new algorithm with best performing previously existing algorithms based on (non-linearised) tree pattern matching using finite tree automata or stringpath matchers and show that it outperforms these for single pattern matching.

It was shown before that the NP-hard problem of deterministic finite automata (DFA) identification can be translated to Boolean satisfiability (SAT). Modern SAT-solvers can efficiently tackle hard DFA identification instances. We present a technique to reduce SAT search space by enforcing an enumeration of DFA states in breadth-first search (BFS) order. We propose symmetry breaking predicates, which can be added to Boolean formulae representing various DFA identification problems. We show how to apply this technique to DFA identification from both noiseless and noisy data. The main advantage of the proposed approach is that it allows to exactly determine the existence or non-existence of a solution of the noisy DFA identification problem.

Approaches based on the idea generically called distributional learning have been making great success in the algorithmic learning of context-free languages and their extensions. We in this paper show that conjunctive grammars are also learnable by a distributional learning technique. Conjunctive grammars are context-free grammars enhanced with conjunctive rules to extract the intersection of two languages. We also compare our result with the closely related work by Clark et al. (JMLR 2010) on contextual binary feature grammars (

cbfg

s). Our learner is stronger than theirs. In particular our learner learns every

exact

cbfg

, while theirs does not. Clark et al. emphasized the importance of exact

cbfg

s but they only conjectured there should be a learning algorithm for exact

cbfg

s. This paper shows that their conjecture is true.

We introduce the notion of

Hypergraph Weighted Model

(HWM) that generically associates a tensor network to a hypergraph and then computes a value by tensor contractions directed by its hyperedges. A series

$$r$$

defined on a hypergraph family is said to be recognizable if there exists a HWM that computes it. This model generalizes the notion of recognizable series on strings and trees. We present some properties of the model and study at which conditions finite support series are recognizable.

To check a system, some verification techniques consider a set of terms

$$I$$

that represents the initial configurations of the system, and a rewrite system

$$R$$

that represents the system behavior. To check that no undesirable configuration is reached, they compute an over-approximation of the set of descendants (successors) issued from

$$I$$

by

$$R$$

, expressed by a tree language. Their success highly depends on the quality of the approximation. Some techniques have been presented using regular tree languages, and more recently using non-regular languages to get better approximations: using context-free tree languages [

16

] on the one hand, using synchronized tree languages [

2

] on the other hand. In this paper, we merge these two approaches to get even better approximations: we compute an over-approximation of the descendants, using synchronized-context-free tree languages expressed by logic programs. We give several examples for which our procedure computes the descendants in an exact way, whereas the former techniques compute a strict over-approximation.

This paper studies properties of the back end of a sorting network and illustrates the utility of these in the search for networks of optimal size or depth. All previous works focus on properties of the front end of networks and on how to apply these to break symmetries in the search. The new properties help shed understanding on how sorting networks sort and speed-up solvers for both optimal size and depth by an order of magnitude.

Given two graphs

$$H_1$$

and

$$H_2$$

, a graph

$$G$$

is

$$(H_1,H_2)$$

-free if it contains no subgraph isomorphic to

$$H_1$$

or

$$H_2$$

. We continue a recent study into the clique-width of

$$(H_1,H_2)$$

-free graphs and present three new classes of

$$(H_1,H_2)$$

-free graphs that have bounded clique-width. We also show the implications of our results for the computational complexity of the

Colouring

problem restricted to

$$(H_1,H_2)$$

-free graphs. The three new graph classes have in common that one of their two forbidden induced subgraphs is the diamond (the graph obtained from a clique on four vertices by deleting one edge). To prove boundedness of their clique-width we develop a technique based on bounding clique covering number in combination with reduction to subclasses of perfect graphs.

Traces are equivalence classes of action sequences which can be represented by partial orders capturing the causality in the behaviour of a concurrent system. Generalised traces, on the other hand, are equivalence classes of step sequences. They are represented by order structures that can describe non-simultaneity and weak causality, phenomena which cannot be expressed by partial orders alone. In this paper, we provide a systematic classification of different subclasses of generalised traces in terms of the order structures representing them. We also show how the original trace model fits into the overall framework.

Picture languages have been intensively investigated by several research groups. In this paper, we define weighted two-dimensional on-line tessellation automata (W2OTA) taking weights from a new weight structure called picture valuation monoid. The behavior of this automaton model is a picture series mapping pictures over an alphabet to a picture valuation monoid. As one of our main results, we prove a Nivat theorem for W2OTA. It shows that recognizable picture series can be obtained precisely as projections of particularly simple unambiguously recognizable series restricted to unambiguous recognizable picture languages. In addition, we introduce a weighted MSO logic which can model average density of pictures. As the other main result of this paper, we show that W2OTA and a suitable fragment of our weighted MSO logics are expressively equivalent.

We consider rational relations made of pairs

$$(u,v)$$

of finite words such that

$$v$$

is a subword of

$$u$$

. We show that such a selecting relation can be realized by a transducer such that the output label of each transition is a subword of its input label. We also show that it is decidable whether a given relation has this property.

We mainly investigate the power of weight-reducing string-rewriting systems in the context of transducing observer systems. First we relate them to a special type of restarting transducer. Then we situate them between painter and length-reducing systems. Further we show that for every weight-reducing system there is an equivalent one that uses only weight-reducing painter rules. This result enables us to prove that the class of relations that is computed by transducing observer systems with weight-reducing rules is closed under intersection.

We present an efficient algorithm for testing approximate

dtd

validity modulo the strong tree edit distance. Our algorithm inspects

xml

documents in a probabilistic manner. It detects with high probability the nonvalidity of

xml

documents with a large fraction of errors, measured in terms of the strong tree edit distance from the

dtd

. The run time depends polynomially on the depth of the

xml

document tree but not on its size, so that it is sublinear in most cases (because in practice XML documents tend to be shallow). Therefore, our algorithm can be used to speed up exact

dtd

validators that run in linear time.