Recently there has been a significant effort to handle quantitative properties in formal verification and synthesis. While weighted automata over finite and infinite words provide a natural and flexible framework to express quantitative properties, perhaps surprisingly, some basic system properties such as average response time cannot be expressed using weighted automata, nor in any other know decidable formalism. In this work, we introduce nested weighted automata as a natural extension of weighted automata which makes it possible to express important quantitative properties such as average response time. In nested weighted automata, a master automaton spins off and collects results from weighted slave automata, each of which computes a quantity along a finite portion of an infinite word. Nested weighted automata can be viewed as the quantitative analogue of monitor automata, which are used in run-time verification. We establish an almost complete decidability picture for the basic decision problems about nested weighted automata, and illustrate their applicability in several domains. In particular, nested weighted automata can be used to decide average response time properties.
Weighted counterpart of Boolean nested automata. Weighted nested automata have been considered in @cite_3 in the context of finite words, where the weights are given over semirings. It is further required that the semirings of all master and slave automata coincide, while in our case, the value functions may differ. Since the semirings of master and slave automata must coincide for @cite_3 , it can be interpreted as defining weighted counterpart of Boolean nested automata over finite words. Adding nesting structure to words and trees have been extensively studied for non-weighted automata in @cite_12 @cite_4 and also applied to software model checking @cite_24 . The work of @cite_3 defines a weighted counterpart of nesting of finite words, whereas we consider nesting of various weighted automata to express properties of infinite behaviors of systems. Properties such as long-run average response time cannot be expressed in the framework of @cite_3 .
@cite_24 @cite_4 @cite_12 @cite_3
2075969214 2131886132 2135909702 2096531026
We propose the model of nested words for representation of data with both a linear ordering and a hierarchically nested matching of items. Examples of data with such dual linear-hierarchical structure include executions of structured programs, annotated linguistic data, and HTML XML documents. Nested words generalize both words and ordered trees, and allow both word and tree operations. We define nested word automata—finite-state acceptors for nested words, and show that the resulting class of regular languages of nested words has all the appealing theoretical properties that the classical regular word languages enjoys: deterministic nested word automata are as expressive as their nondeterministic counterparts; the class is closed under union, intersection, complementation, concatenation, Kleene-*, prefixes, and language homomorphisms; membership, emptiness, language inclusion, and language equivalence are all decidable; and definability in monadic second order logic corresponds exactly to finite-state recognizability. We also consider regular languages of infinite nested words and show that the closure properties, MSO-characterization, and decidability of decision problems carry over. The linear encodings of nested words give the class of visibly pushdown languages of words, and this class lies between balanced languages and deterministic context-free languages. We argue that for algorithmic verification of structured programs, instead of viewing the program as a context-free language over words, one should view it as a regular language of nested words (or equivalently, a visibly pushdown language), and this would allow model checking of many properties (such as stack inspection, pre-post conditions) that are not expressible in existing specification logics. We also study the relationship between ordered trees and nested words, and the corresponding automata: while the analysis complexity of nested word automata is the same as that of classical tree automata, they combine both bottom-up and top-down traversals, and enjoy expressiveness and succinctness benefits over tree automata. We introduce a weighted logic with discounting and we establish the Buchi-Elgot theorem for weighted automata over finite words and arbitrary commutative semirings. Then we investigate Buchi and Muller automata with discounting over the max-plus and the min-plus semiring. We show their expressive equivalence with weighted MSO-sentences with discounting. In this case our logic has a purely syntactic definition. For the finite case, we obtain a purely syntactically defined weighted logic if the underlying semiring is additively locally finite. We study languages of nested trees—structures obtained by augmenting trees with sets of nested jump-edges. These graphs can naturally model branching behaviors of pushdown programs, so that the problem of branching-time software model checking may be phrased as a membership question for such languages. We define finite-state automata accepting such languages—these automata can pass states along jump-edges as well as tree edges. We find that the model-checking problem for these automata on pushdown systems is EXPTIME-complete, and that their alternating versions are expressively equivalent to NT-μ, a recently proposed temporal logic for nested trees that can express a variety of branching-time, “context-free” requirements. We also show that monadic second order logic (MSO) cannot exploit the structure: MSO on nested trees is too strong in the sense that it has an undecidable model checking problem, and seems too weak to capture NT-μ. We introduce new classes of weighted automata on words. Equipped with pebbles and a two-way mechanism, they go beyond the class of recognizable formal power series, but capture a weighted version of first-order logic with bounded transitive closure. In contrast to previous work, this logic allows for unrestricted use of universal quantification. Our main result states that pebble weighted automata, nested weighted automata, and this weighted logic are expressively equivalent. We also give new logical characterizations of the recognizable series. While model checking of pushdown systems is by now an established technique in software verification, temporal logics and automata traditionally used in this area are unattractive on two counts. First, logics and automata traditionally used in model checking cannot express requirements such as pre post-conditions that are basic to analysis of software. Second, unlike in the finite-state world, where the μ-calculus has a symbolic model-checking algorithm and serves as an “assembly language” to which temporal logics can be compiled, there is no common formalism—either fixpoint-based or automata-theoretic—to model-check requirements on pushdown models. In this article, we introduce a new theory of temporal logics and automata that addresses the above issues, and provides a unified foundation for the verification of pushdown systems. The key idea here is to view a program as a generator of structures known as nested trees as opposed to trees. A fixpoint logic (called N T -μ) and a class of automata (called nested tree automata) interpreted on languages of these structures are now defined, and branching-time model-checking is phrased as language inclusion and membership problems for these languages. We show that N T -μ and nested tree automata allow the specification of a new frontier of requirements usable in software verification. At the same time, their model checking problem has the same worst-case complexity as their traditional analogs, and can be solved symbolically using a fixpoint computation that generalizes, and includes as a special case, “summary”-based computations traditionally used in interprocedural program analysis. We also show that our logics and automata define a robust class of languages—in particular, just as the μ-calculus is equivalent to alternating parity automata on trees, NT-μ is equivalent to alternating parity automata on nested trees. Weighted finite automata are classical nondeterministic finite automata in which the transitions carry weights. These weights may model, for example, the cost involved when executing a transition, the resources or time needed for this, or the probability or reliability of its successful execution. Weights can also be added to classical automata with infinite state sets like pushdown automata, and this extension constitutes the general concept of weighted automata. Since their introduction in the 1960s they have stimulated research in related areas of theoretical computer science, including formal language theory, algebra, logic, and discrete structures. Moreover, weighted automata and weighted context-free grammars have found application in natural-language processing, speech recognition, and digital image compression. This book covers all the main aspects of weighted automata and formal power series methods, ranging from theory to applications. The contributors are the leading experts in their respective areas, and each chapter presents a detailed survey of the state of the art and pointers to future research. The chapters in Part I cover the foundations of the theory of weighted automata, specifically addressing semirings, power series, and fixed point theory. Part II investigates different concepts of weighted recognizability. Part III examines alternative types of weighted automata and various discrete structures other than words. Finally, Part IV deals with applications of weighted automata, including digital image compression, fuzzy languages, model checking, and natural-language processing. Computer scientists and mathematicians will find this book an excellent survey and reference volume, and it will also be a valuable resource for students exploring this exciting research area. In the classic problem of sequence prediction, a predictor receives a sequence of values from an emitter and tries to guess the next value before it appears. The predictor masters the emitter if there is a point after which all of the predictor’s guesses are correct. In this paper we consider the case in which the predictor is an automaton and the emitted values are drawn from a finite set; i.e., the emitted sequence is an infinite word. We examine the predictive capabilities of finite automata, pushdown automata, stack automata (a generalization of pushdown automata), and multihead finite automata. We relate our predicting automata to purely periodic words, ultimately periodic words, and multilinear words, describing novel prediction algorithms for mastering these sequences. Weighted automata map input words to numerical values. Applications of weighted automata include formal verification of quantitative properties, as well as text, speech, and image processing. In the 90's, Krob studied the decidability of problems on rational series, which strongly relate to weighted automata. In particular, it follows from Krob's results that the universality problem (that is, deciding whether the values of all words are below some threshold) is decidable for weighted automata with weights in N ∪ ∞ , and that the equality problem is undecidable when the weights are in N ∪ ∞ . In this paper we continue the study of the borders of decidability in weighted automata, describe alternative and direct proofs of the above results, and tighten them further. Unlike the proofs of Krob, which are algebraic in their nature, our proofs stay in the terrain of state machines, and the reduction is from the halting problem of a two-counter machine. This enables us to significantly simplify Krob's reasoning and strengthen the results to apply already to a very simple class of automata: all the states are accepting, there are no initial nor final weights, and all the weights are from the set -1, 0, 1 . The fact we work directly with automata enables us to tighten also the decidability results and to show that the universality problem for weighted automata with weights in N ∪ ∞ , and in fact even with weights in Q≥0 ∪ ∞ , is PSPACE-complete. Our results thus draw a sharper picture about the decidability of decision problems for weighted automata, in both the front of equality vs. universality and the front of the N ∪ ∞ vs. the Z ∪ ∞ domains. Weighted automata and transducers are widely used in modern applications in bioinformatics and text, speech, and image processing. This chapter describes several fundamental weighted automata and shortest-distance algorithms including composition, determinization, minimization, and synchronization, as well as single-source and all-pairs shortest distance algorithms over general semirings. It presents the pseudocode of these algorithms, gives an analysis of their running time complexity, and illustrates their use in some simple cases. Many other complex weighted automata and transducer algorithms used in practice can be obtained by combining these core algorithms. Inspired by distributed algorithms, we introduce a new class of finite graph automata that recognize precisely the graph languages definable in monadic second-order logic. For the cases of words and trees, it has been long known that the regular languages are precisely those definable in monadic second-order logic. In this regard, the automata proposed in the present work can be seen, to some extent, as a generalization of finite automata to graphs. Furthermore, we show that, unlike for finite automata on words and trees, the deterministic, nondeterministic and alternating variants of our automata form a strict hierarchy with respect to their expressive power. For the weaker variants, the emptiness problem is decidable. Alur, R. and D.L. Dill, A theory of timed automata, Theoretical Computer Science 126 (1994) 183-235. We propose timed (j&e) automata to model the behavior of real-time systems over time. Our definition provides a simple, and yet powerful, way to annotate state-transition graphs with timing constraints using finitely many real-valued clocks. A timed automaton accepts timed words-infinite sequences in which a real-valued time of occurrence is associated with each symbol. We study timed automata from the perspective of formal language theory: we consider closure properties, decision problems, and subclasses. We consider both nondeterministic and deterministic transition structures, and both Biichi and Muller acceptance conditions. We show that nondeterministic timed automata are closed under union and intersection, but not under complementation, whereas deterministic timed Muller automata are closed under all Boolean operations. The main construction of the paper is an (PSPACE) algorithm for checking the emptiness of the language of a (nondeterministic) timed automaton. We also prove that the universality problem and the language inclusion problem are solvable only for the deterministic automata: both problems are undecidable (II i-hard) in the nondeterministic case and PSPACE-complete in the deterministic case. Finally, we discuss the application of this theory to automatic verification of real-time requirements of finite-state systems. We introduce two natural variants of prefix rewriting on nested-words. One captures precisely the transition graphs of order-2 pushdown automata and the other precisely those of order-2 collapsible pushdown automata (2-CPDA). To our knowledge this is the first precise ‘external' characterisation of 2-CPDA graphs and demonstrates that the class is robust and hence interesting in its own right. The comparison with our characterisation for 2-PDA graphs also gives an idea of what ‘collapse means' in terms outside of higher-order automata theory. Additionally, a related construction gives us a decidability result for first-order logic on a natural subclass of 3-CPDA graphs, which in some sense is optimal. Weighted automata are a generalisation of non-deterministic automata where each transition, in addition to an input letter, has also a quantity expressing the weight (e.g. cost or probability) of its execution. As for non-deterministic automata, their behaviours can be expressed in terms of either (weighted) bisimilarity or (weighted) language equivalence. Coalgebras provide a categorical framework for the uniform study of state-based systems and their behaviours. In this work, we show that coalgebras can suitably model weighted automata in two different ways: coalgebras on Set (the category of sets and functions) characterise weighted bisimilarity, while coalgebras on Vect (the category of vector spaces and linear maps) characterise weighted language equivalence. Relying on the second characterisation, we show three different procedures for computing weighted language equivalence. The first one consists in a generalisation of the usual partition refinement algorithm for ordinary automata. The second one is the backward version of the first one. The third procedure relies on a syntactic representation of rational weighted languages. We characterize the infinite words determined by one-way stack automata. An infinite language L determines an infinite word alpha if every string in L is a prefix of alpha. If L is regular or context-free, it is known that alpha must be ultimately periodic. We extend this result to the class of languages recognized by one-way nondeterministic checking stack automata (1-NCSA). We then consider stronger classes of stack automata and show that they determine a class of infinite words which we call multilinear. We show that every multilinear word can be written in a form which is amenable to parsing. Finally, we consider the class of one-way multihead deterministic finite automata (1:multi-DFA). We show that every multilinear word can be determined by some 1:multi-DFA, but that there exist infinite words determined by 1:multi-DFA which are not multilinear. We investigate extensions of temporal logic by finite automata on infinite words. There are three different types of acceptance conditions (finite, looping and repeating) that one can give for these finite automata. This gives rise to three different logics. It turns out, however. that these logics have the same expressive power but differ in the complexity of their decision problem. We also investigate the addition of alternation and show that it does not increase the complexity of the decision problem. We introduce the notion of regular cost functions: a quantitative extension to the standard theory of regular languages. We provide equivalent characterisations of this notion by means of automata (extending the nested distance desert automata of Kirsten), of history-deterministic automata (history-determinism is a weakening of the standard notion of determinism, that replaces it in this context), and a suitable notion of recognisability by stabilisation monoids. We also provide closure and decidability results. Abstract Documents in computer-readable form can be used to provide information about other documents, i.e. those they cite. To do this efficiently requires procedures for computer recognition of citing statements. This is not easy, especially for multi-sentence citing statements. Computer recognition procedures have been developed which are accurate to the following extent: 73 of the words in statements selected by computer procedures as being citing statements are words which are correctly attributable to the corresponding documents. The retrieval effectiveness of computer-recognized citing statements was tested in the following way. First, for eight retrieval requests in inorganiic chemistry, average recall by search of Chemical Abstracts Service indexing and Chemical Abstracts abstract text words was found to be 50 . Words from citing statements referring to the papers to be retrieved were then added to the index terms and abstract words as additional access points, and searching was repeated. Average recall increased to 70 . Only words from citing statements published within a year of the cited papers were used. The retrieval effect of citing statement words alone (published within a year) without index or abstract terms was the following: average recall was 40 . When just the words of the titles of the cited papers were added to those citing statement words, average recall increased to 50 . We study bisimulation and minimization for weighted automata, relying on a geometrical representation of the model, linear weighted automata ( lwa ). In a lwa , the state-space of the automaton is represented by a vector space, and the transitions and weighting maps by linear morphisms over this vector space. Weighted bisimulations are represented by sub-spaces that are invariant under the transition morphisms. We show that the largest bisimulation coincides with weighted language equivalence, can be computed by a geometrical version of partition refinement and that the corresponding quotient gives rise to the minimal weighted-language equivalence automaton. Relations to Larsen and Skou's probabilistic bisimulation and to classical results in Automata Theory are also discussed. We describe an automata-theoretic approach for the competitive analysis of online algorithms. Our approach is based on weighted automata, which assign to each input word a cost in R≥0. By relating the "unbounded look ahead" of optimal offline algorithms with nondeterminism, and relating the "no look ahead" of online algorithms with determinism, we are able to solve problems about the competitive ratio of online algorithms, and the memory they require, by reducing them to questions about determinization and approximated determinization of weighted automata. Motivated by formal models recently proposed in the context of XML, we study automata and logics on strings over infinite alphabets. These are conservative extensions of classical automata and logics defining the regular languages on finite alphabets. Specifically, we consider register and pebble automata, and extensions of first-order logic and monadic second-order logic. For each type of automaton we consider one-way and two-way variants, as well as deterministic, nondeterministic, and alternating control. We investigate the expressiveness and complexity of the automata and their connection to the logics, as well as standard decision problems. Some of our results answer open questions of Kaminski and Francez on register automata.