Bidirectional Nested Weighted Automata
Krishnendu Chatterjee, Thomas A. Henzinger, Jan Otop

TL;DR
This paper introduces bidirectional nested weighted automata (NWA), expanding their expressive power by allowing input processing in both directions, while maintaining similar computational complexity for key decision problems.
Contribution
The paper presents a novel bidirectional NWA framework, demonstrating increased expressiveness without added complexity for emptiness and universality problems.
Findings
Bidirectional NWA can express properties not possible with forward-only NWA.
Decidability and complexity results for emptiness and universality are preserved in the bidirectional setting.
Bidirectionality does not increase computational complexity for these decision problems.
Abstract
Nested weighted automata (NWA) present a robust and convenient automata-theoretic formalism for quantitative specifications. Previous works have considered NWA that processed input words only in the forward direction. It is natural to allow the automata to process input words backwards as well, for example, to measure the maximal or average time between a response and the preceding request. We therefore introduce and study bidirectional NWA that can process input words in both directions. First, we show that bidirectional NWA can express interesting quantitative properties that are not expressible by forward-only NWA. Second, for the fundamental decision problems of emptiness and universality, we establish decidability and complexity results for the new framework which match the best-known results for the special case of forward-only NWA. Thus, for NWA, the increased expressiveness of…
| Value | Restrictions | Complexity | Complexity |
| func. | Bidirectional | Forward case | |
| Min,Max, | None | PSpace-complete | PSpace-complete [13] |
| (Thm 6) | |||
| finite | PSpace-hard | PSpace-hard | |
| width | ExpSpace | ExpSpace [13] | |
| (Thm 11) | |||
| , | constant width | NLogSpace-complete | NLogSpace-complete |
| Sum | unary weights | (Thm 17) | [14] |
| , | constant width | PTime | PTime [14] |
| Sum | binary weights | (Thm 17) | |
| , | width given | PSpace-complete | PSpace-complete [14] |
| Sum | in unary | (Thm 17) |
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Bidirectional Nested Weighted Automata
Krishnendu Chatterjee
IST Austria
{krish.chat,tah}@ist.ac.at
Thomas A. Henzinger
IST Austria
{krish.chat,tah}@ist.ac.at
Jan Otop
University of Wrocław
Abstract
Nested weighted automata (NWA) present a robust and convenient automata-theoretic formalism for quantitative specifications. Previous works have considered NWA that processed input words only in the forward direction. It is natural to allow the automata to process input words backwards as well, for example, to measure the maximal or average time between a response and the preceding request. We therefore introduce and study bidirectional NWA that can process input words in both directions. First, we show that bidirectional NWA can express interesting quantitative properties that are not expressible by forward-only NWA. Second, for the fundamental decision problems of emptiness and universality, we establish decidability and complexity results for the new framework which match the best-known results for the special case of forward-only NWA. Thus, for NWA, the increased expressiveness of bidirectionality is achieved at no additional computational complexity. This is in stark contrast to the unweighted case, where bidirectional finite automata are no more expressive but exponentially more succinct than their forward-only counterparts.
1 Introduction
We study an extension of nested weighted automata (NWA) [13] that can process words in both directions. We show that this new and natural framework can express many interesting quantitative properties that the previous formalism could not. We establish decidability and complexity results of the basic decision problems for the new framework. We start with the motivation for quantitative properties, then describe NWA and our new framework, and finally the contributions.
Weighted automata. Automata-theoretic formalisms provide a natural way to express quantitative properties of systems. Weighted automata extend finite automata where every transition is assigned an integer number called weight. Thus a run of an automaton gives rise to a sequence of weights. A value function aggregates the sequence of weights into a single value. For non-deterministic weighted automata, the value of a word is the infimum value of all runs over . First, weighted automata were studied over finite words with weights from a semiring, and ring multiplication as value function [18], and later extended to infinite words with limit averaging or supremum as value function [12, 11, 10]. While weighted automata over semirings can express several quantitative properties [21], they cannot express long-run average properties that weighted automata with limit averaging can [12]. However, even weighted automata with limit averaging cannot express some basic quantitative properties (see [13]).
Nested weighted automata. A natural extension of weighted automata is to add nesting, which leads to nested weighted automata (NWA) [13]. A nested weighted automaton consists of a master automaton and a set of slave automata. The master automaton runs over input infinite words. At every transition the master can invoke a slave automaton that runs over a finite subword of the infinite word, starting at the position where the slave automaton is invoked. Each slave automaton terminates after a finite number of steps and returns a value to the master automaton. Each slave automaton is equipped with a value function for finite words, and the master automaton aggregates the returned values from slave automata using a value function for infinite words.
Advantages of NWA. We discuss the various advantages of NWA.
For Boolean finite automata, nested automata are equivalent to the non-nested counterpart, whereas NWA are strictly more expressive than non-nested weighted automata [13, Example 5]. It has been shown in [13] that NWA provide a specification framework where many basic quantitative properties can be expressed, which cannot be expressed by weighted automata. 2. 2.
NWA provide a natural and convenient way to express quantitative properties. Every slave automaton computes a subproperty, which is then combined using the master automaton. Thus NWA allow to decompose properties conveniently, and provide a natural framework to study quantitative run-time verification. 3. 3.
Finally, subclasses of NWA are equivalent in expressive power with automata with monitor counters [16], and thus they provide a robust framework to express quantitative properties.
Bidirectional NWA. Previous works considered slave automata that can only process input words in the forward direction (forward-only NWA). However, to specify quantitative properties, it is natural to allow slave automata to run backwards, for example, to measure the maximal or average time between a response and the preceding request. In this work we consider this natural extension of NWA, namely bidirectional NWA, where slave automata can process words in the forward as well as the backward direction.
Natural properties. First, we show that many natural properties can be expressed in the bidirectional NWA framework. We present two examples below (details in Section 3).
Average energy level. Consider a quantitative setting where each weight represents energy gain or consumption, and thus the sum of weights represents the energy level. To express the average energy level property, the master automaton has long-run average as the value function, and at every transition it invokes a slave automaton that walks backward with sum value function for the weights. Thus the average energy level property is naturally expressed by NWA with backward-walking slave automata, while this property is not expressible by NWA with forward-walking slave automata. 2. 2.
Data-consistency property (DCP). Consider the data-consistency property (DCP) where the input letters correspond to reads, writes, null instructions, and commits. For each read, the distance to the previous commit measures how fresh is the read with respect to the last commit, and this can be measured with a backward-walking slave automaton. For each write, the distance to the next commit measures how fresh is the write with respect to the following commit, and this can be measured with a forward-walking slave automaton. Thus the average freshness, called DCP, is expressed with bidirectional NWA. Moreover, the DCP can neither be expressed by NWA with only forward-walking slave automata nor by NWA with only backward-walking slave automata.
Our contributions. We propose bidirectional NWA as a specification framework for quantitative properties. First, we show that the classes of forward-only NWA and backward-only NWA have incomparable expressiveness, and bidirectional NWA strictly generalize both classes. Second, we establish complexity of the emptiness and universality problems for bidirectional NWA, where we consider the limit-average value function for the master automaton and for the slave automata we consider standard value functions for finite words (such as min, max, and variants of sum). The obtained complexity results coincide with the results for forward-only NWA, and range from NLogSpace-complete, PTime to PSpace-complete to ExpSpace. However the proofs for bidirectional NWA are much more involved than forward-only NWA. Thus bidirectional NWA have all the advantages of NWA but provide a more expressive framework for natural quantitative properties. Moreover, the added expressiveness of bidirectionality is achieved with no increase in the computational complexity of the decision problems (Table 1). We highlight two significant differences as compared to the unweighted case: (1) In the unweighted case bidirectionality does not change expressiveness, whereas we show for NWA it does; and (2) in the unweighted case for deterministic automata bidirectionality leads to exponential succinctness and increase in complexity of the decision problems, whereas for NWA bidirectionality does not change the computational complexity. Thus the combination of nesting and bidirectionality is very interesting in the weighted automata setting, which we study in this work.
Related works. Quantitative automata and logic have been extensively studied in recent years in many different contexts [18, 12, 4, 2]. The book [18] presents an excellent collection of results of weighted automata on finite words. Weighted automata on infinite words have been studied in [12, 11, 19]. Weighted automata over finite words extended with monitor counters have been considered (under the name of cost register automata) in [3, 20]. A version of nested weighted automata over finite words has been studied in [6], and nested weighted automata over infinite words has been studied in [13, 15, 14]. Several quantitative logics have also been studied, such as [5, 7, 1]. However, none of these works consider the rich and expressive formalism of quantitative properties expressible by NWA with slaves that walk both forward and backward, retaining decidability of the basic decision problems.
In the main paper, we present the key ideas and main intuitions of the proofs of selected results, and detailed proofs are relegated to the appendix.
2 Definitions
2.1 Words and automata
Words. We consider a finite alphabet of letters . A word over is a (finite or infinite) sequence of letters from . We denote the -th letter of a word by , and for we define as the word . The length of a finite word is denoted by ; and the length of an infinite word is . For an infinite word , word is the suffix of with first letters removed. For a finite word of length , we define the reverse of , denoted by , as the word .
Labeled automata. For a set , an -labeled automaton is a tuple , where (1) is the alphabet, (2) is a finite set of states, (3) is the set of initial states, (4) is a transition relation, (5) is a set of accepting states, and (6) is a labeling function. A labeled automaton is deterministic if and only if is a function from into and is a singleton.
Semantics of (labeled) automata. A run of a (labeled) automaton on a word is a sequence of states of of length such that belongs to the initial states of and for every we have is a transition of . A run on a finite word is accepting if and only if the last state of the run is an accepting state of . A run on an infinite word is accepting if and only if some accepting state of occurs infinitely often in . For an automaton and a word , we define as the set of accepting runs on . Note that for deterministic automata, every word has at most one accepting run ().
Weighted automata and their semantics. A weighted automaton is a -labeled automaton, where is the set of integers. The labels are called weights. We define the semantics of weighted automata in two steps. First, we define the value of a run. Second, we define the value of a word based on the values of its runs. To define values of runs, we will consider value functions that assign real numbers to sequences of integers. Given a non-empty word , every run of on defines a sequence of weights of successive transitions of , i.e., ; and the value of the run is defined as . We denote by the weight of the -th transition, i.e., . The value of a non-empty word assigned by the automaton , denoted by , is the infimum of the set of values of all accepting runs; i.e., , and we have the usual semantics that the infimum of the empty set is infinite, i.e., the value of a word that has no accepting run is infinite. Every run on the empty word has length and the sequence is empty, hence we define the value as an external (not a real number) value . Thus, the value of the empty word is either , if the empty word is accepted by , or otherwise. To indicate a particular value function that defines the semantics, we call a weighted automaton with value function an -automaton.
Value functions. For finite runs we consider the following classical value functions: for runs of length we have
- •
Max and min: and .
- •
Sum and absolute sum: the sum function , the absolute sum , where is the absolute value of .
- •
Variants of bounded sum: we consider a family of functions called the (variant of) bounded sum value function . Each of these functions returns the sum if all the partial sums are in the interval , otherwise there are many possibilities which lead to multiple variants. For example, we can require that for all prefixes of we have . We can impose a similar restriction on all suffixes, all infixes etc. Moreover, if partial sums are not contained in , a bounded sum can return , the first violated bound, etc.
For infinite runs we consider:
- •
Limit average: .
Silent moves. Consider a -labeled automaton. We consider such an automaton as an extension of a weighted automaton in which transitions labeled by are silent, i.e., they do not contribute to the value of a run. Formally, for every function we define as the value function that applies on sequences after removing symbols. The significance of silent moves is as follows: it allows to ignore transitions, and thus provides robustness where properties could be specified based on desired events rather than steps.
2.2 Nested weighted automata
Nested weighted automata (NWA) have been introduced in [13] and originally allowed slave automata to move only forward. The variant we define here allow two types of slave automata, forward walking and backward walking. The original definition of NWA from [13] is versatile and hence it can be seamlessly extended to the case with bidirectional (forward- and backward-walking) slave automata. We follow the description of [13].
Informal description. A nested weighted automaton consists of a labeled automaton over infinite words, called the master automaton, a value function for infinite words, and a set of weighted automata over finite words, called slave automata. A nested weighted automaton can be viewed as follows: given a word, we consider the run of the master automaton on the word, but the weight of each transition is determined by dynamically running slave automata; and then the value of a run is obtained using the value function . That is, the master automaton proceeds on an input word as an usual automaton, except that before taking a transition, it starts a slave automaton corresponding to the label of the current transition. The slave automaton starts at the current position of the master automaton in the input word and works on some finite part of it. There are two types of slave automata: (a) forward walking, which move onward the input word (toward higher positions), and (b) backward walking, which move towards the beginning of the input word. Once a slave automaton finishes, it returns its value to the master automaton, which treats the returned value as the weight of the current transition that is being executed. The slave automaton might immediately accept and return value , which corresponds to a silent transition, i.e., transition with no weight. If one of slave automata rejects, the nested weighted automaton rejects. We present two examples of properties expressible by NWA. Additional examples are presented in Section 3.
Example 1** (Average response time and its dual).**
Consider infinite words over , where represents requests, represents grants, and represents idle. A basic and interesting property is the average number of letters between a request and the corresponding grant, which represents the long-run average response time (ART) of the system. This property cannot be expressed by a non-nested automaton [13]. ART can be expressed by a deterministic nested weighted automaton, which basically implements the definition of ART. This automaton invokes at every request a forward-walking slave automaton with value function, which counts the number of events until the following grant. On the other events the NWA takes silent transitions. Finally, the master automaton applies LimAvg value function to the values returned by slave automata. Figure 1 presents a run of the NWA computing ART.
We define the average workload property (AW), which measures the average number of pending requests. The average is computed over all positions in a word. Intuitively, if we pick a position in word at random, the expected number of pending requests is the average workload of . Formally, we define the workload at in , denoted , as the number of letters among , where is the last position in where occurs or if such a position does not exist. The average workload of is the limit average over all positions of .
AW can be expressed by a deterministic -automaton with backward-walking slave automata. Basically, the NWA invokes at every position a slave automaton, which counts the number of letter from its current position to the first position containing letter , where it terminates. Since slave automata run backwards, each of them computes the workload at the position of its invocation. Figure 1 presents a run of the NWA computing AW.
Now, we present a formal definition of NWA and their semantics.
Nested weighted automata. A nested weighted automaton (NWA) with bidirectional slave automata is a tuple , with where (1) , called the master automaton, is a -labeled automaton over infinite words (the labels are the indexes of automata ), (2) is a value function on infinite words, called the master value function, and (3) are weighted automata over finite words called slave automata. Intuitively, an NWA can be regarded as an -automaton whose weights are dynamically computed at every step by the corresponding slave automaton. The automata (resp., ) are called backward walking (resp., forward walking) slave automata. We refer to NWA with both forward and backward walking slave automata as bidirectional NWA. The automaton immediately accepts and returns no weight; it is used to implement silent transitions, which have no weight. We define an -automaton as an NWA where the master value function is and all slave automata are -automata.
Semantics: runs and values. A run of on an infinite word is an infinite sequence such that (1) is a run of on ; (2) for every the label pointers at a slave automaton and (a) if , then is a run of the automaton on some prefix of the reverse word , and (b) if , then is a run of the automaton on some finite prefix of . The run is accepting if all runs are accepting (i.e., satisfies its acceptance condition and each ends in an accepting state) and infinitely many runs of slave automata have length greater than (the master automaton takes infinitely many non-silent transitions). The value of the run is defined as , where is the value of the run in the corresponding slave automaton, and is the value function that takes its input sequence, removes symbols and applies to the remaining sequence. The value of a word assigned by the automaton , denoted by , is the infimum of the set of values of all accepting runs. We require accepting runs to contain infinitely many non-silent transitions as is a value function over infinite sequences, hence the sequence with removed must be infinite.
Deterministic nested weighted automata. An NWA is deterministic if (1) the master automaton and all slave automata are deterministic, and (2) in all slave automata, accepting states have no outgoing transitions. Intuitively, a slave automaton in an accepting state can choose (non-deteministically) to terminate or continue running; condition (2) removes this source of non-determinism.
Width of NWA. An NWA has width if and only if in every run at every position at most slave automata are active.
3 Examples
In this section we present several examples of quantitative properties that can be expressed with bidirectional NWA.
Example 2** (Average energy level).**
We consider the average energy level property studied in [17, 8]. Consider and an alphabet consisting of integers from interval . These letters correspond to the energy change, i.e., negative values represent energy consumption whereas positive values represent energy gain. For we define the energy level at as the sum . The average energy property (AE) is the limit average of the energy levels at every position. For example, the average energy level of is .
AE can be expressed by a -automaton with backward-walking slave automata, but it is not expressible by -automata with forward-walking slave automata. To express AE, a -automaton with backward-walking slave automata invokes at every position a slave automaton, which runs backward to the beginning of the word and sums up all the letters. In contrast, -automata with forward-walking slave automata can use finite memory of the master automaton, but finite prefixes influence only finitely many values returned by slave slave automata and the limit-average value function neglects finite prefixes. Formally, we can show with a simple pumping argument that for every -automaton with forward-walking slave automata, among words there exists a pair of words with the same value. In contrast, all these words have different AE (AE of is ).
AE property is often considered in conjunction with bounds on energy values. Typically, energy should not drop below some threshold, in particular, it should not be negative. In addition, the energy storage is limited, which motivates the upper bound on the stored energy, where the excess energy is released. These two restrictions lead to the interval constraint on energy levels, i.e., we require the energy level at every position to belong to a given interval , which results in a variant of the bounded sum .
Example 3** (Data consistency).**
Consider a database server, which processes instructions grouped into transactions. There are four instructions: read , write , void and commit . The commit instruction applies all writes, finishes the current transaction and starts a new one. The read instructions refer to writes applied before the previous commit.
In the presence of multiple clients connected to the database, there are two options to achieve consistency. One option is to use locks that can limit concurrency. A second approach is optimistic concurrency which proceeds without locks, and then rolls back in case there was a collision between transactions. In ordered to limit the number of roll backs, it is preferred that the read instructions occur shortly after commit, while write instructions are followed by the commit instruction as quickly as possible. Formally, we define (a) consistency (or freshness) of a read instruction as the number of steps to the first preceding commit instruction, and (b) consistency of a write instruction as the number of steps to the following commit instruction. The data consistency property (DCP) of is the limit average of consistency of reads and writes in .
DCP is expressed by the following deterministic -automaton with bidirectional slave automata. On every read (resp., ), the NWA invokes a slave automaton which walks backward (resp., forward) and counts the number of steps to the first encountered . On the remaining instructions , the NWA invokes a dummy slave automaton which corresponds to a silent transition.
Example 4**.**
Consider the framework of Example 3. For every position with read or write we define a regret at position as the minimal distance to the preceding or the following commit . Intuitively, the regret corresponds to the number of instructions by which we have to prepone or postpone the commit to include the instruction at the current position. We consider the minimal regret property (MR) on words over defined the limit average over positions with and of the regret at these positions. MR can be expressed by a non-deterministic -automaton with bidirectional slave automata, which basically implements the definition of MR (the non-deterministic guess is whether it is the preceding or the following commit). The NWA invokes at every or position one of the following two slave automata . The automaton counts the number of steps to the preceding grant, while counts the number of steps to the following grant.
4 Decision questions
For NWA with bidirectional slave automata, we consider the quantitative counterparts of the fundamental problems of emptiness and universality. The (quantitative) emptiness and universality problems are defined in the same way for weighted automata and all variants of NWA; in the following definition denotes either a weighted automaton or an NWA.
Emptiness and universality. Given an automaton and a threshold , the emptiness (resp. universality) problem asks whether there exists a word with (resp., for every word we have ).
Remark 5**.**
The emptiness and universality problems have been studied for forward-only NWA in [13].
- •
For NWA the value functions considered for the master automaton are the infimum (or limit-infimum), the supremum (or limit-supremum), and the limit-average. For all the decidability results for the infimum (limit-infimum) and the supremum (limit-supremum) value functions the techniques are similar to unweighted automata **[13]**, which can be easily adapted to the bidirectional framework. Hence in the sequel we only focus on bidirectional NWA with the limit-average value function for the master automaton.
- •
Moreover, we study only the emptiness problem for the following reasons. First, for the deterministic case the emptiness and the universality problems are similar and hence we focus on the emptiness problem. Second, in the non-deterministic case the universality problem is already undecidable for LimAvg-automata even with no nesting **[9]**.
4.1 The minimum, maximum and bounded sum value functions
First, we show that for being , or a variant of the bounded sum value function , the emptiness problem for -automata with bidirectional slave automata is decidable in PSpace. To show that, we prove a stronger result, i.e., every -automaton can be effectively transformed to a LimAvg-automaton of exponential size.
Key ideas. Weighted automata with value functions are close to (non-weighted) finite-state automata. In particular, these automata have finite range and for each value from the range, the set of words of value is regular. Thus, instead of invoking a slave automaton, the master automaton can non-deterministically pick value and verify that the value returned by this slave automaton is . For backward-walking slave automata the guessing can be avoided as the master automaton can simulate (the reverse of) runs of all backward-walking slave automata until the current position. Thus, we can eliminate slave automata from NWA, i.e., we transform such NWA to weighted automata. Formally, we show that for , every -automaton with bidirectional slave automata can be transformed into an equivalent LimAvg-automaton of exponential size. The emptiness problem for non-deterministic LimAvg-automata is in NLogSpace (assuming weights given in unary) and hence we have the containment part in the following Theorem 6. The hardness part follows from PSpace-hardness of the emptiness problem for -automata with forward-walking slave automata only [13].
Theorem 6**.**
Let . The emptiness problem for non-deterministic -automata with bidirectional slave automata is PSpace-complete.
Note. The complexity in Theorem 6 does not depend on encoding of weights in slave automata, i.e., the problem is PSpace-hard even for a fixed set of weights, and it remains in PSpace for weights encoded in binary.
The average energy property from Example 2 with bounds on energy levels can be expressed with -automata. The emptiness problem for these automata is decidable by Theorem 6.
Remark 7** (Parametrized complexity).**
If we assume that the size of slave automata in Theorem 6 is bounded by a constant, the complexity of the emptiness problem drops to NLogSpace-complete. NLogSpace-hardness follows from NLogSpace-hardness of the emptiness problem for LimAvg-automata, which can be considered as a special case of NWA.
The results of this section apply to general bidirectional NWA. In the following section we consider bidirectional NWA with the sum value function, where we consider additional restrictions of finite width (Section 5) and bounded width (Section 6). We also justify in Remark 9 that the finite width restriction is natural.
5 Finite-width case
In this section we study NWA satisfying the finite width condition. First, we briefly discuss the finite-width condition and argue that it is a natural restriction. Next, we show that the emptiness problem for (finite-width) -automata with bidirectional slave automata is decidable in ExpSpace. We conclude this section with the expressiveness results; we show that classical NWA with forward-walking slave automata and NWA with backward-walking slave automaton have incomparable expressive power. Hence, (finite-width) -automata with bidirectional slave automata are strictly more expressive than NWA with one-direction slave automata.
5.1 The finite-width condition
Finite width. An NWA has finite width if and only if in every accepting run of at every position at most finitely many slave automata are active. Classical NWA with forward-walking slave automata only have finite width. Indeed, in any run, at any position at most slave automata can be active.
Example 8**.**
Consider an NWA over such that the master automaton accepts a single word and all slave automata are backward walking and accept words . All slave automata terminate at the first position of and hence this NWA does not have finite width.
The automata expressing properties from Examples 1, 3 and 4 are finite-width -automata with bidirectional slave automata. Observe that an NWA does not have finite width if and only if it has an accepting run, in which at some position infinitely many backward-walking slave automata terminate.
Remark 9** (Finite width is natural for positive sum).**
Let be a -automaton with bidirectional slave automata. Except for degenerate cases, runs of , which do not have finite width, have infinite value. Indeed, consider a run and a position at which infinitely many automata are active. Since only finitely many forward-walking slave automata are active at , infinitely many of them are backward-walking and for some position , infinitely many slave automata terminate at position . Then, one of the following holds: either that value of this run is infinite or one of the following two degenerate cases happen: (a) The slave automata from are invoked with zero density (i.e., if consider the long-run average of the frequency of invoking slave automata, then it is zero). This situation represents that monitoring with slave automata happens with vanishing frequency which is a degenerate case. (b) The values returned by the slave automata from are bounded. It follows that these automata take transitions of non-zero weight only in some finite subword of the input word . This situation represents monitoring of an infinite sequence, in which all events past position are irrelevant. This is a degenerate case in the infinite-word case.
The finite-width property does not depend on weights and hence we can construct an exponential-size Büchi automaton , which simulates runs of a given NWA . Having , we can check whether it has a run corresponding to an accepting run of , in which infinitely many backward-walking slave automata terminate at the same position. This check can be done in logarithmic space and hence checking the finite-width property is in PSpace. A simple reduction from the non-emptiness problem for NWA shows PSpace-hardness of checking the finite-width property.
Theorem 10**.**
The problem whether a given NWA has finite width is PSpace-complete.
5.2 The absolute sum value function
We present the main result on NWA of finite width.
Theorem 11**.**
The emptiness problem for finite-width -automata with bidirectional slave automata is PSpace-hard and it is decidable in ExpSpace.
Key ideas. PSpace-hardness follows from PSpace-hardness of the emptiness problem for -automata with forward-walking slave automata only. Containment in ExpSpace is shown by reduction to the bounded-width case, which is shown decidable in the following section (Theorem 17). We briefly describe this reduction. Consider a finite-width -automaton with bidirectional slave automata. First, we observe that without loss of generality, we can assume that is deterministic. Second, we observe that in every word accepted by , at almost every position there exists a barrier, which is a word such that (a) the word , i.e., with inserted at position , is accepted by , and the runs on and coincide except for positions in corresponding to , (b) in the run on , backward-walking slave automata active at the end of terminate within , (c) in the run on , forward-walking slave automata active at the beginning of terminate within , and (d) has exponential length. Basically, active slave automata cannot cross in and in the effect insertion of bounds the number of active slave automata. Existence of barriers follows from the finite-width property of .
We insert barriers in to reduce the number of active slave automata. While inserting at a certain position may increase the partial average, we show that if at position in , exponentially many active slave automata accumulates exponential weight past crossing (some slave automata walk forward while other backwards), all partial averages (of values returned by slave automata) in are bounded by the corresponding partial averages in . We conclude that for every word , there exists a word such that (i) at every position at most exponentially many slave automata accumulate exponential values, and (ii) the value of does not exceed the value of . Thus, to compute the infimum over all runs of , we can focus on runs in which at every position at most exponentially many slave automata accumulate exponential value. Runs of slave automata in which they accumulate bounded (exponential) values can be eliminated as in Theorem 6, i.e., we can construct an exponential size NWA , which simulates , and such that its slave automata run as long as they can accumulate value exponential (in ) and otherwise they non-deterministically pick the remaining value and the master automaton verifies that the pick is correct. Therefore, the infimum over all runs of coincides with the infimum over all runs of of width exponentially bounded.
Remark 12** (Parametrized complexity).**
If we assume that the size of slave automata in Theorem 11 is bounded by a constant, the complexity of the emptiness problem drops to NLogSpace-complete. NLogSpace-hardness follows from NLogSpace-hardness of the emptiness problem for LimAvg-automata, which can be viewed as a special case of NWA.
5.3 Expressive power
DCP defined in Example 3 can be expressed by a deterministic finite-width -automaton with bidirectional slave automata. We show that both forward-walking and backward-walking slave automata are required to express DCP. That is, we formally show that DCP cannot be expressed by any (non-deterministic) -automaton with slave automata walking in one direction only.
Classes of NWA. We define as the class of all finite-width -automata with bidirectional slave automata. We define (resp., ) as the subclass of consisting of NWA with forward-walking (resp., backward-walking) slave automata only.
We establish that classes and have incomparable expressive power and hence they are strictly less expressive than class .
Key ideas. Consider a word for some big and much bigger . An NWA from computes DCP of by invoking (non-dummy) slave automata at every letter and taking silent transitions on letters . We show that an NWA from cannot invoke the right number of slave automata, even if it uses non-determinism. More precisely, we show that computing DCP has to invoke at most non-dummy slave automata on average on subwords . Since is much bigger than , we conclude that has a cycle over letters at which it takes only silent transitions and a cycle over letters on which it increases the multiplicity of active slave automata. Using these two cycles, we construct a run of value smaller than DCP, which contradicts the assumption that computes DCP. Similarly, we can show that an NWA from cannot compute correctly DCP of words of the form , while on these words DCP is expressible by an NWA from .
Lemma 13**.**
(1) DCP restricted to alphabet is expressed by an NWA from , but it is not expressible by NWA from . (2) DCP restricted to alphabet is expressed by an NWA from , but it is not expressible by NWA from .
The above lemma implies that DCP over alphabet is not expressible by any NWA from nor from . In conclusion, we have:
Theorem 14**.**
(1) and have incomparable expressive power. (2) are strictly more expressive than and .
6 Bounded-width case
In this section, we study -automata with bidirectional slave automata, which have bounded width. The bounded width restriction has been introduced in [14] to improve the complexity of the emptiness problem and to establish decidability of the emptiness problem for -automata. NWA considered in [14] have only forward-walking slave automata, while we extend these results to NWA with bidirectional slave automata. This extension preserves the complexity bounds from [14], i.e., the emptiness problem is in PTime for constant width and PSpace-complete for width given in unary.
The bounded width restriction emerges naturally in examples presented so far. If we bound the number of pending requests, we can express ART and AW (Examples 1 and 1) by automata of bounded width. If we bound the number of writes and reads between any two commits, then DCP and MR (Examples 3 and 4) can be expressed by NWA of bounded width. These natural restrictions lead to more efficient decision procedures.
The decision procedure in this section differs from the one from [14]. The key step in the decidability proof from [14] is establishing the following dichotomy: either the infimum over values of all words is or the infimum is realized by dense runs. A run is dense if for the values returned by slave automata invoked at positions we have converges to [math], i.e., values returned by slave automata are sublinear in the positions of their invocation. Properties of dense runs allow for further reductions, which lead to a decision procedure. However, we show in the following Example 15 that in case of NWA with bidirectional slave automata, dense runs may not attain the infimum of all runs.
Example 15**.**
Consider a -automaton with bidirectional slave automata over . The NWA accepts words and it works as follows. On letters , invokes a forward-walking slave automaton , which returns the number of the following letters up to . On letters , invokes a backward-walking slave automaton , which returns the number of the preceding letters since . Finally, on letters, invokes a slave automaton , which takes a single transition and returns value [math]. The NWA has width . We can show that the value of any dense run, is . However, the infimum over values of all words is . The partial average of the values returned by slave automata on finite word is , while the partial average over is . Therefore, the value, which is limit infimum over partial averages, of word is if sequence is grows rapidly (e.g. doubly-exponentially).
Main ideas. In Example 15, the words attaining the least value contain long blocks of letter , at which the NWA is (virtually) in the same state, i.e., it loops in this state. On letters , the sum of all weights collected by all active slave automata is , i.e., automata collect weight and collect [math]. However, in computing limit infimum over partial averages, we pick positions just before letter as they correspond to the local minima, i.e., we compute the partial average over prefixes , and hence the weights collected by do not contribute to this partial average. Then, the sum of all weights collected by slave automata over a letter is , which is equal to the least value of the limit infimum of the partial averages. In the following, we extend this idea and present the solution of all bounded-width -automata with bidirectional slave automata. We show that the infimum over all words of a given NWA is the least average value over all cycles. In the following, we define appropriate notions of cycles of NWA and their average with exclusion of some slave automata.
The graph of -configurations. Let be a non-deterministic -automaton of width . We define a -configuration of as a tuple where is a state of the master automaton, and each is either a state of a slave automaton of or . Given a run of , we say that is the -configuration at position in the run if is the state of the master automaton at position and there are active slave automata at position , whose states are ordered by position of invocation (backward-walking slave automata are invoked past position ). If , then . We say that a -configuration is a successor of a -configuration if there exists an accepting run of and such that is the -configuration at and is the -configuration at The graph of -configurations of is the set of -configurations of , which occur infinitely often in some accepting run, with the successor relation.
Characteristics of cycles. Let be a cycle in a graph of -configurations of . Let (resp., ) be the set of forward-walking (resp., backward-walking) slave automata, which are active throughout , i.e., which are not invoked nor terminated within . A focus (for ) is a downward closed subset of , i.e., it contains all automata from invoked before some position. We define a focused gain as the sum of weights which automata from accumulate over . A restriction (for ) is an upward closed subset of , i.e., it contains all automata from invoked past certain position. We define an average weight of excluding , denoted by , as the sum of weights of all transitions of slave automata within , except of transitions of slave automata from , divided by the number of slave automata invoked within .
Intuitively, a focused gain refers to the value, which forward-walking slave automata invoked before some position , accumulate over the part of run corresponding to (see Figure 2). If the focused gain is negative, then by pumping we can arbitrarily decrease the partial average of the values of slave automata invoked before . In consequence, we can construct a run of the value . Formally, we define condition (), which implies that there exists a run of value , as follows: () there exists a cycle in the graph of -configurations of and a focus such that .
If the focused gain of every cycle is non-negative, we need to examine averages of cycles, while excluding some backward-walking slave automata. The average weight with restriction corresponds to the partial average of values aggregated over by all slave automata invoked before position (which can be past ). Backward-walking slave automata in the restriction correspond to automata invoked past , and hence their values do not contribute to the partial average (up to ) (see Figure 2). In Example 15, we compute the average of slave automata over letters , but we exclude the backward-walking slave automaton invoked at the following letter . Observe that for any cycle and any restriction , having a run containing occurring infinitely often, we can repeat each occurrence of cycle sufficiently many times so that the partial average of values of slave automata up to position corresponding to becomes arbitrarily close to the average . The resulting run contains a subsequence of partial averages convergent to and hence its value does not exceed . We can now state our key technical lemma. This lemma is a direct extension of an intuition behind computing the infimum over values of all words of the NWA from Example 15.
Lemma 16**.**
Let be a -automaton of bounded width with bidirectional slave automata. (1) If condition () holds, then has a run of value . (2) If () does not hold, then the infimum equals the infimum , where is the set of all cycles in the graph of -configurations of .
If the width of is constant, then the graph of -configurations has polynomial size in and it can be constructed in polynomial time by employing reachability checks on the set of all -configurations w.r.t. to relaxation of the successor relation. Therefore, for every focus and every -configuration we can check in polynomial time whether there exists a cycle such that and . Thus, condition (1) can be check in logarithmic space assuming that weights are given in unary. If weights are given in binary, condition (1) can be checked in polynomial time. Checking condition (2) has the same complexity as condition (1). If the width is given in unary in input, the graph of -configurations is exponential in and conditions (1) and (2) can be checked in polynomial space. Weights in this case are logarithmic in the size of the graph and hence changing representation from binary to unary does not affect the (asymptotic) size of the graph.
Theorem 17**.**
The emptiness problem for -automaton of width with bidirectional slave automata is (a) NLogSpace-complete for constant and weights given in unary, (b) in PTime for constant and weights given in binary, and (c) PSpace-complete for given in unary.
7 Extensions
In this section we briefly discuss some extensions of the model of bidirectional NWA, i.e., we discuss the possibility of invoking multiple slave automata in one transition and two-way walking slave automata.
Invocation of multiple slave automata. The master automaton of an NWA invokes exactly one slave automaton at every transition. We can generalize the definition of NWA and allow the master automaton to invoke up to some constant slave automata at every transition. We call such a model -NWA. First note that -NWA contain NWA. Conversely, we briefly describe a reduction of the emptiness problem for -NWA to the emptiness problem for NWA. First, observe that without loss of generality we can assume that -NWA always invokes exactly -slave automata as it can always invoke a dummy slave automaton, which immediately accepts. Invocation of such a slave automaton is equivalent to taking a silent transition. Next, given a -NWA with bidirectional slave automata over the alphabet , we can construct an NWA with bidirectional slave automata over the alphabet , which accepts words of the form . The runs of on the word correspond to all runs of on ; the invokes at letters exactly slave automata which invokes at the corresponding transition over letter . Observe that the emptiness problems for and coincide.
Two-way walking slave automata. For the ease of presentation we focus on bidirectional NWA where each slave automaton is either forward walking or backward walking. However, in general, we can allow slave automata that change direction while running, i.e., allow two-way slave automata and obtain the same complexity results. Observe that in case of two-way -automata, we can assume that such an automaton does not visit the same position in the same state twice. Indeed, such a cycle can be eliminated without increase of the value of the run. Thus, without loss of generality we assume that every two-way slave automaton visits every position at most times. Therefore, instead of invoking a two-way slave -automaton the master automaton invokes multiple forward-walking and backward walking slave automata, two automata, a forward walking and a backward walking such that (resp., ) simulates the run of past its invocation position (resp., before its invocation position). This reduction shows that every -automaton with two-way walking slave automata is equivalent to a -NWA with bidirectional slave automata. This reduction however involves exponential blow-up as slave automata can have exponential size in . This follows from the fact that due to reversals each visited position by can be visited times in different states. To simulate that in one run, and have to simulate instances of in different states. This exponential blow-up can be avoided by dividing into multiple slave automata, each of which tracks only one loop in the run of as shown in Figure 3 with automata . Each of these automata have to track at most two instances of and hence it involves only quadratic blow-up. The resulting automaton is an -NWA as up to slave automata have to be invoked at every position. Still, the emptiness problems for -NWA and for NWA have the same complexity and hence we conclude that allowing two-way slave automata does not increase the emptiness problem for -automata.
8 Discussion and Conclusion
Discussion. We established decidability of the emptiness problem for classes of bidirectional NWA, which include all NWA presented in the examples. An NWA from Example 2 is covered by Theorem 6, while NWA from Examples 1, 3 and 4 are covered by Theorem 11. The lower bounds in the presented theorems follow from the lower bounds of the special case of forward-only NWA. The established complexity bounds (Table 1) coincide with the bounds for forward-only NWA.
Concluding remarks. In this work we present bidirectional NWA as a specification formalism for quantitative properties. In this formalism many natural quantitative properties can be expressed, and we present decidability and complexity results for the basic decision problems. There are several interesting directions for future work. The study of bidirectional NWA with other value functions is an interesting direction. The second direction of future work is to consider other formalism (such as a logical framework) which has the same expressive power as bidirectional NWA.
Acknowledgements.
This research was supported in part by the Austrian Science Fund (FWF) under grants S11402-N23,S11407-N23 (RiSE/SHiNE) and Z211-N23 (Wittgenstein Award), ERC Start grant (279307: Graph Games), Vienna Science and Technology Fund (WWTF) through project ICT15-003 and by the National Science Centre (NCN), Poland under grant 2014/15/D/ST6/04543.
Appendix
In the appendix we recall statements of theorems and lemmas from the main body of the paper keeping their original numbering. Lemmas introduced in the appendix have subsequent numbers. For this reason, the numbering of theorem and lemmas in the appendix is mixed.
Appendix A Proofs from Section 4
See 6
The PSpace-hardness part follows from PSpace-hardness of the emptiness problem for -automata with forward-walking slave automata only [13]. Therefore, we focus on the containment in PSpace. We begin with a definition of a unifying framework of regular value functions.
Regular weighted automata and regular value functions. Following [13], we say that a weighted automaton over finite words is a regular weighted automaton if and only if there is a finite set of rationals and there are regular languages such that
- (i)
every word accepted by belongs to , and 2. (ii)
for every , its value w.r.t. is .
A value function is a regular value function if and only if all -automata are regular weighted automata. Examples of regular value functions are and variants of the bounded sum with regular conditions, i.e., the partial sum of every prefix, suffix, infix of the run belongs to interval , e.t.c. Having the definition of regular value function, we can easily check whether our variant of the bounded sum is admissible.
We define the description size of a given regular weighted automaton , as the size of automata recognizing languages that witness being a regular weighted automaton.
Lemma 18**.**
Let be a regular value function. Every -automaton with bidirectional slave automata is equivalent to an exponential-size LimAvg-automaton . The automaton can be constructed implicitly in polynomial time.
Since the emptiness problem for LimAvg-automata can be solved in NLogSpace, Lemma 18 implies Theorem 6. Moreover, Remark 7 follows directly from the construction in the following proof.
Proof.
Let be the set of states of the master automaton of . Since is a regular value function, every slave automaton has a finite range and for each value there exists a finite-state automaton recognizing the set of words of value . Let (resp., ) be the union of the sets of states of all automata , where if a forward-walking (resp., backward-walking) slave automaton and . We assume that sets of states of automata are disjoint.
We define a LimAvg-automaton with generalized Büchi condition as follows. The set of states of is . States of are of the form , whose objectives are as follows.
Component is used to simulate the run of the master automaton. Components are used to simulate finite-state automata corresponding to forward-walking slave automata. Accepting states correspond to termination of a slave automaton and hence they are removed from . Every newly invoked forward-walking slave automaton is added to component , i.e., automaton picks a transition invoking slave automaton and picks weight of this transition , then it adds to an initial state of finite-state automaton . The weight of such a transition is ,
If every slave automaton has finite run than becomes empty at some point of time. Then, we move all states from to , and put . Observe that runs of all forward-walking slave automaton are finite if and only if is empty infinitely often.
Component is used to simulate finite-state automata corresponding to backward-walking slave automata. Accepting states of backward-walking slave automata correspond to their termination. Since moves in the opposite direction w.r.t. , the automaton adds to component some subset of accepting states from . There is only one position in the run of at which it adds states to . Whenever a backward-walking slave automaton is invoked in a state , we require that belongs to . This state may be removed from the corresponding set but does not have to. Removal corresponds to a situation when only a single slave automaton is in the state , while leaving in corresponds the situation when more than one slave automaton is in state .
Due to the construction we have (i) for every run of , the automaton has a run of the same weight, and conversely (ii) for every run of , there exists a run of the same value. ∎
Appendix B Proofs from Section 5
B.1 The proof of Theorem 10
See 10
Proof.
Let (resp., ) be the set of states of forward-walking (resp., backward-walking) slave automata of and let be the set of states of the master automaton of . We define a (generalized) Büchi-automaton (with no weights) as follows. The set of states of is . Initially starts with , where is some initial state of the master automaton. We use sets of states to simulate runs of slave automata and to ensure that every forward-walking slave automaton runs for finitely many steps. We treat backward-walking slave automata in a similar way to forward-walking slave automata except that backward-walking slave automata are started at the termination step of the corresponding slave automata, and they can terminate (which correspond to invocation) multiple, but finitely many times. More precisely, states of are of the form , whose objectives are as follows.
Component is used to simulate the run of the master automaton. Components are used to simulate forward-walking slave automata. Accepting states correspond to termination of a slave automaton and hence they are removed from . A newly invoked forward-walking slave automaton is added to component . Thus, if every slave automaton has finite run than becomes empty at some point of time. Then, we move all states from to , and put . Observe that runs of all forward-walking slave automaton are finite if and only if is empty infinitely often.
Components are used to simulate backward-walking slave automata. Component contains the states of slave automata that all finish at the same position, while contains states of other slave automata. We require that and are disjoint at every position. Accepting states of backward-walking slave automata correspond to their termination. However, as the simulating automaton moves in the opposite direction, it guesses at every step whether some (backward-walking) slave automaton have been terminated at the current position and it may add some accepting states to or . There is only one position in the run of at which it adds states to . Whenever a backward-walking slave automaton is invoked in a state , we require that belongs to or . This state may be removed from the corresponding set but does not have to. Removal corresponds to a situation when only a single slave automaton is in the state , while leaving in or corresponds the situation when more than one slave automaton is in state .
Consider an infinite run of , in which (a) component equals infinitely often to some accepting state of the master automaton, (b) component is empty infinitely often, and (c) component is never empty and infinitely often contains an initial state of the slave automaton invoked at the current position. The run corresponds to an accepting run of in which infinitely many backward-walking slave automata terminate at the same position (which is the position at which becomes non-empty for the first time). Conversely, having a run of of infinite width, the corresponding run of satisfies (a), (b) and (c). Checking existence of a run of satisfying (a), (b) and (c) can be done in non-deterministic logarithmic space. Thus, checking whether has infinite width can be done in polynomial space.
We show PSpace-hardness of checking finite-width, by reduction from the emptiness problem for NWA with forward-walking slave automata only, which is PSpace-complete [13]. Let be an NWA with forward-walking slave automata only over the alphabet . We extend the alphabet by \,#\mathbb{A}^{\prime}$w[1]#w[2]#\mathbb{A}w[1]w[2]\ldots\mathbb{A}#(q,a,q^{\prime})\mathbb{A}(q,a,q^{\prime}{#})(q^{\prime}{#},#,q^{\prime})\mathbb{A}^{\prime}\mathbb{A}#\mathbb{A}^{\prime}$\mathbb{A}\mathbb{A}^{\prime}\mathbb{A}w\mathbb{A}^{\prime}$w[1]#w[2]#\mathbb{A}\mathbb{A}^{\prime}$ does not have finite width.
∎
B.2 The proof of Theorem 11
See 11
The PSpace-hardness part follows from PSpace-hardness of the emptiness problem for -automata with forward-walking slave automata only [13]. Therefore, we focus on the containment in ExpSpace.
Overview. The proof is by reduction to the bounded-width case, which is decidable due to Theorem 17. First, we show that without loss of generality we can assume that a given NWA is deterministic (Lemma 19). Next, we define words, called barriers, upon which all active (backward- and forward-walking) slave automata terminate. We show that for finite-width NWA such words do exist (Lemma 21). Properties of barriers ensure that if as some position in the input word, exponentially many slave automata accumulate exponential values, then inserting a barrier actually decreases the partials sum of values returned by slave automata (Lemma 22), and hence we can insert barriers even at infinitely many positions and the value of the resulting word does not exceed the value of the original word. Thanks to barriers, we can show that for every word , there exists a word such that at every position at most exponentially many slave automata aggregate exponential values and the value of does not exceed the value of . Slave automata which aggregate bounded (exponential) values can be eliminated, i.e., we construct an NWA which simulates in such a way that runs of slave automata that accumulate at most exponential values are compressed into a single transition. Observe that on word as above has exponential width. Hence, the infimum of over all words coincides with the infimum of over words on which it has a run of exponential width. We can encode the bound on width into and decide the emptiness problem of in non-deterministic logarithmic space (Theorem 17). The size of is doubly-exponentially bounded in the size of , and hence the emptiness problem for finite-width -automata with bidirectional slave automata is in ExpSpace.
Configuration and multiplicities. Invocation of a slave automaton in an NWA is a form of a universal transition in the sense of alternating automata. We adapt the power-set construction, which is used to convert alternating automata to non-deterministic automata, to the NWA case. Given a (non-deterministic) NWA with bidirectional slave automata, we define configurations and multiplicities of as follows. Let be the disjoint union of the sets of states of all slave automata of . For a run of , we say that is the configuration at position if is the state of the master automaton at position and is the set of states of slave automata at position . We denote by the number of configurations of . We define the multiplicity at position as the function , such that specifies the number of slave automata in the state at position . The configuration together with the multiplicity give a complete description of the state of at position .
We observe that without loss of generality we can assume that NWA are deterministic. Basically, non-deterministic choices of the master automaton and slave automata can be encoded in the input alphabet. More precisely, the proof consists of two steps. First, we define simple runs as follows. A run of an NWA is simple if at every position in the run slave automata that are in the same state take the same transition. We show that (i) for every run of there exists a simple run of of the value not exceeding the value of . Second, we show that (ii) there exists a deterministic -automaton over an extended alphabet such that the sets of accepting simple runs of and accepting runs of coincide and each run has the same value in both automata.
The proof of the following lemma is virtually the same as in the case of NWA with forward-walking slave automata only [13].
Lemma 19**.**
Given a -automaton over with bidirectional slave automata, (i) for every run of , there exists a simple run of at most the same value, and (ii) one can compute in polynomial space a deterministic -automaton over an alphabet such that: (1) , and (2) .
Proof.
(i): Consider a run of . Suppose that are runs of the same slave automaton invoked at positions and , such that its both instances are in the same state at position in the word, i.e., , where are the positions in corresponding to the position in . We pick from the suffixes the one with the smaller sum, and in case of the equal sum we pick the shorter. Then, we change the suffixes of both runs to the picked one. Such a transformation does not increase the value of the partial sums and does not introduce infinite runs of slave automata. Indeed, a run of each slave automaton can be changed by such an operation only finitely many times. Thus, this transformation can be applied to any pair of slave runs to obtain a simple run of the value not exceeding the value of .
(ii): Without loss of generality, we can assume that for every slave automaton in final states have no outgoing transitions. Let be the disjoint union of the sets of states of the master automaton and all slave automata of . We define as the set of all partial functions . We define a -automaton over the alphabet by modifying only the transition relations and labeling functions of the master automaton and slave automata of ; the sets of states and accepting states are the same as in the original automata. The transition relation and the labeling function of the master automaton of are defined as follows: is a transition of if and only if and has the transition . The label of the transition is the same as the label of the transition in . Similarly, for each slave automaton in , the transition relation and the labeling function of the corresponding slave automaton in are defined as follows: is a transition of if and only if and has the transition . The label of the transition is the same as the label of the transition in .
First, we see that . Second, observe that the master automaton and all slave automata are deterministic. Moreover, since we assumed that for every slave automaton in final states have no outgoing transitions, slave automata recognize prefix free languages. Finally, it follows from the construction that (i) every simple run of is a run of of the same value. Basically, we encode in the input word all transitions in functions . The value of each transition is the same by the construction. Conversely, (ii) every run of is a simple run of of the same value. Indeed, the fact that transitions are directed by functions implies that the run is simple. ∎
In the following definition we introduce barriers, which are words on which all active slave automata terminate, i.e., if is a barrier, then forward-walking slave automata terminate while reading , and backward-walking slave automata terminate while reading (word from right to left). Barriers have additional properties, which allow us tho show that if exponentially many slave automata accumulate exponential values, then inserting a barrier decreases multiplicities of slave automata and does not increase the partial sums of values returned by slave automata.
Definition 20** (Barriers).**
Let be an infinite word, be a position and be the first position such that all backward-walking slave automata invoked past terminate past . A finite word is a barrier at in if in word we have
- BC1
backward-walking slave automata invoked past position terminate past position (between positions and ) 2. BC2
forward-walking slave automata invoked before position terminate before position , 3. BC3
the configurations at and in are the same as the one at in , 4. BC4
the length of is bounded by , 5. BC5
for every state of some backward-walking (resp., forward-walking) slave automaton, the multiplicity at in (resp., at in ) is bounded by at in , and 6. BC6
every backward-walking (resp., forward-walking) slave automaton active at position , accumulates over (resp., ) a value greater or equal to the value accumulated over (resp., ).
The above conditions simply state that a barrier terminates all slave automata active and reduces their multiplicities, i.e., the multiplicity of backward-walking slave automata, which are invoked in the suffix is reduced by word (BC1) and the multiplicity of forward-walking slave automata invoked in prefix is reduced by word (BC2). Property BC3 ensures that inserting a barrier at position does not change the run essentially (except for it only reduces the multiplicities of slave automata). These properties and the bound on the length of barriers (BC4) allow us to reduce the multiplicity of slave automata along words. Properties BC5, BC6 are necessary to show that such a reduction of multiplicities does not increase the values of words.
Lemma 21**.**
Let be a deterministic -automaton of finite width with bidirectional slave automata. Then, for every word , at almost every position a barrier exists.
Proof.
Let be a word. We consider the unique run of on and refer to the positions in and the corresponding positions in the run, i.e., we refer to “the configuration at in ” as the unique configuration of at while processing word .
We define the profile at position in as a pair of the configuration at and multiplicities at bounded by , defined for every as . Let positions in such that every profile that occurs infinitely often in occurs between and . Next, we define as the minimal position past such that every backward-walking slave automaton invoked past terminates at some position past , i.e., any backward-walking slave automaton invoked past terminates before it reaches . The NWA has finite width and hence such exists. We show that there exists a barrier in for every position .
Construction of a barrier at position . Let . We pick positions such that all slave automata active at terminate within and the profiles at positions and letters in are the same. Since such exist. Observe that satisfies first three conditions of the barrier definition, but it does not have to satisfy the remaining conditions. Consider word . It satisfies all barrier conditions except for BC4. We take and transform it into a barrier by removing certain subwords corresponding to cycles in , i.e., subwords such that at the beginning and at the end of this subword is in the same configuration. Removal of such subwords does not change runs of the master automaton or slave automata in the suffix of the word. However, to show condition RC5 we need to ensure that the removal operation does not change the profile, i.e., the profiles at positions and in are the same as the profile at in .
We define an extended configuration in a finite word at position as the pair of the configuration at and the equivalence relation on states of slave automata active at position such that if and only if either
- •
are states of forward-walking slave automata and slave automata in states and at position reach the same state at the end of word , or
- •
are states of backward-walking slave automata and slave automata in states and at position reach the same state at the beginning of word .
The slave automata that do not reach the end o word (resp., the beginning of ) are in the same equivalence class . Given two positions in with the same extended configuration, we define transformation from to as a function from the set of equivalence classes of (which is equal ) into itself such that
- •
for a state of a forward-walking slave automaton, the equivalence class is transformed into a class if some slave automaton in state at position reaches state from at position , and
- •
for a state of a backward-walking slave automaton, the equivalence class is transformed into a class if some slave automaton in state at position reaches state from at position .
Due to determinicity of , the transformation is, indeed, a function and a permutation.
Now we describe the subword removal process. First, we mark positions in at which each of slave automata active at position in terminates. Observe that these belong to the interval . Now, starting with word we iteratively remove subwords such that (a) the extended configurations at the first and the last position of are the same, (b) the transformation between these positions is the identity, and (c) does not contain any position corresponding to positions . The last word, from which no such a subword can be removed is . We show that is a barrier.
Word is a barrier. The positions at which slave automata are terminated are not removed from and hence satisfies conditions BC1, BC2. Removal of a word satisfying (a) and (b) preserves profile at every step and hence condition BC3 holds for .
Condition BC4 follows from the fact that there are at most different extended configurations. Transformations are permutations of equivalence classes, i.e., they are permutations of sets of size at most . Therefore, if , then among positions with the same extended configuration there exists a pair such that the transformation between these positions is the identity. Thus, words of length at least contain a subword satisfying (a) and (b). Furthermore, words of length at least , contain a subword satisfying (a), (b) and (c). Therefore, the length of is bounded by .
We show that satisfies BC5. Let be a state of some slave automaton and let be the multiplicity of in at position and be multiplicities of in at positions and respectively. Observe that (a) and (b) imply the the profiles at positions and in are the same as the profile at in . It follows that . Now, if is a state of a backward-walking slave automaton, then all such automata active at position in have been invoked in and hence . It follows that . Otherwise, similarly if is a state of a forward-walking slave automaton we have and . Therefore, condition BC5 holds.
Finally, word satisfies condition BC6. Consider a backward-walking slave automaton active at position in . This automaton terminates before position and hence it accumulates equal values on subwords and . Now, word results from by deletion of certain subwords, while it preserves positions corresponding to termination of slave automata. Moreover, the deletion process only shortens runs; the transitions taken by slave automata correspond to the transitions in the original run. Thus, accumulates over a value smaller or equal to the value accumulated over . The case of forward-walking slave automata is symmetric. ∎
Now, we show the key property of barriers, i.e., they decrease the partial sum of values if inserted at a position where exponentially many slave automata accumulate exponential values. This enables us to reduce the emptiness problem for finite-width NWA to the bounded-width case.
Lemma 22**.**
Let be a deterministic -automaton with bidirectional slave automata. Let be the maximal weight of slave automata of . Let be a word and let be a barrier for at position . If more than slave automata accumulate the value exceeding past in (i.e, for backward-walking slave automata it is at ), then for almost all , the sum of values returned by slave automata invoked up to in is greater than the sum of values of returned by slave automata invoked up to in .
Proof.
Let be the first position past such that all backward-walking slave automata invoked past terminate before position . We show that the partial sum of values returned by slave automata invoked up to in is greater than the partial sum of values of returned by slave automata invoked up to in . This argument works for every . The partial sum of values returned by slave automata invoked up to in consists of the sum of weights: (1) accumulated by slave automata before they reach position , and (2) accumulated by slave automata after they reach position . In (1) we include values of backward-walking (resp., forward-walking) slave automata that do not reach position . Let be the set of states of slave automata active at position in . For , we define (resp., ) as the multiplicity at (resp., the value accumulated past ) in by slave automata that are in the state at . Observe that (2) = .
The partial sum of values returned by slave automata invoked up to in consists of four components, which are the sum of weights (1’) aggregated by slave automata before they reach any of positions , (2’a) aggregated over positions by backward-walking slave automata invoked past and forward-walking slave automata invoked before , (2’b) aggregated past positions by slave automata invoked on positions , i.e., the values aggregated by backward-walking slave automata over and forward-walking slave automata over , and (2’c) aggregated over positions by slave automata invoked on positions .
We observe that (1)(1’) and we show that (2) (2’a)+(2’b)+(2’c). Observe that (2’c) is bounded by . In (2’a), the multiplicities of slave automata are the same as the multiplicities of the corresponding slave automata active at in while the values they accumulate are bounded by the minimum of the values accumulated within and . Indeed, consider a backward-walking slave automaton, which is in state at position in . The multiplicity of such automata is equal to the multiplicity of slave automata that are in state at position in . Moreover, due to condition BC6 satisfied by , the value which such an automaton accumulates along is bounded by the value it accumulates at . Also, such an automaton terminates within and hence its value is bounded by as well. The similar reasoning holds for forward-walking slave automata active at position in and hence (2’a) is bounded by . In (2’b), slave automata accumulate the same values as the corresponding slave automata in , but multiplicities are bounded by and the values of the corresponding slave automata at position in . Indeed, consider a backward-walking slave automaton, which is in state at position in . Since the profile at in and is the same, the multiplicity of such automata is bounded by the multiplicity of slave automata that are in state at position in . Moreover, all backward-walking slave automata active at position in have been invoked within positions and hence the sum of their multiplicities is bounded by . Since , a backward-walking slave automaton in state at position in accumulates value at past position , i.e, the value which accumulates the same automaton in . Similar estimates hold for forward-walking slave automata past position . Therefore, (2’b) is bounded by , where . Due to condition BC5 of barriers, for every we have . Now, we estimate , which equals . We partition into , the states of slave automata at position , which accumulate the value at least past position in , and the reaming states from . Then, (2) - (2’a)+(2’b)+(2’c) . Since and , we get (2) - (2’a)+(2’b)+(2’c) . Recall that and for every we have . Therefore, and hence (2) (2’a)+(2’b)+(2’c). This concludes the proof that insertion of a barrier decreases the partial sum.
∎
Using the above lemma we can reduce the emptiness problem for finite-width -automata with bidirectional slave automata to the bounded-width case.
Lemma 23**.**
Let be a deterministic -automaton of finite width with bidirectional slave automata. There exists a deterministic -automaton over an extended alphabet with bidirectional slave automata of width bounded exponentially in , such that the emptiness problems for and coincide, i.e., . The size of is .
Proof.
We define an exponential size -automaton with bidirectional slave automata of width bounded by exponentially in such that simulates a subset of runes of which satisfy the following condition (): at almost every position , among slave automata active at , at most will accumulate value greater than . Next, we show that for every run of there exists a run satisfying () of at most the same value. It follows that the emptiness problems for and coincide.
Definition of . The alphabet consists of and additional marking letters described below. First, the automaton invokes only dummy slave automata before the initiation marking. Past initial marking the master automaton keeps track of the number of invoked slave automata and rejects if the number of slave automata exceeds . Second, we modify each slave automaton of so that they work only as long as they can accumulate the value exceeding , where is the maximal weight among all slave automata of . In particular, slave automata, which accumulate the value below , are invoked for a single transition only. We encode in the alphabet whether a slave automaton is invoked for a single transition and the weight of this transition. Moreover, we encode in the alphabet that slave automata in state ought to terminate as in the following run they accumulate the value below . The master automaton checks whether the external markings are correct. These constructions involve a single exponential blow up of the master automaton, slave automata and the alphabet. Observe that accepting runs of correspond to accepting runs of , which satisfy condition (). The values of the corresponding runs are the same. Now, we need to show that while computing the infimum over all accepting runs of , we can restrict ourselves to runs satisfying ().
The emptiness problems for and coincide. Since simulates a subset of runs of we have . We show how to transform any word of into a word whose unique run satisfies (*), which means that is can be simulated by , and whose value does not exceed the value of . It follows that .
Let be a word accepted by . Let be a position such that on every position in a barrier exists (Lemma 21). We start with , word and . We iteratively at step , pick first position at which more than slave automata accumulate the values exceeding and we insert a barrier at position . Barrier exists as a barrier for at the corresponding position. Then, we start the next iteration with word and . Observe that iterations past change only positions past in words , i.e., all words share the prefix . Thus, there exists the limit word , which is the result of the iterative process. We argue that the resulting word satisfies () and its value does not exceed the value of . First, we show that satisfies ().
Let be a barrier at position in and let . The forward-walking slave automata active at in are terminated within in and hence accumulate the value below in , where is the maximal weight of slave automata of . The number of forward-walking slave automata active between positions and which are not terminated within is bounded by . Therefore, at every position between and in , at most forward-walking slave automata accumulate the value exceeding . The similar argument applies to backward-walking slave automata, which shows that at positions to condition (*) is satisfied.
It remains to comment on the value of . Barriers inserted in the iterative process satisfy conditions of Lemma 22, and hence the partial sums decrease from to and so on. It follows partial sums in are bounded by partial sums in every word and hence the value of does not exceed the value of . ∎
Algorithm. Let be a non-deterministic finite-width -automaton with bidirectional slave automata. Lemma 19 reduces the emptiness problem of to the emptiness problem of , which has the same properties as , but it is deterministic. The reduction takes exponential time and produces an exponential-size automaton, while it does not change the number of configurations. Therefore, the value of for and is the same. Next, Lemma 23 reduces the emptiness problem for to the emptiness problem of which is a deterministic -automaton with bidirectional slave automata and the width of is linear in , i.e., it is exponential in . The size of is , i.e., it is exponential in . Therefore, the emptiness problem for can be solved in polynomial space in (Theorem 17) and in the exponential space in the size of .
B.3 The proof of Theorem 14
In the finite-automata framework, the pumping lemma is a standard tool to show inexpressibility results. It is difficult to state a pumping lemma for NWA as their state space is infinite. While there is finitely many configurations of NWA, the multiplicity of running slave automata is unbounded. We consider the graph of configurations of an NWA to reduce the infinite-space case to the finite-state case.
Recall that we assume that slave automata do not have outgoing transitions from accepting states. We also assume (without loss of generality) that initial states of slave automata do not have ingoing transitions.
Graph of configurations. Let be an NWA with bidirectional slave automata over an alphabet . We define the graph of configurations of an NWA as a -labeled graph whose nodes are configurations of . For , there exists an -labeled edge from configuration to if and only if
- •
the master automaton of has a transition invoking a slave automaton in an initial state ,
- •
for , states are partitioned into states of backward-walking slave automata and forward-walking slave automata ,
- •
there exists a function , which transforms all non-final states from onto such that for every tuple is a transition of some slave automaton,
- •
there exists a function , which transforms all non-final states from onto such that for every tuple is a transition of some slave automaton, and
- •
if is forward-walking ; otherwise .
Paths in are related to simple runs of . Consider a simple run of . Its sequence of configurations is an infinite path in . Conversely, given a path in starting in the initial configuration , we can specify regular conditions ensuring (a) existence of a simple run corresponding to and (b) existence of a simple accepting run corresponding to . Regularity of these conditions follows from the fact that unweighted parts of runs of can be simulated by an alternating Büchi automaton. This automaton checks whether runs of all slave automata are finite; this suffices to ensure that a path corresponds to a valid simple run. It can also check acceptance condition, i.e., whether runs of all slave automata terminate in accepting states and the master automaton visits some accepting state infinitely often.
The graph of configurations of enables us to construct accepting runs of with desired properties. Having an accepting run of with a sequence of configurations such that is a cycle in the graph of configurations of , we know that for every there exists an accepting run of whose sequence of configurations is . This is a key observation used in the following lemma.
See 13
Proof.
We show (i) in detail and next we comment on (ii). Suppose that is a -automaton with forward-walking slave automata which computes DCP (Example 3) restricted to the alphabet . First, we show that in the graph of configurations of there exist two cycles such that is an -labeled cycle in which at least one (non-dummy) slave automaton is invoked, and is an -labeled cycle in which takes only silent transitions, i.e., it invokes only slave automata that immediately accept returning no value. Next, we use to construct of a run on some word such that the value of is smaller than DCP of , which contradicts the assumption that computes DCP.
Existence of and . Let be greater than the number of configurations of and let . To simplify the calculations, we denote by some natural number from interval . For example, we write .
Consider a word . DCP of is . Let be a run of on of the value . We can assume that is simple (Lemma 19). In every block in , there exist positions such that the configurations in at and are the same and . We remove these parts of . The resulting sequence is a run of on some word such that are at most . Observe that DCP of is at least and hence the value of is at least . However, the partial sums of the values returned by slave automata in are bounded by the corresponding partial sums in . Therefore, the value of increases due to the fact that the removed parts of contain invocations of slave automata returning small values and removal of these parts of increase partial averages. It follows that infinitely often at least one (non-dummy) slave automaton is invoked over the block . Consider the sequence of configurations of run . There exists infinitely many subsequences of , which correspond to transitions over letters and satisfy: (A1) the first and the last configuration of is the same, (A2) along at least one slave automaton is invoked and (A3) the length of is bounded by . Such a sequence corresponds to an -labeled cycle in the graph of configurations of of length at most . There are finitely many such cycles and hence there exists a cycle satisfying condition (A1), (A2) and (A3) which occurs infinitely often in .
In a similar we show that contains infinitely often a subsequence , which corresponds to transitions over letters , such that (B1) the first and the last configuration of is the same, (B2) slave automata invoked along return no value (correspond to silent transitions), and (B3) the length of is bounded by . To see that, we divide runs and into blocks separated by letter . In transformation from to , the average number of invocations of (non-dummy) slave automata per block decreases by at most . Yet, the value of increases by at least w.r.t. the value of . Therefore, the average number of invoked slave automata per block cannot exceed in . It follows that at most non-dummy slave automata are invoked on average in a block of letters . Thus, there exists infinitely many occurrences of subsequences of satisfying (B1), (B2) and (B3), and hence there exists a -labeled cycle satisfying conditions (B1), (B2) and (B3), which occurs infinitely often in .
Observe that there exist infinitely many subwords of such that in the corresponding positions in occur both and . Thus, there exists a path in the graph of configurations of such that leads from the last configuration of to the first configuration of over letters . Moreover, all slave automata in terminate after finite number of steps, while and occur infinitely often. Therefore, there exists a path from the first configuration of to the last configuration of over letters such that (C1) at least one transition is over letter , and (C2) all slave automata active at the first configuration of are terminated before the end of , (C3) the master automaton of visits an accepting state within . Let (resp., ) be a subword of at which configurations of form the sequence (resp., ). Next, we show the construction of using , and .
The construction of . Let be natural numbers, which we fix later. We define as some simple accepting run that corresponds to the sequence of configurations , where is a sequence of configurations from an initial configuration to the first configuration of . Such a run exists as we can ensure that at positions corresponding to all slave automata terminate in accepting states and the master automaton visits an accepting state. Let be a word at which there exists a run with the sequence of configurations . We define . The run is an accepting run on . Observe that DCP of exceeds . However, we show that the value of is smaller. Run is a lasso and its limit average is the average of the cycle, which corresponds to the average of excluding values of slave automata invoked in the second occurrence of . The non-dummy slave automata are invoked only in and in . All slave automata invoked within this cycle terminate by the end of it, and hence (a) the values of slave automata invoked in are bounded by the length of the cycle multiplied by , the maximal weight of , i.e., , and (b) the values of slave automata invoked in are bounded by . We have , however there are at most slave automata invoked in , which accumulate value at most . The remaining slave automata are invoked in and there are at least of them. Thus, the average value of the cycle is at most . Now, for , we have and . Let , then the average of the cycle, which is bounded by , is smaller than . However, DCP of exceeds , which contradicts the fact that computes DCP.
Backward-walking slave automata. The proof for backward-walking slave automata is similar. We consider numbers and a word ; we show that there exist cycles in , with similar properties to from the forward case. Moreover, there exist sequences of configurations from the last configuration of to the first configuration of , and from the last configuration of to the first configuration of , with the properties similar to (C1), (C2) and (C3). To show (C2) we use the fact that and occur infinitely often and has finite-width, and hence for every position there exists position such that every (backward-walking) slave automaton active at position terminates before (i.e., at some position within ). Next, we construct from a run of the value lower than DCP of the corresponding word. The construction is virtually the same as in the forward case. ∎
Appendix C Proofs from Section 6
See 16
Proof.
(1): Assume that (*) is satisfied. Consider an accepting run with configuration occurring infinitely often. Let be a position at which configuration occurs. Let be the last position at which any automaton from is invoked. Consider the run resulting from inserting cycle repeated times at position in . The only slave automata active past position , which has been invoked before are the automata from . Therefore, the partial sum of values returned by slave automata up to position decreases by at least , where is the value of forward slave automata invoked before , which terminate in . The number of slave automata invoked before does not change and hence by picking large enough we can decease the partial average up to arbitrarily. We can apply such a pumping step at every position with configuration obtaining a run whose limit infimum of partial averages diverges to .
(2): : Assume that there exists a cycle in the graph of configurations of and a restriction such that and there exists an accepting run with configuration occurring infinitely often. Let be a position at which configuration occurs. We insert at position and obtain run . Let be the last position in such that and all automata active at position , which are not in , are invoked before . Due to presence of backward-walking slave automata can be strictly grater than . Consider the run resulting from inserting cycle repeated times at position in . Then, the partial average up to position is given by the expression , where
- •
is the partial sum of values returned by slave automata invoked up to in run ,
- •
is the number of slave automata invoked up to in run ,
- •
and is the number of slave automata invoked in , and
- •
is the value accumulated by backward-walking slave automata invoked past , which terminate within interval .
Now, by taking large enough we can bring the partial average arbitrarily close to . Using that and simple iteration, we can construct an accepting run of the value .
: Assume that does not satisfy () from (1). It follows that in every accepting run of for almost every position , slave automata invoked before , accumulate past the value exceeding value defined as , where is the maximal weight occurring in and is the number of configurations of . Indeed, if there exists such a position , there exists a cycle past which we can pump to lower the sum of value returned by slave automata invoked before . Hence, existence of infinitely many such positions , implies that condition () holds.
Let be an accepting run of of value . Consider . There exists a prefix of up to position such that the partial average of values returned by slave automata up to is at most , the sum of values accumulated by slave automata invoked before exceeds and and the number of slave automata before exceeds . Then, the partial average of the values accumulated by slave automata invoked before within positions is at most .
Now, we can decompose the prefix up to into simple cycles one by one, i.e., having a prefix of up to position , we pick a simple cycle, remove it from and repeat the process. We terminate when we end up with run which has no simple cycle to remove; the remaining run has length bounded by the number of configurations and therefore its sum of values is greater than . Thus, the partial average of the values accumulated by slave automata invoked before within positions equals (a) the weighted average of average weights of simple cycles excluding backward-walking slave automata invoked past , plus (b) the average of bounded by . It follows that there exist a simple cycle and a restriction such that ; otherwise the weighted average in (a) exceeds , which contradicts the choice of prefix of .
However, there are infinitely many , while there are finitely many simple cycles. Therefore, there exist a simple cycle and a restriction such that . ∎
See 17
Proof.
It suffices to show that conditions from Lemma 16 can be checked (a) in logarithmic space for constant and unary weights, (b) polynomial time for constant and binary weights, and (c) polynomial space for given in unary. Observe that these conditions reduce to weighted reachability, which can be computed in logarithmic space in the size of the graph of -configurations of , provided that weights can fit in logarithmic space. Otherwise, if weights are represented in binary and are of length greater than logarithmic in the size of the graph, weighted reachability can be implemented using Dijkstra algorithm in polynomial time. The size of the graph of -configurations is polynomial in the size of and exponential in . Thus, the graph of -configurations of is polynomial if is constant, and exponential if is given in unary. Finally, we comment how to compute the successor relation.
We define a presuccessor relation on -configurations as follows. We have if and only if for some the master automaton of has a transition invoking a slave automaton in an initial state , and for every component one of the following holds
- •
is a non-final state of a forward-walking slave automaton and is a transition of this automaton,
- •
is a final state of a forward-walking slave automaton, and or ,
- •
is a non-final state of a backward-walking slave automaton and is a transition of this automaton,
- •
is a final state of a backward-walking slave automaton, and or ,
if is forward-walking (resp., backward-walking) slave automaton, then for exactly one component we have (resp., ). Observe that encodes a local consistency of transitions of the master and slave automata. A sequence of -configurations consistent with satisfying the following conditions (a) and (b) corresponds to an accepting simple run. These conditions are: (a) the master automaton visits one of its accepting states infinitely often, and (b) every slave automaton terminates after finitely many steps. Now observe that the successor relation defined in Section 6 is the presuccessor relation restricted to -configurations , which are (1) reachable through from the initial configuration and (2) a cycle w.r.t. satisfying conditions (a) and (b) is reachable through from . Indeed, for such configurations satisfying there exists a sequence of -configurations consistent with , which corresponds to an accepting run. It follows that the successor relation in the graph of -configurations can be computed based on reachability w.r.t. presuccessor relation, which is computable in logarithmic space. ∎
The reference list from the paper itself. Each links out to its DOI / PubMed record.
- 1[1] Shaull Almagor, Udi Boker, and Orna Kupferman. Discounting in LTL. In TACAS, 2014 , pages 424–439, 2014.
- 2[2] Shaull Almagor, Udi Boker, and Orna Kupferman. Formally reasoning about quality. J. ACM , 63(3):24:1–24:56, 2016.
- 3[3] Rajeev Alur, Loris D’Antoni, Jyotirmoy V. Deshmukh, Mukund Raghothaman, and Yifei Yuan. Regular functions and cost register automata. In LICS 2013 , pages 13–22, 2013.
- 4[4] Mikołaj Bojańczyk and Thomas Colcombet. Bounds in w-regularity. In 21th IEEE Symposium on Logic in Computer Science (LICS 2006), 12-15 August 2006, Seattle, WA, USA, Proceedings , pages 285–296, 2006.
- 5[5] Udi Boker, Krishnendu Chatterjee, Thomas A. Henzinger, and Orna Kupferman. Temporal specifications with accumulative values. ACM TOCL , 15(4):27:1–27:25, 2014.
- 6[6] Benedikt Bollig, Paul Gastin, Benjamin Monmege, and Marc Zeitoun. Pebble weighted automata and transitive closure logics. In ICALP 2010, Part II , pages 587–598. Springer, 2010.
- 7[7] Patricia Bouyer, Nicolas Markey, and Raj Mohan Matteplackel. Averaging in LTL. In CONCUR 2014 , pages 266–280, 2014.
- 8[8] Patricia Bouyer, Nicolas Markey, Mickael Randour, Kim Guldstrand Larsen, and Simon Laursen. Average-energy games. In Gand ALF 2015. , pages 1–15, 2015.
