Narrow Results

We introduce a certain restriction of weighted automata over the rationals, called image-binary automata. We show that such automata accept the regular languages, can be exponentially more succinct than corresponding NFAs, and allow for polynomial complementation, union, and intersection. This compares favourably with unambiguous automata whose complementation requires a superpolynomial state blowup. We also study an infinite-word version, image-binary Büchi automata. We show that such automata are amenable to probabilistic model checking, similarly to unambiguous Büchi automata. We provide algorithms to translate $k$-ambiguous Büchi automata to image-binary Büchi automata, leading to model-checking algorithms with optimal computational complexity.

This paper presents a novel application of automata algorithms to machine learning. It introduces the first optimization solution for support vector machines used with sequence kernels that is purely based on weighted automata and transducer algorithms, without requiring any specific solver. The algorithms presented apply to a family of kernels covering all those commonly used in text and speech processing or computational biology. We show that these algorithms have significantly better computational complexity than previous ones and report the results of large-scale experiments demonstrating a dramatic reduction of the training time, typically by several orders of magnitude.

Quantitative aspects of systems like consumption of resources, output of goods, or reliability can be modeled by weighted automata. Recently, objectives like the average cost or the longtime peak power consumption of a system have been modeled by weighted automata which are not semiring weighted anymore. Instead, operations like limit superior, limit average, or discounting are used to determine the behavior of these automata. Here, we introduce a new class of weight structures subsuming a range of these models as well as semirings. Our main result shows that such weighted automata and Kleene-type regular expressions are expressively equivalent both for finite and infinite words.

The evolution from non-deterministic to weighted automata represents a shift from qualitative to quantitative methods in computer science. The trend calls for a language able to reconcile quantitative reasoning with formal logic and set theory, which have for so many years supported qualitative reasoning. Such a lingua franca should be typed, polymorphic, diagrammatic, calculational and easy to blend with conventional notation.

This paper puts forward typed linear algebra as a candidate notation for such a unifying role. This notation, which emerges from regarding matrices as morphisms of suitable categories, is put at work in describing weighted automata as coalgebras in such categories.

Some attention is paid to the interface between the index-free (categorial) language of matrix algebra and the corresponding index-wise, set-theoretic notation.

Nested words have been introduced by Alur and Madhusudan as a model for e.g. recursive programs or XML documents and have received much recent interest. In this paper, we investigate a quantitative automaton model and a quantitative logic for nested words. The behavior resp. the semantics map nested words to weights which are taken from a strong bimonoid. Strong bimonoids can be viewed as semirings without requiring the distributivity assumption which was essential in the classical theory of formal power series; strong bimonoids include e.g. all bounded lattices and many other structures from multi-valued logics. Our main results show that weighted nested word automata and suitable weighted MSO logics are expressively equivalent. This extends the classical Büchi-Elgot result from words to a weighted setting for nested words.

This paper deals with one-way and two-way weighted automata. When the semiring of weights is commutative, we prove that unambiguous one-way automata, unambiguous two-way automata and deterministic two-way automata realize the same (rational) power series. If the semiring of weights is not commutative, unambiguous one-way automata and deterministic two-way automata realize the same rational power series, but unambiguous two-way automata may realize non rational power series.

Let $S$ be a complete star-omega semiring and $\mathrm{\Sigma }$ be an alphabet. For a weighted $\omega$-pushdown automaton ${𝒫}$ with stateset $\{1,\dots ,n\}$, $n\ge 1$, we show that there exists a mixed algebraic system over a complete semiring-semimodule pair $({(S〈〈{\mathrm{\Sigma }}^{\ast }〉〉)}^{n\times n},{(S〈〈{\mathrm{\Sigma }}^{\omega }〉〉)}^n)$ such that the behavior $\parallel {𝒫}\parallel$ of ${𝒫}$ is a component of a solution of this system. In case the basic semiring is $𝔹$ or ${\mathbb{N}}^{\infty }$ we show that there exists a mixed context-free grammar that generates $\parallel {𝒫}\parallel$. The construction of the mixed context-free grammar from ${𝒫}$ is a generalization of the well known triple construction and is called now triple-pair construction for $\omega$-pushdown automata.

In this paper we combine two classical generalisations of finite automata (weighted automata and automata on infinite words) into a model of integer weighted automata on infinite words and study the universality and the emptiness problems under zero weight acceptance. We show that the universality problem is undecidable for three-state automata by a direct reduction from the infinite Post correspondence problem. We also consider other more general acceptance conditions as well as their complements with respect to the universality and the emptiness problems. Additionally, we build a universal integer weighted automaton with fixed transitions. This automaton has an additional integer input that allows it to simulate any semi-Thue system.

Weighted tree automata (WTA) extend classical weighted automata (WA) to the non-linear structure of trees. The expressive power of WA with varying degrees of ambiguity has been extensively studied. Unambiguous, finitely ambiguous, and polynomially ambiguous WA over the tropical (as well as the arctic) semiring strictly increase in expressive power. The recently developed pumping results of Mazowiecki and Riveros (STACS 2018) are lifted to trees in order to achieve the same strict hierarchy for WTA over the tropical (as well as the arctic) semiring.

We introduce a weighted linear dynamic logic (weighted LDL for short) and show the expressive equivalence of its formulas to weighted rational expressions. This adds a new characterization for recognizable series to the fundamental Schützenberger theorem. Surprisingly, the equivalence does not require any restriction to our weighted LDL. Our results hold over arbitrary (resp. totally complete) semirings for finite (resp. infinite) words. As a consequence, the equivalence problem for weighted LDL formulas over fields is decidable in doubly exponential time. In contrast to classical logics, we show that our weighted LDL is expressively incomparable to weighted LTL for finite words. We determine a fragment of the weighted LTL such that series over finite and infinite words definable by LTL formulas in this fragment are definable also by weighted LDL formulas. This is an extended version of [17].

We investigate Büchi automata with weights for the transitions. Assuming that the weights are taken in a suitable ordered semiring, we show how to define the behaviors of these automata on infinite words. Our main result shows that the formal power series arising in this way are precisely the ones which can be constructed using ω-rational operations. This extends the classical Kleene–Schützenberger result for weighted finite automata to the case of infinite words and generalizes Büchi's theorem on languages of infinite words. We also derive versions of our main result for non-complete semirings and for other automata models.

This paper addresses the problem of the validity of weighted automata in which the presence of ε-circuits results in infinite summations. Earlier works either rule out such automata or characterize the semirings in which these infinite sums are all well-defined.

By means of a topological approach, we take here a definition of validity that is strong enough to insure that in any kind of semirings, any closure algorithm will succeed on every valid weighted automaton and turn it into an equivalent proper automaton. This definition is stable with respect to natural transformations of automata.

The classical closure algorithms, in particular algorithms based on the computation of the star of the matrix of ε-transitions, cannot be used to decide validity. This decision problem remains open for general topological semirings.

We present a closure algorithm that yields a decision procedure for the validity of automata in the case where the weights are taken in ℚ or ℝ, two cases that had never been treated before. These algorithm and procedure are implemented in the VAUCANSON platform.