On weighted first-order logics with discounting

Abstract

We introduce a linear temporal logic and a first-order logic in the weighted setup of the max-plus semiring with discounting parameters in $[0,1)$. Furthermore, we define $\omega \hbox {-}d$-star-free series and counter-free weighted Büchi automata. We show that the classes of series definable in fragments of the weighted linear temporal logic and first-order logic, the class of $\omega \hbox {-}d$-star-free series, and a subclass of $\omega \hbox {-}d$-counter-free series coincide. This extends a fundamental result, for first-order logic theory, to series over the max-plus semiring with discounting.

1 Introduction

Linear temporal logic (LTL for short) and its variations play an important role in model checking, especially for practical applications (cf. for instance [2, 19, 30]). LTL definable languages are known to coincide with languages definable by first-order (FO for short) logic, star-free languages, aperiodic languages and counter-free languages. More interestingly, this result holds for finitary languages, i.e., languages over finite words, as well as for infinitary languages (over infinite words). These different characterizations of the same class of languages were proved by several authors; the results for infinite words required more sophisticated techniques than the ones for finite words. In order to avoid a long list of relative references, we refer the reader to the excellent survey of Diekert and Gastin [7] (and the references of that paper).

Here, we establish the above result (excluding the aperiodic characterization) in the weighted setup of the max-plus semiring. Our motivation lies in the last years’ increasing interest in the development of model checking tools incorporating quantitative features. This need, but also the deep theoretical interest, led several researchers to consider quantitative versions of logics. The first achievement was done by Droste and Gastin in [8] (cf. also [9]), where they introduced a weighted MSO logic over finite words and established the expressive equivalence of a fragment of weighted MSO sentences and weighted automata over semirings, i.e., an Elgot and Büchi type result. Weighted versions of MSO logics were investigated also for other structures like infinite words, trees, pictures, traces, texts. For the corresponding results and/or references, we suggest Chapters 5, 9, 10, 12 of [10]. Another extension, of weighted MSO logics, concerns the algebraic structure where the weights are taken from. More precisely, in [14] the authors considered arbitrary bounded lattices and recently, in [12], a weighted MSO logic was investigated over structures with operations like average, limit superior, limit inferior, limit average or discounting.

A quantitative version of the LTL appeared for the first time in [18]. In that paper, the authors considered a weighted LTL and weighted automata over De Morgan algebras and presented the translation of such an LTL formula to a weighted automaton. Then, in [14], the authors considered weighted MSO and FO logic, and weighted LTL over arbitrary bounded lattices and they showed the aforementioned equivalence for FO and LTL definable, star-free, and aperiodic series. The considered underlying structure provides an important property: every recognizable (resp. $\omega$-recognizable) series is a recognizable (resp. $\omega$-recognizable) step function. Similarly, any aperiodic series is an aperiodic step function. The “step function” characterization, on the positive side, permits elegant proofs, but on the other side, restricts the series to a finite image. In [21] the author introduced a weighted LTL with discounting over the max-plus semiring $\mathbb {R}_{\max }=(\mathbb {R}_{+}\cup \{-\infty \},\max ,+,-\infty ,0)$ and established the translation of weighted LTL formulas to weighted Büchi automata with discounted behavior. The max-plus semiring has important practical applications, especially to dynamic programming and discrete event systems (cf. for instance [1, 17]). On the other hand, the discounting method has been incorporated in automata and tree automata theory [3, 5, 13, 22], in model checking [6, 15], in game theory [27] as well as in equational theories [16].

In this paper, we consider the weighted LTL of [21] and a slight expansion of the weighted FO logic with discounting (the discounting parameters will be numbers in $[0,1)$), as it is obtained by [13], by adding a discounted first-order existential quantifier. Moreover, we introduce $d$-star-free and $\omega \hbox {-}d$-star-free series, and counter-free weighted automata as well as counter-free weighted Büchi automata. The main result of the paper shows that series definable by formulas in a fragment of our weighted LTL, series definable in a fragment of our weighted FO logic, $\omega \hbox {-}d$-star-free series and a subclass of $\omega \hbox {-}d$-counter-free series coincide. Though we present our results and proofs for infinitary series, one can transform them, using even simpler constructions, to the finitary case.

In the sequel, we present the structure of our paper. Except of this section, and the preliminary notions in Sect. 2, we introduce the weighted LTL in Sect. 3. As it is already mentioned, it is the one from [21] but we add a new next operator called boolean since it does not use the discounting parameters in its semantics. Then, we define the semantics of the weighted LTL formulas and introduce the fragments of $U$-nesting and restricted LTL formulas; the first one is included into the latter. An infinitary series definable by a weighted LTL formula in the $U$-nesting (resp. restricted) fragment is called $\omega \hbox {-} ULTL$-$d$-definable (resp. $\omega$-rLTL-$d$-definable).

In Sect. 4, we introduce the weighted FO logic with discounting. In comparison to [13], we add a new existential quantifier. This in fact gives discounted values of the semantics of the formula under the quantifier and it is mostly needed for technical reasons. We show in Sect. 8, that the addition of this quantifier it is not “too much”, in the sense that its addition to the weighted MSO logic with discounting of [13], does not change the expressive equivalence of weighted Büchi automata and weighted MSO logic formulas. We consider a fragment of our weighted FO logic whose formulas are called weakly quantified and the series definable by such formulas $\omega$-wqFO-$d$-definable. The main result of this section states that every $\omega$-rLTL-$d$-definable series is also $\omega$-wqFO-$d$-definable. In fact, the weakly quantified FO logic formula corresponding to a restricted LTL formula uses at most three variables.

In Sect. 5, we deal with the notion of star-freeness in the weighted setup. It is well-known (cf. for instance [7, 20, 24, 28]) that the class of star-free languages over an alphabet $A$ is the smallest family of languages over $A$ which contains $\emptyset$, the singleton $\{a\}$ for every $a\in A$, and which is closed under finite union, complementation and concatenation. Furthermore, the class of $\omega$-star-free languages over $A$ is the closure of the empty set under the operations of union, complement and concatenation with star-free languages on the left. In our case, for series, we faced the problem of how to determine a corresponding class which captures the aforementioned features. To be precise, the problem is that the application of the star-operation (whenever it is permitted) to star-free languages is implemented by the other operations. But in the setup of series over the max-plus semiring (or over an arbitrary semiring) the complement operation is not “too strong”. This means, that we had to involve somehow the $+$-iteration operation, of course under restrictions. Hence, we defined the class of $d$-star-free series as the least class of series which contains the monomials and is closed under the operations of maximum, sum, Cauchy sum $(+_{d})$, complement, and $+$-iteration applied to series of the form $\max _{a\in A}\big (\big (k_{a}\big )_{a}\big )$ where $k_{a}\in \mathbb {R}_{\max }$. We could extend the application of the $+$-iteration operation to series whose support is a finite pure code (cf. [26]) but then we could not prove the equivalence to the other characterizations. There is an alternative definition for the class of star-free languages, using the concept of bounded synchronization delay (instead of complementation) (cf. [24] and our Sect. 7). But a corresponding definition for series is not convenient for our scope. In our main result of this section, we show that the class of $\omega$-wqFO-$d$-definable series is contained into the class of $\omega \hbox {-}d$-star-free series.

Section 6 contains the theory of counter-free weighted and counter-free weighted Büchi automata. Our models are nondeterministic. Recall that a finite (resp. Büchi) automaton is counter-free if for every state $q$, finite word $w$, and $n\ge 1$, the existence of a path from $q$ to $q$ with label $w^{n}$ implies the existence of a path from $q$ to $q$ with label $w$. In our weighted models we had also to take care of the weights of the paths. Hence, we assumed that the maximum weight of the paths from $q$ to $q$ with label $w^{n}$ is the same with the weight of the path from $q$ to $q$ with label $w^{n}$ using $n$-times the $w$-labelled loop from $q$ to $q$ with the maximum weight. We consider also simple counter-free weighted (resp. Büchi) automata whose initial distribution assigns only one weight $\ne -\infty$, and for every $a\in A$ there is at most one weight $\ne -\infty$ assigned to every $a$-labelled transition. An infinitary series is called almost simple if it is of the form $\max _{1\le i\le n}\left( r_{1}^{(i)}+_{d}\ldots +_{d}r_{m_{i}}^{(i)}\right)$ where, for every $1\le i\le n,\; r_{1}^{(i)},\ldots ,r_{m_{i}-1}^{(i)}$ are simple $d$-counter-free series and $r_{m_{i}}^{(i)}$ is a simple $\omega \hbox {-}d$-counter-free series. We show that the class of $\omega \hbox {-}d$-star-free series is contained into the class of almost simple $\omega \hbox {-}d$-counter-free series.

In Sect. 7, we close the cycle, namely we show that the class of almost simple $\omega \hbox {-}d$-counter-free series is contained into the class of $\omega \hbox {-} ULTL$-$d$-definable series. For this result, we needed some technical matter on our weighted LTL.

Finally, in Sect. 8 we show that the addition of the discounted first-order quantifier to the weighted MSO logics of [13] does not change the expressive power of the weighted restricted MSO sentences.

We assume the reader to be familiar with the concepts of FO logic, LTL, star-freeness, and counter-freeness and their expressive equivalence (cf. for instance [7, 24]).

2 Preliminaries

Let $A$ be an alphabet, i.e., a finite non-empty set. As usually, we denote by $A^{*}$ the set of all finite words over $A$ and $A^{+}=A^{*} \setminus \{\varepsilon \}$, where $\varepsilon$ is the empty word. The set of all infinite sequences with elements in $A$, i.e., the set of all infinite words over $A$, is denoted by $A^{\omega }$. A finite word $w=a_{0}\ldots a_{n-1}$, where $a_{0},\ldots ,a_{n-1}\in A$ ($n\ge 1$), is written also as $w=w(0)\ldots w(n-1)$ where $w(i)=a_{i}$ for every $0\le i\le n-1$. For every $0\le i\le n-1$, we denote by $w_{<i}$ (resp. $w_{\le i}$) the prefix $w(0)\ldots w(i-1)$ (resp. $w(0)\ldots w(i)$) of $w$ and by $w_{>i}$ (resp. $w_{\ge i}$) the suffix $w(i+1)\ldots w(n-1)$ (resp. $w(i)\ldots w(n-1)$) of $w$. For every infinite word $w=a_{0}a_{1}\ldots$ which is written also as $w=w(0)w(1)\ldots$, the words $w_{<i},w_{\le i},w_{>i},w_{\ge i}$ are defined in the same way, with the suffixes $w_{>i},w_{\ge i}$ being infinite words.

A semiring $(K,+,\cdot ,0,1)$ is an algebraic structure such that $(K,+,0)$ is a commutative monoid, $(K,\cdot ,1)$ is a monoid, $0\ne 1,\,\cdot$ is both left- and right-distributive over $+$, and $0\cdot k=k \cdot 0=0$ for every $k\in K$. We denote the semiring simply by $K$ if no confusion arises. The semiring $K$ is called commutative if the monoid $(K,\cdot ,1)$ is commutative. We shall denote, as usual, by $\mathbb {B=(\{} \mathbf {0},\mathbf {1}\},+,\cdot ,\mathbf {0},\mathbf {1})$ the Boolean semiring. In this paper we deal with the max-plus or arctic semiring $\mathbb {R}_{\max }=( \mathbb {R} _{+}\cup \{-\infty \},\max ,+,-\infty ,0)$ where $\mathbb {R} _{+}=[0,\infty )$ and $-\infty +k=-\infty$ for every $k\in \mathbb {R} _{+}\cup \{-\infty \}$. Note that $\mathbb {R}_{\max }$ is commutative. We extend the multiplication of real numbers in $\mathbb {R}_{+}\cup \{-\infty \}$ by letting $k(-\infty )=(-\infty )k=-\infty$ for every $k\in \mathbb {R} _{+}\cup \{-\infty \}$. In the following, sometimes, we shall identify $\mathbb {R}_{\max }$ with $\mathbb {R}_{+}\cup \{-\infty \}$. For every $p\in \mathbb {R}_{+}$ the mapping $\overline{p}: \mathbb {R} _{\max }\rightarrow \mathbb {R}_{\max }$ given by $x\longmapsto p\cdot x$ is an endomorphism of $\mathbb {R}_{\max }$. Conversely, every endomorphism of $\mathbb {R}_{\max }$ is of this form (cf. [11]). The set $End ( \mathbb {R}_{\max })$ of all endomorphisms of $\mathbb {R}_{\max }$ is a monoid with the usual composition mapping as operation and the identity mapping $id$ on $\mathbb {R}_{\max }$ as unit element. We shall alternatively denote the multiplication of $\mathbb {R}_{\max }$ and the composition operation of $End ( \mathbb {R}_{\max })$ also by concatenation.

Let $A$ be an alphabet. A family $d=\left( \overline{d_{a}}\right) _{a\in A}$ of endomorphisms of $\mathbb {R}_{\max }$ with $0\le d_{a}<1$ for every $a\in A$ is called a $d$ -discounting over $A$. For every finite word $w=a_{0}a_{1}\ldots a_{n-1}\in A^{+}$ we shall denote by $\overline{d_{w}}$ the morphism $\overline{d_{a_{0}}d_{a_{1}}\ldots d_{a_{n-1}}}$ and by $\overline{d_{\varepsilon }}$ the identity mapping id on $\mathbb {R}_{\max }.$ We put $d_{w}={\prod \nolimits _{a\in A}}d_{a}^{\left| w\right| _{a}}$ where $\left| w\right| _{a}$ denotes the number of $a$’s in $w.$ Clearly, $\overline{d_{w}}(x)=d_{w}x$ for every $x\in \mathbb {R} _{\max }$ and the mapping $w\mapsto \overline{d_{w}}$ induced by $d$ is a monoid morphism $d:A^{*}\rightarrow End (\mathbb {R}_{\max })$.

Throughout the paper $A$ will denote an alphabet and $d\!=\!(\overline{d_{a}})_{a\in A}$ a $d$-discounting over $A$.

Let $Q$ be a set. A formal series (or simply series) over $Q$ and $\mathbb {R}_{\max }$ is a mapping $s:Q\rightarrow \mathbb {R}_{\max }$. For every $v\in Q$ we write $(s,v)$ for the value $s(v)$ and refer to it as the coefficient of $s$ at $v$. The support of $s$ is the set $supp (s)=\{v\in Q\mid (s,v)\ne -\infty \}$. The series $s$ is called bounded if there is a number $K\in \mathbb {R}_{\max }$ such that $(s,v)\le K$ for every $v\in Q$. The constant series $\widetilde{k}\; (k\in \mathbb {R}_{\max })$ is defined, for every $v\in Q$, by $(\widetilde{k},v) =k$. The characteristic series $0_{P}$ of a set $P\subseteq Q$ is given by $(0_{P},v) =0$ if $v\in P$ and $-\infty$ otherwise. We denote by $\mathbb {R}_{\max }\left\langle \left\langle Q\right\rangle \right\rangle$ the class of all series over $Q$ and $\mathbb {R}_{\max }$.

Let $s,r\in \mathbb {R}_{\max }\left\langle \left\langle Q\right\rangle \right\rangle$ and $k\in \mathbb {R}_{\max }$. The maximum $\max (s,r)$ of $s$ and $r$, the scalar sum $k+s$ of $s$ with $k$, and the sum $s+r$ of $s$ and $r$ are series in $\mathbb {R}_{\max }\left\langle \left\langle Q\right\rangle \right\rangle$ which are defined elementwise by $(\max (s,r),v)=\max ((s,v),(r,v)),\; (k+s,v)=k+(s,v)$, and $(s+r,v)=(s,v)+(r,v)$ for every $v\in Q$. Abusing notations, if $P\subseteq Q$, then we shall identify the restriction $s|_{P}$ of $s$ on $P$ with the series $s+0_{P}$. It is a folklore result that the structure $\left( \mathbb {R}_{\max }\left\langle \left\langle Q\right\rangle \right\rangle ,\max ,+,\widetilde{-\infty },\widetilde{0}\right)$ is a commutative semiring. In our paper, we work with the semirings $\mathbb {R} _{\max }\left\langle \left\langle A^{*}\right\rangle \right\rangle$ and $\mathbb {R}_{\max }\left\langle \left\langle A^{\omega }\right\rangle \right\rangle$ of finitary and infinitary series over $A$ and $\mathbb {R}_{\max }$, respectively.

Let $B$ be another alphabet and $h:A^{*}\rightarrow B^{*}$ a strict alphabetic homomorphism, i.e., $h\left( a\right) \in B$ for every $a\in A$. Then $h$ can be extended, in the natural way, to a mapping $h:A^{\omega }\rightarrow B^{\omega }$ by letting $h(w)=(h(w(i)))_{i\ge 0}$ for every $w\in A^{\omega }$. Moreover, $h$ is extended to a mapping $h: \mathbb {R}_{\max }\left\langle \left\langle A^{*}\right\rangle \right\rangle \rightarrow \mathbb {R}_{\max }\left\langle \left\langle B^{*}\right\rangle \right\rangle$ as follows. For every $s\in \mathbb {R} _{\max }\left\langle \left\langle A^{*}\right\rangle \right\rangle$ the series $h(s)\in \mathbb {R}_{\max }\left\langle \left\langle B^{*}\right\rangle \right\rangle$ is given by $(h(s),u)=\max _{w\in h^{-1}(u)}((s,w))$ for every $u\in B^{*}$. Similarly, $h$ is extended to partial mapping $h: \mathbb {R} _{\max }\left\langle \left\langle A^{\omega }\right\rangle \right\rangle \rightarrow \mathbb {R}_{\max }\left\langle \left\langle B^{\omega }\right\rangle \right\rangle$ which is defined for every bounded series $s\in \mathbb {R} _{\max }\left\langle \left\langle A^{\omega }\right\rangle \right\rangle$ by $h(s)\in \mathbb {R}_{\max }\left\langle \left\langle B^{\omega }\right\rangle \right\rangle$ with $(h(s),u)=\sup _{w\in h^{-1}(u)}((s,w))$ for every $u\in B^{\omega }$. If $r\in \mathbb {R}_{\max }\left\langle \left\langle B^{*}\right\rangle \right\rangle$ (resp. $r\in \mathbb {R} _{\max }\left\langle \left\langle B^{\omega }\right\rangle \right\rangle$), then the series $h^{-1}(r)\in \mathbb {R} _{\max }\left\langle \left\langle A^{*}\right\rangle \right\rangle$ (resp. $h^{-1}(r)\in \mathbb {R}_{\max }\left\langle \left\langle A^{\omega }\right\rangle \right\rangle$) is determined by $(h^{-1}(r),w)=(r,h(w))$ for every $w\in A^{*}$ (resp. $w\in A^{\omega }$).

3 Weighted LTL with discounting

The weighted linear temporal logic (weighted LTL for short) with discounting was introduced by Mandrali in [21]. In this paper, we consider a slightly extended version of that logic, namely, we equip the logic of [21] with an alternative next operator which does not involve the discounting parameter. For every letter $a\in A$ we consider a proposition $p_{a}$ and we let $AP =\{p_{a}\mid a\in A\}$. As usually, for every $p\in AP$ we identify $\lnot \lnot p$ with $p.$

Definition 1

The syntax of formulas of the weighted LTL with discounting over $A$ and $\mathbb {R}_{\max }$ is given by the grammar

$$\begin{aligned} \varphi \,{:}{:}{=}\,k\mid p_{a}\mid \lnot \varphi \mid \varphi \vee \varphi \mid \varphi \wedge \varphi \mid \bigcirc _{b}\varphi \mid \bigcirc \varphi \mid \varphi U\varphi \mid \square \varphi \end{aligned}$$

where $k\in \mathbb {R}_{\max }$ and $p_{a}\in AP$.

We shall denote by $LTL (\mathbb {R}_{\max },A)$ the set of all such weighted LTL formulas $\varphi$. We represent the semantics $\left\| \varphi \right\|$ of formulas $\varphi \in LTL (\mathbb {R}_{\max },A)$ as infinitary series in $\mathbb {R}_{\max }\left\langle \left\langle A^{\omega }\right\rangle \right\rangle$.

Definition 2

Let $\varphi \in LTL (\mathbb {R}_{\max },A).$ The $d$-semantics of $\varphi$ is a series $\left\| \varphi \right\| \in \mathbb {R}_{\max }\left\langle \left\langle A^{\omega }\right\rangle \right\rangle$ which is defined inductively as follows. For every $w\in A^{\omega }$ we set

• $\left( \left\| k\right\| ,w\right) =k,$

• $\left( \left\| p_{a}\right\| ,w\right) =\left\{ \begin{array}{l@{\quad }l} 0 &{} \text {if }w(0)=a\\ -\infty &{} \text {otherwise} \end{array}\right. ,$

• $\left( \left\| \lnot \varphi \right\| ,w\right) =\left\{ \begin{array}{l@{\quad }l} 0 &{} \text {if }\left( \left\| \varphi \right\| ,w\right) =-\infty \\ -\infty &{} \text {otherwise} \end{array}\right. ,$

• $\left( \left\| \varphi \vee \psi \right\| ,w\right) =\max \left( \left( \left\| \varphi \right\| ,w\right) ,\left( \left\| \psi \right\| ,w\right) \right) ,$

• $\left( \left\| \varphi \wedge \psi \right\| ,w\right) =\left( \left\| \varphi \right\| ,w\right) +\left( \left\| \psi \right\| ,w\right) ,$

• $\left( \left\| \bigcirc _{b}\varphi \right\| ,w\right) =\left( \left\| \varphi \right\| ,w_{\ge 1}\right) ,$

• $\left( \left\| \bigcirc \varphi \right\| ,w\right) =d_{w\left( 0\right) }\left( \left\| \varphi \right\| ,w_{\ge 1}\right) ,$

• $\left( \left\| \varphi U\psi \right\| ,w\right) ={\sup \nolimits _{i\ge 0}}\left( {\sum \nolimits _{0\le j<i}}d_{w_{<j}}\left( \left\| \varphi \right\| ,w_{\ge j}\right) +d_{w_{<i}}\left( \left\| \psi \right\| ,w_{\ge i}\right) \right) ,$

• $(\left\| \square \varphi \right\| ,w)={\sum \nolimits _{i\ge 0}}d_{w_{<i}}\left( \left\| \varphi \right\| ,w_{\ge i}\right) .$

It is not difficult to see, that all the above suprema and infinite sums exist due to the involvement of the discounting parameters.

The eventually operator is defined as in the classical LTL, i.e., by $\Diamond \varphi \,{:}{=}\,0U\varphi$, and then we have $(\left\| \Diamond \varphi \right\| ,w)=\sup _{i\ge 0}\left( d_{w_{<i}}\left( \left\| \varphi \right\| ,w_{\ge i}\right) \right)$ for every $w\in A^{\omega }$.

The syntactic boolean fragment $bLTL (\mathbb {R}_{\max },A)$ of $LTL ( \mathbb {R}_{\max },A)$ is given by the grammar

$$\begin{aligned} \varphi \,{:}{:}{=}\,-\!\infty \mid 0\mid p_{a}\mid \lnot \varphi \mid \varphi \vee \varphi \mid \bigcirc _{b}\varphi \mid \varphi U\varphi \end{aligned}$$

where $p_{a}\in AP$. For every formula $\varphi \in bLTL ( \mathbb {R}_{\max },A)$ it is easily obtained, by structural induction on $\varphi$, that $\left\| \varphi \right\|$ gets only values in $\left\{ -\infty ,0\right\}$. By identifying $-\infty$ with $\mathbf {0}$ and $0$ with $\mathbf {1}$ it is trivially concluded that $\left\| \varphi \right\|$ coincides with the semantics in the boolean semiring $\mathbb {B}$. The conjunction and always operators are defined, respectively, by the macros $\varphi \underline{\wedge }\psi \,{:}{=}\,\lnot (\lnot \varphi \vee \lnot \psi )$ and $\underline{\square }\varphi \,{:}{=}\,\lnot \Diamond \lnot \varphi$. Trivially, we get $\left\| \varphi \underline{\wedge }\psi \right\| =\left\| \varphi \wedge \psi \right\|$ and $\left\| \underline{\square }\varphi \right\| =\left\| \square \varphi \right\|$ for every $\varphi ,\psi \in bLTL ( \mathbb {R}_{\max },A)$. On the other hand, the application of the operators $\underline{\wedge }$ and $\underline{\square }$ coincides semantically with the application of the classical operators $\wedge$ and $\square$ respectively, to boolean formulas.

In the sequel, we define two fragments of $LTL ( \mathbb {R}_{\max },A)$. In fact, the first one is included into the latter. For this we need some preliminary notions.

An atomic-step formula is an $LTL ( \mathbb {R}_{\max },A)$ formula of the form $\bigvee \nolimits _{a\in A}\left( k_{a}\wedge p_{a}\right)$ where $k_{a}\in \mathbb {R}_{\max }$ and $p_{a}\in AP$ for every $a\in A$. An LTL-step formula is an $LTL ( \mathbb {R}_{\max },A)$ formula of the form $\bigvee \nolimits _{1\le i\le n}\left( k_{i}\wedge \varphi _{i}\right)$ where $k_{i}\in \mathbb {R}_{\max }$ and $\varphi _{i}\in bLTL ( \mathbb {R}_{\max },A)$ for every $1\le i\le n$. We shall denote by $stLTL \left( \mathbb {R}_{\max },A\right)$ the class of LTL-step formulas over $A$ and $\mathbb {R}_{\max }$. Furthermore, we shall denote by $abLTL \left( \mathbb {R}_{\max },A\right)$ the class of almost boolean LTL formulas over $A$ and $\mathbb {R}_{\max }$, i.e., formulas of the form $\bigwedge \nolimits _{1\le i\le n}\varphi _{i}$ with $\varphi _{i}\in bLTL \left( \mathbb {R}_{\max },A\right)$ or $\varphi _{i}=\bigvee \nolimits _{a\in A}\left( k_{a}\wedge p_{a}\right)$, for every $1\le i\le n$.

Definition 3

The fragment $ULTL \left( \mathbb {R}_{\max },A\right)$ of $U$ -nesting LTL formulas over $A$ and $\mathbb {R}_{\max }$ is the least class of formulas in $LTL \left( \mathbb {R}_{\max },A\right)$ which is defined inductively in the following way.

• $k\in ULTL \left( \mathbb {R}_{\max },A\right)$ for every $k\in \mathbb {R}_{\max }$.

• $abLTL \left( \mathbb {R}_{\max },A\right) \subseteq ULTL \left( \mathbb {R}_{\max },A\right)$.

• If $\varphi \in ULTL \left( \mathbb {R}_{\max },A\right)$, then $\lnot \varphi \in ULTL \left( \mathbb {R}_{\max },A\right)$.

• If $\varphi ,\psi \in ULTL \left( \mathbb {R}_{\max },A\right)$, then $\varphi \wedge \psi ,\varphi \vee \psi \in ULTL \left( \mathbb {R}_{\max },A\right)$.

• If $\varphi \in ULTL \left( \mathbb {R}_{\max },A\right)$, then $\bigcirc \varphi \in ULTL \left( \mathbb {R}_{\max },A\right)$.

• If $\varphi \in bLTL \left( \mathbb {R}_{\max },A\right)$ or $\varphi$ is an atomic-step formula, then $\square \varphi \in ULTL \left( \mathbb {R}_{\max },A\right)$.

• If $\varphi \in abLTL \left( \mathbb {R}_{\max },A\right)$ and $\psi \in ULTL \left( \mathbb {R}_{\max },A\right)$, then $\varphi U\psi \in ULTL \left( \mathbb {R}_{\max },A\right)$.

A series $r\in \mathbb {R}_{\max }\left\langle \left\langle A^{\omega }\right\rangle \right\rangle$ is called $\omega \hbox {-}U$ LTL-$d$-definable if there is a formula $\varphi \in ULTL \left( \mathbb {R}_{\max },A\right)$ such that $r=\left\| \varphi \right\|$. We shall denote by $\omega \hbox {-} ULTL \left( \mathbb {R}_{\max },A,d\right)$ the class of all $\omega \hbox {-} ULTL$-$d$-definable series over $A$ and $\mathbb {R}_{\max }$.

Definition 4

The fragment $RLTL \left( \mathbb {R}_{\max },A\right)$ of restricted LTL formulas over $A$ and $\mathbb {R} _{\max }$ is the least class of formulas in $LTL \left( \mathbb {R}_{\max },A\right)$ which is defined inductively in the following way.

• $ULTL \left( \mathbb {R}_{\max },A\right) \subseteq RLTL \left( \mathbb {R}_{\max },A\right)$.

• If $\varphi ,\psi \in RLTL \left( \mathbb {R}_{\max },A\right)$, then $\varphi \wedge \psi ,\varphi \vee \psi \in RLTL \left( \mathbb {R}_{\max },A\right)$.

• If $\varphi \in stLTL \left( \mathbb {R}_{\max },A\right)$, then $\bigcirc _{b}\varphi \in RLTL \left( \mathbb {R}_{\max },A\right)$.

A series $r\in \mathbb {R}_{\max }\left\langle \left\langle A^{\omega }\right\rangle \right\rangle$ is called $\omega$-rLTL-$d$-definable if there is a formula $\varphi \in RLTL \left( \mathbb {R}_{\max },A\right)$ such that $r=\left\| \varphi \right\|$. We shall denote by $\omega$-$rLTL \left( \mathbb {R}_{\max },A,d\right)$ the class of all $\omega$-rLTL-$d$-definable series over $A$ and $\mathbb {R}_{\max }$.

4 Weighted FO logic with discounting

In this section, we introduce the weighted first-order logic (weighted FO logic, for short) with discounting, and we show that the class of semantics in a fragment of this logic contains the class $\omega \hbox {-} rLTL \left( \mathbb {R}_{\max },A,d\right)$. In comparison to weighted MSO logic with discounting of [13], our FO logic here is enriched with an alternative first-order existential quantification which employs the discounting parameters. As we show in Sect. 8, the addition of the new existential quantification does not increase the power of the sentences, in the fragment of the weighted MSO logic of [13], which we will prove to be expressively equivalent to $\omega \hbox {-}d$-recognizable series.

Definition 5

The syntax of formulas of the weighted FO logic with discounting over $A$ and $\mathbb {R}_{\max }$ is given by the grammar

$$\begin{aligned} \varphi \,{:}{:}{=}\,k\mid P_{a}(x)\mid x\le y\mid \lnot \varphi \mid \varphi \vee \varphi \mid \varphi \wedge \varphi \mid \exists x\cdot \varphi \mid \exists _{d}x\cdot \varphi \mid \forall x\cdot \varphi \end{aligned}$$

where $k\in \mathbb {R}_{\max }$ and $a\in A.$

We shall denote by $FO ( \mathbb {R}_{\max },A)$ the set of all weighted FO logic formulas over $A$ and $\mathbb {R}_{\max }$. In order to define the semantics of $FO (\mathbb {R}_{\max },A)$ formulas, we recall the notions of extended alphabet and valid assignment (cf. for instance [29]). Let $\mathcal {V}$ be a finite set of first-order variables. For an infinite word $w\in A^{\omega }$ we let $dom (w)=\omega$. A $(\mathcal {V},w)$-assignment $\sigma$ is a mapping associating variables from $\mathcal {V}$ to elements of $\omega$. For every $x\in \mathcal {V}$ and $i\in \omega$, we denote by $\sigma [x\rightarrow i]$ the $(\mathcal {V},w)$-assignment which associates $i$ to $x$ and acts as $\sigma$ on $\mathcal {V}\setminus \{x\}.$ We encode pairs $(w,\sigma )$ for every $w\in A^{\omega }$ and $(\mathcal {V},w)$-assignment $\sigma$, by using the extended alphabet $A_{\mathcal {V}}=A\times \{0,1\}^{\mathcal {V}}$. Each pair $(w,\sigma )$ is a word in $A_{\mathcal {V}}^{\omega }$ where $w$ is the projection over $A$ and $\sigma$ is the projection over $\{0,1\}^{\mathcal {V} }$. Then $\sigma$ is called a valid $(\mathcal {V},w)$-assignment whenever for every $x\in \mathcal {V}$ the $x$-row contains exactly one $1$. In this case, we identify $\sigma$ with the $(\mathcal {V},w)$-assignment so that for each first-order variable $x\in \mathcal {V},$ $\sigma (x)$ is the position of the $1$ on the $x$-row. It is well-known (cf. [7]) that the set $\mathcal {N}_{\mathcal {V}}=\left\{ \left( w,\sigma \right) \mid w\in A^{\omega },\sigma \,\text {is a valid}\,\left( \mathcal {V},w\right) \,\hbox {-assignment}\,\right\}$ is an $\omega$-star-free language over $A_{\mathcal {V}}$. The set $free (\varphi )$ of free variables in a formula $\varphi \in FO (\mathbb {R}_{\max },A)$ is defined as usual.

Definition 6

Let $\varphi \in FO (\mathbb {R}_{\max },A)$ and $\mathcal {V}$ be a finite set of variables with $free (\varphi )\subseteq \mathcal {V}$. The $d$-semantics of $\varphi$ is a series $\left\| \varphi \right\| _{\mathcal {V}}\in \mathbb {R}_{\max }\left\langle \left\langle A_{\mathcal {V}}^{\omega }\right\rangle \right\rangle .$ Consider an element $(w,\sigma )\in A_{\mathcal {V}}^{\omega }.$ If $\sigma$ is not a valid assignment, then we put $\left( \left\| \varphi \right\| _{\mathcal {V}},(w,\sigma )\right) =-\infty .$ Otherwise, we inductively define $\left( \left\| \varphi \right\| _{\mathcal {V} },(w,\sigma )\right) \in \mathbb {R}_{\max }$ as follows.

• $\left( \left\| k\right\| _{\mathcal {V}},(w,\sigma )\right) =k,$

• $\left( \left\| P_{a}(x)\right\| _{\mathcal {V}},(w,\sigma )\right) =\left\{ \begin{array}{l@{\quad }l} 0 &{} \text {if }\,w(\sigma (x))=a\\ -\infty &{} \text {otherwise} \end{array} ,\right.$

• $\left( \left\| x\le y\right\| _{\mathcal {V}},(w,\sigma )\right) =\left\{ \begin{array}{l@{\quad }l} 0 &{} \text {if }\,\sigma (x)\le \sigma (y)\\ -\infty &{} \text {otherwise} \end{array} ,\right.$

• $\left( \left\| \lnot \varphi \right\| _{\mathcal {V}} ,(w,\sigma )\right) =\left\{ \begin{array}{l@{\quad }l} 0 &{} \text {if }\,\left( \left\| \varphi \right\| _{\mathcal {V}} ,(w,\sigma )\right) =-\infty \\ -\infty &{} \text {otherwise} \end{array},\right.$

• $\left( \left\| \varphi \vee \psi \right\| _{\mathcal {V} },(w,\sigma )\right) =\max \left( \left( \left\| \varphi \right\| _{\mathcal {V}},(w,\sigma )\right) ,\left( \left\| \psi \right\| _{\mathcal {V}},(w,\sigma )\right) \right) ,$

• $\left( \left\| \varphi \wedge \psi \right\| _{\mathcal {V} },(w,\sigma )\right) =\left( \left\| \varphi \right\| _{\mathcal {V} },(w,\sigma )\right) +\left( \left\| \psi \right\| _{\mathcal {V} },(w,\sigma )\right) ,$

• $\left( \left\| \exists x\cdot \varphi \right\| _{\mathcal {V}},(w,\sigma )\right) ={\sup \nolimits _{i\ge 0}}\left( \left( \left\| \varphi \right\| _{\mathcal {V}\cup \{x\}},(w,\sigma [x\rightarrow i])\right) \right) ,$

• $\left( \left\| \exists _{d}x\cdot \varphi \right\| _{\mathcal {V}},(w,\sigma )\right) ={\sup \nolimits _{i\ge 0}}\left( d_{w_{<i} }\left( \left\| \varphi \right\| _{\mathcal {V}\cup \{x\}},(w,\sigma [x\rightarrow i])\right) \right) ,$

• $\left( \left\| \forall x\cdot \varphi \right\| _{\mathcal {V}},(w,\sigma )\right) ={{\sum \nolimits _{i\ge 0}} }d_{w_{<i}}\left( \left\| \varphi \right\| _{\mathcal {V}\cup \{x\}},(w,\sigma [x\rightarrow i])\right) .$

As in our weighted LTL, all the above suprema and infinite sums exist due to the involvement of the discounting parameters. If $\mathcal {V} = free (\varphi )$, then we simply write $\left\| \varphi \right\|$ for $\left\| \varphi \right\| _{ free (\varphi )}$. Moreover, with similar arguments, as in Proposition 3.3 in [8], we can show that

$$\begin{aligned} \left( \left\| \varphi \right\| _{\mathcal {V}},\left( w,\sigma \right) \right) =\left( \left\| \varphi \right\| ,\left( w,\sigma |_{ free \left( \varphi \right) }\right) \right) \end{aligned}$$

for every $\left( w,\sigma \right) \in \mathcal {N}_{\mathcal {V}}$.

The syntactic boolean fragment $bFO ( \mathbb {R}_{\max },A)$ of $FO (\mathbb {R}_{\max },A)$ is defined by the grammar

$$\begin{aligned} \varphi \,{:}{:}{=}\,-\infty \mid 0\mid P_{a}(x)\mid x\le y\mid \lnot \varphi \mid \varphi \vee \varphi \mid \exists x\cdot \varphi \end{aligned}$$

where $a\in A$. For every formula $\varphi \in bFO ( \mathbb {R}_{\max },A)$ it is easily obtained, by structural induction on $\varphi$, that $\left\| \varphi \right\|$ gets only values in $\left\{ -\infty ,0\right\}$. By identifying $-\infty$ with $\mathbf {0}$ and 0 with $\mathbf {1}$ it is trivially concluded that $\left\| \varphi \right\|$ coincides with the semantics in the boolean semiring $\mathbb {B}$. The conjunction and universal quantification are defined, respectively, by the macros $\varphi \underline{\wedge }\psi \,{:}{=}\,\lnot (\lnot \varphi \vee \lnot \psi )$ and $\underline{\forall }x\cdot \varphi \,{:}{=}\,\lnot \exists x\cdot \lnot \varphi$. Trivially, we get $\left\| \varphi \underline{\wedge }\psi \right\| =\left\| \varphi \wedge \psi \right\|$ and $\left\| \underline{\forall }x\cdot \varphi \right\| =\left\| \forall x\cdot \varphi \right\|$ for every $\varphi ,\psi \in bFO (\mathbb {R}_{\max },A)$. On the other hand, the application of the operators $\underline{\wedge }$ and $\underline{\forall }$ coincides semantically with the application of the classical operators $\wedge$ and $\forall$ respectively, to boolean formulas.

Next, we define a fragment of our logic. For this, we recall the notion of an FO-step formula from [4]. More precisely, a formula $\varphi \in FO ( \mathbb {R}_{\max },A)$ is called an FO-step formula if $\varphi =\bigvee \nolimits _{1\le i\le n}\left( k_{i}\wedge \varphi _{i}\right)$ with $\varphi _{i}\in bFO ( \mathbb {R}_{\max },A)$ and $k_{i}\in \mathbb {R}_{\max }$ for every $1\le i\le n$. Moreover, a formula $\varphi \in FO (\mathbb {R}_{\max },A)$ is called a letter-step formula whenever $\varphi =\bigvee \nolimits _{a\in A}\left( k_{a}\wedge P_{a}(x)\right)$ with $k_{a}\in \mathbb {R}_{\max }$ for every $a\in A$. We shall need also the following macros:

• $first (x)\,{:}{=}\,\forall y\cdot x\le y,$

• $x=y\,{:}{=}\,x\le y\wedge y\le x,$

• $x<y\,{:}{=}\,x\le y\wedge \lnot (x=y),$

• $z\le x<y\,{:}{=}\,z\le x\wedge x<y,$

• $y\le x\rightarrow \varphi \,{:}{=}\,\lnot \left( y\le x\right) \vee \left( (y\le x)\wedge \varphi \right) ,$

• $z\le x<y\rightarrow \varphi \,{:}{=}\,\lnot (z\le x<y)\vee \left( (z\le x<y)\wedge \varphi \right) .$

Definition 7

A formula $\varphi \in FO ( \mathbb {R}_{\max },A)$ will be called weakly quantified if (i) whenever $\varphi$ contains a subformula of the form $\exists _{d}x\cdot \psi$, then $\psi$ is an FO-step formula, and (ii) whenever $\varphi$ contains a subformula of the form $\forall x\cdot \psi$, then $\psi$ is either a boolean or a letter-step formula or a formula of the form $z\le x<y\rightarrow \psi ^{\prime }$, or a formula of the form $y\le x\rightarrow \psi ^{\prime }$, where $\psi ^{\prime }$ is a letter-step formula with free variable $x$.

We denote by $WQFO ( \mathbb {R}_{\max },A)$ the set of all weakly quantified $FO (\mathbb {R}_{\max },A)$ formulas over $A$ and $\mathbb {R}_{\max }$. A series $s\in \mathbb {R}_{\max }\left\langle \left\langle A^{\omega }\right\rangle \right\rangle$ is called $\omega$-wqFO-$d$-definable if there is a sentence $\varphi \in WQFO ( \mathbb {R}_{\max },A)$ such that $s=\left\| \varphi \right\|$. We write $\omega \hbox {-} wqFO ( \mathbb {R}_{\max },A,d)$ for the class of all $\omega$-wqFO-$d$-definable series in $\mathbb {R}_{\max }\left\langle \left\langle A^{\omega }\right\rangle \right\rangle$.

We aim to show that every $\omega$-rLTL-$d$-definable series over $A$ and $\mathbb {R}_{\max }$ is also $\omega$-wqFO-$d$-definable over $A$ and $\mathbb {R}_{\max }$. For this, we will prove that for every $\varphi \in RLTL \left( \mathbb {R}_{\max },A\right)$ there exists a sentence $\varphi ^{\prime }\in WQFO (\mathbb {R}_{\max },A)$ such that $\left\| \varphi \right\| =\left\| \varphi ^{\prime }\right\|$, using the subsequent technical results below.

Lemma 8

Let $\varphi \in ULTL \left( \mathbb {R}_{\max },A\right)$ such that there exists $\varphi ^{\prime }\left( y\right) \in WQFO \left( \mathbb {R}_{\max },A\right)$ with $\left( \left\| \varphi ^{\prime }\left( y\right) \right\| ,\left( w,\left[ y\rightarrow i\right] \right) \right) =d_{w_{<i}}\left( \left\| \varphi \right\| ,w_{\ge i}\right)$ for every $w\in A^{\omega },i\ge 0$. Then $\left( \left\| \lnot \varphi ^{\prime }\left( y\right) \right\| ,\left( w,\left[ y\rightarrow i\right] \right) \right) =d_{w_{<i}}\left( \left\| \lnot \varphi \right\| ,w_{\ge i}\right)$ for every $w\in A^{\omega },i\ge 0$.

Proof

Let $\varphi \in ULTL \left( \mathbb {R}_{\max },A\right)$ such that there exists $\varphi ^{\prime }\left( y\right) \in WQFO \left( \mathbb {R}_{\max },A\right)$ with $\left( \left\| \varphi ^{\prime }\left( y\right) \right\| ,\left( w,\left[ y\rightarrow i\right] \right) \right) =d_{w_{<i}}\left( \left\| \varphi \right\| ,w_{\ge i}\right)$ for every $w\in A^{\omega },i\ge 0$. Then, for every $w\in A^{\omega },i\ge 0$, in case $\left( \left\| \varphi \right\| ,w_{\ge i}\right) =-\infty$ we get, by our assumption, $\left( \left\| \varphi ^{\prime }\left( y\right) \right\| ,\left( w,\left[ y\rightarrow i\right] \right) \right) =-\infty$. By Definitions 2 and 6, we obtain $\left( \left\| \lnot \varphi \right\| ,w_{\ge i}\right) =0$ and $\left( \left\| \lnot \varphi ^{\prime }\left( y\right) \right\| ,\left( w,\left[ y\rightarrow i\right] \right) \right) =0$, respectively. If $\left( \left\| \varphi \right\| ,w_{\ge i}\right) \ne -\infty$, again by our assumption we have $\left( \left\| \varphi ^{\prime }\left( y\right) \right\| ,\left( w,\left[ y\rightarrow i\right] \right) \right) \ne -\infty$ and by Definitions 2 and 6 $\left( \left\| \lnot \varphi \right\| ,w_{\ge i}\right) =-\infty$ and $\left( \left\| \lnot \varphi ^{\prime }\left( y\right) \right\| ,\left( w,\left[ y\rightarrow i\right] \right) \right) =-\infty$, as required.$\square$

Lemma 9

Let $\varphi ,\psi \!\in \! ULTL \left( \mathbb {R}_{\max },A\right)$ such that there exist $\varphi ^{\prime }\left( y\right) ,\psi ^{\prime }\left( x\right) \!\in \! WQFO \!\left( \mathbb {R}_{\max },A\right)$ with $\left( \left\| \varphi ^{\prime }\left( y\right) \right\| ,\left( w,\left[ y\rightarrow i\right] \right) \right) =d_{w_{<i}}\left( \left\| \varphi \right\| ,w_{\ge i}\right)$ and $\left( \left\| \psi ^{\prime }\left( x\right) \right\| ,\left( w,\left[ x\rightarrow i\right] \right) \right) =d_{w_{<i}}\left( \left\| \psi \right\| ,w_{\ge i}\right)$ for every $w\in A^{\omega },i\ge 0$. Then, there exist $\xi _{1}\left( x\right) ,\xi _{2}\left( x\right) \in WQFO \left( \mathbb {R}_{\max },A\right)$ with

$$\begin{aligned} \left( \left\| \xi _{1}\left( x\right) \right\| ,\left( w,\left[ x\rightarrow i\right] \right) \right) =d_{w_{<i}}\left( \left\| \varphi \wedge \psi \right\| ,w_{\ge i}\right) \end{aligned}$$

and

$$\begin{aligned} \left( \left\| \xi _{2}\left( x\right) \right\| ,\left( w,\left[ x\rightarrow i\right] \right) \right) =d_{w_{<i}}\left( \left\| \varphi \vee \psi \right\| ,w_{\ge i}\right) \end{aligned}$$

for every $w\in A^{\omega },i\ge 0.$

Proof

Without any loss, we assume that the variable $x$ does not occur in $\varphi ^{\prime }$ (otherwise we apply a renaming). We replace every occurrence of $y$ with $x$ in $\varphi ^{\prime }$, and we let $\xi _{1}\left( x\right) =\varphi ^{\prime }\left( x\right) \wedge \psi ^{\prime }\left( x\right)$ and $\xi _{2}\left( x\right) =\varphi ^{\prime }\left( x\right) \vee \psi ^{\prime }\left( x\right)$ which trivially satisfy our claim.$\square$

Lemma 10

Let $\varphi \in \mathbb {R}_{\max }\cup abLTL \left( \mathbb {R}_{\max },A\right) \cup stLTL \left( \mathbb {R}_{\max },A\right)$. Then, the following statements hold.

• (i) There exists $\varphi ^{\prime }\left( x\right) \!\in \! WQFO \left( \mathbb {R}_{\max },A\right)$ such that $\left( \left\| \varphi ^{\prime }\left( x\right) \right\| ,\left( w,\left[ x\!\rightarrow \! i\right] \right) \right) \!=\!\left( \left\| \varphi \right\| ,w_{\ge i}\right)$ for every $w\in A^{\omega },i\ge 0$.

• (ii) There exists $\varphi ^{\prime \prime }\left( x\right) \in WQFO \left( \mathbb {R}_{\max },A\right)$ such that $\left( \left\| \varphi ^{\prime \prime }\left( x\right) \right\| ,\left( w,\left[ x\rightarrow i\right] \right) \right) =d_{w_{<i}}\left( \left\| \varphi \right\| ,w_{\ge i}\right)$ for every $w\in A^{\omega },i\ge 0$.

Proof

• (i) Let $\varphi =k\in \mathbb {R}_{\max }$. Then we set $\varphi ^{\prime }(x)=k$. Next, let $\varphi \in abLTL \left( \mathbb {R}_{\max },A\right)$, i.e., $\varphi =\bigwedge \nolimits _{1\le j\le n}\psi _{j}$ with $\psi _{j}\in bLTL \left( \mathbb {R}_{\max },A\right)$ or $\psi _{j}=\bigvee \nolimits _{a\in A}\left( k_{a}\wedge p_{a}\right)$, for every $1\le j\le n$. If $\psi _{j}\in bLTL ( \mathbb {R}_{\max },A)$, then it is well-known that there exists a formula $\psi _{j}^{\prime }(x_{j})\in bFO (\mathbb {R}_{\max },A)$ with one free variable $x_{j}$, such that $(\left\| \psi _{j}\right\| ,w_{\ge i})=\left( \left\| \psi _{j}^{\prime } (x_{j})\right\| ,(w,[x_{j}\rightarrow i])\right)$ for every $w\in A^{\omega },i\ge 0$. Without any loss, we can assume that the variable $x_{j}\; (1\le j\le n)$ does not occur in any $\psi _{k}^{\prime }$ (whenever $\psi _{k}\in bLTL \left( \mathbb {R}_{\max },A\right)$) with $k\ne j$ (if this is not the case, then we apply a renaming of variables). Therefore, we can replace $x_{j}$ in $\psi _{j}^{\prime }$ with a new variable $x$. In case $\psi _{j}=\bigvee \nolimits _{a\in A}\left( k_{a}\wedge p_{a}\right)$, then we consider the $WQFO \left( \mathbb {R}_{\max },A\right)$ letter-step formula $\psi _{j}^{\prime }(x)=\bigvee \nolimits _{a\in A}\left( k_{a}\wedge P_{a}(x)\right)$. Now it is a routine matter to show that the $WQFO \left( \mathbb {R}_{\max },A\right)$ formula $\varphi ^{\prime }(x)=\bigwedge \nolimits _{1\le j\le n}\psi _{j}^{\prime }(x)$ satisfies our claim. The remaining case $\varphi \in stLTL \left( \mathbb {R}_{\max },A\right)$ is treated similarly.

• (ii) Again, let first $\varphi =k\in \mathbb {R}_{\max }$. We set $\varphi ^{\prime \prime }\left( x\right) =\exists _{d}y.\left( \left( x=y\right) \wedge k\right) ,$ and we get

  $$\begin{aligned} \left( \left\| \varphi ^{\prime \prime }\left( x\right) \right\| ,\left( w,\left[ x\rightarrow i\right] \right) \right)&=\left( \left\| \exists _{d}y.\left( \left( x=y\right) \wedge k\right) \right\| ,\left( w,\left[ x\rightarrow i\right] \right) \right) \\&={\sup \limits _{j\ge 0}}\left( d_{w_{<j}}\left( \left\| \left( x=y\right) \wedge k\right\| ,\left( w,\left[ x\rightarrow i,y\rightarrow j\right] \right) \right) \right) \\&=d_{w_{<i}}k=d_{w_{<i}}\left( \left\| k\right\| ,w_{\ge i}\right) , \end{aligned}$$

  for every $w\in A^{\omega },i\ge 0$. Next let $\varphi \in abLTL \left( \mathbb {R}_{\max },A\right)$ with $\varphi =\bigwedge \nolimits _{1\le j\le n}\psi _{j}$ and $\psi _{j}\in bLTL \left( \mathbb {R}_{\max },A\right)$ or $\psi _{j}=\bigvee \nolimits _{a\in A}\left( k_{a}\wedge p_{a}\right)$, for every $1\le j\le n$. By Statement (i) we get that $\left( \left\| \psi _{j}^{\prime }(x)\right\| ,(w,[x\rightarrow i])\right) =\left( \left\| \psi _{j}\right\| ,w_{\ge i}\right) =d_{w_{<i} }(\left\| \psi _{j}\right\| ,w_{\ge i})$, for every $\psi _{j}\in bLTL (\mathbb {R}_{\max },A)$ and $w\in A^{\omega },i\ge 0$. Therefore, we let $\psi _{j} ^{\prime \prime }(x)=\psi _{j}^{\prime }(x)$. In case $\psi _{j}=\bigvee \nolimits _{a\in A}\left( k_{a}\wedge p_{a}\right)$ we set $\psi _{j}^{\prime \prime }(x)=\bigvee \nolimits _{a\in A}(\exists _{d}y.\left( \left( x=y\right) \wedge k_{a}\right) \wedge P_{a}(x))$ and we have

  $$\begin{aligned} \left( \left\| \psi _{j}^{\prime \prime }(x)\right\| ,(w,[x\rightarrow i])\right)&=\left( \left\| \bigvee \limits _{a\in A}\left( \exists _{d}y.\left( \left( x=y\right) \wedge k_{a}\right) \wedge P_{a}(x)\right) \right\| ,(w,[x\rightarrow i])\right) \\&=\max _{a\in A}\left( \left( \left\| \exists _{d}y.\left( \left( x=y\right) \wedge k_{a}\right) \wedge P_{a}(x)\right\| ,(w,[x\rightarrow i])\right) \right) \\&=\max _{a\in A}\left( \left( \left\| \exists _{d}y.\left( x=y\right) \wedge k_{a}\right\| ,(w,[x\rightarrow i])\right) \right. \\&\qquad \qquad \,\, \left. +\left( \left\| P_{a}(x)\right\| ,(w,[x\rightarrow i])\right) \right) \\&=\max _{a\in A}\left( d_{w_{<i}}\left( \left\| k_{a}\right\| ,w_{\ge i}\right) +\left( \left\| p_{a}\right\| ,w_{\ge i}\right) \right) \\&=d_{w_{<i}}\left( \left\| \bigvee \limits _{a\in A}\left( k_{a}\wedge p_{a}\right) \right\| ,w_{\ge i}\right) =d_{w_{<i}}\left( \left\| \psi _{j}\right\| ,w_{\ge i}\right) \end{aligned}$$

  for every $w\in A^{\omega },i\ge 0.$ Then, we let $\varphi ^{\prime \prime }(x)=\bigwedge \nolimits _{1\le j\le n}\psi _{j}^{\prime \prime }(x)$ and trivially $\left( \left\| \varphi ^{\prime \prime }\left( x\right) \right\| ,\left( w,\left[ x\rightarrow i\right] \right) \right) =d_{w_{<i}}\left( \left\| \varphi \right\| ,w_{\ge i}\right)$ for every $w\in A^{\omega },i\ge 0$. Finally, let $\varphi =\bigvee \nolimits _{1\le j\le n}\left( k_{j}\wedge \psi _{j}\right)$ where $k_{j}\in \mathbb {R}_{\max }$ and $\psi _{j}\in bLTL (\mathbb {R}_{\max },A)$ for every $1\le j\le n$. By our arguments in (i), there exist $\psi _{j}^{\prime }(x)\in bFO (\mathbb {R}_{\max },A)$ such that $\left( \left\| \psi _{j}^{\prime }(x)\right\| ,(w,[x\rightarrow i])\right) =\left( \left\| \psi _{j}\right\| ,w_{\ge i}\right) =d_{w_{<i}}(\left\| \psi _{j}\right\| ,w_{\ge i})$ for every $1\le j\le n$ and $w\in A^{\omega },i\ge 0$. We set $\varphi ^{\prime \prime }\left( x\right) =\bigvee \nolimits _{1\le j\le n}\left( \exists _{d}y.\left( \left( x=y\right) \wedge k_{j}\right) \wedge \psi _{j}^{\prime }\right)$ and with a similar computation as in the previous case, we conclude that$\ \varphi ^{\prime \prime }\left( x\right)$ satisfies our claim. $\square$

Lemma 11

Let $\varphi \in ULTL \left( \mathbb {R}_{\max },A\right)$ such that there exists a formula $\varphi ^{\prime }\left( y\right) \in WQFO \left( \mathbb {R}_{\max },A\right)$ with $\left( \left\| \varphi ^{\prime }\left( y\right) \right\| ,\left( w,\left[ y\rightarrow i\right] \right) \right) =d_{w_{<i}}\left( \left\| \varphi \right\| ,w_{\ge i}\right)$ for every $w\in A^{\omega },i\ge 0$. Then, there exists a $WQFO \left( \mathbb {R}_{\max },A\right)$ formula $\psi \left( x\right)$ such that $\left( \left\| \psi \left( x\right) \right\| ,\left( w,\left[ x\rightarrow i\right] \right) \right) =d_{w_{<i}}\left( \left\| \bigcirc \varphi \right\| ,w_{\ge i}\right)$ for every $w\in A^{\omega },i\ge 0$.

Proof

We let $\psi \left( x\right) =\exists y.\left( y=x+1\wedge \varphi ^{\prime }\left( y\right) \right)$ and we have

$$\begin{aligned} \left( \left\| \psi \left( x\right) \right\| ,\left( w,\left[ x\rightarrow i\right] \right) \right)&=\left( \left\| \exists y.\left( y=x+1\wedge \varphi ^{\prime }\left( y\right) \right) \right\| ,\left( w,\left[ x\rightarrow i\right] \right) \right) \\&={\sup \limits _{j\ge 0}}\left( \left( \left\| y=x+1\wedge \varphi ^{\prime }\left( y\right) \right\| ,\left( w,\left[ x\rightarrow i,y\rightarrow j\right] \right) \right) \right) \\&=\left( \left\| y=x+1\wedge \varphi ^{\prime }\left( y\right) \right\| ,\left( w,\left[ x\rightarrow i,y\rightarrow i+1\right] \right) \right) \\&=\left( \left\| \varphi ^{\prime }\left( y\right) \right\| ,\left( w,\left[ y\rightarrow i+1\right] \right) \right) \\&=d_{w_{<i+1}}\left( \left\| \varphi \right\| ,w_{\ge i+1}\right) =d_{w_{<i}}\left( d_{w(i)}\left( \left\| \varphi \right\| ,\left( w_{\ge i}\right) _{\ge 1}\right) \right) \\&=d_{w_{<i}}\left( \left\| \bigcirc \varphi \right\| ,w_{\ge i}\right) . \end{aligned}$$

for every $w\in A^{\omega },i\ge 0$. $\square$

Lemma 12

Let $\varphi \in bLTL \left( \mathbb {R}_{\max },A\right)$ or $\varphi$ be an atomic-step formula. Then, there exists $\psi \left( y\right) \in WQFO \left( \mathbb {R}_{\max },A\right)$ such that $\left( \left\| \psi \left( y\right) \right\| ,\left( w,\left[ y\rightarrow i\right] \right) \right) =d_{w_{<i}}\left( \left\| \square \varphi \right\| ,w_{\ge i}\right)$ for every $w\in A^{\omega },i\ge 0$.

Proof

If $\varphi \in bLTL ( \mathbb {R}_{\max },A)$, then $\square \varphi \in bLTL (\mathbb {R}_{\max },A)$, and thus there exists a formula $\psi \left( x\right) \in bFO ( \mathbb {R}_{\max },A)$ with one free variable $x$, such that $\left( \left\| \psi \left( x\right) \right\| ,\left( w,\left[ x\rightarrow i\right] \right) \right) =\left( \left\| \square \varphi \right\| ,w_{\ge i}\right) =d_{w_{<i}}\left( \left\| \square \varphi \right\| ,w_{\ge i}\right)$ for every $w\in A^{\omega },i\ge 0$. If $\varphi =\bigvee \nolimits _{a\in A}\left( k_{a}\wedge p_{a}\right)$, then we consider the $WQFO \left( \mathbb {R}_{\max },A\right)$ letter-step formula $\varphi ^{\prime }(x)=\bigvee \nolimits _{a\in A}\left( k_{a}\wedge P_{a}(x)\right)$. We also consider the $WQFO \left( \mathbb {R}_{\max },A\right)$ formula $\psi \left( y\right) =\forall x.\left( y\le x\rightarrow \varphi ^{\prime }(x)\right)$. Then, for every $w\in A^{\omega },j\ge 0$ we have

$$\begin{aligned} \left( \left\| \psi \left( y\right) \right\| ,\left( w,\left[ y\rightarrow i\right] \right) \right)&={\sum \limits _{j\ge 0}} d_{w_{<j}}\left( \left\| y\le x\rightarrow \varphi ^{\prime }(x)\right\| ,\left( w,\left[ y\rightarrow i,x\rightarrow j\right] \right) \right) \\&=\underset{i\le j}{\sum }d_{w_{<j}}\left( \left\| y\le x\wedge \varphi ^{\prime }(x)\right\| ,\left( w,\left[ y\rightarrow i,x\rightarrow j\right] \right) \right) \\&=\underset{i\le j}{\sum }d_{w_{<j}}\left( \left\| \varphi ^{\prime }(x)\right\| ,\left( w,\left[ x\rightarrow j\right] \right) \right) \\&=\underset{i\le j}{\sum }d_{w_{<j}}\left( \left\| \varphi \right\| ,w_{\ge j}\right) \\&=d_{w_{<i}}\underset{0\le j}{\sum }d_{\left( w_{\ge i}\right) _{<j} }\left( \left\| \varphi \right\| ,\left( w_{\ge i}\right) _{\ge j}\right) \\&=d_{w_{<i}}\left( \left\| \square \varphi \right\| ,w_{\ge i}\right) \end{aligned}$$

where in the right-handside of the second equality the sum is taken over $j,$ and the fourth equality holds by Lemma 10(i).$\square$

Lemma 13

Let $\varphi \in abLTL \left( \mathbb {R}_{\max },A\right)$ and $\psi \in ULTL \left( \mathbb {R}_{\max },A\right)$ such that there exists $\psi ^{\prime }\left( y\right) \in WQFO \left( \mathbb {R}_{\max },A\right)$ with $\left( \left\| \psi ^{\prime }\left( y\right) \right\| ,\left( w,\left[ y\rightarrow i\right] \right) \right) =d_{w_{<i}}\left( \left\| \psi \right\| ,w_{\ge i}\right)$ for every $w\in A^{\omega },i\ge 0$. Then, there exists $\xi \left( z\right) \in WQFO \left( \mathbb {R}_{\max },A\right)$ such that $\left( \left\| \xi \left( z\right) \right\| ,\left( w,\left[ z\rightarrow i\right] \right) \right) =d_{w_{<i}}\left( \left\| \varphi U\psi \right\| ,w_{\ge i}\right)$ for every $w\in A^{\omega },i\ge 0$.

Proof

Let $\varphi =\bigwedge \nolimits _{1\le l\le m}\varphi _{l}$. Then, by the proof of Lemma 10(i), there exists a formula $\varphi ^{\prime }\left( x\right) =\bigwedge \nolimits _{1\le l\le m}\varphi _{l}^{\prime }\left( x\right)$ where for every $1\le l\le m,\; \varphi _{l}^{\prime }\left( x\right) \in bFO \left( \mathbb {R}_{\max },A\right)$ or it is a letter-step formula with $(\left\| \varphi _{l}^{\prime }\left( x\right) \right\| \left( w,\left[ x\rightarrow i\right] \right) )=\left( \left\| \varphi _{l}\right\| ,w_{\ge i}\right)$ for every $w\in A^{\omega },i\ge 0$. Moreover, we have $\left( \left\| \varphi ^{\prime }\left( x\right) \right\| ,\left( w,\left[ x\rightarrow i\right] \right) \right) =\left( \left\| \varphi \right\| ,w_{\ge i}\right)$ for every $w\in A^{\omega },i\ge 0$. We consider the $FO \left( \mathbb {R}_{\max },A\right)$ formula $\xi ^{\prime }\left( z\right) =\exists y.\left( \forall x.\left( \left( z\le x<y\right) \rightarrow \varphi ^{\prime }\left( x\right) \right) \wedge \left( z\le y\right) \wedge \psi ^{\prime }\left( y\right) \right)$. For every $w\in A^{\omega },i\ge 0$ we compute

$$\begin{aligned}&\left( \left\| \xi ^{\prime }\left( z\right) \right\| ,\left( w,\left[ z\rightarrow i\right] \right) \right) \\&\quad =\underset{j\ge 0}{\sup }\left( \left( \left\| \forall x.\left( \left( z\le x<y\right) \rightarrow \varphi ^{\prime }\left( x\right) \right) \wedge \left( z\le y\right) \wedge \psi ^{\prime }\left( y\right) \right\| ,\left( w,\left[ z\rightarrow i,y\rightarrow j\right] \right) \right) \right) \\&\quad =\underset{j\ge 0}{\sup }\left( \left( \left\| \forall x.\left( \left( z\le x<y\right) \rightarrow \varphi ^{\prime }\left( x\right) \right) \wedge \psi ^{\prime }\left( y\right) \right\| ,\left( w,\left[ z\rightarrow i,y\rightarrow i+j\right] \right) \right) \right) \\&\quad =\underset{j\ge 0}{\sup }\left( \underset{0\le k<j}{\sum }d_{w_{<i+k} }\left( \left\| \varphi ^{\prime }\left( x\right) \right\| ,\left( w,\left[ x\rightarrow i+k\right] \right) \right) +\left( \left\| \psi ^{\prime }\left( y\right) \right\| ,\left( w,\left[ y\rightarrow i+j\right] \right) \right) \right) \\&\quad =\underset{j\ge 0}{\sup }\left( \underset{0\le k<j}{\sum }d_{w_{<i+k} }\left( \left\| \varphi \right\| ,w_{\ge i+k}\right) +d_{w_{<i+j} }\left( \left\| \psi \right\| ,w_{\ge i+j}\right) \right) \\&\quad =d_{w_{<i}}\underset{j\ge 0}{\sup }\left( \underset{0\le k<j}{\sum }d_{\left( w_{\ge i}\right) _{<k}}\left( \left\| \varphi \right\| ,w_{\ge i+k}\right) +d_{\left( w_{\ge i}\right) _{<j}}\left( \left\| \psi \right\| ,w_{\ge i+j}\right) \right) \\&\quad =d_{w_{<i}}\left( \left\| \varphi U\psi \right\| ,w_{\ge i}\right) . \end{aligned}$$

Now, we consider the formula $\xi \left( z\right) =\exists y.\left( \bigwedge \nolimits _{1\le l\le m}\left( \forall x.\left( \left( z\le x\!<\!y\right) \!\rightarrow \!\varphi _{l}^{\prime }\left( x\right) \right) \right) \wedge \left( z\le y\right) \wedge \psi ^{\prime }\left( y\right) \right)$ and we get $\left( \left\| \xi \left( z\right) \right\| ,\left( w,\left[ z\rightarrow i\right] \right) \right) =\left( \left\| \xi ^{\prime }\left( z\right) \right\| ,\left( w,\left[ z\rightarrow i\right] \right) \right) =d_{w_{<i}}\left( \left\| \varphi U\psi \right\| ,w_{\ge i}\right)$ for every $w\in A^{\omega },i\ge 0$. Since $\xi \left( z\right) \in WQFO \left( \mathbb {R}_{\max },A\right)$, we conclude our proof.$\square$

Lemma 14

For every $ULTL \left( \mathbb {R}_{\max },A\right)$ formula $\varphi$ we can construct a $WQFO \left( \mathbb {R}_{\max },A\right)$ formula $\varphi ^{\prime }\left( x\right)$ such that $\left( \left\| \varphi ^{\prime }\left( x\right) \right\| ,\left( w,\left[ x\rightarrow i\right] \right) \right) =d_{w_{<i}}\left( \left\| \varphi \right\| ,w_{\ge i}\right)$ for every $w\in A^{\omega },i\ge 0$.

Proof

We use Lemmas 8, 9, 10(ii), 11, 12, and 13. In fact, we apply a partial structural induction, since in the proof of Lemmas 12 and 13 we use Lemma 10(i) for the formula $\varphi$.   $\square$

Proposition 15

For every $\varphi \in ULTL \left( \mathbb {R}_{\max },A\right)$ we can construct a $WQFO \left( \mathbb {R}_{\max },A\right)$ sentence $\varphi ^{\prime }$ with $\left\| \varphi ^{\prime }\right\| =\left\| \varphi \right\|$.

Proof

Let $\varphi \in ULTL \left( \mathbb {R}_{\max },A\right)$. By the previous lemma, there exists a $WQFO \left( \mathbb {R} _{\max },A\right)$ formula $\psi \left( x\right)$ such that $\left( \left\| \psi \left( x\right) \right\| ,\left( w,\left[ x\rightarrow i\right] \right) \right) =d_{w_{<i}}\left( \left\| \varphi \right\| ,w_{\ge i}\right)$, for every $w\in A^{\omega },i\ge 0.$ We consider the $WQFO \left( \mathbb {R}_{\max },A\right)$ sentence $\varphi ^{\prime }=\exists x\cdot \left( first \left( x\right) \wedge \psi \left( x\right) \right)$ and we get $\left( \left\| \varphi ^{\prime }\right\| ,w\right) =\left( \left\| \psi \left( x\right) \right\| ,\left( w,\left[ x\rightarrow 0\right] \right) \right) =d_{w_{<0}}\left( \left\| \varphi \right\| ,w_{\ge 0}\right) =\left( \left\| \varphi \right\| ,w\right)$ for every $w\in A^{\omega }$, i.e., $\left\| \varphi ^{\prime }\right\| =\left\| \varphi \right\|$, as required.$\square$

Proposition 16

For every $\varphi \in RLTL \left( \mathbb {R}_{\max },A\right)$ we can construct a $WQFO (\mathbb {R}_{\max },A)$ sentence $\varphi ^{\prime }$ such that $\left\| \varphi ^{\prime }\right\| =\left\| \varphi \right\|$.

Proof

We prove our claim by structural induction on $\varphi$. If $\varphi \in ULTL \left( \mathbb {R}_{\max },A\right)$, then our claim holds by the previous proposition.

Let $\psi _{1},\psi _{2}\in RLTL ( \mathbb {R}_{\max },A)$ and $\psi _{1}^{\prime },\psi _{2}^{\prime }\in WQFO \left( \mathbb {R}_{\max },A\right)$ be their corresponding sentences. We prove our claim for $\psi _{1}\vee \psi _{2}$ and $\psi _{1}\wedge \psi _{2}$. Consider the $WQFO (\mathbb {R}_{\max },A)$ sentence $\psi _{1}^{\prime }\vee \psi _{2}^{\prime }$. Then, for every $w\in A^{\omega }$, we have

$$\begin{aligned} \left( \left\| \psi _{1}\vee \psi _{2}\right\| ,w\right)&=\max \left( \left( \left\| \psi _{1}\right\| ,w\right) ,\left( \left\| \psi _{2}\right\| ,w\right) \right) \\&=\max \left( \left( \left\| \psi _{1}^{\prime }\right\| ,w\right) ,\left( \left\| \psi _{2}^{\prime }\right\| ,w\right) \right) \\&=\left( \left\| \psi _{1}^{\prime }\vee \psi _{2}^{\prime }\right\| ,w\right) . \end{aligned}$$

By replacing, $\vee$ with $\wedge$ and $\max$ with $+$, in the above computation, we get $\left( \left\| \psi _{1}\wedge \psi _{2}\right\| ,w\right) =\left( \left\| \psi _{1}^{\prime }\wedge \psi _{2}^{\prime }\right\| ,w\right)$.

We proceed with the boolean next operator, therefore let $\varphi =\bigcirc _{b}\psi$ with $\psi \in stLTL \left( \mathbb {R}_{\max },A\right)$. By Lemma 10(i) we get a $WQFO \left( \mathbb {R}_{\max },A\right)$ formula $\psi ^{\prime }(y)$ and consider the $WQFO \left( \mathbb {R}_{\max },A\right)$ sentence $\varphi ^{\prime }=\exists x\cdot \left( first (x)\wedge \exists y\cdot (\left( y=x+1\right) \wedge \psi ^{\prime }(y))\right)$. Then, for every $w\in A^{\omega }$, we compute

$$\begin{aligned} \left( \left\| \bigcirc _{b}\psi \right\| ,w\right)&=\left( \left\| \psi \right\| ,w_{\ge 1}\right) \\&=\left( \left\| \psi ^{\prime }(y)\right\| , (w,[y\rightarrow 1])\right) \\&=\underset{j\ge 0}{\sup }\left( \left( \left\| \left( y=x+1\right) \wedge \psi ^{\prime }(y)\right\| ,(w,[x\rightarrow 0,y\rightarrow j])\right) \right) \\&=\left( \left\| \exists y\cdot (\left( y=x+1\right) \wedge \psi ^{\prime }(y))\right\| ,(w,[x\rightarrow 0])\right) \\&=\left( \left\| \exists x\cdot \left( first(x)\wedge \exists y\cdot (\left( y=x+1\right) \wedge \psi ^{\prime }(y))\right) \right\| ,w\right) \\&=\left( \left\| \varphi ^{\prime }\right\| ,w\right) , \end{aligned}$$

as required.$\square$

Example 17

Let $A=\left\{ a,b\right\}$ and $d_{a}=1/4,d_{b}=1/2$. We consider the weighted LTL formula

$$\begin{aligned} \varphi =\left( p_{a}\wedge 2\right) U\left( \square \left( p_{b} \wedge 3\right) \right) . \end{aligned}$$

Clearly $\varphi \in ULTL \left( \mathbb {R}_{\max },A\right)$. Furthermore $supp (\left\| \varphi \right\| )=a^{*}b^{\omega }$ and

$$\begin{aligned} \left( \left\| \varphi \right\| ,a^{n}b^{\omega }\right) =\sum \limits _{0\le i\le n-1}\left( 1/4\right) ^{i}2+\left( 1/4\right) ^{n}\sum \limits _{j\ge 0}\left( 1/2\right) ^{j}3 \end{aligned}$$

for every $n\ge 0,a^{n}b^{\omega }\in A^{\omega }$.

By Proposition 15, we get that $\left\| \varphi ^{\prime }\right\| =\left\| \varphi \right\|$ where

$$\begin{aligned} \varphi ^{\prime }=\exists z\cdot \left( first \left( z\right) \wedge \psi \left( z\right) \right) \end{aligned}$$

is a $WQFO \left( \mathbb {R}_{\max },A\right)$ formula with

$$\begin{aligned} \psi \left( z\right) =\exists y\cdot \left( \left( z\le y\right) \wedge \forall x\cdot \left( z\le x<y\rightarrow \left( 2\wedge P_{a}(x)\right) \right) \wedge \forall x\cdot \left( y\le x\rightarrow \left( 3\wedge P_{b}(x)\right) \right) \right) . \end{aligned}$$

By Proposition 16, we get the main result of this section.

Theorem 18

$\omega \hbox {-} rLTL \left( \mathbb {R}_{\max },A,d\right) \subseteq \omega \hbox {-} wqFO (\mathbb {R}_{\max },A,d)$.

By the constructive proofs of this section’s Lemmas and Propositions, we obtain the following corollary.

Corollary 19

For every $\varphi \in RLTL \left( \mathbb {R}_{\max },A\right)$ we can construct a $WQFO ( \mathbb {R}_{\max },A)$ sentence $\varphi ^{\prime },$ that uses at most three different names of variables, such that $\left\| \varphi ^{\prime }\right\| =\left\| \varphi \right\| .$

5 Star-free series

In this section, we introduce the notions of $d$-star-free and $\omega \hbox {-}d$-star-free series over $A$ and $\mathbb {R}_{\max }$, and we show that the class of $\omega$-wqFO-$d$-definable series is contained into the class of $\omega \hbox {-}d$-star-free series.

Let $L\subseteq A^{*}$ (resp. $L\subseteq A^{\omega })$. As usually, we denote by $0_{L}$ the characteristic series of $L$. If $L$ is a singleton, i.e., $L=\{w\}$, then we simply write $0_{w}$ for $0_{\{w\}}$. Furthermore, we simply denote by $k_{L}$ the series $k+0_{L}$ for $k\in \mathbb {R}_{\max }$. The monomials over $A$ and $\mathbb {R}_{\max }$ are series of the form $\left( k_{a}\right) _{a}$ for $a\in A$ and $k_{a}\in \mathbb {R}_{\max }$. For simplicity reasons, we shall consider also the series of the form $k_{\varepsilon }$ with $k\in \mathbb {R} _{\max }$ as monomials. A series $s\in \mathbb {R}_{\max }\left\langle \left\langle A^{*}\right\rangle \right\rangle$ is called a letter-step series if $s=\max _{a\in A}\left( \left( k_{a}\right) _{a}\right)$ where $a\in A$ and $k_{a}\in \mathbb {R}_{\max }$ for every $a\in A$. The complement $\overline{s}$ of a series $s$ is given by $(\overline{s},w)=0$ if $(s,w)=-\infty$ and $-\infty$ otherwise. Let $r,s\in \mathbb {R}_{\max }\left\langle \left\langle A^{*}\right\rangle \right\rangle$. The (Cauchy) sum $+_{d}$ of $r$ and $s$ is the series $r+_{d}s\in \mathbb {R}_{\max }\left\langle \left\langle A^{*}\right\rangle \right\rangle$ defined for every $w\in A^{*}$ by

$$\begin{aligned} (r+_{d}s,w)=\max \left\{ (r,u)+d_{u}(s,v)\mid u,v\in A^{*},w=uv\right\} . \end{aligned}$$

The $n$th-iteration $r^{n}\in \mathbb {R}_{\max }\left\langle \left\langle A^{*}\right\rangle \right\rangle$ ($n\ge 0$) of a series $r\in \mathbb {R}_{\max }\left\langle \left\langle A^{*}\right\rangle \right\rangle$ is defined inductively by

$$\begin{aligned} r^{0}=0_{\varepsilon } \quad \hbox {and} \quad r^{n+1}=r+_{d}r^{n} \quad \hbox {for}\; n\ge 0. \end{aligned}$$

Then, we have $\left( r^{n},w\right) =\max \left\{ \sum \nolimits _{1\le i\le n}d_{u_{1}\ldots u_{i-1}}(r,u_{i})\mid u_{i}\in A^{*},w=u_{1}\ldots u_{n}\right\}$ for every $w\in A^{*}$. A series $r\in \mathbb {R}_{\max }\left\langle \left\langle A^{*}\right\rangle \right\rangle$ is called proper if $(r,\varepsilon )=-\infty$. If $r$ is proper, then for every $w\in A^{*}$ and $n>\left| w\right|$ we have $\left( r^{n},w\right) =-\infty$. The iteration $r^{+}\in \mathbb {R}_{\max }\left\langle \left\langle A^{*}\right\rangle \right\rangle$ of a proper series $r\in \mathbb {R}_{\max }\left\langle \left\langle A^{*}\right\rangle \right\rangle$ is defined by $r^{+}=\max \left( r^{n}\mid n>0\right)$. Thus, for every $w\in A^{+}$ we have $\left( r^{+},w\right) =\max \left\{ \left( r^{n},w\right) \mid 1\le n\le \left| w\right| \right\}$ and $\left( r^{+},\varepsilon \right) =-\infty$.

Example 20

Let $A=\{a,b\},\;k\in \mathbb {R}_{+}$, and consider the series $r\in \mathbb {R}_{\max }\left\langle \left\langle A^{*}\right\rangle \right\rangle$ given by

$$\begin{aligned} (r,w)=\left\{ \begin{array}{l@{\quad }l} \sum \nolimits _{0\le i\le n-1}\left( d_{ab}\right) ^{i}k &{} \text {if }w=(ab)^{n}\,\text { for }\,n>0\\ -\infty &{} \text {otherwise.} \end{array} \right. \end{aligned}$$

Clearly $supp (r^{+})=\{(ab)^{n}\mid n>0\}$. Furthermore, for every $n\ge m>0$ we can easily show, by induction on $m$, that $(r^{m},(ab)^{n})=(r,(ab)^{n})$, whereas $(r^{m},( ab )^{n})=-\infty$ for every $m>n>0$. Hence we get $r^{+}=r$.

Definition 21

The class of $d$-star-free series over $A$ and $\mathbb {R}_{\max }$, denoted by $SF ( \mathbb {R}_{\max },A,d)$, is the least class of series containing the monomials (over $A$ and $\mathbb {R}_{\max }$) and being closed under maximum, sum, complement, $+_{d}$, and iteration restricted to letter-step series.

By structural induction we get that series in $SF ( \mathbb {R}_{\max },A,d)$ are bounded.

Next, let $r\in \mathbb {R}_{\max }\left\langle \left\langle A^{*}\right\rangle \right\rangle$ be a finitary and $s\in \mathbb {R}_{\max }\left\langle \left\langle A^{\omega }\right\rangle \right\rangle$ an infinitary series. We assume that both $r$ and $s$ are bounded. Then, the (Cauchy) sum $+_{d}$ of $r$ and $s$ is the infinitary series $r+_{d}s\in \mathbb {R}_{\max }\left\langle \left\langle A^{\omega }\right\rangle \right\rangle$ defined for every $w\in A^{\omega }$ by

$$\begin{aligned} (r+_{d}s,w)=\sup \left\{ (r,u)+d_{u}(s,v)\mid u\in A^{*},w=uv\right\} . \end{aligned}$$

The $\omega$ -iteration of a proper bounded finitary series $r\in \mathbb {R}_{\max }\left\langle \left\langle A^{*}\right\rangle \right\rangle$ is the infinitary series $r^{\omega }\in \mathbb {R}_{\max }\left\langle \left\langle A^{\omega }\right\rangle \right\rangle$ which is defined by

$$\begin{aligned} (r^{\omega },w)=\sup \left\{ \sum \limits _{i\ge 1}d_{u_{1}\ldots u_{i-1}}(r,u_{i})\mid u_{i}\in A^{*},w=u_{1}u_{2}\ldots \right\} \end{aligned}$$

for every $w\in A^{\omega }$.

Example 22

Let $r=\max _{a\in A}\left( \left( k_{a}\right) _{a}\right) \in \mathbb {R}_{\max }\left\langle \left\langle A^{*}\right\rangle \right\rangle$ be a letter-step series. We will show that $\left( r^{+}\right) ^{+}=r^{+}$. Moreover, for every $w\in A^{\omega }$ we have $\left( r^{\omega },w\right) =\sum \nolimits _{i\ge 0}d_{w_{<i}}\left( r,w\left( i\right) \right)$.

Let $w=w\left( 0\right) \ldots w\left( n-1\right) \in A^{+}.$ Then

$$\begin{aligned} \left( r^{+},w\right)&=\max \left\{ \underset{1\le j\le k}{\sum }d_{u_{1}\ldots u_{j-1}}\left( r,u_{j}\right) \mid w=u_{1}\ldots u_{k},1\le k\le n\right\} \\&=\underset{0\le j\le n-1}{ {\displaystyle \sum }}d_{w_{<j}}\left( r,w\left( j\right) \right) . \end{aligned}$$

Furthermore, we get

$$\begin{aligned}&\left( \left( r^{+}\right) ^{+},w\right) \\&\quad =\max \left\{ \underset{1\le j\le k}{ {\displaystyle \sum }}d_{u_{1}\ldots u_{j-1}}\left( r^{+},u_{j}\right) \mid w=u_{1}\ldots u_{k},1\le k\le n\right\} \\&\quad =\max \left\{ \underset{1\le j\le k}{ {\displaystyle \sum }}d_{u_{1}\ldots u_{j-1}}\left( \underset{0\le i_{j}\le \left| u_{j}\right| -1}{ {\displaystyle \sum }}d_{\left( u_{j}\right) _{<i_{j}}}\left( r,u_{j}\left( i_{j}\right) \! \right) \right) \mid w=u_{1}\ldots u_{k},1\le k\le n\right\} \\&\quad =\max \left\{ \underset{1\le j\le k}{ {\displaystyle \sum }}\,\left( \underset{0\le i_{j}\le \left| u_{j}\right| -1}{\sum }d_{u_{1}\ldots u_{j-1}\left( u_{j}\right) _{<i_{j}}}\left( r,u_{j}\left( i_{j}\right) \right) \right) \mid w=u_{1}\ldots u_{k},1\le k\le n\right\} \\&\quad =\underset{0\le j\le n-1}{ {\displaystyle \sum }}d_{w_{<j}}\left( r,w\left( j\right) \right) =\left( r^{+},w\right) . \end{aligned}$$

Similarly, we can show that $\left( r^{\omega },w\right) =\sum \nolimits _{i\ge 0}d_{w_{<i}}\left( r,w\left( i\right) \right)$, for every $w\in A^{\omega }$.

Definition 23

The class of $\omega \hbox {-}d$-star-free series over $A$ and $\mathbb {R}_{\max }$, denoted by $\omega \hbox {-} SF ( \mathbb {R}_{\max },A,d)$, is the least class of infinitary series generated by the monomials (over $A$ and $\mathbb {R}_{\max }$) by applying finitely many times the operations of maximum, sum, complement, $+_{d}$, iteration restricted to letter-step series, and $\omega$-iteration restricted to letter-step series.

Remark 24

We could assume the application of the $\omega$-iteration, in the definition above, being applied to bounded series $r\in \omega \hbox {-} SF ( \mathbb {R}_{\max },A,d)$ with $r^{+}=r$. This induces a greater class of infinitary series (cf. Example 20) which, by Example 22, contains the class $\omega \hbox {-} SF ( \mathbb {R}_{\max },A,d)$ as defined above. Then, all of our results in this section can be established for this greater class. But we could not show that this class is contained in a fragment of our $\omega$-$d$-counter-free series (cf. Sect. 6).

The next result is trivially proved by Definitions 21, 23 and standard arguments.

Lemma 25

Let $r\in SF (\mathbb {R}_{\max },A,d)$ $($resp. $r\in \omega \hbox {-} SF ( \mathbb {R}_{\max },A,d))$ and $supp (r)\subseteq B^{*}$ $($resp. $supp (r)\subseteq B^{\omega })$ where $B\subseteq A$. Then $r\in SF ( \mathbb {R}_{\max },B,d)$ $($resp. $r\in \omega \hbox {-} SF ( \mathbb {R}_{\max },B,d))$.

In the sequel, we state several properties of the classes $SF (\mathbb {R}_{\max },A,d)$ and $\omega \hbox {-} SF ( \mathbb {R}_{\max },A,d)$.

Lemma 26

If $r\in SF (\mathbb {R}_{\max },A,d)$ $($resp. $r\in \omega \hbox {-} SF ( \mathbb {R}_{\max },A,d))$ and $k\in \mathbb {R}_{\max }$, then $k+r\in SF (\mathbb {R}_{\max },A,d)$ $($resp. $k+r\in \omega \hbox {-} SF ( \mathbb {R}_{\max },A,d))$.

Proof

We have $k+r=k_{\varepsilon }+_{d}r$, hence we get the proof of our claim.$\square$

Lemma 27

Let $L,L^{\prime }\subseteq A^{*}$ and $K,K^{\prime }\subseteq A^{\omega }$. Then

• $0_{L\cup L^{\prime }}=\max (0_{L},0_{L^{\prime }})$, $\ \ 0_{K\cup K^{\prime }}=\max (0_{K},0_{K^{\prime }})$

• $0_{L\cap L^{\prime }}=0_{L}+0_{L^{\prime }}$, $\ \ 0_{K\cap K^{\prime }}=0_{K}+0_{K^{\prime }}$

• $0_{LL^{\prime }}=0_{L}+_{d}0_{L^{\prime }},$ $0_{LK}=0_{L} +_{d}0_{K}$

• $0_{L^{+}}=\left( 0_{L}\right) ^{+}$ whenever $\varepsilon \notin L$

• $0_{L^{\omega }}=\left( 0_{L}\right) ^{\omega }$ whenever $\varepsilon \notin L.$

Proof

Trivial by standard arguments.$\square$

The two subsequent results are shown by induction on the structure of star-free (resp. $\omega$-star-free) languages and series using Lemma 27.

Lemma 28

For every $L\subseteq A^{*}$ the following statements are equivalent.

• (i) $L$ is a star-free language.

• (ii) $0_{L}\in SF \left( \mathbb {R} _{\max },A,d\right)$.

Lemma 29

For every $L\subseteq A^{\omega }$ the following statements are equivalent.

• (i) $L$ is an $\omega$-star-free language.

• (ii) $0_{L}\in \omega$-$SF \left( \mathbb {R} _{\max },A,d\right)$.

Since for every $L\subseteq A^{*}$ (resp. $L\subseteq A^{\omega }$) and $k\in \mathbb {R}_{\max }$ we have $k_{L}=k_{\varepsilon }+_{d}0_{L}$, by Lemmas 28 and 29, we get Lemma 30 below.

Lemma 30

Let $L\subseteq A^{*}$ $($resp. $L\subseteq A^{\omega })$ and $k\in \mathbb {R}_{\max }$. If $L$ is star-free $($resp. $\omega$-star-free$)$, then $k_{L}\in SF \left( \mathbb {R}_{\max },A,d\right)$ $($resp. $k_{L}\in \omega \hbox {-} SF \left( \mathbb {R}_{\max },A,d\right) )$.

A series $r\in \mathbb {R}_{\max }\left\langle \left\langle A^{*}\right\rangle \right\rangle$ (resp. $r\in \mathbb {R}_{\max }\left\langle \left\langle A^{\omega }\right\rangle \right\rangle$) is called a star-free (resp. an $\omega$-star-free) step function if $r=\max _{1\le i\le n}\left( \left( k_{i}\right) _{L_{i} }\right)$ where $k_{i}\in \mathbb {R}_{\max }$ and $L_{i}$ is a star-free (resp. an $\omega$-star-free) language for every $1\le i\le n$. The class of star-free (resp. $\omega$-star-free) languages is closed under intersection and complement, hence we can assume that the family $\left( L_{i}\right) _{1\le i\le n}$ is a partition of $A^{*}$ (resp. $A^{\omega }$).

Since the class of $d$-star-free (resp. $\omega$-$d$-star-free) series is closed under maximum, by Lemma 30 we get that every star-free (resp. $\omega$-star-free) step function is a $d$-star-free (resp. an $\omega \hbox {-}d$-star-free) series.

Proposition 31

The class of star-free $($resp. $\omega$-star-free$)$ step functions over $A$ and $\mathbb {R}_{\max }$ is closed under the operations of maximum and sum.

Proof

Let $r_{1}=\max _{1\le i\le n}\left( \left( k_{i}\right) _{L_{i}}\right)$ and $r_{2}=\max _{1\le j\le m}\left( \left( l_{j}\right) _{F_{j} }\right)$ be star-free (resp. $\omega$-star-free) step functions. Closure under maximum is obvious. Moreover, for every $1\le i\le n$ and $1\le j\le m$ the language $L_{i}\cap F_{j}$ is star-free (resp. $\omega$-star-free), hence the series $r_{1}+r_{2}=\max _{1\le i\le n,1\le j\le m}\left( \left( k_{i}+l_{j}\right) _{L_{i}\cap F_{j}}\right)$ is a star-free (resp. an $\omega$-star-free) step function.$\square$

Lemma 32

If $s\in SF \left( \mathbb {R}_{\max },A,d\right)$ $($resp. $s\in \omega \hbox {-} SF \left( \mathbb {R}_{\max },A,d\right) )$, then $supp (s)$ is a star-free language $($resp. an $\omega$-star-free$)$ language over $A$.

Proof

Using standard arguments, we state the proof by induction on the structure of $s$.$\square$

Lemma 33

• (i) Let $L\subseteq A^{*}$ be a star-free language and $B,\Gamma \subseteq A$ with $B\cap \Gamma =\emptyset$. Then $0_{L}|_{B^{*}\Gamma B^{*}}=\max _{1\le i\le n}\left( 0_{K_{i}}+_{d}\left( 0_{\gamma _{i}}+_{d}0_{K_{i}^{\prime }}\right) \right)$ where for every $1\le i\le n,$ $K_{i},K_{i}^{\prime }\subseteq B^{*}$ are star-free languages, and $\gamma _{i}\in \Gamma .$

• (ii) Let $L\subseteq A^{\omega }$ be an $\omega$-star-free language and $B,\Gamma \subseteq A$ with $B\cap \Gamma =\emptyset$. Then $0_{L}|_{B^{*}\Gamma B^{\omega }}=\max _{1\le i\le n}\left( 0_{K_{i}}+_{d}\left( 0_{\gamma _{i}}+_{d}0_{K_{i}^{\prime }}\right) \right)$ where for every $1\le i\le n,$ $K_{i}\subseteq B^{*}$ is star-free, $K_{i}^{\prime }\subseteq B^{\omega }$ is $\omega$-star-free, and $\gamma _{i}\in \Gamma .$

Proof

We prove only (ii); Statement (i) is shown with the same arguments. By the splitting lemma for $\omega$-star-free languages (cf. Lemma 3.2. in [7]), we get $L\cap B^{*}\Gamma B^{\omega }=\bigcup \nolimits _{1\le i\le n}K_{i}\gamma _{i}K_{i}^{\prime }$ where for every $1\le i\le n,$ $K_{i}\subseteq B^{*}$ is star-free, $\gamma _{i}\in \Gamma$, and $K_{i}^{\prime }\subseteq B^{\omega }$ is $\omega$-star-free. Since $0_{L}|_{B^{*}\Gamma B^{\omega }}=0_{L\cap B^{*}\Gamma B^{\omega }}$, we complete our proof using Lemma 27.$\square$

Now, we are ready to prove a splitting lemma for star-free and $\omega$-star-free series as well as the closure of these classes under inverse strict alphabetic epimorphisms.

Proposition 34

(Splitting lemma for finitary series) Let $s\in SF \left( \mathbb {R}_{\max },A,d\right)$ and $B,\Gamma \subseteq A$ with $B\cap \Gamma =\emptyset .$ Then $s|_{B^{*}\Gamma B^{*}}=\max _{1\le i\le n}\left( s_{1}^{(i)}+_{d}\left( s_{2}^{(i)}+_{d}s_{3}^{(i)}\right) \right)$ where for every $1\le i\le n,\; s_{1}^{(i)},s_{3}^{(i)}\in SF \left( \mathbb {R}_{\max },B,d\right)$ and $s_{2}^{(i)}=\left( k_{i}\right) _{\gamma _{i}}$ with $\gamma _{i}\in \Gamma ,k_{i}\in \mathbb {R}_{\max }$.

Proof

We use induction on the structure of $s$. Let $s=\left( k_{a}\right) _{a}, a\in A$, be a monomial. Then, if $a\in \Gamma$, we have $s|_{B^{*}\Gamma B^{*}}=0_{\varepsilon }+_{d}\left( \left( k_{a}\right) _{a} +_{d}0_{\varepsilon }\right)$, otherwise $s|_{B^{*}\Gamma B^{*} }=0_{\emptyset }+_{d}\left( \left( k_{\gamma }\right) _{\gamma } +_{d}0_{\emptyset }\right)$ for an arbitrary $\gamma \in \Gamma$. If $s=k_{\varepsilon }$, then again $s|_{B^{*}\Gamma B^{*}}=0_{\emptyset }+_{d}\left( \left( k_{\gamma }\right) _{\gamma }+_{d}0_{\emptyset }\right)$ for an arbitrary $\gamma \in \Gamma$.

Let $s,r\in SF \left( \mathbb {R}_{\max },A,d\right)$ satisfying the induction hypothesis. This means that $s|_{B^{*}\Gamma B^{*}}=\max _{1\le i\le n}\left( s_{1}^{(i)} +_{d}\left( s_{2}^{(i)}+_{d}s_{3}^{(i)}\right) \right)$ and $r|_{B^{*}\Gamma B^{*}}=\max _{1\le j\le m}\left( r_{1}^{(j)}+_{d}\left( r_{2}^{(j)}+_{d}r_{3}^{(j)}\right) \right)$ where for every $1\le i\le n$ and $1\le j\le m,$ we have $s_{1}^{(i)},s_{3}^{(i)},r_{1}^{(j)},r_{3}^{(j)}\in SF \left( \mathbb {R}_{\max },B,d\right) ,$ $s_{2}^{(i)}=\left( k_{i}\right) _{\gamma _{i}},\;r_{2}^{(j)}=\left( l_{j}\right) _{\gamma _{j}^{\prime }},\;\gamma _{i} ,\gamma _{j}^{\prime }\in \Gamma ,\;k_{i},l_{j}\in \mathbb {R}_{\max }$. Obviously, $\max \left( s,r\right) |_{B^{*}\Gamma B^{*}}$ has the required form.

Next let $w\in B^{*}\Gamma B^{*}$ and $0\le k\le \left| w\right| -1$ with $w(k)\in \Gamma$. Then $w_{<k},w_{>k}\in B^{*}$ and we have

$$\begin{aligned} \left( s|_{B^{*}\Gamma B^{*}},w\right)&=\left( \underset{1\le i\le n}{\max }\left( s_{1}^{(i)}+_{d}\left( s_{2}^{(i)}+_{d}s_{3}^{(i)}\right) \right) ,w\right) \\&=\underset{1\le i\le n}{\max }\left( \left( s_{1}^{(i)}+_{d}\left( s_{2}^{(i)}+_{d}s_{3}^{(i)}\right) ,w\right) \right) \\&=\underset{1\le i\le n}{\max }\left( \left( s_{1}^{(i)},w_{<k}\right) +d_{w_{<k}}\left( \left( s_{2}^{(i)},w(k)\right) +d_{w(k)}\left( s_{3}^{(i)},w_{>k}\right) \right) \right) \\&=\underset{1\le i\le n}{\max }\left( \left( s_{1}^{(i)},w_{<k}\right) +d_{w_{<k}}\left( s_{2}^{(i)},w(k)\right) +d_{w_{<k+1}}\left( s_{3} ^{(i)},w_{>k}\right) \right) \end{aligned}$$

where the third equality holds since for every $1\le i\le n$ and every decomposition $w=u_{1}u_{2}u_{3}$ with $u_{2}\ne w(k)$ we have $\left( s_{2}^{(i)},u_{2}\right) =-\infty$.

Similarly

$$\begin{aligned} \left( r|_{B^{*}\Gamma B^{*}},w\right)&=\left( \underset{1\le j\le m}{\max }\left( r_{1}^{(j)}+_{d}\left( r_{2}^{(j)}+_{d}r_{3}^{(j)}\right) \right) ,w\right) \\&=\underset{1\le j\le m}{\max }\left( \left( r_{1}^{(j)},w_{<k}\right) +d_{w_{<k}}\left( r_{2}^{(j)},w(k)\right) +d_{w_{<k+1}}\left( r_{3} ^{(j)},w_{>k}\right) \right) . \end{aligned}$$

Hence,

$$\begin{aligned} \left( \left( s+r\right) |_{B^{*}\Gamma B^{*}},w\right)&= \left( s|_{B^{*}\Gamma B^{*}},w\right) +\left( r|_{B^{*}\Gamma B^{*}},w\right) \\&= \underset{1\le i\le n}{\max }\left( \left( s_{1}^{(i)},w_{<k}\right) +d_{w_{<k}}\left( s_{2}^{(i)},w(k)\right) +d_{w_{<k+1}}\left( s_{3}^{(i)},w_{>k}\right) \right) \\&+\underset{1\le j\le m}{\max }\left( \left( r_{1}^{(j)},w_{<k}\right) \! +d_{w_{<k}}\left( r_{2}^{(j)},w(k)\right) +d_{w_{<k+1}}\left( r_{3} ^{(j)},w_{>k}\right) \! \right) \\&= \underset{1\le j\le m}{\underset{1\le i\le n}{\max }}\left( \left( s_{1}^{(i)}+r_{1}^{(j)},w_{<k}\right) +d_{w_{<k}}\left( \begin{array}{l} \left( s_{2}^{(i)}+r_{2}^{(j)},w(k)\right) \\ \quad +d_{w(k)}\left( s_{3}^{(i)}+r_{3}^{(j)},w_{>k}\right) \end{array} \right) \! \right) \\&= \left( \underset{1\le j\le m}{\underset{1\le i\le n}{\max }}\left( \left( s_{1}^{(i)}+r_{1}^{(j)}\right) +_{d}\left( \left( s_{2}^{(i)} +r_{2}^{(j)}\right) +_{d}\left( s_{3}^{(i)}+r_{3}^{(j)}\right) \right) \right) ,w\right) . \end{aligned}$$

Since $s_{1}^{(i)}+r_{1}^{(j)},\;s_{3}^{(i)}+r_{3}^{(j)}\in SF \left( \mathbb {R}_{\max },B,d\right) ,$ and $s_{2}^{(i)}+r_{2}^{(j)}=\left( k_{i} +l_{j}\right) _{\gamma _{i}}$ if $\gamma _{i}=\gamma _{j}^{\prime }$, and $s_{2}^{(i)}+r_{2}^{(j)}=-\infty _{\gamma }$ for an arbitrary $\gamma \in \Gamma$ otherwise, our claim is true for sum.

Furthermore,

$$\begin{aligned}&\left( \left( s+_{d}r\right) |_{B^{*}\Gamma B^{*}},w\right) \\&\quad =\max \left\{ \begin{array}{l} \max \left\{ \left( s|_{B^{*}\Gamma B^{*}},u\right) +d_{u}\left( r,v\right) \mid u\in B^{*}\Gamma B^{*},v\in B^{*},w=uv\right\} ,\\ \max \left\{ \left( s,u\right) +d_{u}\left( r|_{B^{*}\Gamma B^{*} },v\right) \mid u\in B^{*},v\in B^{*}\Gamma B^{*},w=uv\right\} \end{array} \right\} \end{aligned}$$

where

$$\begin{aligned}&\max \left\{ \left( s|_{B^{*}\Gamma B^{*}},u\right) +d_{u}\left( r,v\right) \mid u\in B^{*}\Gamma B^{*},v\in B^{*},w=uv\right\} \\&\quad =\max \left\{ \left( \underset{1\le i\le n}{\max }\left( s_{1} ^{(i)}+_{d}\left( s_{2}^{(i)}+_{d}s_{3}^{(i)}\right) \right) ,u\right) +d_{u}\left( r,v\right) \mid u\in B^{*}\Gamma B^{*},v\in B^{*},w=uv\right\} \\&\quad =\max \left\{ \left( \underset{1\le i\le n}{\max }\left( s_{1} ^{(i)}+_{d}\left( s_{2}^{(i)}+_{d}s_{3}^{(i)}\right) \right) ,u\right) +d_{u}\left( r|_{B^{*}},v\right) \mid u,v\in A^{*},w=uv\right\} \\&\quad =\left( \underset{1\le i\le n}{\max }\left( s_{1}^{(i)}+_{d}\left( s_{2}^{(i)}+_{d}s_{3}^{(i)}\right) \right) +_{d}r|_{B^{*}},w\right) \\&\quad =\left( \underset{1\le i\le n}{\max }\left( \left( s_{1}^{(i)} +_{d}\left( s_{2}^{(i)}+_{d}s_{3}^{(i)}\right) \right) +_{d}r|_{B^{*} }\right) ,w\right) \\&\quad =\left( \underset{1\le i\le n}{\max }\left( s_{1}^{(i)}+_{d}\left( s_{2}^{(i)}+_{d}\left( s_{3}^{(i)}+_{d}r|_{B^{*}}\right) \right) \right) ,w\right) \end{aligned}$$

where $r|_{B^{*}}=r+0_{B^{*}}\in SF \left( \mathbb {R} _{\max },B,d\right)$, and

$$\begin{aligned}&\max \left\{ \left( s,u\right) +d_{u}\left( r|_{B^{*}\Gamma B^{*}},v\right) \mid u\in B^{*},v\in B^{*}\Gamma B^{*},w=uv\right\} \\&\quad =\max \left\{ \left( s,u\right) +d_{u}\left( \underset{1\le j\le m}{\max }\left( r_{1}^{(j)}+_{d}\left( r_{2}^{(j)}+_{d}r_{3}^{(j)}\right) \right) ,v\right) \mid u\in B^{*},v\in B^{*}\Gamma B^{*},w=uv\right\} \\&\quad =\max \left\{ \left( s|_{B^{*}},u\right) +d_{u}\left( \underset{1\le j\le m}{\max }\left( r_{1}^{(j)}+_{d}\left( r_{2}^{(j)}+_{d}r_{3} ^{(j)}\right) \right) ,v\right) \mid u,v\in A^{*},w=uv\right\} \\&\quad =\left( s|_{B^{*}}+_{d}\underset{1\le j\le m}{\max }\left( r_{1}^{(j)}+_{d}\left( r_{2}^{(j)}+_{d}r_{3}^{(j)}\right) \right) ,w\right) \\&\quad =\left( \underset{1\le j\le m}{\max }\left( s|_{B^{*}}+_{d}\left( r_{1}^{(j)}+_{d}\left( r_{2}^{(j)}+_{d}r_{3}^{(j)}\right) \right) \right) ,w\right) \\&\quad =\left( \underset{1\le j\le m}{\max }\left( \left( s|_{B^{*}} +_{d}r_{1}^{(j)}\right) +_{d}\left( r_{2}^{(j)}+_{d}r_{3}^{(j)}\right) \right) ,w\right) . \end{aligned}$$

Thus,

$$\begin{aligned} \left( \left( s+_{d}r\right) |_{B^{*}\Gamma B^{*}},w\right) =\max \left\{ \begin{array} [c]{c} \left( \underset{1\le i\le n}{\max }\left( s_{1}^{(i)}+_{d}\left( s_{2}^{(i)}+_{d}\left( s_{3}^{(i)}+_{d}r|_{B^{*}}\right) \right) \right) ,w\right) ,\\ \left( \underset{1\le j\le m}{\max }\left( \left( s|_{B^{*}}+_{d} r_{1}^{(j)}\right) +_{d}\left( r_{2}^{(j)}+_{d}r_{3}^{(j)}\right) \right) ,w\right) \end{array} \right\} . \end{aligned}$$

Therefore, the series $\left( s+_{d}r\right) |_{B^{*}\Gamma B^{*}}$ has the required form.

Now, let $s$ be a letter-step series. Then, $s|_{B^{*}\Gamma B^{*} }=s|_{\Gamma }=\max _{\gamma \in \Gamma }\left( \left( k_{\gamma }\right) _{\gamma }\right)$. Let $w\in supp (s^{+})\cap B^{*}\Gamma B^{*}$, which implies that there is an index $0\le k\le \left| w\right| -1$ such that $w_{<k},w_{>k}\in B^{*}$ and $w(k)\in \Gamma$. Then

$$\begin{aligned} \left( \left( s^{+}\right) |_{B^{*}\Gamma B^{*}},w\right)&= \max \left\{ \left( s^{m}|_{B^{*}\Gamma B^{*}},w\right) \mid 1\le m\le \left| w\right| \right\} =\left( s^{\left| w\right| }|_{B^{*}\Gamma B^{*}},w\right) \\&= \underset{0\le j\le \left| w\right| -1}{\sum }d_{w_{<j}}\left( s,w(j)\right) \\&= \underset{0\le j\le k-1}{\sum }d_{w_{<j}}\left( s,w(j)\right) +d_{w_{<k}}\left( s,w(k)\right) +\underset{k<j\le \left| w\right| -1}{\sum }d_{w_{<j}}\left( s,w(j)\right) \\&= \left( \left( s|_{B^{*}}\right) ^{+}+_{d}\left( s|_{\Gamma } +_{d}\left( s|_{B^{*}}\right) ^{+}\right) ,w\right) \\&= \left( \max _{\gamma \in \Gamma }\left( \left( s|_{B^{*}}\right) ^{+}+_{d}\left( \left( k_{\gamma }\right) _{\gamma }+_{d}\left( s|_{B^{*}}\right) ^{+}\right) \right) ,w\right) \end{aligned}$$

and this concludes the induction for letter-step series.

Finally, let $s\in SF \left( \mathbb {R}_{\max },A,d\right)$. Then $\overline{s}=0_{\overline{ supp (s) }}$. Since $supp (s)$ is a star-free language, we get that $\overline{ supp (s) }$ is also star-free. Hence, by Lemma 33(i) we conclude our proof.$\square$

Proposition 35

(Splitting lemma for infinitary series) Let $s\in \omega \hbox {-} SF \left( \mathbb {R}_{\max },A,d\right)$ and $B,\Gamma \subseteq A$ with $B\cap \Gamma =\emptyset .$ Then $s|_{B^{*}\Gamma B^{\omega }}=\max _{1\le i\le n}\left( s_{1} ^{(i)}+_{d}\left( s_{2}^{(i)}+_{d}s_{3}^{(i)}\right) \right)$ where for every $1\le i\le n,\;s_{1}^{(i)}\in SF \left( \mathbb {R}_{\max },B,d\right) ,\;s_{3}^{(i)}\in \omega \hbox {-} SF \left( \mathbb {R}_{\max },B,d\right)$, and $s_{2}^{(i)}=\left( k_{i}\right) _{\gamma _{i}}$ with $\gamma _{i}\in \Gamma ,k_{i}\in \mathbb {R}_{\max }$.

Proof

Taking into account the definition of $\omega$-$d$-star-free series, firstly we embed the proof of Lemma 34. Furthermore, we use arguments of that proof as follows. For the operations of maximum and sum we let $s,r\in \omega \hbox {-} SF \left( \mathbb {R}_{\max },A,d\right)$, and for $+_{d}$ we let $s\in SF \left( \mathbb {R}_{\max },A,d\right)$ and $r\in \omega \hbox {-} SF \left( \mathbb {R}_{\max },A,d\right)$. For the complement operation, we let $s\in \omega \hbox {-} SF \left( \mathbb {R}_{\max },A,d\right)$ and we use the corresponding argument for $\omega$-star-free languages and Lemma 33(ii). Finally, let $s$ be a letter-step series. Then, $s|_{B^{*}\Gamma B^{*}}=s|_{\Gamma } =\max _{\gamma \in \Gamma }\left( \left( k_{\gamma }\right) _{\gamma }\right)$. Let $w\in supp (s^{\omega })\cap B^{*}\Gamma B^{\omega }$, i.e., there exists an index $k\ge 0$ such that $w_{<k}\in B^{*},w_{>k}\in B^{\omega }$, and $w(k)\in \Gamma$. Then we get

$$\begin{aligned} \left( \left( s^{\omega }\right) |_{B^{*}\Gamma B^{\omega }},w\right)&=\sup \left\{ \underset{i\ge 1}{\sum }d_{u_{1}\ldots u_{i-1}}(s,u_{i})\mid u_{i}\in A^{*},w=u_{1}u_{2}\ldots \right\} \\&=\underset{j\ge 0}{\sum }d_{w_{<j}}\left( s,w(j)\right) \\&=\underset{0\le j\le k-1}{\sum }d_{w_{<j}}\left( s,w(j)\right) +d_{w_{<k}}\left( s,w(k)\right) +\underset{j>k}{\sum }d_{w_{<j}}\left( s,w(j)\right) \\&=\left( \left( s|_{B^{*}}\right) ^{+}+_{d}\left( s|_{\Gamma } +_{d}\left( s|_{B^{*}}\right) ^{\omega }\right) ,w\right) \\&=\left( \max _{\gamma \in \Gamma }\left( \left( s|_{B^{*}}\right) ^{+}+_{d}\left( \left( k_{\gamma }\right) _{\gamma }+_{d}\left( s|_{B^{*}}\right) ^{\omega }\right) \right) ,w\right) \end{aligned}$$

i.e.,

$$\begin{aligned} \left( s^{\omega }\right) |_{B^{*}\Gamma B^{\omega }}=\max _{\gamma \in \Gamma }\left( \left( s|_{B^{*}}\right) ^{+}+_{d}\left( \left( k_{\gamma }\right) _{\gamma }+_{d}\left( s|_{B^{*}}\right) ^{\omega }\right) \right) \end{aligned}$$

and this completes our proof.$\square$

Proposition 36

Let $A,B$ be two alphabets and $h:A\rightarrow B$ a bijection. Furthermore, let $d=\Big (\overline{d_{a}}\Big )_{a\in A}$ be a discounting over $A$ and $\mathbb {R}_{\max }$, and $d^{\prime }=\left( \overline{d_{b}^{\prime }}\right) _{b\in B}$ a discounting over $B$ and $\mathbb {R}_{\max }$ determined for every $b\in B$ by $d_{b}^{\prime }=d_{h^{-1}\left( b\right) }$. Then, $s\in SF \left( \mathbb {R}_{\max },A,d\right)$ (resp. $s\in \omega \hbox {-} SF \left( \mathbb {R}_{\max },A,d\right)$) implies $h(s) \in SF \left( \mathbb {R}_{\max },B,d^{\prime }\right)$ (resp. $h(s) \in \omega \hbox {-} SF \left( \mathbb {R}_{\max },B,d^{\prime }\right)$).

Proof

Since $h$ is a bijection, the morphism $h:A^{*}\rightarrow B^{*}$ (resp. the mapping $h:A^{\omega }\rightarrow B^{\omega }$), that is derived by $h$ in the usual way, is an isomorphism (resp. a bijection). Therefore, $h$ defines a one-to-one correspondence between the words of $A^{*}$ and $B^{*}$ (resp. the words of $A^{\omega }$ and $B^{\omega }$). Then, we can easily state our proof by induction on the structure of $d$-star-free (resp. $\omega \hbox {-}d$-star-free) series.$\square$

Proposition 37

Let $A,B$ be alphabets and $h:A^{*}\rightarrow B^{*}$ a strict alphabetic epimorphism. Furthermore, let $d=\Big ( \overline{d_{a}}\Big ) _{a\in A}$ be a discounting over $A$ and $\mathbb {R}_{\max }$ such that $d_{a}=d_{a^{\prime }}$ whenever $h(a)=h(a^{\prime })$ for every $a,a^{\prime }\in A,$ and $d^{\prime }=\left( \overline{d_{b}^{\prime }}\right) _{b\in B}$ a discounting over $B$ and $\mathbb {R}_{\max }$ determined for every $b\in B$ by $d_{b}^{\prime }=d_{a}$ for $a\in A$ with $h(a)=b.$ Then $s\in SF \left( \mathbb {R}_{\max },B,d^{\prime }\right)$ $($resp. $s\in \omega \hbox {-} SF \left( \mathbb {R}_{\max },B,d^{\prime }\right) )$ implies $h^{-1}(s) \in SF \left( \mathbb {R}_{\max },A,d\right)$ $($resp. $h^{-1}(s) \in \omega \hbox {-} SF \left( \mathbb {R}_{\max },A,d\right) )$.

Proof

We prove our claim by induction on the structure of $d^{\prime }$-star-free $($resp. $\omega \hbox {-}d^{\prime }$-star-free$)$ series. Let $s=\left( k_{b}\right) _{b}$ be a monomial over $B$ and $\mathbb {R}_{\max }$. Then, $h^{-1}(s)$ is a letter-step series and thus a $d$-star-free series over $A$ and $\mathbb {R}_{\max }.$ If $s=k_{\varepsilon }$, then $h^{-1}(s) =k_{\varepsilon }$ since $h$ is strict. Next let $s_{1},s_{2}\in SF \left( \mathbb {R}_{\max },B,d^{\prime }\right)$ $($resp. $s_{1},s_{2}\in \omega \hbox {-} SF \left( \mathbb {R}_{\max },B,d^{\prime }\right) )$ such that $h^{-1}\left( s_{1}\right) ,h^{-1}\left( s_{2}\right) \in SF \left( \mathbb {R}_{\max },A,d\right)$ $($resp. $h^{-1}\left( s_{1}\right) ,h^{-1}\left( s_{2}\right) \in \omega \hbox {-} SF \left( \mathbb {R}_{\max },A,d\right) )$. Trivially $h^{-1}\left( s_{1}+s_{2}\right) =h^{-1}\left( s_{1}\right) +h^{-1}\left( s_{2}\right)$ and $h^{-1}\left( \max \left( s_{1},s_{2}\right) \right) =\max \left( h^{-1}\left( s_{1}\right) ,h^{-1}\left( s_{2}\right) \right)$.

Furthermore, for every $w\in A^{*}$ we have

$$\begin{aligned} \left( h^{-1}\left( s_{1}+_{d^{\prime }}s_{2}\right) ,w\right)&=\left( s_{1}+_{d^{\prime }}s_{2},h\left( w\right) \right) \\&=\max \left\{ \left( s_{1},u_{1}\right) +d_{u_{1}}^{\prime }\left( s_{2},u_{2}\right) \mid u_{1},u_{2}\in B^{*},u_{1}u_{2}=h\left( w\right) \right\} \\&=\max \left\{ \left( s_{1},h\left( w_{1}\right) \right) +d_{h\left( w_{1}\right) }^{\prime }\left( s_{2},h\left( w_{2}\right) \right) \mid w_{1},w_{2}\in A^{*},w_{1}w_{2}=w\right\} \\&=\max \left\{ \left( h^{-1}\left( s_{1}\right) ,w_{1}\right) +d_{w_{1} }\left( h^{-1}\left( s_{2}\right) ,w_{2}\right) \mid w_{1},w_{2}\in A^{*},w_{1}w_{2}\!=\!w\right\} \\&=\left( h^{-1}\left( s_{1}\right) +_{d}h^{-1}\left( s_{2}\right) ,w\right) \end{aligned}$$

where the third equality holds since $h$ is strict alphabetic. Hence $h^{-1}\left( s_{1}+_{d^{\prime }}s_{2}\right) =h^{-1}\left( s_{1}\right) +_{d}h^{-1}\left( s_{2}\right)$. If $s_{1}\in SF \left( \mathbb {R}_{\max },B,d^{\prime }\right) ,\; s_{2}\in \omega \hbox {-} SF \left( \mathbb {R}_{\max },B,d^{\prime }\right)$, and $w\in A^{\omega }$, then we use the same with above argument, where we write $\sup$ for $\max ,\; u_{2}\in B^{\omega }$, and $w_{2}\in A^{\omega }$.

Assume now that $s$ is a letter-step series over $B$ and $\mathbb {R}_{\max }$. Then, the series $h^{-1}(s)$ is a letter-step series over $A$ and $\mathbb {R}_{\max }$, hence $h^{-1}(s) \in SF \left( \mathbb {R}_{\max },A,d\right)$. For every $w\in A^{+}$ we get

$$\begin{aligned} (h^{-1}(s^{+}),w)&=(s^{+},h(w))=\underset{0\le j\le \left| h(w)\right| -1}{\sum }d_{h(w)_{<j}}^{\prime }(s,h(w)(j))\\&=\underset{0\le j\le \left| h(w)\right| -1}{\sum }d_{h(w)_{<j} }^{\prime }(s,h(w(j)))=\underset{0\le j\le \left| w\right| -1}{\sum }d_{w_{<j}}(h^{-1}(s),w(j))\\&=((h^{-1}(s))^{+},w), \end{aligned}$$

i.e., $h^{-1}(s^{+})=(h^{-1}(s))^{+}\in SF \left( \mathbb {R}_{\max },A,d\right)$.

Next, let $s\in SF \left( \mathbb {R}_{\max },B,d^{\prime }\right)$. Then, $\overline{s}=0_{\overline{ supp (s) }}$ and $\overline{ supp (s) }$ is, by Lemma 28, a star-free language over $B$. Moreover, the language $h^{-1}\left( \overline{ supp (s) }\right) \subseteq A^{*}$ is star-free (cf. for instance [25]) hence, the series $h^{-1}\left( \overline{s}\right) =h^{-1}\left( 0_{\overline{ supp (s) } }\right) =0_{h^{-1}\left( \overline{ supp (s) }\right) }$ is $d$-star-free by Lemma 28. The case $s\in \omega$-$SF \left( \mathbb {R}_{\max },B,d^{\prime }\right)$ is treated similarly.

Finally, assume that $s$ is a letter-step series over $B$ and $\mathbb {R}_{\max }$. Then, $h^{-1}(s)$ is a letter-step series over $A$ and $\mathbb {R}_{\max }$. Moreover, for every $w\in A^{\omega }$ we have

$$\begin{aligned} (h^{-1}(s^{\omega }),w)&=(s^{\omega },h(w))=\underset{j\ge 0}{\sum }d_{h(w)_{<j}}^{\prime }(s,h(w)(j))\\&=\underset{j\ge 0}{\sum }d_{h(w)_{<j}}^{\prime }(s,h(w(j)))=\underset{j\ge 0}{\sum }d_{w_{<j}}(h^{-1}(s),w(j))\\&=((h^{-1}(s))^{\omega },w), \end{aligned}$$

i.e., $h^{-1}\left( s^{\omega }\right) =\left( h^{-1}(s) \right) ^{\omega }\in \omega \hbox {-} SF \left( {\mathbb {R}}_{\max }, A,d\right)$, and our proof is completed.$\square$

Our next task is to show that every $\omega$-wqFO-$d$-definable series over $A$ and $\mathbb {R}_{\max }$ is an $\omega \hbox {-}d$-star-free series, i.e., $\omega \hbox {-} wqFO \left( \mathbb {R}_{\max },A,d\right) \subseteq \omega \hbox {-} SF \left( \mathbb {R}_{\max },A,d\right)$. For this, we use induction on the structure of $WQFO\left( \mathbb {R}_{\max },A\right)$ formulas.

Let $\mathcal {V}$ be a finite set of first-order variables and $A_{\mathcal {V} }=A\times \left\{ 0,1\right\} ^{\mathcal {V}}$. We define the discounting $\widetilde{d}=\left( \widetilde{d}_{\left( a,f\right) }\right) _{\left( a,f\right) \in A_{\mathcal {V}}}$ by setting $\widetilde{d}_{\left( a,f\right) }=d_{a}$ for every $\left( a,f\right) \in A_{\mathcal {V}}.$ Clearly for every $\left( w,\sigma \right) \in A_{\mathcal {V}}^{*}$ it holds $\widetilde{d}_{\left( w,\sigma \right) }=d_{w}$. In the sequel, for simplicity we identify $\widetilde{d}$ by $d.$ We shall need the following auxiliary result.

Lemma 38

Let $\varphi \in FO \left( \mathbb {R}_{\max },A\right)$ and $\mathcal {V}$ be a finite set of first-order variables containing $free\left( \varphi \right)$. If $\left\| \varphi \right\|$ is an $\omega \hbox {-}d$-star-free series $($resp. an $\omega$-star-free step function$)$, then $\left\| \varphi \right\| _{\mathcal {V}}$ is an $\omega \hbox {-}d$-star-free series $($resp. an $\omega$-star-free step function$)$.

Proof

Let $\left\| \varphi \right\| \$be an $\omega$-$d$-star-free series and $h:A_{\mathcal {V}}\rightarrow A_{ free \left( \varphi \right) }$ be the strict alphabetic epimorphism erasing the $x$-row for every $x\in \mathcal {V}\setminus free\left( \varphi \right)$. It holds $\left\| \varphi \right\| _{\mathcal {V}}=h^{-1}\left( \left\| \varphi \right\| \right) +0_{\mathcal {N}_{\mathcal {V}}}.$ Then by Proposition 37 we get that $h^{-1}\left( \left\| \varphi \right\| \right) \in \omega \hbox {-} SF \left( \mathbb {R}_{\max },A_{\mathcal {V}},d\right)$, and thus $\left\| \varphi \right\| _{\mathcal {V}}\in \omega \hbox {-} SF \left( \mathbb {R}_{\max },A_{\mathcal {V}},d\right)$ as wanted. Assume now that $\left\| \varphi \right\| =\max _{1\le i\le n}\left( \left( k_{i}\right) _{L_{i} }\right)$ where for every $1\le i\le n,\;k_{i}\in \mathbb {R}_{\max }$ and $L_{i}$ is an $\omega$-star-free language over $A_{ free \left( \varphi \right) }.$ Then for every $k\in \mathbb {R}_{\max }$, if $k\ne -\infty$ we get $\left\| \varphi \right\| _{\mathcal {V}}^{-1}(k)=h^{-1}\left( \left\| \varphi \right\| ^{-1}(k)\right) \cap \mathcal {N}_{\mathcal {V}}$ and for $k=-\infty$ we get $\left\| \varphi \right\| _{\mathcal {V}}^{-1}(-\infty )=h^{-1}\left( \left\| \varphi \right\| ^{-1}(-\infty )\right) \cup \left( A_{\mathcal {V}}^{\omega }\setminus \mathcal {N}_{\mathcal {V}}\right)$. Hence, for every $k\in \mathbb {R}_{\max }$ the language $\left\| \varphi \right\| _{\mathcal {V}}^{-1}(k)$ is $\omega$-star-free if the language $h^{-1}\left( \left\| \varphi \right\| ^{-1}(k)\right)$ is $\omega$-star-free. Since $\omega$-star-free languages are preserved by inverse strict alphabetic epimorphisms (cf. [25]) we are done.   $\square$

Lemma 39

Let $\varphi \in FO \left( \mathbb {R}_{\max },A\right)$ be an atomic formula. Then, $\left\| \varphi \right\|$ is an $\omega$-star-free step function.

Proof

If $\varphi =k\in \mathbb {R}_{\max }$, then $\left\| \varphi \right\| =k_{A^{\omega }}$. Next, if $\varphi =P_{a}\left( x\right)$ or $x<y$, then $\varphi$ is a boolean first-order formula, hence $\mathcal {L}(\varphi )$ is an $\omega$-star-free language and $\left\| \varphi \right\| =0_{\mathcal {L}\left( \varphi \right) }$ is an $\omega$-star-free step function.$\square$

Lemma 40

Let $\varphi \in FO \left( \mathbb {R}_{\max },A\right)$ such that $\left\| \varphi \right\|$ is an $\omega$-$d$-star-free series. Then $\left\| \lnot \varphi \right\|$ is also an $\omega$-$d$-star-free series.

Proof

By definition, we have $\left\| \lnot \varphi \right\| =\overline{\left\| \varphi \right\| }$.$\square$

Lemma 41

Let $\varphi ,\psi \in FO \left( \mathbb {R}_{\max },A\right)$. If $\left\| \varphi \right\| ,\left\| \psi \right\|$ are $\omega \hbox {-}d$-star-free series $($resp. $\omega$-star-free step functions$)$, then $\left\| \varphi \wedge \psi \right\| ,\left\| \varphi \vee \psi \right\|$ are $\omega$ -$d$-star-free series $($resp. $\omega$-star-free step functions$)$.

Proof

Let $\mathcal {V}= free \left( \varphi \right) \cup free\left( \psi \right)$. We have $\left\| \varphi \wedge \psi \right\| =\left\| \varphi \right\| _{\mathcal {V}}+\left\| \psi \right\| _{\mathcal {V}}$ and $\left\| \varphi \vee \psi \right\| =\max \left( \left\| \varphi \right\| _{\mathcal {V}},\left\| \psi \right\| _{\mathcal {V}}\right)$, hence our claim follows by definition of $\omega \hbox {-}d$-star-free series (resp. Proposition 31) and Lemma 38.$\square$

Lemma 42

Let $\varphi \in FO \left( \mathbb {R}_{\max },A\right)$ such that $\left\| \varphi \right\|$ is an $\omega \hbox {-}d$-star-free series. Then $\left\| \exists x.\varphi \right\|$ is also an $\omega \hbox {-}d$-star-free series.

Proof

Let $\mathcal {W=} free \left( \varphi \right) \cup \{x\}$ and $\mathcal {V} = free (\exists x.\varphi )=\mathcal {W}\setminus \left\{ x\right\}$. We define two subalphabets $B,\Gamma$ of $A_{\mathcal {W}}$ by letting $B=\left\{ \left( a,f\right) \in A_{\mathcal {W}}\mid f\left( x\right) =0\right\}$ and $\Gamma =\left\{ \left( a,f\right) \in A_{\mathcal {W}}\mid f\left( x\right) \!=\!1\right\}$. Since $\left\| \varphi \right\| _{\mathcal {W} }\in \omega \hbox {-} SF \left( \mathbb {R}_{\max },A_{\mathcal {W}},d\right)$ (by Lemma 38, in case $x\notin free (\varphi )$), by Proposition 35 we get

$$\begin{aligned} \left\| \varphi \right\| _{\mathcal {W}}|_{B^{*}\Gamma B^{*}} =\max _{1\le i\le n}\left( s_{1}^{(i)}+_{d}\left( s_{2}^{(i)}+_{d} s_{3}^{(i)}\right) \right) \end{aligned}$$

with $s_{1}^{(i)}\in SF \left( \mathbb {R}_{\max },B,d\right) ,\;s_{3}^{(i)}\in \omega \hbox {-} SF \left( \mathbb {R}_{\max },B,d\right) ,$ and $s_{2}^{(i)}=\left( k_{i}\right) _{\gamma _{i}},$ where $k_{i}\in \mathbb {R}_{\max },\;\gamma _{i}\in \Gamma$ for every $1\le i\le n$. We show that

$$\begin{aligned} \left\| \exists x.\varphi \right\| =\underset{1\le i\le n}{\max }\left( h|_{B}\left( s_{1}^{(i)}\right) +_{d}\left( \left( k_{i}\right) _{h\left( \gamma _{i}\right) }+_{d}h|_{B}\left( s_{3}^{(i)}\right) \right) \right) +0_{\mathcal {N}_{\mathcal {V}}} \end{aligned}$$

where $h:A_{\mathcal {W}}\rightarrow A_{\mathcal {V}}$ is the strict alphabetic epimorphism assigning $\left( a,f|_{\mathcal {V}}\right)$ to $\left( a,f\right)$ for every $\left( a,f\right) \in A_{\mathcal {W}}$.

Let $\left( w,\sigma \right) \in \mathcal {N}_{\mathcal {V}}$. Then we have

$$\begin{aligned}&\left( \left\| \exists x.\varphi \right\| ,\left( w,\sigma \right) \right) \\&\quad =\underset{j\ge 0}{\sup }\left( \left( \left\| \varphi \right\| _{\mathcal {W}},\left( w,\sigma \left[ x\rightarrow j\right] \right) \right) \right) \\&\quad =\underset{j\ge 0}{\sup }\left( \left( \left\| \varphi \right\| _{\mathcal {W}}|_{B^{*}\Gamma B^{\omega }},\left( w,\sigma \left[ x\rightarrow j\right] \right) \right) \right) \\&\quad =\underset{j\ge 0}{\sup }\left( \left( \underset{1\le i\le n}{\max }\left( s_{1}^{(i)}+_{d}\left( s_{2}^{(i)}+_{d}s_{3}^{(i)}\right) \right) ,\left( w,\sigma \left[ x\rightarrow j\right] \right) \right) \right) \\&\quad =\underset{j\ge 0}{\sup }\left( \underset{1\le i\le n}{\max }\left( \begin{array} [c]{l} \left( s_{1}^{(i)},\left( w,\sigma \left[ x\rightarrow j\right] \right) _{<j}\right) +d_{w_{<j}}\left( s_{2}^{(i)},\left( w,\sigma \left[ x\rightarrow j\right] \right) \left( j\right) \right) \\ \;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;+d_{w_{\le j}}\left( s_{3}^{(i)},\left( w,\sigma \left[ x\rightarrow j\right] \right) _{>j}\right) \end{array} \right) \right) \\&\quad =\underset{1\le i\le n}{\max }\left( \underset{j\ge 0}{\sup }\left( \begin{array} [c]{l} \left( s_{1}^{(i)},\left( w,\sigma \left[ x\rightarrow j\right] \right) _{<j}\right) +d_{w_{<j}}\left( s_{2}^{(i)},\left( w,\sigma \left[ x\rightarrow j\right] \right) \left( j\right) \right) \\ \;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;+d_{w_{\le j}}\left( s_{3}^{(i)},\left( w,\sigma \left[ x\rightarrow j\right] \right) _{>j}\right) \end{array} \right) \right) \\&\quad =\underset{1\le i\le n}{\max }\left( \underset{j\ge 0}{\sup }\left( \begin{array} [c]{l} \left( h|_{B}\left( s_{1}^{(i)}\right) ,\left( w,\sigma \right) _{<j}\right) +d_{w_{<j}}\left( \left( k_{i}\right) _{h\left( \gamma _{i}\right) },\left( w,\sigma \right) \left( j\right) \right) \\ \;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;+d_{w_{\le j}}\left( h|_{B}\left( s_{3}^{(i)}\right) ,\left( w,\sigma \right) _{>j}\right) \end{array} \right) \right) \\&\quad =\underset{1\le i\le n}{\max }\left( \left( h|_{B}\left( s_{1} ^{(i)}\right) +_{d}\left( \left( k_{i}\right) _{h\left( \gamma _{i}\right) }+_{d}h|_{B}\left( s_{3}^{(i)}\right) \right) ,\left( w,\sigma \right) \right) \right) \\&\quad =\left( \underset{1\le i\le n}{\max }\left( h|_{B}\left( s_{1} ^{(i)}\right) +_{d}\left( \left( k_{i}\right) _{h\left( \gamma _{i}\right) }+_{d}h|_{B}\left( s_{3}^{(i)}\right) \right) \right) ,\left( w,\sigma \right) \right) \end{aligned}$$

where the sixth equality holds since $h\left( k_{\gamma _{i}}\right) =k_{h(\gamma _{i})}$ and $h|_{B}:B\rightarrow A_{\mathcal {V}}$ is a bijection. On the other hand, for every $\left( w,\sigma \right) \in A_{\mathcal {V} }^{\omega }\setminus \mathcal {N}_{\mathcal {V}}$ we have

$$\begin{aligned} \left( \underset{1\le i\le n}{\max }\left( h|_{B}\left( s_{1} ^{(i)}\right) +_{d}\left( \left( k_{i}\right) _{h\left( \gamma _{i}\right) }+_{d}h|_{B}\left( s_{3}^{(i)}\right) \right) \right) +0_{\mathcal {N}_{\mathcal {V}}},\left( w,\sigma \right) \right) =-\infty . \end{aligned}$$

Hence, $\left\| \exists x.\varphi \right\| ={\max \nolimits _{1\le i\le n}}\left( h|_{B}\left( s_{1}^{(i)}\right) +_{d}\left( \left( k_{i}\right) _{h\left( \gamma _{i}\right) }+_{d}h|_{B}\left( s_{3}^{(i)}\right) \right) \right) +0_{\mathcal {N}_{\mathcal {V}}}$. By Proposition 36, for every $1\le i\le n$, we get that $h|_{B}\left( s_{1}^{i}\right) \in SF \left( \mathbb {R}_{\max },A_{\mathcal {V}},d\right) ,\;h|_{B}\left( s_{3}^{(i)}\right) \in \omega \hbox {-} SF \left( \mathbb {R}_{\max },A_{\mathcal {V}},d\right)$. Therefore $\left\| \exists x.\varphi \right\|$ is an $\omega \hbox {-}d$-star-free series.$\square$

Lemma 43

Let $\varphi \in FO \left( \mathbb {R}_{\max },A\right)$ be an FO-step formula. Then $\left\| \exists _{d}x.\varphi \right\|$ is an $\omega \hbox {-}d$-star-free series.

Proof

Let $\mathcal {W=}free\left( \varphi \right) \cup \{x\}$, $\mathcal {V} =\mathcal {W}\setminus \left\{ x\right\}$, and $\varphi =\bigvee \nolimits _{1\le i\le n}\left( k_{i}\wedge \varphi _{i}\right)$ where $\varphi _{i}\in bFO \left( \mathbb {R}_{\max },A\right)$ for every $1\le i\le n$. Then $L_{i}=\mathcal {L}(\varphi _{i})$ is an $\omega$-star-free language over $A_{\mathcal {W}}$ and $\left\| \varphi \right\| _{\mathcal {W}} =\max _{1\le i\le n}\left( \left( k_{i}\right) _{L_{i}}\right)$, i.e., $\left\| \varphi \right\| _{\mathcal {W}}$ is an $\omega$-star-free-step function (by Lemma 38, in case $x\notin free(\varphi )$). We consider the subalphabets $B,\Gamma$ of $A_{\mathcal {W}}$ as in the proof of the previous lemma. Then, for every $1\le i\le n,$ by Lemma 33(ii), we get

$$\begin{aligned} \left( 0_{L_{i}}\right) |_{B^{*}\Gamma B^{\omega }}=\underset{1\le l_{i}\le m_{i}}{\max }\left( 0_{L_{l_{i}}}+_{d}\left( 0_{\gamma _{l_{i}} }+_{d}0_{L_{l_{i}}^{\prime }}\right) \right) \end{aligned}$$

where $0_{L_{l_{i}}}\in SF \left( \mathbb {R}_{\max },B,d\right) ,\;0_{L_{l_{i}}^{\prime }}\in \omega \hbox {-} SF \left( \mathbb {R}_{\max },B,d\right)$, and $\gamma _{l_{i}}\in \Gamma$ for every $1\le l_{i}\le m_{i}$. Thus

$$\begin{aligned} \left\| \varphi \right\| _{\mathcal {W}}|_{B^{*}\Gamma B^{\omega }}&=\underset{1\le i\le n}{\max }\left( k_{i}+\underset{1\le l_{i}\le m_{i} }{\max }\left( 0_{L_{l_{i}}}+_{d}\left( 0_{\gamma _{l_{i}}}+_{d}0_{L_{l_{i} }^{\prime }}\right) \right) \right) \\&=\underset{1\le i\le n}{\max }\left( \underset{1\le l_{i}\le m_{i} }{\max }\left( k_{i}+\left( 0_{L_{l_{i}}}+_{d}\left( 0_{\gamma _{l_{i}}} +_{d}0_{L_{l_{i}}^{\prime }}\right) \right) \right) \right) . \end{aligned}$$

We show that

$$\begin{aligned} \left\| \exists _{d}x.\varphi \right\| =\underset{1\le i\le n}{\max }\left( \underset{1\le l_{i}\le m_{i}}{\max }\left( 0_{h|_{B}\left( L_{l_{i}}\right) }+_{d}\left( \left( k_{i}\right) _{h\left( \gamma _{l_{i}}\right) }+_{d}0_{h|_{B}\left( L_{l_{i}}^{\prime }\right) }\right) \right) \right) +0_{\mathcal {N}_{\mathcal {V}}} \end{aligned}$$

where $h:A_{\mathcal {W}}\rightarrow A_{\mathcal {V}}$ is the strict alphabetic epimorphism of Lemma 42. For every $\left( w,\sigma \right) \in \mathcal {N}_{\mathcal {V}}$ we have

$$\begin{aligned}&\left( \left\| \exists _{d}x.\varphi \right\| ,\left( w,\sigma \right) \right) \\&\quad =\underset{j\ge 0}{\sup }\left( d_{w_{<j}}\left( \left\| \varphi \right\| _{\mathcal {W}},\left( w,\sigma \left[ x\rightarrow j\right] \right) \right) \right) \\&\quad =\underset{j\ge 0}{\sup }\left( d_{w_{<j}}\left( \left\| \varphi \right\| _{\mathcal {W}}|_{B^{*}\Gamma B^{\omega }},\left( w,\sigma \left[ x\rightarrow j\right] \right) \right) \right) \\&\quad =\underset{j\ge 0}{\sup }\left( d_{w_{<j}}\left( \underset{1\le i\le n}{\max }\left( \underset{1\le l_{i}\le m_{i}}{\max }\left( k_{i}+\left( 0_{L_{l_{i}}}+_{d}\left( 0_{\gamma _{l_{i}}}+_{d}0_{L_{l_{i}}^{\prime } }\right) \right) \right) \right) ,\left( w,\sigma \left[ x\rightarrow j\right] \right) \right) \right) \\&\quad =\underset{j\ge 0}{\sup }\left( d_{w_{<j}}\left( \underset{1\le i\le n}{\max }\left( \underset{1\le l_{i}\le m_{i}}{\max }\left( \begin{array}{l} k_{i}+\left( 0_{L_{l_{i}}},\left( w,\sigma \left[ x\rightarrow j\right] \right) _{<j}\right) \\ \;\;\;\;\;\;\;+d_{w_{<j}}\left( 0_{\gamma _{l_{i}}},\left( w,\sigma \left[ x\rightarrow j\right] \right) \left( j\right) \right) \\ \;\;\;\;\;\;\;+d_{w_{\le j}}\left( 0_{L_{l_{i}}^{\prime } },\left( w,\sigma \left[ x\rightarrow j\right] \right) _{>j}\right) \end{array} \right) \! \right) \! \right) \! \right) \\&\quad =\underset{1\le i\le n}{\max }\left( \underset{1\le l_{i}\le m_{i}}{\max }\left( \underset{j\ge 0}{\sup }\left( \begin{array}{l} d_{w_{<j}}k_{i}+\left( 0_{h|_{B}\left( L_{l_{i}}\right) },\left( w,\sigma \right) _{<j}\right) \\ \;\;\;\;\;\;\;+\left( 0_{h\left( \gamma _{l_{i}}\right) },\left( w,\sigma \right) \left( j\right) \right) +\left( 0_{h|_{B}\left( L_{l_{i}}^{\prime }\right) },\left( w,\sigma \right) _{>j}\right) \end{array}\! \right) \! \right) \! \right) \\&\quad =\underset{1\le i\le n}{\max }\left( \underset{1\le l_{i}\le m_{i}}{\max }\left( \underset{j\ge 0}{\sup }\left( \begin{array}{l} \left( 0_{h|_{B}\left( L_{l_{i}}\right) },\left( w,\sigma \right) _{<j}\right) \\ \;\;\;\;+\left( d_{w_{<j}}\left( k_{i}\right) _{h\left( \gamma _{l_{i} }\right) },\left( w,\sigma \right) \left( j\right) \right) +\left( 0_{h|_{B}\left( L_{l_{i}}^{\prime }\right) },\left( w,\sigma \right) _{>j}\right) \end{array}\! \right) \! \right) \! \right) \\&\quad =\left( \underset{1\le i\le n}{\max }\left( \underset{1\le l_{i}\le m_{i}}{\max }\left( 0_{h|_{B}\left( L_{l_{i}}\right) }+_{d}\left( \left( k_{i}\right) _{h\left( \gamma _{l_{i}}\right) }+_{d}0_{h|_{B}\left( L_{l_{i}}^{\prime }\right) }\right) \right) \right) ,\left( w,\sigma \right) \right) . \end{aligned}$$

Hence, as in previous lemma, we get

$$\begin{aligned} \left\| \exists _{d}x.\varphi \right\| =\underset{1\le i\le n}{\max }\left( \underset{1\le l_{i}\le m_{i}}{\max }\left( 0_{h|_{B}\left( L_{l_{i}}\right) }+_{d}\left( \left( k_{i}\right) _{h\left( \gamma _{l_{i}}\right) }+_{d}0_{h|_{B}\left( L_{l_{i}}^{\prime }\right) }\right) \right) \right) +0_{\mathcal {N}_{\mathcal {V}}}. \end{aligned}$$

Since $h:B\rightarrow A_{\mathcal {V}}$ is a bijection, we get that $h|_{B}\left( L_{l_{i}}\right)$ is a star-free language and $h|_{B}\left( L_{l_{i}}^{\prime }\right)$ is an $\omega$-star-free language for every $1\le i\le n$ and $1\le l_{i}\le m_{i}$. Thus $\left\| \exists _{d}x.\varphi \right\|$ is an $\omega \hbox {-}d$-star-free series.$\square$

Lemma 44

Let $\varphi \in FO \left( \mathbb {R}_{\max },A\right)$ be a boolean, or a letter-step formula, or $\varphi =y\le x<z\rightarrow \psi$, or $\varphi =y\le x\rightarrow \psi$ where $\psi$ is a letter-step formula with free variable $x$. Then $\left\| \forall x.\varphi \right\|$ is an $\omega \hbox {-}d$-star-free series.

Proof

If $\varphi \in bFO \left( \mathbb {R}_{\max },A\right)$, then $\forall x.\varphi \in bFO \left( \mathbb {R}_{\max },A\right)$, hence the language $\mathcal {L}(\forall x.\varphi )$ is $\omega$-star-free and the series $\left\| \forall x.\varphi \right\| =0_{\mathcal {L}(\forall x.\varphi )}$ is $\omega \hbox {-}d$-star-free.

Next, assume that $\varphi =\bigvee \nolimits _{a\in A}\left( k_{a}\wedge P_{a}(x)\right)$ is a letter-step formula with $a\in A,\;k_{a}\in \mathbb {R}_{\max }$. We consider the letter-step series $r=\max _{a\in A}\left( \left( k_{a}\right) _{a}\right)$. Then for every word $w\in A^{\omega }$ we have

$$\begin{aligned} \left( \left\| \forall x.\varphi \right\| ,w\right)&=\underset{i\ge 0}{\sum }d_{w_{<i}}\left( \left\| \varphi \right\| ,\left( w,\left[ x\rightarrow i\right] \right) \right) \\&=\underset{i\ge 0}{\sum }d_{w_{<i}}\left( \left\| \bigvee \limits _{a\in A}\left( k_{a}\wedge P_{a}(x)\right) \right\| ,\left( w,\left[ x\rightarrow i\right] \right) \right) \\&=\underset{i\ge 0}{\sum }d_{w_{<i}}(r,w(i))\\&=\left( r^{\omega },w\right) \end{aligned}$$

where the fourth equality holds by Example 22. Hence, we get $\left\| \forall x.\varphi \right\| =r^{\omega }$ which implies that $\left\| \forall x.\varphi \right\|$ is an $\omega \hbox {-}d$-star-free series.

Next, let $\varphi =(y\le x)\rightarrow \bigvee \nolimits _{a\in A}\left( k_{a}\wedge P_{a}(x)\right)$. We consider the subset $F=\{(a,0)\mid a\in A\}$ of $A_{\{y\}}$. The language $F^{*}$ is star-free, hence, the series $0_{F^{*}}$ is $d$-star-free. Consider the series $s=\max _{a\in A}\left( \left( k_{a}\right) _{(a,0)}\right)$ and $s^{\prime }=\max _{a\in A}\left( \left( k_{a}\right) _{(a,1)}\right)$ over $A_{\{y\}}$ and $\mathbb {R}_{\max }$. Now for every $w\in A^{\omega }$ and $l\ge 0$, we get

$$\begin{aligned}&\left( \left\| \forall x.\varphi \right\| ,(w,[y\rightarrow l]\right) )\\&\quad =\underset{j\ge 0}{\sum }d_{w_{<j}}\left( \left\| (y\le x)\rightarrow \bigvee \limits _{a\in A}\left( k_{a}\wedge P_{a}(x)\right) \right\| ,\left( w,\left[ x\rightarrow j,y\rightarrow l\right] \right) \right) \\&\quad =\underset{j\ge l}{\sum }d_{w_{<j}}\left( \left\| \bigvee \limits _{a\in A}\left( k_{a}\wedge P_{a}(x)\right) \right\| ,\left( w,\left[ x\rightarrow j\right] \right) \right) \\&\quad =d_{w_{<l}}(s^{\prime },(w(l),1))+\underset{j>l}{\sum }d_{w_{<j} }(s,(w(j),0))\\&\quad =\left( 0_{F^{*}}+_{d}\left( s^{\prime }+_{d}s^{\omega }\right) ,(w,[y\rightarrow l]\right) ), \end{aligned}$$

i.e., $\left\| \forall x.\varphi \right\| =0_{F^{*}}+_{d}\left( s^{\prime }+_{d}s^{\omega }\right)$ is an $\omega \hbox {-}d$-star-free series.

Finally, let $\varphi =(y\le x<z)\rightarrow \bigvee \nolimits _{a\in A}\left( k_{a}\wedge P_{a}(x)\right)$. We consider the finite languages $F=\{(a,0,0)\mid a\in A\},\; F_{1}=\{(a,1,0)\mid a\in A\},\;F_{2} =\{(a,0,1)\mid a\in A\}$ and $F_{3}=\{(a,1,1)\mid a\in A\}$ over $A_{\{y,z\}}$. The languages $F,F_{1},F_{2},F_{3},F^{+},F^{*}$ are star-free, hence the series $0_{F_{1}},0_{F_{2}},0_{F_{3}},0_{F^{+}},0_{F^{*}}$ are $d$-star-free. Since $(F^{+})^{+}=F^{+}$ the languages $L=(F^{+})^{\omega },L^{\prime }=F_{2}L$ are $\omega$-star-free and the infinitary series $0_{L},0_{L^{\prime }}$ are $\omega \hbox {-}d$-star-free. We consider the series $s=\max _{a\in A}\left( k_{(a,0,0)}\right) _{(a,0,0)}$ and $s^{\prime } =\max _{a\in A}\left( k_{(a,1,0)}\right) _{(a,1,0)}$ over $A_{\{y,z\}}$ and $\mathbb {R}_{\max }$, where $k_{(a,0,0)}=k_{(a,0,1)}=k_{a}$ for every $a\in A$. Moreover, we let $r_{1}=0_{F^{*}}+_{d}\left( s^{\prime }+_{d}\left( \max \left( 0_{\varepsilon },s^{+}\right) +_{d}0_{L^{\prime }}\right) \right) ,\;r_{2}=0_{F^{*}}+_{d}\left( 0_{F_{3}}+_{d}0_{L}\right) ,$ and $r_{3}=0_{F^{*}}+_{d}\left( 0_{F_{2}}+_{d}\left( 0_{F^{*}}+_{d}\left( 0_{F_{1}}+_{d}0_{L}\right) \right) \right)$.

Now, for every $w\in A^{\omega }$ and $j,l\ge 0$ with $j<l$, we have $\left( \max \left( r_{2},r_{3}\right) ,(w,[y\rightarrow j,z\rightarrow l])\right) =-\infty$, and

$$\begin{aligned}&\left( \left\| \forall x.\varphi \right\| ,(w,[y\rightarrow j,z\rightarrow l]\right) )\\&\quad =\underset{i\ge 0}{\sum }d_{w_{<i}}\left( \left\| (y\le x<z)\rightarrow \bigvee \limits _{a\in A}\left( k_{a}\wedge P_{a}(x)\right) \right\| ,\left( w,\left[ x\rightarrow i,y\rightarrow j,z\rightarrow l\right] \right) \right) \\&\quad =\underset{j\le i<l}{\sum }d_{w_{<i}}\left( \left\| \bigvee \limits _{a\in A}\left( k_{a}\wedge P_{a}(x)\right) \right\| ,\left( w,\left[ x\rightarrow i\right] \right) \right) \\&\quad =d_{w_{<j}}(s^{\prime },(w(j),1,0))+\underset{j<i<l}{\sum }d_{w_{<i} }(s,(w(i),0,0))\\&\quad =\left( r_{1},(w,[y\rightarrow j,z\rightarrow l])\right) \\&\quad =\left( \max \left( r_{1},\max \left( r_{2},r_{3}\right) \right) ,(w,[y\rightarrow j,z\rightarrow l])\right) . \end{aligned}$$

Furthermore, for every $w\in A^{\omega }$ and $j,l\ge 0$ with $j\ge l$, we get $\left( r_{1},(w,[y\rightarrow j,z\rightarrow l])\right) =-\infty$, and

$$\begin{aligned}&\left( \left\| \forall x.\varphi \right\| ,(w,[y\rightarrow j,z\rightarrow l]\right) )\\&\quad =\underset{i\ge 0}{\sum }d_{w_{<i}}\left( \left\| (y\le x<z)\rightarrow \bigvee \limits _{a\in A}\left( k_{a}\wedge P_{a}(x)\right) \right\| ,\left( w,\left[ x\rightarrow i,y\rightarrow j,z\rightarrow l\right] \right) \right) \\&\quad =\underset{i\ge 0}{\sum }d_{w_{<i}}\left( \left\| \lnot \left( y\le x<z\right) \right\| ,\left( w,\left[ x\rightarrow i,y\rightarrow j,z\rightarrow l\right] \right) \right) \\&\quad =\left( \max \left( r_{2},r_{3}\right) ,\left( w,[y\rightarrow j,z\rightarrow l]\right) \right) \\&\quad =\left( \max \left( r_{1},\max \left( r_{2},r_{3}\right) \right) ,(w,[y\rightarrow j,z\rightarrow l])\right) . \end{aligned}$$

We conclude that $\left\| \forall x.\varphi \right\| =\max \left( r_{1},\max \left( r_{2},r_{3}\right) \right)$, hence $\left\| \forall x.\varphi \right\|$ is an $\omega \hbox {-}d$-star-free series, as required.$\square$

Now, we are ready to state the main result of the section.

Theorem 45

$\omega \hbox {-} wqFO \left( \mathbb {R}_{\max },A,d\right) \subseteq \omega \hbox {-} SF \left( \mathbb {R}_{\max },A,d\right)$.

Proof

We combine Lemmas 39, 40, 41, 42, 43, and 44.$\square$

Example 46

We consider the $WQFO \left( \mathbb {R}_{\max },A\right)$ sentence $\varphi ^{\prime }$ of Example 17 and the $\omega$-$d$-star-free series $r=\max \left( \left( 2_{a}\right) ^{+}+_{d}\left( 3_{b}\right) ^{\omega },\left( 3_{b}\right) ^{\omega }\right)$. It should be clear that $r=\left\| \varphi ^{\prime }\right\|$.

6 Counter-free series

In this section, we consider the concept of counter-freeness within weighted (resp. weighted Büchi) automata over $A$ and $\mathbb {R}_{\max }$. Our models will be nondeterministic. Furthermore, for simplicity reasons, we equip our finitary models with a set of final states instead of a terminal distribution. The main result of the section states that the class of $\omega \hbox {-}d$-star-free series is contained into a subclass of the behaviors of our counter-free weighted Büchi automata. First, we recall the notions of weighted automata and weighted Büchi automata with discounted behavior over $A$ and $\mathbb {R}_{\max }$ [11, 13].

A weighted automaton over $A$ and $\mathbb {R}_{\max }$ is a quadruple $\mathcal {A}=(Q,in,wt,F)$ where $Q$ is the finite state set, $in :Q\rightarrow \mathbb {R}_{\max }$ is the initial distribution, $wt :Q\times A\times Q\rightarrow \mathbb {R}_{\max }$ is a mapping assigning weights to the transitions of the automaton and $F\subseteq Q$ is the final state set.

Given a word $w=a_{0}\ldots a_{n-1}\in A^{*}$, a path of $\mathcal {A}$ over $w$ is a finite sequence of transitions $P_{w}\,{:}{=}\,\left( \left( q_{i},a_{i},q_{i+1}\right) \right) _{0\le i\le n-1}$. The running weight of $P_{w}$ is the value

$$\begin{aligned} rwt (P_{w})\,{:}{=}\,\sum \limits _{0\le i\le n-1}d_{w_{<i}} wt \left( \left( q_{i},a_{i},q_{i+1}\right) \right) \end{aligned}$$

and the weight of $P_{w}$ is given by

$$\begin{aligned} weight (P_{w})\,{:}{=}\, in (q_{0})+ rwt (P_{w}). \end{aligned}$$

The path $P_{w}$ is called successful if $q_{n}\in F$. Then, the $d$-behavior of $\mathcal {A}$ is the series $\left\| \mathcal {A} \right\| :A^{*}\rightarrow \mathbb {R}_{\max }$ which is defined, for every $w\in A^{*}$, by $\left( \left\| \mathcal {A}\right\| ,w\right) ={\max \nolimits _{P_{w}\text { succ}}}\left( weight (P_{w})\right)$. A series $r\in \mathbb {R}_{\max }\left\langle \left\langle A^{*}\right\rangle \right\rangle$ is called $d$-recognizable if it is the $d$-behavior of a weighted automaton over $A$ and $\mathbb {R}_{\max }$.

A weighted Büchi automaton $\mathcal {A}=(Q, in , wt ,F)$ over $A$ and $\mathbb {R}_{\max }$ is defined as a weighted automaton. Given an infinite word $w=a_{0}a_{1}\ldots \in A^{\omega }$, a path of $\mathcal {A}$ over $w$ is an infinite sequence of transitions $P_{w}\,{:}{=}\,\left( \left( q_{i},a_{i},q_{i+1}\right) \right) _{i\ge 0}$. The running weight of $P_{w}$ is the value

$$\begin{aligned} rwt (P_{w})\,{:}{=}\,\sum \limits _{i\ge 0}d_{w_{<i}}wt\left( \left( q_{i} ,a_{i},q_{i+1}\right) \right) \end{aligned}$$

and the weight of $P_{w}$ is given by

$$\begin{aligned} weight (P_{w})\,{:}{=}\,in(q_{0})+rwt(P_{w}) \end{aligned}$$

where the infinite sum converges, since $\sum \nolimits _{i\ge 0}d_{w_{<i}} wt \left( \left( q_{i},a_{i},q_{i+1}\right) \right) \le m/(1-M_{d})$ with $m=\max \left\{ wt \left( \left( q,a,q^{\prime }\right) \right) \mid \left( q,a,q^{\prime }\right) \in Q\times A\times Q\right\}$ and $M_{d}=\max \left\{ d_{a}\mid a\in A\right\}$.

A path $P_{w}$ is called successful if at least one final state occurs infinitely often along $P_{w}$. Then, the $d$-behavior of $\mathcal {A}$ is the infinitary series $\left\| \mathcal {A}\right\| :A^{\omega }\rightarrow \mathbb {R}_{\max }$ whose coefficients are given by $\left( \left\| \mathcal {A} \right\| ,w\right) ={\sup \nolimits _{P_{w}\text { succ}}}\left( weight (P_{w})\right)$, for every $w\in A^{\omega }$. An infinitary series $r\in \mathbb {R}_{\max }\left\langle \left\langle A^{\omega }\right\rangle \right\rangle$ is called $\omega \hbox {-}d$-recognizable if it is the $d$-behavior of a weighted Büchi automaton over $A$ and $\mathbb {R}_{\max }$.

It should be clear that $d$-recognizable and $\omega \hbox {-}d$-recognizable series are bounded. We shall need also the following notation. Given a weighted (resp. weighted Büchi) automaton $\mathcal {A}=(Q, in , wt ,F)$, a word $w=a_{0}\ldots a_{n-1}\in A^{*}$, and states $q,q^{\prime }\in Q$, we shall denote by $P_{\left( q,w,q^{\prime }\right) }$ a path of $\mathcal {A}$ over $w$ starting at state $q$ and terminating at state $q^{\prime }$, i.e., $P_{\left( q,w,q^{\prime }\right) }=\left( q,a_{0},q_{1}\right) \left( \left( q_{i},a_{i},q_{i+1}\right) \right) _{1\le i\le n-2}\left( q_{n-1},a_{n-1},q^{\prime }\right)$. Then

$$\begin{aligned} rwt \left( P_{\left( q,w,q^{\prime }\right) }\right)&= wt \left( \left( q,a_{0},q_{1}\right) \right) +\sum \limits _{1\le i\le n-2}d_{w_{<i} } wt \left( \left( q_{i},a_{i},q_{i+1}\right) \right) \\&+\,d_{w_{<n-1}} wt \left( \left( q_{n-1},a_{n-1},q^{\prime }\right) \right) . \end{aligned}$$

Now, we are ready to introduce our counter-free weighted and counter-free weighted Büchi automata.

Definition 47

A weighted automaton (resp. weighted Büchi automaton) $\mathcal {A} =(Q, in , wt ,F)$ over $A$ and $\mathbb {R}_{\max }$ is called counter-free (cfwa, resp. cfwBa, for short) if for every $q\in Q, w\in A^{*}$, and $n\ge 1$, the relation ${\max \nolimits _{P_{\left( q,w^{n},q\right) }}}\left( rwt \left( P_{\left( q,w^{n},q\right) }\right) \right) \ne -\infty$ implies ${\max \nolimits _{P_{\left( q,w^{n},q\right) }}}\left( rwt \left( P_{\left( q,w^{n},q\right) }\right) \right) ={\sum \nolimits _{0\le i\le n-1}}\left( d_{w}\right) ^{i}{\max \nolimits _{P_{\left( q,w,q\right) }}}\left( rwt \left( P_{\left( q,w,q\right) }\right) \right)$.

A series $r\in \mathbb {R}_{\max }\left\langle \left\langle A^{*}\right\rangle \right\rangle$ (resp. $r\in \mathbb {R}_{\max }\left\langle \left\langle A^{\omega }\right\rangle \right\rangle$) is called $d$-counter-free (resp. $\omega \hbox {-}d$-counter-free) if it is accepted by a cfwa (resp. cfwBa) over $A$ and $\mathbb {R}_{\max }$. We shall denote by $CF (\mathbb {R}_{\max },A,d)$ (resp. $\omega \hbox {-} CF ( \mathbb {R}_{\max },A,d)$) the class of all $d$-counter-free (resp. $\omega \hbox {-}d$-counter-free) series over $A$ and $\mathbb {R}_{\max }$.

A cfwa $\mathcal {A}=(Q, in , wt ,F)$ over $A$ and $\mathbb {R}_{\max }$ is called normalized if there are two states $q_{0},q_{t}\in Q$ such that $F=\{q_{t}\}$ and for every $q\in Q,\; a\in A$, we have $in (q)=0$ if $q=q_{0}$ and $-\infty$ otherwise, and $wt ((q,a,q_{0}))=-\infty = wt ((q_{t},a,q))$. We denote a normalized cfwa $\mathcal {A}$ simply by $\mathcal {A}=(Q,q_{0}, wt ,q_{t})$.

The following result has been proved for weighted automata in [11].

Lemma 48

For every cfwa $\mathcal {A}=(Q, in , wt ,F)$ we can effectively construct a normalized cfwa $\mathcal {A}^{\prime }=(Q\cup \{q_{0},q_{t} \},q_{0},wt^{\prime },q_{t})$ such that $\left( \left\| \mathcal {A}^{\prime }\right\| ,w\right) =\left( \left\| \mathcal {A}\right\| ,w\right)$ for every $w\in A^{+}$ and $\left( \left\| \mathcal {A}^{\prime }\right\| ,\varepsilon \right) =-\infty$.

Proof

We adapt the proof of Lemma 7 in [11]. In fact, it remains to show that the normalized weighted automaton $\mathcal {A}^{\prime }$ is counter-free. Indeed, let $q\in Q\cup \{q_{0},q_{t}\},\;w\in A^{+},\;n\ge 1,$ and $P_{(q,w^{n},q)}^{\prime }$ be a path of $\mathcal {A}^{\prime }$ over $w$ with $rwt (P_{(q,w^{n},q)}^{\prime })\ne -\infty .$ Since $\mathcal {A}^{\prime }$ is normalized we get that the states $q_{0},q_{t}$ do not occur in the path $P_{(q,w^{n},q)}^{\prime }$ hence $P_{(q,w^{n},q)}^{\prime }$ is also a path of $\mathcal {A}.$ This implies that ${\max \nolimits _{P_{\left( q,w^{n},q\right) } }}\left( rwt \left( P_{\left( q,w^{n},q\right) }\right) \right) ={\sum \nolimits _{0\le i\le n-1}}\left( d_{w}\right) ^{i}{\max \nolimits _{P_{\left( q,w,q\right) }}}\left( rwt \left( P_{\left( q,w,q\right) }\right) \right)$, and we are done.$\square$

A cfwBa $\mathcal {A}=(Q, in , wt ,F)$ over $A$ and $\mathbb {R}_{\max }$ is called initial weight normalized if there is a state $q_{0}\in Q$ such that for every $q\in Q$ and $a\in A$ we have $in(q)=0$ if $q=q_{0}$ and $-\infty$ otherwise, and $wt ((q,a,q_{0}))=-\infty$. We denote an initial weight normalized cfwBa $\mathcal {A}$ simply by $\mathcal {A} =(Q,q_{0}, wt ,F).$

Lemma 49

For every cfBwa $\mathcal {A}=(Q, in , wt ,F)$ we can effectively construct an initial weight normalized cfwBa $\mathcal {A}^{\prime } =(Q\cup \{q_{0}\},q_{0}, wt ^{\prime },F)$ such that $\left\| \mathcal {A}^{\prime }\right\| =\left\| \mathcal {A}\right\|$.

Proof

We use the same arguments, as in Lemma 48 for the modification of the initial distribution.$\square$

In the sequel, we prove closure properties of the classes $CF ( \mathbb {R}_{\max },A,d)$ and $\omega \hbox {-} CF ( \mathbb {R}_{\max },A,d)$. We shall need these properties in order to relate $d$-star-free and $\omega \hbox {-}d$-star-free series with $d$-counter-free and $\omega \hbox {-}d$-counter-free series, nevertheless, these results have also their own interest.

Proposition 50

The class $CF ( \mathbb {R}_{\max },A,d)$ contains the monomials and it is closed under maximum, sum, complement, $+_{d}$, and iteration restricted to letter-step series.

Proof

The closure of $CF ( \mathbb {R}_{\max },A,d)$ under maximum, is shown by taking the disjoint union of two cfwa. In this case, any “loop” belongs either to the first or to the second automaton, hence the derived weighted automaton is also counter-free. Since monomials over $A$ and $\mathbb {R}_{\max }$ are obviously $d$-counter-free series, we get that letter-step series are also $d$-counter-free.

Closure under sum is proved by using the standard “product construction” of two cfwa. More precisely, let $\mathcal {A}_{1}\mathcal {=}(Q_{1}, in _{1}, wt _{1},F_{1})$ and $\mathcal {A}_{2}\,\mathcal {=}(Q_{2}, in _{2}, wt _{2},F_{2})$ be two cfwa over $A$ and $\mathbb {R}_{\max }$. Consider the weighted automaton $\mathcal {A=}(Q, in , wt ,F)$ with $Q=Q_{1}\times Q_{2}$, $F=F_{1}\times F_{2},$ and $in ((q_{1},q_{2} ))=in_{1}(q_{1})+in_{2}(q_{2}), wt (((q_{1},q_{2}),a,(p_{1},p_{2} )))= wt _{1}((q_{1},a,p_{1}))+ wt _{2}((q_{2},a,p_{2}))$, for every $(q_{1},q_{2}),(p_{1},p_{2})\in Q,a\in A$. Then, for every $w\in A^{*}$ and path $P_{w}$ of $\mathcal {A}$ over $w$, there are two unique paths $P_{1,w}$ of $\mathcal {A}_{1}$ over $w$, and $P_{2,w}$ of $\mathcal {A}_{2}$ over $w$ (obtained by projections of $P_{w}$ on $Q_{1}$ and $Q_{2}$, respectively, in the obvious way) and vice-versa. Furthermore, we have $weight (P_{w} )= weight (P_{1,w})+ weight (P_{2,w}).$ Now assume that for some $(q_{1},q_{2})\in Q,\;w\in A^{*},$ and $n\ge 1$ there is a path $P_{\left( (q_{1},q_{2}),w^{n},(q_{1},q_{2})\right) }$ with $rwt \left( P_{\left( (q_{1},q_{2}),w^{n},(q_{1},q_{2})\right) }\right) \ne -\infty$. Then

$$\begin{aligned}&\underset{0\le i\le n-1}{\sum }\left( d_{w}\right) ^{i}\underset{P_{\left( (q_{1}q_{2}),w,(q_{1},q_{2})\right) }}{\max }\left( rwt \left( P_{\left( (q_{1},q_{2}),w,(q_{1},q_{2})\right) }\right) \right) \\&\quad =\underset{0\le i\le n-1}{\sum }\left( d_{w}\right) ^{i}\underset{P_{1,\left( q_{1},w,q_{1}\right) },P_{2,\left( q_{2},w,q_{2}\right) } }{\max }\left( rwt \left( P_{1,\left( q_{1},w,q_{1}\right) }\right) + rwt \left( P_{2,\left( q_{2},w,q_{2}\right) }\right) \right) \\&\quad =\underset{0\le i\le n-1}{\sum }\left( d_{w}\right) ^{i}\left( \underset{P_{1,\left( q_{1},w,q_{1}\right) }}{\max }\left( rwt \left( P_{1,\left( q_{1},w,q_{1}\right) }\right) \right) +\underset{P_{2,\left( q_{2},w,q_{2}\right) }}{\max }\left( rwt \left( P_{2,\left( q_{2} ,w,q_{2}\right) }\right) \right) \right) \\&\quad =\underset{P_{1,\left( q_{1},w^{n},q_{1}\right) }}{\max }\left( rwt \left( P_{1,\left( q_{1},w^{n},q_{1}\right) }\right) \right) +\underset{P_{2,\left( q_{2},w^{n},q_{2}\right) }}{\max }\left( rwt \left( P_{2,\left( q_{2},w^{n},q_{2}\right) }\right) \right) \\&\quad =\underset{P_{\left( (q_{1}q_{2}),w^{n},(q_{1},q_{2})\right) }}{\max }\left( rwt \left( P_{\left( (q_{1},q_{2}),w^{n},(q_{1},q_{2})\right) }\right) \right) \end{aligned}$$

which implies that $\mathcal {A}$ is counter-free, and by construction $\left\| \mathcal {A}\right\| =\left\| \mathcal {A}_{1}\right\| +\left\| \mathcal {A}_{2}\right\|$.

Next, let $r\in CF ( \mathbb {R}_{\max },A,d)$ and $\mathcal {A}=(Q, in , wt ,F)$ be a cfwa accepting $r$. We consider the nondeterministic finite automaton $\mathcal {A}^{\prime }=(Q,A,I,\Delta ,F)$ with $I=\{q\in Q\mid in (q)\ne -\infty \}$ and $\Delta =\{(q,a,q^{\prime })\in Q\times A\times Q\mid wt ((q,a,q^{\prime } ))\ne -\infty \}$. By construction of $\mathcal {A}^{\prime }$, we get that for every $q_{1},q_{2}\in Q$ and $w\in A^{*}$ the path $P_{(q_{1},w,q_{2})}$ exists in $\mathcal {A}^{\prime }$ iff $rwt (P_{(q_{1},w,q_{2})})\ne -\infty$ in $\mathcal {A}$. Therefore, $\mathcal {A}^{\prime }$ accepts the language $supp (r)$ and it is trivially counter-free hence, $supp (r)$ is a counter-free language. Then, $\overline{ supp (r)}$ is a counter-free language and let $\mathcal {B}$ be a counter-free automaton accepting it. We convert $\mathcal {B}$, in the obvious way, to a weighted automaton $\mathcal {B}^{\prime }$ (with weights only 0 and $-\infty$) over $A$ and $\mathbb {R}_{\max }$. Now, $\mathcal {B}^{\prime }$ trivially accepts $0_{\overline{ supp (r)}}=\overline{r}$, and it is easily obtained that it is counter-free. We conclude that the series $\overline{r}$ is $d$-counter-free, as required.

Let now $\mathcal {A}_{1}\mathcal {=}(Q_{1}, in _{1}, wt _{1},F_{1})$ and $\mathcal {A}_{2} =(Q_{2}, in _{2}, wt _{2},F_{2})$ be two cfwa over $A$ and $\mathbb {R}_{\max }$. Using Lemma 48 we consider the normalized cfwa $\mathcal {A}_{1}^{\prime }\mathcal {=}(Q_{1}\cup \{q_{0,1},q_{t,1}\},q_{0,1} , wt _{1}^{\prime },q_{t,1})$ and $\mathcal {A}_{2}^{\prime }\mathcal {=}(Q_{2} \cup \{q_{0,2},q_{t,2}\},q_{0,2}, wt _{2}^{\prime },q_{t,2})$ such that $\left\| \mathcal {A}_{i}^{\prime }\right\|$ coincides with $\left\| \mathcal {A}_{i}\right\|$ on $A^{+}$ for $i=1,2$. Without any loss, we assume that $(Q_{1}\cup \{q_{0,1},q_{t,1}\})\cap (Q_{2}\cup \{q_{0,2} ,q_{t,2}\})=\emptyset$. We construct the weighted automaton $\mathcal {A=} (Q,q_{0,1}, wt ,q_{t,2})$ with $Q=Q_{1}\cup \{q_{0,1}\}\cup Q_{2}\cup \{q_{0,2},q_{t,2}\}$ where we identify the states $q_{t,1}$ and $q_{0,2}$, and define the weight assignment mapping $wt$ for every $q,q^{\prime }\in Q,a\in A$ as follows:

$$\begin{aligned} wt ((q,a,q^{\prime }))=\left\{ \begin{array}{l@{\quad }l} wt _{1}^{\prime }((q,a,q^{\prime })) &{} \hbox {if}\; q,q^{\prime }\in Q_{1}\cup \{q_{0,1}\}\\ wt _{2}^{\prime }((q,a,q^{\prime })) &{} \hbox {if}\; q,q^{\prime }\in Q_{2}\cup \{q_{0,2},q_{t,2}\}\\ wt _{1}^{\prime }((q,a,q_{t,1})) &{} \hbox {if} \; q\in Q_{1}\cup \{q_{0,1}\}\; \hbox {and}\; q^{\prime }=q_{0,2}\\ -\infty &{} \hbox {otherwise}. \end{array}\right. \end{aligned}$$

It is a routine matter to formally state that $\left\| \mathcal {A}\right\| =\left\| \mathcal {A} _{1}^{\prime }\right\| +_{d}\left\| \mathcal {A}_{2}^{\prime }\right\| .$ Furthermore, the weighted automaton $\mathcal {A}$ is counter-free since, by construction, any “loop” with weight $\ne -\infty$ belongs either to $\mathcal {A}_{1}^{\prime }$ or to $\mathcal {A}_{2}^{\prime }$. Now we let $k_{i}=(\left\| \mathcal {A}_{i}\right\| ,\varepsilon )$ for $i=1,2.$ Then $\left\| \mathcal {A}_{1}\right\| +_{d}\left\| \mathcal {A}_{2}\right\| =\max (\left\| \mathcal {A}_{1}^{\prime }\right\| +_{d}\left\| \mathcal {A}_{2}^{\prime }\right\| ,\left( k_{1}\right) _{\varepsilon }+_{d}\left\| \mathcal {A}_{2}^{\prime }\right\| ,\left\| \mathcal {A}_{1}^{\prime }\right\| +_{d}\left( k_{2}\right) _{\varepsilon },\left( k_{1}\right) _{\varepsilon }+_{d}\left( k_{2}\right) _{\varepsilon })$. One can trivially construct cfwa accepting $\left( k_{1}\right) _{\varepsilon }$ and $\left( k_{2}\right) _{\varepsilon }$ and using simplifications of our previous construction¹ for $\mathcal {A}$ can easily show that the series $\left( k_{1}\right) _{\varepsilon }+_{d}\left\| \mathcal {A}_{2}^{\prime }\right\| ,\; \left\| \mathcal {A}_{1}^{\prime }\right\| +_{d}\left( k_{2}\right) _{\varepsilon }$, and $\left( k_{1}\right) _{\varepsilon }+_{d}\left( k_{2}\right) _{\varepsilon }$ are $d$-counter-free which implies, by what we have shown, that $\left\| \mathcal {A}_{1}\right\| +_{d}\left\| \mathcal {A}_{2}\right\|$ is a $d$-counter-free series.

Finally, let $r=\max _{a\in A}\left( \left( k_{a}\right) _{a}\right)$ be a letter-step series with $k_{a}\in \mathbb {R}_{\max }$ for every $a\in A$. We consider the cfwa $\mathcal {A}=(\{q_{0},q_{t}\},q_{0}, wt ,q_{t})$ with $wt \left( \left( q_{0},a,q_{t}\right) \right) = wt \left( \left( q_{t},a,q_{t}\right) \right) =k_{a}$ for every $a\in A$, and the weight of any other transition is $-\infty$. Obviously $r^{+}=\left\| \mathcal {A}\right\|$, and we are done.$\square$

Proposition 51

The class $\omega \hbox {-} CF ( \mathbb {R}_{\max },A,d)$ is closed under maximum, complement, $+_{d}$ and $\omega$-iteration restricted to letter-step series.

Proof

The closure under maximum and complement is shown as in Proposition 50. Especially, for the complement we use the fact that the class of counter-free Büchi recognizable (i.e., $\omega$-star-free) languages is closed under complement (cf. [7]).

Next, let $s_{1}\in CF ( \mathbb {R}_{\max },A,d)$ and $s_{2}\in \omega \hbox {-} CF ( \mathbb {R}_{\max },A,d)$, and $\mathcal {A}_{1}=(Q_{1}, in _{1}, wt _{1},F_{1}),\mathcal {A} _{2}=(Q_{2}, in _{2}, wt _{2},F_{2})$ be a cfwa and a cfwBa over $A$ and $\mathbb {R}_{\max }$ accepting $s_{1}$ and $s_{2}$, respectively. Furthermore, let $\mathcal {A}_{1}^{\prime }\mathcal {=}(Q_{1}\cup \{q_{0,1},q_{t}\},q_{0,1} , wt _{1}^{\prime },q_{t})$ be the normalized automaton derived by $\mathcal {A}_{1}$ (cf. Lemma 48), and $\mathcal {A}_{2}^{\prime }\mathcal {=} (Q_{2}\cup \{q_{0,2}\},q_{0,2}, wt _{2}^{\prime },F_{2})$ be the initial weight normalized cfwBa derived by $\mathcal {A}_{2}$ (cf. Lemma 49). Without any loss, we assume that $(Q_{1}\cup \{q_{0,1},q_{t}\})\cap (Q_{2}\cup \{q_{0,2}\})=\emptyset$. Consider the weighted automaton $\mathcal {A} =(Q,q_{0,1}, wt ,F_{2})$ with $Q=(Q_{1}\cup \{q_{0,1}\})\cup \left( Q_{2} \cup \{q_{0,2}\}\right)$ where we have identified the states $q_{t}$ and $q_{0,2}$. The weight assignment mapping $wt$ is defined for every $q,q^{\prime }\in Q$ and $a\in A$ by

$$\begin{aligned} wt ((q,a,q^{\prime }))=\left\{ \begin{array}{l@{\quad }l} wt _{1}^{\prime }((q,a,q^{\prime })) &{} \text {if }q,q^{\prime }\in Q_{1} \cup \{q_{0,1}\}\\ wt _{2}^{\prime }((q,a,q^{\prime })) &{} \text {if }q,q^{\prime }\in Q_{2} \cup \{q_{0,2}\}\\ wt _{1}^{\prime }((q,a,q_{t})) &{} \text {if }q\in Q_{1}\cup \{q_{0,1}\}\text { and }q^{\prime }=q_{0,2}\\ -\infty &{} \text {otherwise.} \end{array} \right. \end{aligned}$$

Trivially, $\left\| \mathcal {A}\right\| =s_{1}|_{A^{+}}+_{d}s_{2}$. Furthermore, the weighted Büchi automaton $\mathcal {A}$ is counter-free since every “loop” with weight $\ne -\infty$ belongs either to $\mathcal {A}_{1}^{\prime }$ or to $\mathcal {A}_{2}^{\prime }$. Let $(s_{1},\varepsilon )=k$. Then $s_{1}+_{d}s_{2}=\max (s_{1}|_{A^{+} }+_{d}s_{2},k_{\varepsilon }+_{d}s_{2})$ which concludes our claim since $k_{\varepsilon }+_{d}s_{2}$ is trivially $\omega \hbox {-}d$-counter-free.

Finally, let $r=\max _{a\in A}\left( \left( k_{a}\right) _{a}\right)$ be a letter-step series with $k_{a}\in \mathbb {R}_{\max }$ for every $a\in A$. We consider the initial weight normalized cfwBa $\mathcal {A}=(\{q_{0},q_{t}\},q_{0}, wt ,\{q_{t}\})$ with $wt \left( \left( q_{0},a,q_{t}\right) \right) = wt \left( \left( q_{t},a,q_{t}\right) \right) =k_{a}$ for every $a\in A$, and the weight of any other transition is $-\infty$. Obviously $r^{\omega }=\left\| \mathcal {A}\right\|$, and our proof is completed.$\square$

Next, we introduce the subclass of almost simple $d$-counter-free (resp. almost simple $\omega \hbox {-}d$-counter-free) series and we show that it contains the class $SF ( \mathbb {R}_{\max },A,d)$ (resp. $\omega \hbox {-} SF ( \mathbb {R}_{\max },A,d)$).

Definition 52

A cfwa (resp. cfwBa) $\mathcal {A}=(Q, in , wt ,F)$ over $A$ and $\mathbb {R}_{\max }$ is called simple if for every $q,q^{\prime },p,p^{\prime }\in Q$, and $a\in A$, $in (q)\ne -\infty \ne in (q^{\prime })$ implies $in (q)= in (q^{\prime })$, and $wt ((q,a,q^{\prime }))\ne -\infty \ne wt ((p,a,p^{\prime })$ implies $wt ((q,a,q^{\prime }))= wt ((p,a,p^{\prime }))$. Furthermore, a series $r\in \mathbb {R}_{\max }\left\langle \left\langle A^{*}\right\rangle \right\rangle$ (resp. $r\in \mathbb {R}_{\max }\left\langle \left\langle A^{\omega }\right\rangle \right\rangle$) is simple if it is the $d$-behavior of a simple cfwa (resp. cfwBa) over $A$ and $\mathbb {R}_{\max }$.

Proposition 53

If $r,s\in \mathbb {R}_{\max }\left\langle \left\langle A^{\omega }\right\rangle \right\rangle$ are simple infinitary series, then $r+s$ is also simple.

Proof

Let $\mathcal {A},\mathcal {B}$ be two simple cfwBa accepting $r,s$, respectively. By definition, the initial distribution of $\mathcal {A}$ (resp. $\mathcal {B}$) assigns to every state of $\mathcal {A}$ (resp. $\mathcal {B}$) either $-\infty$ or a value $k\ne -\infty$ (resp. $l\ne -\infty )$. Similarly, the weight assignment mapping of $\mathcal {A}$ (resp. $\mathcal {B}$) assigns to every transition of $\mathcal {A}$ (resp. $\mathcal {B}$) labelled by $a\in A$ either $-\infty$ or a value $k_{a}\ne -\infty$ (resp. $l_{a}\ne -\infty )$. Without any loss, we assume that $k_{a},l_{a}$ exist for every $a\in A$, otherwise we consider a subalphabet. Then the language $L= supp \left( \left\| \mathcal {A}\right\| \right) \cap supp \left( \left\| \mathcal {B}\right\| \right)$ is $\omega$-counter-free (cf. the proof of Proposition 51), and we easily get that $\left\| \mathcal {A}\right\| +\left\| \mathcal {B}\right\| =0_{L}+\left( k+l+\left( \max _{a\in A}\left( \left( k_{a}+l_{a}\right) _{a}\right) \right) ^{\omega }\right)$. Let $\mathcal {C}=(Q,A,I,\Delta ,F)$ be a counter-free nondeterministic Büchi automaton accepting $L$ and consider the weighted Büchi automaton $\mathcal {C}^{\prime }\mathcal {=} (Q, in , wt ,F)$ where for every $q,q^{\prime }\in Q,a\in A$ we let $in \left( q\right) =k+l$ if $q\in I$ and $-\infty$ otherwise, and $wt \left( \left( q,a,q^{\prime }\right) \right) =k_{a}+l_{a}$ if $\left( q,a,q^{\prime }\right) \in \Delta$ and $-\infty$ otherwise. By definition, $\mathcal {C}^{\prime }$ is simple, and since $\mathcal {C}$ is counter-free, we can easily show that it is also counter-free. Moreover $\left\| \mathcal {C}^{\prime }\right\| =\left\| \mathcal {A}\right\| +\left\| \mathcal {B} \right\|$, and this concludes our proof.$\square$

Definition 54

• A series $r\in \mathbb {R} _{\max }\left\langle \left\langle A^{*}\right\rangle \right\rangle$ is called almost simple if $r=\max _{1\le i\le n}\left( r_{1}^{(i)} +_{d}\ldots +_{d}r_{m_{i}}^{(i)}\right)$ where, for every $1\le i\le n,\; r_{1}^{(i)},\ldots ,r_{m_{i}}^{(i)}$ are simple $d$-counter free series over $A$ and $\mathbb {R}_{\max }$.

• A series $r\in \mathbb {R}_{\max }\left\langle \left\langle A^{\omega }\right\rangle \right\rangle$ is called almost simple if $r=\max _{1\le i\le n}\left( r_{1}^{(i)} +_{d}\ldots +_{d}r_{m_{i}}^{(i)}\right)$ where, for every $1\le i\le n$, $r_{1}^{(i)},\ldots ,r_{m_{i}-1}^{(i)}$ are simple $d$-counter free series and $r_{m_{i}}^{(i)}$ is a simple $\omega \hbox {-}d$-counter-free series over $A$ and $\mathbb {R}_{\max }$.

From the above definition and Proposition 50 (resp. Proposition 51), we get that a finitary (resp. infinitary) almost simple series is a $d$-counter-free (resp. an $\omega$-$d$-counter-free) series². We shall denote by $asCF ( \mathbb {R}_{\max },A,d)$ the class of all almost simple $d$-counter-free series and by $\omega \hbox {-} asCF ( \mathbb {R}_{\max },A,d)$ the class of all almost simple $\omega \hbox {-}d$-counter-free series over $A$ and $\mathbb {R}_{\max }$. Now we are ready to state the first main result of this section.

Theorem 55

$SF (\mathbb {R}_{\max },A,d)\subseteq asCF ( \mathbb {R}_{\max },A,d)$.

Proof

The class $asCF ( \mathbb {R}_{\max },A,d)$ trivially contains the monomials over $A$ and $\mathbb {R}_{\max }$. Therefore, it suffices to show that it is closed under maximum, sum, complement, $+_{d}$, and iteration restricted to letter-step series.

Closure under maximum and $+_{d}$ is easily obtained by definition of the class of almost simple $d$-counter-free series. For the closure under complement, let $r\in asCF ( \mathbb {R}_{\max },A,d)$, i.e., $r\in CF ( \mathbb {R}_{\max },A,d)$. Then the weighted automaton $\mathcal {B}^{\prime }$ in the proof of Proposition 50 is simple and moreover accepts the complement $\overline{r}$ hence, $\overline{r}\in asCF ( \mathbb {R}_{\max },A,d)$. Trivially, we get that $asCF (\mathbb {R}_{\max },A,d)$ contains the letter-step series. Furthermore, the automaton $\mathcal {A}$ accepting $r^{+}$ for a letter-step series $r$, in the proof of Proposition 50, is trivially simple, hence the class $asCF ( \mathbb {R}_{\max },A,d)$ is closed under iteration restricted to letter-step series. Therefore, it remains to prove the closure under sum. Since, sum distributes over maximum it suffices to show that if $\mathcal {A}_{i}=(Q_{i}, in _{i} , wt _{i},F_{i}),\mathcal {B}_{j}=(P_{j}, in _{j}^{\prime }, wt _{j}^{\prime },T_{j})$ (for $1\le i\le n,1\le j\le m)$ are simple cfwa over $A$ and $\mathbb {R}_{\max }$, then the $d$-counter-free series $(\left\| \mathcal {A}_{1}\right\| +_{d}\ldots +_{d}\left\| \mathcal {A}_{n}\right\| )+(\left\| \mathcal {B}_{1}\right\| +_{d}\ldots +_{d}\left\| \mathcal {B}_{m}\right\| )$ is almost simple. We proceed by induction on $m$, hence, assume firstly that $m=1$. Without any loss, we suppose the state sets $Q_{i}$ ($1\le i\le n$) to be pairwise disjoint³. For every $p,p^{\prime }\in P_{1}$ and $2\le i\le n-1$, we consider the simple cfwa $\mathcal {C}_{1,p}=(Q_{1}\times P_{1},\overline{ in }_{1},\overline{ wt }_{1},F_{1}\times \{p\})$, $\mathcal {C}_{i,(p,p^{\prime })}=(Q_{i}\times P_{1},\overline{ in }_{i,(p,p^{\prime } )},\overline{ wt }_{i},F_{i}\times \{p^{\prime }\})$, and $\mathcal {C} _{n,p}=(Q_{n}\times P_{1},\overline{ in }_{n,p},\overline{ wt }_{n},F_{n}\times T_{1})$ by

• $\overline{ in }_{1}\left( \left( q^{(1)},p_{1}\right) \right) = in _{1}(q^{(1)})+ in _{1}^{\prime }(p_{1})$ for every $q^{(1)}\in Q_{1} ,p_{1}\in P_{1}$,

• $\overline{ wt }_{1}\left( \left( (q_{1}^{(1)},p_{1}),a,(q_{2} ^{(1)},p_{2})\right) \right) = wt _{1}\left( \left( q_{1}^{(1)} ,a,q_{2}^{(1)}\right) \right) + wt _{1}^{\prime }\left( (p_{1},a,p_{2} )\right)$ for every $q_{1}^{(1)},q_{2}^{(1)}\in Q_{1},p_{1},p_{2}\in P_{1},a\in A$, and

for every $2\le i\le n-1$

• $\overline{ in }_{i,(p,p^{\prime })}\left( \left( q^{(i)} ,p_{1}\right) \right) = in _{i}(q^{(i)})$ if $p_{1}=p$ and $-\infty$ otherwise, for every $q^{(i)}\in Q_{i},p_{1}\in P_{1}$,

• $\overline{ wt }_{i}\left( \left( (q_{1}^{(i)},p_{1}),a,(q_{2} ^{(i)},p_{2})\right) \right) = wt _{i}\left( \left( q_{1}^{(i)} ,a,q_{2}^{(i)}\right) \right) + wt _{1}^{\prime }(\left( p_{1},a,p_{2}\right) )$ for every $q_{1}^{(i)},q_{2}^{(i)}\in Q_{i},p_{1},p_{2}\in P_{1},a\in A$, and

• $\overline{ in }_{n,p}\left( \left( q^{(n)},p_{1}\right) \right) = in _{n}(q^{(n)})$ if $p_{1}=p$ and $-\infty$ otherwise, for every $q^{(n)}\in Q_{n},p_{1}\in P_{1}$,

• $\overline{ wt }_{n}\left( \left( (q_{1}^{(n)},p_{1}),a,(q_{2} ^{(n)},p_{2})\right) \right) = wt _{n}\left( \left( q_{1}^{(n)} ,a,q_{2}^{(n)}\right) \right) + wt _{1}^{\prime }(\left( p_{1},a,p_{2}\right) )$, for every $q_{1}^{(n)},q_{2}^{(n)}\in Q_{n},p_{1},p_{2}\in P_{1},a\in A$.

We claim that

$$\begin{aligned}&(\left\| \mathcal {A}_{1}\right\| +_{d}\ldots +_{d}\left\| \mathcal {A}_{n}\right\| )+\left\| \mathcal {B}_{1}\right\| \\&\quad =\max _{p_{1},\ldots ,p_{n-1}\in P_{1}}\left( \left\| \mathcal {C}_{1,p_{1} }\right\| +_{d}\left\| \mathcal {C}_{2,(p_{1},p_{2})}\right\| +_{d}\ldots +_{d}\left\| \mathcal {C}_{n-1,(p_{n-2},p_{n-1})}\right\| +_{d}\left\| \mathcal {C}_{n,p_{n-1}}\right\| \right) . \end{aligned}$$

Indeed, let $w=a_{0}a_{1}\ldots a_{m-1}\in supp (\left( \left\| \mathcal {A}_{1}\right\| +_{d}\ldots +_{d}\left\| \mathcal {A} _{n}\right\| \right) +\left\| \mathcal {B}_{1}\right\| )$ with $a_{0},a_{1},\ldots ,a_{m-1}\in A$. This means that there is an analysis $w=w_{1}\ldots w_{n}$, and for every $1\le i\le n$ there is a successful path $P_{w_{i}}^{(i)}$ of $\mathcal {A}_{i}$ over $w_{i}$, and a successful path $P_{w}$ of $\mathcal {B}_{1}$ over $w$, such that $((\left\| \mathcal {A}_{1}\right\| +_{d}\ldots +_{d}\left\| \mathcal {A}_{n}\right\| )+\left\| \mathcal {B}_{1}\right\| ,w)= weight \left( P_{w_{1}}^{(1)}\right) +d_{w_{1}} weight \left( P_{w_{2}}^{(2)}\right) +\ldots +d_{w_{1}\ldots w_{n-1}} weight \left( P_{w_{n}}^{(n)}\right) + weight (P_{w})$. Let us assume that

$$\begin{aligned}&P_{w_{1}}^{(1)}:\left( q_{0}^{(1)},a_{0},q_{1}^{(1)}\right) \left( q_{1}^{(1)},a_{1},q_{2}^{(1)}\right) \ldots \left( q_{i_{1}}^{(1)},a_{i_{1} },q_{i_{1}+1}^{(1)}\right) ,\\&P_{w_{2}}^{(2)}:\left( q_{i_{1}+1}^{(2)},a_{i_{1}+1},q_{i_{1}+2} ^{(2)}\right) \left( q_{i_{1}+2}^{(2)},a_{i_{1}+2},q_{i_{1}+3}^{(2)}\right) \ldots \left( q_{i_{2}}^{(2)},a_{i_{2}},q_{i_{2}+1}^{(2)}\right) ,\\&\vdots \\&P_{w_{n}}^{(n)}:\left( q_{i_{n-1}+1}^{(n)},a_{i_{n-1}+1},q_{i_{n-1}+2} ^{(n)}\right) \left( q_{i_{n-1}+2}^{(n)},a_{i_{n-1}+2},q_{i_{n-1}+3} ^{(n)}\right) \ldots \left( q_{m-1}^{(n)},a_{m-1},q_{m}^{(n)}\right) ,\quad \! \hbox {and}\\&P_{w}:\left( p_{0},a_{0},p_{1}\right) \left( p_{1},a_{1},p_{2}\right) \ldots \left( p_{m-1},a_{m-1},p_{m}\right) . \end{aligned}$$

Now, by definition of $\mathcal {C}_{1,p_{i_{1}+1}},\mathcal {C} _{2,(p_{i_{1}+1},p_{i_{2}+1})},\ldots ,\mathcal {C}_{n,p_{i_{n-1}+1}}$, we can construct from $P_{w_{1}}^{(1)},\ldots ,P_{w_{n}}^{(n)}$ and $P_{w}$ the paths $\overline{P}_{w_{1}},\ldots ,\overline{P}_{w_{n}}$ of $\mathcal {C} _{1,p_{i_{1}+1}},\ldots ,\mathcal {C}_{n,p_{i_{n-1}+1}}$ over $w_{1} ,\ldots ,w_{n}$, respectively, as follows

$$\begin{aligned}&\overline{P}_{w_{1}}:\left( \left( q_{0}^{(1)},p_{0}\right) ,a_{0},\left( q_{1}^{(1)},p_{1}\right) \right) \left( \left( q_{1}^{(1)},p_{1}\right) ,a_{1},\left( q_{2}^{(1)},p_{2}\right) \right) \\&\qquad \quad \,\, \ldots \left( \left( q_{i_{1}}^{(1)},p_{i_{1}}\right) ,a_{i_{1}},\left( q_{i_{1}+1}^{(1)},p_{i_{1}+1}\right) \right) ,\\&\overline{P}_{w_{2}}:\left( \left( q_{i_{1}+1}^{(2)},p_{i_{1}+1}\right) ,a_{i_{1}+1},\left( q_{i_{1}+2}^{(2)},p_{i_{1}+2}\right) \right) \left( \left( q_{i_{1}+2}^{(2)},p_{i_{1}+2}\right) ,a_{i_{1}+2},\left( q_{i_{1} +3}^{(2)},p_{i_{1}+3}\right) \right) \\&\qquad \quad \,\,\ldots \left( \left( q_{i_{2}}^{(2)},p_{i_{2}}\right) ,a_{i_{2}},\left( q_{i_{2}+1} ^{(2)},p_{i_{2}+1}\right) \right) ,\\&\vdots \\&\overline{P}_{w_{n}}:\left( \left( q_{i_{n-1}+1}^{(n)},p_{i_{n-1} +1}\right) ,a_{i_{n-1}+1},\left( q_{i_{n-1}+2}^{(n)},p_{i_{n-1}+2}\right) \right) \\&\quad \left( \left( q_{i_{n-1}+2}^{(n)},p_{i_{n-1}+2}\right) ,a_{i_{n-1}+2},\left( q_{i_{n-1}+3}^{(n)},p_{i_{n-1}+3}\right) \right) \\&\qquad \quad \ldots \left( \left( q_{m-1}^{(n)},p_{m-1}\right) ,a_{m-1},\left( q_{m}^{(n)},p_{m}\right) \right) . \end{aligned}$$

Since $weight \left( \overline{P}_{w_{1}}\right) +d_{w_{1} } weight \left( \overline{P}_{w_{2}}\right) +\ldots +d_{w_{1}\ldots w_{n-1} } weight \left( \overline{P}_{w_{n}}\right) = weight \left( P_{w_{1}}^{(1)}\right) +d_{w_{1}} weight \left( P_{w_{2}}^{(2)}\right) +\ldots +d_{w_{1}\ldots w_{n-1}} weight \left( P_{w_{n}}^{(n)}\right) + weight (P_{w})$, by definition of $\mathcal {C}_{1,p_{i_{1}+1}},\ldots ,\mathcal {C}_{n,p_{i_{n-1}+1}}$, we get that $\left( \left\| \mathcal {C} _{1,p_{i_{1}+1}}\right\| +_{d}\ldots +_{d}\left\| \mathcal {C} _{n,p_{i_{n-1}+1}}\right\| ,w\right) = weight \left( \overline{P}_{w_{1} }\right) +d_{w_{1}} weight \left( \overline{P}_{w_{2}}\right) +\ldots +d_{w_{1}\ldots w_{n-1}} weight \left( \overline{P}_{w_{n} }\right)$ which implies that $\left( (\left\| \mathcal {A}_{1}\right\| +_{d}\ldots +_{d}\left\| \mathcal {A}_{n}\right\| )+\left\| \mathcal {B}_{1}\right\| ,w\right) =\left( \left\| \mathcal {C}_{1,p_{i_{1}+1}}\right\| +_{d}\ldots +_{d}\left\| \mathcal {C}_{n,p_{i_{n-1}+1}}\right\| ,w\right)$.

Conversely, keeping the previous notations, let $p_{i_{1}+1},\ldots ,p_{i_{n-1}+1}\in P_{1}$ such that $w\in \; supp \left( \left\| \mathcal {C}_{1,p_{i_{1}+1}}\right\| +_{d}\ldots +_{d}\left\| \mathcal {C}_{n,p_{i_{n-1}+1}}\right\| \right)$. Using similar arguments as above, we get that $\left( \left\| \mathcal {C}_{1,p_{i_{1}+1} }\right\| +_{d}\ldots +_{d}\left\| \mathcal {C}_{n,p_{i_{n-1}+1} }\right\| ,w\right) \le \left( (\left\| \mathcal {A}_{1}\right\| +_{d}\ldots +_{d}\left\| \mathcal {A}_{n}\right\| )+\left\| \mathcal {B}_{1}\right\| ,w\right)$ and this concludes our claim for $m=1$.

For the induction step, for simplicity, we prove our claim for $m=2$. For every $1\le i\le n$ and $q^{(i)}\in Q_{i}$, we define the simple cfwa $\mathcal {A}_{i,q^{(i)}}=(Q_{i}, in _{i}, wt _{i},\{q^{(i)}\})$ and $\mathcal {A}_{i,q^{(i)}}^{\prime }=(Q_{i}, in _{i}^{\prime }, wt _{i},F_{i})$ with $in _{i}^{\prime }(q)=0$ if $q=q^{(i)}$ and $-\infty$ otherwise, for every $q\in Q_{i}$. Then, with similar as above arguments, we can show that $(\left\| \mathcal {A}_{1}\right\| +_{d}\ldots +_{d}\left\| \mathcal {A}_{n}\right\| )+(\left\| \mathcal {B}_{1}\right\| +_{d}\left\| \mathcal {B}_{2}\right\| )$ equals

$$\begin{aligned} \max _{1\le i\le n}\left( \max \left( \begin{array}{c} \left( (\left\| \mathcal {A}_{1}\right\| +_{d}\ldots +_{d}\left\| \mathcal {A}_{i}\right\| )+\left\| \mathcal {B}_{1}\right\| \right) +_{d}\left( (\left\| \mathcal {A}_{i+1}\right\| +_{d}\ldots +_{d}\left\| \mathcal {A}_{n}\right\| )+\left\| \mathcal {B} _{2}\right\| \right) ,\\ \underset{q^{(i)}\in Q_{i}}{\max }\left( \begin{array}{c} \left( \left( \left\| \mathcal {A}_{1}\right\| +_{d}\ldots +_{d}\left\| \mathcal {A}_{i,q^{(i)}}\right\| \right) +\left\| \mathcal {B}_{1}\right\| \right) +_{d}\\ \left( \left( \left\| \mathcal {A}_{i,q^{(i)}}^{\prime }\right\| +_{d}\ldots +_{d}\left\| \mathcal {A}_{n}\right\| \right) +\left\| \mathcal {B}_{2}\right\| \right) \end{array} \right) \end{array} \right) \! \right) . \end{aligned}$$

Hence, by induction hypothesis we conclude our claim.$\square$

In our second main result below, we show that every $\omega \hbox {-}d$-star-free series is an almost simple $\omega \hbox {-}d$-counter-free series.

Theorem 56

$\omega \hbox {-} SF ( \mathbb {R}_{\max },A,d)\subseteq \omega \hbox {-} asCF ( \mathbb {R}_{\max },A,d)$.

Proof

By Definition 23 and Theorem 55, it suffices to show that the class $\omega \hbox {-} asCF (\mathbb {R}_{\max }, A, d)$ is closed under maximum, sum, complement, $\omega$-iteration restricted to letter-step series, and if $s_{1}\in asCF ( \mathbb {R}_{\max },A,d)$ and $s_{2}\in \omega \hbox {-} asCF ( \mathbb {R}_{\max },A,d)$, then $s_{1}+_{d}s_{2}\in \omega \hbox {-} asCF ( \mathbb {R}_{\max },A,d)$. The last property as well as closure under maximum are easily obtained by Definition 54. For the closure under complement, we use a similar argument as in the corresponding part of the proof of Theorem 55. Furthermore, the automaton $\mathcal {A}$ accepting $r^{\omega }$ for a letter-step series $r$, in the proof of Proposition 51, is trivially simple, hence the class $\omega \hbox {-} asCF ( \mathbb {R}_{\max },A,d)$ is closed under $\omega$-iteration restricted to letter-step series. Again, the most complicated case is to prove the closure under sum, i.e., to prove that if $\mathcal {A}_{i}=(Q_{i}, in _{i}, wt _{i},F_{i} ),\mathcal {B}_{j}=(P_{j}, in _{j}^{\prime }, wt _{j}^{\prime },T_{j})$ (for $1\le i\le n-1,1\le j\le m-1)$ are simple cfwa and $\mathcal {A}_{n}=(Q_{n} , in _{n}, wt _{n},F_{n}),\mathcal {B}_{m}=(P_{m}, in _{m}^{\prime }, wt _{m}^{\prime },T_{m})$ are simple cfwBa over $A$ and $\mathbb {R}_{\max }$, then the $\omega \hbox {-}d$-counter-free series $(\left\| \mathcal {A}_{1}\right\| +_{d}\ldots +_{d}\left\| \mathcal {A} _{n}\right\| )+(\left\| \mathcal {B}_{1}\right\| +_{d}\ldots +_{d}\left\| \mathcal {B}_{m}\right\| )$ is almost simple. We state our proof by induction on $m$, hence, let firstly $m=1$, i.e., $\mathcal {B}_{1}=(P_{1}, in _{1}^{\prime }, wt _{1}^{\prime },T_{1})$ be a simple cfwBa (again we assume $n>1$, otherwise if $n=m=1$ we get our result by Proposition 53). We keep the notations of Theorem 55 and consider the simple cfwa $\mathcal {C}_{1,p}$, and $\mathcal {C}_{i,(p,p^{\prime })}$ for every $2\le i\le n-1$. Furthermore, for every $p\in P_{1}$ we define the weighted Büchi automaton $\mathcal {C}_{n,p}=\left( Q_{n}\times P_{1}\times \{0,1,2\},\overline{ in }_{n,p},\overline{ wt }_{n},Q_{n}\times P_{1}\times \{2\}\right)$ with the initial distribution $\overline{ in }_{n,p}$ given for every $q^{(n)}\in Q_{n},p_{1}\in P_{1},x\in \{0,1,2\}$ by

$$\begin{aligned} \overline{ in }_{n,p}(q^{(n)},p_{1},x)=\left\{ \begin{array}{l@{\quad }l} in _{n}(q^{(n)}) &{} \hbox {if}\; p_{1}=p,x=0 \\ -\infty &{} \hbox {otherwise} \end{array} , \right. \end{aligned}$$

and the weight assignment mapping $\overline{ wt }_{n}$ defined for every $q_{1}^{(n)},q_{2}^{(n)}\in Q_{n},p_{1},p_{2}\in P_{1},a\in A,x,y\in \{0,1,2\}$ as follows.

$\overline{ wt }_{n}\left( \left( \left( q_{1}^{(n)},p_{1},x\right) ,a,\left( q_{2}^{(n)},p_{2},y\right) \right) \right) = wt _{n}\left( \left( q_{1}^{(n)},a,q_{2}^{(n)}\right) \right) + wt _{1}^{\prime }\left( \left( p_{1},a,p_{2}\right) \right)$ if ($x=y=0$ or $q_{2}^{(n)}\in F_{n},x=0,y=1$ or $p_{2}\notin T_{1},x=y=1$ or $p_{2}\in T_{1},x=1,y=2$ or $x=2,y=0$), and $-\infty$ otherwise. We note that, since $\mathcal {A}_{n}$ (resp. $\mathcal {B}_{1},\mathcal {C}_{n,p}$)⁴ is simple, for every $w\in A^{\omega }$, all the successful paths of $\mathcal {A}_{n}$ (resp. $\mathcal {B}_{1},\mathcal {C}_{n,p}$) over $w$ with weight $\ne -\infty$ have the same weight. Again we will show that $(\left\| \mathcal {A}_{1}\right\| +_{d}\ldots +_{d}\left\| \mathcal {A}_{n}\right\| )+\left\| \mathcal {B}_{1}\right\| =\max _{p_{1},\ldots ,p_{n-1}\in P_{1}}\left( \left\| \mathcal {C}_{1,p_{1} }\right\| +_{d}\left\| \mathcal {C}_{2,(p_{1},p_{2})}\right\| +_{d}\ldots +_{d}\left\| \mathcal {C}_{n-1,(p_{n-2},p_{n-1})}\right\| +_{d}\left\| \mathcal {C}_{n,p_{n-1}}\right\| \right)$. To this end, let $w=a_{0}a_{1}\ldots \in supp (\left( \left\| \mathcal {A}_{1}\right\| +_{d}\ldots +_{d}\left\| \mathcal {A}_{n}\right\| \right) +\left\| \mathcal {B}_{1}\right\| )$ with $a_{0},a_{1},\ldots \in A$. Then, there is an analysis $w=w_{1}\ldots w_{n-1}w_{n}$ $\left( w_{1},\ldots ,w_{n-1}\in A^{*},w_{n}\in A^{\omega }\right)$, and for every $1\le i\le n$ there is a successful path $P_{w_{i}}^{(i)}$ of $\mathcal {A}_{i}$ over $w_{i}$, and a successful path $P_{w}$ of $\mathcal {B}_{1}$ over $w$, such that $((\left\| \mathcal {A}_{1}\right\| +_{d}\ldots +_{d}\left\| \mathcal {A}_{n}\right\| )+\left\| \mathcal {B}_{1}\right\| ,w)= weight \left( P_{w_{1}}^{(1)}\right) +d_{w_{1}} weight \left( P_{w_{2}}^{(2)}\right) +\ldots +d_{w_{1}\ldots w_{n-1}} weight \left( P_{w_{n}}^{(n)}\right) + weight (P_{w})$. We keep the notations, from the proof of Theorem 55, for the paths $P_{w_{i}}^{(i)}\;(1\le i\le n-1)$, and let

$$\begin{aligned}&P_{w_{n}}^{(n)}:\left( q_{i_{n-1}+1}^{(n)},a_{i_{n-1}+1},q_{i_{n-1}+2}^{(n)}\right) \left( q_{i_{n-1}+2}^{(n)},a_{i_{n-1}+2},q_{i_{n-1}+3} ^{(n)}\right) \ldots ,\quad \hbox {and}\\&P_{w}:\left( p_{0},a_{0},p_{1}\right) \left( p_{1},a_{1},p_{2}\right) \ldots . \end{aligned}$$

We consider the paths $\overline{P}_{w_{i}}$ ($1\le i\le n-1$) as in the proof of Theorem 55, and let

$$\begin{aligned}&\overline{P}_{w_{n}}:\left( \left( q_{i_{n-1}+1}^{(n)},p_{i_{n-1}+1} ,x_{1}\right) ,a_{i_{n-1}+1},\left( q_{i_{n-1}+2}^{(n)},p_{i_{n-1}+2} ,x_{2}\right) \right) \\&\qquad \quad \left( \left( q_{i_{n-1}+2}^{(n)},p_{i_{n-1} +2},x_{2}\right) ,a_{i_{n-1}+2},\left( q_{i_{n-1}+3}^{(n)},p_{i_{n-1} +3},x_{3}\right) \right) \ldots \end{aligned}$$

where for every $j\ge 1$ the choice of $x_{j}$ is done as follows. We have ($x_{j}=0$ and (nondeterministically) $x_{j+1}=1$ if $q_{i_{n-1} +j+1}^{(n)}\in F_{n}$) or ($x_{j}=1$ and $x_{j+1}=1$ if $p_{i_{n-1}+j+1}\notin T_{1}$) or ($x_{j}=1$ and $x_{j+1}=2$ if $p_{i_{n-1}+j+1}\in T_{1}$) or ($x_{j}=2$ and $x_{j+1}=0$). Clearly, by definition of $\mathcal {C} _{1,p_{i_{1}+1}},\ldots ,\mathcal {C}_{n,p_{i_{n-1}+1}}$, the above paths are successful, and we get that

$$\begin{aligned} \left( \left\| \mathcal {C}_{1,p_{i_{1}+1}}\right\| +_{d}\ldots +_{d}\left\| \mathcal {C}_{n,p_{i_{n-1}+1}}\right\| ,w\right)&= weight \left( \overline{P}_{w_{1}}\right) +d_{w_{1}} weight \left( \overline{P}_{w_{2}}\right) \\&+\ldots +d_{w_{1} \ldots w_{n-1}} weight \left( \overline{P}_{w_{n}}\right) \end{aligned}$$

hence, $\left( \left\| \mathcal {C}_{1,p_{i_{1}+1}}\right\| +_{d}\ldots +_{d}\left\| \mathcal {C}_{n,p_{i_{n-1}+1}}\right\| ,w\right) =\left( (\left\| \mathcal {A}_{1}\right\| +_{d}\ldots +_{d}\left\| \mathcal {A}_{n}\right\| )+\left\| \mathcal {B}_{1}\right\| ,w\right)$.

For the converse, we use similar arguments as in the corresponding part of the proof of Theorem 55.

It remains to prove that the infinitary series $\left\| \mathcal {C}_{n,p}\right\|$ is simple for every $p\in P_{1}$. By construction, we have $\left\| \mathcal {C}_{n,p}\right\| =\left\| \mathcal {A}_{n}\right\| +\left\| \mathcal {B}_{p}\right\|$, where $\mathcal {B}_{p}$ is the simple cfwBa derived by $\mathcal {B}_{1}$ by replacing the initial distribution, with the one assigning the value $0$ to $p$ and $-\infty$ to any other state. Since, $\mathcal {A}_{n},\mathcal {B}_{p}$ are simple, we conclude our claim by Proposition 53.

Next for the induction step, again for simplicity, we state our claim for $m=2$. Now, we consider, for every $1\le i\le n-1$ and $q^{(i)}\in Q_{i}$, the simple cfwa $\mathcal {A}_{i,q^{(i)}}=(Q_{i}, in _{i}, wt _{i},\{q^{(i)}\})$ and $\mathcal {A}_{i,q^{(i)}}^{\prime }=(Q_{i}, in _{i}^{\prime }, wt _{i},F_{i})$ with $in _{i}^{\prime }(q)=0$ if $q=q^{(i)}$ and $-\infty$ otherwise. Moreover, for every $q^{(n)}\in Q_{n}$ we consider the cfwa $\mathcal {A}_{n,q^{(n)} }=(Q_{n}, in _{n}, wt _{n},\{q^{(n)}\})$ and the cfwBa $\mathcal {A}_{n,q^{(n)} }^{\prime }=(Q_{n}, in _{n}^{\prime }, wt _{n},F_{n})$ with $in _{n}^{\prime }(q)=0$ if $q=q^{(n)}$ and $-\infty$ otherwise. Then, we get that the sum $(\left\| \mathcal {A}_{1}\right\| +_{d}\ldots +_{d}\left\| \mathcal {A}_{n}\right\| )+(\left\| \mathcal {B}_{1}\right\| +_{d}\left\| \mathcal {B}_{2}\right\| )$ equals

$$\begin{aligned} \max _{1\le i\le n}\left( \max \left( \begin{array}{c} \left( (\left\| \mathcal {A}_{1}\right\| +_{d}\ldots +_{d}\left\| \mathcal {A}_{i}\right\| )+\left\| \mathcal {B}_{1}\right\| \right) +_{d}\left( (\left\| \mathcal {A}_{i+1}\right\| +_{d}\ldots +_{d}\left\| \mathcal {A}_{n}\right\| )+\left\| \mathcal {B} _{2}\right\| \right) ,\\ \underset{q^{(i)}\in Q_{i}}{\max }\left( \begin{array}{c} \left( \left( \left\| \mathcal {A}_{1}\right\| +_{d}\ldots +_{d}\left\| \mathcal {A}_{i,q^{(i)}}\right\| \right) +\left\| \mathcal {B}_{1}\right\| \right) +_{d}\\ \left( \left( \left\| \mathcal {A}_{i,q^{(i)}}^{\prime }\right\| +_{d}\ldots +_{d}\left\| \mathcal {A}_{n}\right\| \right) +\left\| \mathcal {B}_{2}\right\| \right) \end{array} \right) \end{array} \right) \right) , \end{aligned}$$

and, by induction hypothesis and Theorem 55, we are done.$\square$

Example 57

We consider the $\omega \hbox {-}d$-star-free series $r=\max \left( \left( 2_{a}\right) ^{+}+_{d}\left( 3_{b}\right) ^{\omega },\left( 3_{b}\right) ^{\omega }\right)$ of Example 46. Let $\mathcal {A}_{1}=\left( \{q_{0},q_{1},q_{2}\}, in _{1}, wt _{1},\{q_{2}\}\right)$ be a simple normalized cfwa determined by $in _{1}(q_{0})=0$, $in _{1}(q_{1})= in _{1} (q_{2})=-\infty$ and $wt _{1}((q_{0},a,q_{1}))= wt _{1}((q_{0},a,q_{2} ))= wt _{1}((q_{1},a,q_{1}))= wt _{1}((q_{1},a,q_{2}))=2$. It is easily seen that $\mathcal {A}_{1}$ accepts the series is $\left( 2_{a}\right) ^{+}$. Furthermore, the simple initial weight normalized cfwBa $\mathcal {A}_{2}=\left( \{p_{0},p_{1}\}, in _{2}, wt _{2},\{p_{1}\}\right)$ with $in _{2}(p_{0})=0$, $in _{2}(p_{1})=-\infty$ and $wt _{2}((p_{0},b,p_{1} ))= wt _{2}((p_{1},b,p_{1}))=3$ accepts the series $\left( 3_{b}\right) ^{\omega }$. Then the cfwBa $\mathcal {B}=\left( \{q_{0},q_{1},p_{0} ,p_{1}\}, in , wt ,\{p_{1}\}\right)$ determined by $in (q_{0})=0$, $in (q_{1} )= in (p_{0})= in (p_{1})=-\infty$ and $wt ((q_{0},a,q_{1}))= wt ((q_{0} ,a,p_{0}))= wt ((q_{1},a,q_{1}))= wt ((q_{1},a,p_{0}))=2,$ $wt ((p_{0},b,p_{1}))= wt ((p_{1},b,p_{1}))=3$ has behavior $\left\| \mathcal {B} \right\| =\left( 2_{a}\right) ^{+}+_{d}\left( 3_{b}\right) ^{\omega }$. Finally, the disjoint union of the cfwBa $\mathcal {A}_2$ and $\mathcal {B}$ recognizes the series $r$.

7 Closing the cycle

In this section, we prove that the class of almost simple $\omega$ -$d$-counter-free series is included into the class $\omega \hbox {-} ULTL \left( \mathbb {R}_{\max },A,d\right)$ and thus concluding the main result of our paper. For this, we shall need some preliminary matter on our weighted LTL.

For every $\varphi \in LTL\left( \mathbb {R}_{\max },A\right)$ and $n\ge 0$ we denote by $\bigcirc ^{n}\varphi$ the $n$-th repetitive application of the $\bigcirc$ operator on $\varphi$, i.e., $\bigcirc ^{n}\varphi \,{:}{=}\,\underset{n\text { times}}{\underbrace{\bigcirc (\bigcirc \ldots (\bigcirc }}\varphi )\ldots ),$ and hence $\bigcirc ^{0} \varphi =\varphi$. Then, for every $w\in A^{\omega }$ we have $\left( \left\| \bigcirc ^{n}\varphi \right\| ,w\right) =d_{w_{<n}}\left( \left\| \varphi \right\| ,w_{\ge n}\right)$. The external next depth $exnd \left( \varphi \right)$ of a formula $\varphi \in LTL ( \mathbb {R}_{\max },A)$ is defined inductively as follows. If $\varphi =\bigcirc \psi ,$ then $exnd \left( \varphi \right) = exnd \left( \psi \right) +1$. In any other case, we let $exnd \left( \varphi \right) =0$. For instance $exnd \left( \bigcirc \left( \bigcirc \left( \square \left( \bigcirc \left( p_{a} \wedge 2\right) \right) \right) \right) \right) =2$, and if $\varphi \in LTL \left( \mathbb {R}_{\max },A\right)$ with $exnd \left( \varphi \right) =0$, then $exnd \left( \bigcirc ^{n}\varphi \right) =n$ for every $n\ge 0$. For every $n\ge 0$, we denote by $stLTL \left( \bigcirc ,n,\wedge \right)$ the class of all $LTL \left( \mathbb {R}_{\max },A\right)$ formulas of the form $\bigwedge \nolimits _{0\le j\le m}\bigcirc ^{k_{j}}\psi _{j}$ with $m\ge 0,\; \max _{0\le j\le m}\left( k_{j}\right) =n$, and $\psi _{j}\in stLTL \left( \mathbb {R}_{\max },A\right)$ for every $0\le j\le m$ ⁵. We let $stLTL \left( \bigcirc ,\wedge \right) =\bigcup \nolimits _{n\ge 0} stLTL \left( \bigcirc ,n,\wedge \right)$. Furthermore, for every $m\ge 0$, we let $U_{m}$ to be the set of all $(m+1)$-tuples of the form $\left( \left( \varphi _{0},k_{0}\right) ,\left( \xi _{1},\varphi _{1},k_{1}\right) ,\ldots ,\left( \xi _{m},\varphi _{m},k_{m}\right) \right)$ where $\varphi _{i}\in stLTL \left( \bigcirc ,k_{i},\wedge \right)$ and $\xi _{j}\in abLTL \left( \mathbb {R}_{\max },A\right)$ for every $0\le i\le m$ and $1\le j\le m$.

Definition 58

Let $T=\left( \left( \varphi _{0},k_{0}\right) ,\left( \xi _{1},\varphi _{1},k_{1}\right) ,\ldots ,\left( \xi _{m},\varphi _{m} ,k_{m}\right) \right) \in U_{m}$. For every $w\in A^{\omega }$ and $j\ge 0$ we define the value $\left\langle T\mathbf {,}w,j\right\rangle \in \mathbb {R}_{\max }$ as follows. If $j\le k_{0}+\ldots +k_{m}$, we set $\left\langle T\mathbf {,}w,j\right\rangle =-\infty$. Otherwise, for every $i_{1} ,i_{2},\ldots ,i_{m}\in \mathbb {N}$ and $0\le l\le m$ we define the sum $S_{l}=k_{0}+i_{1}+k_{1}+\ldots +i_{l}+k_{l}$ with the restriction that $S_{m}=j-1$. Then, we let

$$\begin{aligned} \left\langle T\mathbf {,}w,j\right\rangle =\underset{S_{m}=j-1}{\underset{i_{1},i_{2},\ldots ,i_{m}\in \mathbb {N}}{\max }}\left( \left( \left\| \varphi _{0}\right\| ,w\right) +\underset{1\le l\le m}{ {\displaystyle \sum } }\left( \begin{array}{l} \underset{0\le j_{l}<i_{l}}{ {\displaystyle \sum }}d_{w_{<S_{l-1}+j_{l}}}\left( \left\| \xi _{l}\right\| ,w_{\ge S_{l-1}+j_{l}}\right) \\ +d_{w_{<S_{l-1}+i_{l}}}\left( \left\| \varphi _{l}\right\| ,w_{\ge S_{l-1}+i_{l}}\right) \end{array} \right) \right) . \end{aligned}$$

Note that in case $m=0$, the restriction $S_{0}=j-1$, i.e., $k_{0}=j-1$ implies that $\left\langle T\mathbf {,}w,j\right\rangle =-\infty$ for every $j>k_{0}+1$. Therefore, if $m=0$, then $\left\langle T\mathbf {,} w,j\right\rangle =-\infty$ for every $j\ne k_{0}+1$, and $\left\langle T\mathbf {,}w,k_{0}+1\right\rangle =\left( \left\| \varphi _{0}\right\| ,w\right)$.

Composition algorithm. Let $T_{1}=\left( \left( \varphi _{0},k_{0}\right) ,\left( \xi _{1},\varphi _{1},k_{1}\right) ,\ldots ,\left( \xi _{m},\varphi _{m},k_{m}\right) \right) \in U_{m}$ and $T_{2}=\left( \left( \psi _{0},l_{0}\right) ,\left( \theta _{1},\psi _{1},l_{1}\right) ,\ldots ,\left( \theta _{n},\psi _{n},l_{n}\right) \right) \in U_{n}$ with $\psi _{0}={ {\bigwedge \nolimits _{0\le j\le h}}}\bigcirc ^{p_{j}}\varrho _{j}$. We consider the formula $\varrho \in stLTL \left( \bigcirc ,k_{m}+l_{0}+1,\wedge \right)$ by $\varrho =\varphi _{m}\wedge \left( { {\bigwedge \nolimits _{0\le j\le h}}}\bigcirc ^{k_{m}+p_{j}+1}\varrho _{j}\right)$. Then, if $m=0$ we let

$$\begin{aligned} T=\left( \left( \varrho ,k_{m}+l_{0}+1\right) ,\left( \theta _{1},\psi _{1},l_{1}\right) ,\ldots ,\left( \theta _{n},\psi _{n},l_{n}\right) \right) , \end{aligned}$$

otherwise we let

$$\begin{aligned} T=\left( \left( \varphi _{0},k_{0}\right) ,\left( \xi _{1},\varphi _{1},k_{1}\right) ,\ldots ,\left( \xi _{m},\varrho ,k_{m}+l_{0}+1\right) ,\left( \theta _{1},\psi _{1},l_{1}\right) ,\ldots ,\left( \theta _{n},\psi _{n},l_{n}\right) \right) . \end{aligned}$$

Clearly $T\in U_{m+n}$, and we claim that

$$\begin{aligned} \left\langle T,w,j\right\rangle =\underset{0\le i\le j}{\max }\left( \left\langle T_{1},w,i\right\rangle +d_{w_{<i}}\left\langle T_{2},w_{\ge i},j-i\right\rangle \right) \end{aligned}$$

for every $w\in A^{\omega },j\ge 0$. Assume firstly that $m=n=0.$ If $j\ne k_{0}+l_{0}+2$, then both sides of the above relation equal to $-\infty$. If $j=k_{0}+l_{0}+2,$ then $\left\langle T,w,j\right\rangle =\left( \left\| \varrho \right\| ,w\right) =\left( \left\| \varphi _{0}\right\| ,w\right) +d_{w_{<k_{0}+1}}\left( \left\| \psi _{0}\right\| ,w_{\ge k_{0}+1}\right) =\left\langle T_{1},w,k_{0}+1\right\rangle +d_{w_{<k_{0}+1} }\left\langle T_{2},w_{\ge k_{0}+1},j-\left( k_{0}+1\right) \right\rangle ={\max \nolimits _{0\le i\le j}}\left( \left\langle T_{1},w,i\right\rangle +d_{w_{<i}}\left\langle T_{2},w_{\ge i},j-i\right\rangle \right) .$

Next, assume that $n\ne 0$ or $m\ne 0.$ Then, if $j>k_{0}+k_{1}+\ldots +k_{m}+1+l_{0}+\ldots +l_{n}$ there exist $i_{1},\ldots ,i_{m},i_{1}^{\prime },\ldots ,i_{n}^{\prime }\in \mathbb {N}$ with $k_{0}+i_{1}+k_{1}+\ldots +i_{m}+k_{m}+1+l_{0}+i_{1}^{\prime } +l_{1}+\ldots +i_{n}^{\prime }+l_{n}=j-1$ such that $\left\langle T,w,j\right\rangle$ equals to

$$\begin{aligned}&\left( \left( \left\| \varphi _{0}\right\| ,w\right) +\underset{1\le l\le m}{ {\displaystyle \sum }}\left( \begin{array}{l} \underset{0\le j_{l}<i_{l}}{ {\displaystyle \sum }}d_{w_{<S_{l-1}+j_{l}}}\left( \left\| \xi _{l}\right\| ,w_{\ge S_{l-1}+j_{l}}\right) \\ +d_{w_{<S_{l-1}+i_{l}}}\left( \left\| \varphi _{l}\right\| ,w_{\ge S_{l-1}+i_{l}}\right) \end{array} \right) \right) \\&\quad +d_{w_{<S_{m}+1}}\left( \left( \left\| \psi _{0}\right\| ,w_{\ge S_{m}+1}\right) \!+\!\underset{1\le h\le n}{ {\displaystyle \sum }}\left( \begin{array}{l} \underset{0\le j_{h}<i_{h}^{\prime }}{ {\displaystyle \sum }}d_{\left( w_{\ge S_{m}+1}\right) _{<S_{h-1}^{\prime }+j_{h}}}\left( \left\| \theta _{h}\right\| ,w_{\ge S_{m}+1+S_{h-1}^{\prime }+j_{h} }\right) \\ +\,d_{\left( w_{\ge S_{m}+1}\right) _{<S_{h-1}^{\prime }+i_{h}^{\prime }} }\left( \left\| \psi _{h}\right\| ,w_{\ge S_{m}+1+S_{h-1}^{\prime }+i_{h}^{\prime }}\right) \end{array}\!\! \right) \! \right) . \end{aligned}$$

Then, for $i=S_{m}+1,$ we get $\left\langle T,w,j\right\rangle \le \left\langle T_{1},w,i\right\rangle +d_{w_{<i}}\left\langle T_{2},w_{\ge i},j-i\right\rangle ,$ which implies that $\left\langle T,w,j\right\rangle \le {\max \nolimits _{0\le i\le j}}\left( \left\langle T_{1},w,i\right\rangle +d_{w_{<i}}\left\langle T_{2},w_{\ge i},j-i\right\rangle \right)$. Similarly, we can show that $\left\langle T_{1},w,i\right\rangle +d_{w_{<i} }\left\langle T_{2},w_{\ge i},j-i\right\rangle \le \left\langle T,w,j\right\rangle$ for every $0\le i\le j$, and we are done.

Finally, assume that $j\le k_{0}+k_{1}+\ldots +k_{m}+1+l_{0} +\ldots +l_{n}.$ Then, $\left\langle T,w,j\right\rangle =-\infty ,$ and for every $0\le i\le j$ at least one of the following is true: $i\le k_{0}+\ldots +k_{m}$ which implies that $\left\langle T_{1},w,i\right\rangle =-\infty ,$ or $j-i\le l_{0}+\ldots +l_{n},$ which implies that $\left\langle T_{2},w_{\ge i},j-i\right\rangle =-\infty .$

In the sequel, we recall an alternative definition for star-free languages which does not involve the closure under complementation. For this, we shall need the notion of bounded synchronization delay. More precisely, let $k\ge 0$ be an integer. A prefix-free set $L\subseteq A^{+}$ has bounded synchronization delay if $uvw\in L^{*}$ implies $uv,w\in L^{*}$ for every $u,w\in A^{*}$ and $v\in L^{k}$. The least integer $k\ge 0$ satisfying the aforementioned property is called the synchronization delay of $L$.

Lemma 59

[24] A prefix-free set of delay $0$ is also of delay $1$.

It is well-known (cf. for instance Theorem 6.3 p. 378 in [24]) that the class of star-free languages over $A$ is the smallest class of languages over $A$ containing $\emptyset$ and $\{a\}$ for every $a\in A$, and it is closed under union, concatenation and star operation restricted to prefix-free sets with bounded synchronization delay.

For every $L,F\subseteq A^{\omega }$ we define the infinitary language (cf. [24])

$$\begin{aligned} LUF&= \left\{ w\in A^{\omega }\mid w=uv\text { where }u\in A^{*}, v\in F\text { and }u^{\prime }v\in L\text { for each non-empty} \hbox { suffix }u^{\prime }\text { of }u\right\} . \end{aligned}$$

It should be clear that $supp \left( 0_{L}U0_{F}\right) =LUF$, where the operation $U$ among two bounded series $r,s\in \mathbb {R}_{\max }\left\langle \left\langle A^{\omega }\right\rangle \right\rangle$, is defined for every $w\in A^{\omega }$, by

$$\begin{aligned} \left( rUs,w\right) =\underset{i\ge 0}{\sup }\left( {\sum \limits _{0\le j<i}}d_{w_{<j}}\left( r,w_{\ge j}\right) +d_{w_{<i}}\left( s,w_{\ge i}\right) \right) . \end{aligned}$$

Lemma 60

Let $L\subseteq A^{+}$ be a prefix-free set with bounded synchronization delay $k\ge 1$. Let $u\in A^{*}$, $v\in L^{2k}$, and $w\in Y\subseteq A^{\omega }$ such that

• (i) $uvw\in L^{k}A^{\omega }$, and

• (ii) $u^{\prime }vw\in L^{k+1}A^{\omega }\cup (A^{\omega }\backslash L^{k}A^{\omega })$ for every suffix $u^{\prime }$ of $u$.

Then $uv\in L^{+}$.

Proof

We follow the proof of Lemma 6.11 (p. 383) in [24].$\square$

Lemma 61

(Lemma 6.12 in [24]) Let $L\subseteq A^{+}$ be a prefix-free set with bounded synchronization delay $k\ge 1$ and $Y\subseteq A^{\omega }$. Then

$$\begin{aligned} \left( L^{+}\right) Y=LY\cup \ldots \cup L^{2k-1}Y\cup R \end{aligned}$$

with $R=L^{k}A^{\omega }\cap \left( \left( L^{k+1}A^{\omega }\cup \left( A^{\omega }\setminus L^{k}A^{\omega }\right) \right) UL^{2k}Y\right)$.

The subsequent result is a straightforward conclusion from the last lemma above.

Lemma 62

Let $L\subseteq A^{+}$ be a prefix-free set with bounded synchronization delay $k\ge 1$ and $Y\subseteq A^{\omega }.$ Then

$$\begin{aligned} 0_{L^{+}}+_{d}0_{Y}=\max \left( 0_{L}+_{d}0_{Y},\ldots ,0_{L^{2k-1}}+_{d} 0_{Y},r\right) \end{aligned}$$

with $r=0_{L^{k}A^{\omega }}+\left( 0_{L^{k+1}A^{\omega }\cup \left( A^{\omega }\setminus L^{k}A^{\omega }\right) }U\left( 0_{L^{2k}}+_{d}0_{Y}\right) \right)$.

Lemma 63

Let $L\subseteq A^{+}$ be a star-free language. Then, there exists an integer $n>0$ and $T_{i}\in U_{m_{i}}$ ($m_{i}\ge 0$) for every $1\le i\le n$, such that for every $w\in A^{\omega }$ and $j\ge 0$ we have $\left( 0_{L},w_{<j}\right) ={\max \nolimits _{{1\le i\le n}}}\left( \left\langle T_{i},w,j\right\rangle \right)$.

Proof

We state the proof by induction on the structure of $L$. For the empty set the tuple $T=\left( -\infty ,0\right) \in U_{0}$ satisfies our claim. Let $L=\{a\}$ for $a\in A.$ We consider the tuple $T=\left( p_{a},0\right) \in U_{0}$. Then $S_{0}=0$ and since $S_{0}=j-1$ we get that $\left\langle T,w,j\right\rangle =-\infty$ for $j\ne 1$. Moreover, $\left\langle T,w,1\right\rangle =0$ if $w(0)=a$, and $\left\langle T,w,1\right\rangle =-\infty$ otherwise. Therefore $\left\langle T,w,j\right\rangle =\left( 0_{a},w_{<j}\right)$ for every $w\in A^{\omega },j\ge 0$.

Next, assume that the induction hypothesis holds for the star-free languages $L_{1},L_{2}\subseteq A^{+}$. Then, there exist $n,m,l_{i},h_{k}\in \mathbb {N},$ and $T_{i}\in U_{l_{i}},T_{k}^{\prime }\in U_{h_{k}},$ ($1\le i\le n,1\le k\le m$) such that for every $w\in A^{\omega },j\ge 0$ we have $\left( 0_{L_{1}},w_{<j}\right) ={\max \nolimits _{1\le i\le n}}\left( \left\langle T_{i},w,j\right\rangle \right)$ and $\left( 0_{L_{2}},w_{<j}\right) = \mathop {\max }\nolimits _{1\le k\le m}\left( \left\langle T_{k}^{\prime },w,j\right\rangle \right)$. Firstly, let $L=L_{1}\cup L_{2}.$ Then $\left( 0_{L},w_{<j}\right) =\left( \max \left( 0_{L_{1}},0_{L_{2}}\right) ,w_{<j}\right) =\max \left( {\max \nolimits _{1\le i\le n}}\left( \left\langle T_{i},w,j\right\rangle \right) ,{\max \nolimits _{1\le k\le m} }\left( \left\langle T_{k}^{\prime },w,j\right\rangle \right) \right)$, as wanted.

Next, let $L=L_{1}L_{2}$. Then $0_{L_{1}L_{2}}=0_{L_{1}}+_{d}0_{L_{2}}$. For every $1\le i\le n$ and $1\le k\le m$ we derive from $T_{i},T_{k}^{\prime }$ the tuple $T_{i,k}\in U_{l_{i}+h_{k}}$ by applying the Composition algorithm. Then, we get

$$\begin{aligned} \left( 0_{L_{1}}+_{d}0_{L_{2}},w_{<j}\right)&=\underset{0\le p\le j}{\max }\left( \left( 0_{L_{1}},w_{<p}\right) +d_{w_{<p}}\left( 0_{L_{2} },\left( w_{\ge p}\right) _{<j-p}\right) \right) \\&=\underset{0\le p\le j}{\max }\left( \underset{1\le i\le n}{\max }\left( \left\langle T_{i},w,p\right\rangle \right) +d_{w_{<p}}\left( \underset{1\le k\le m}{\max }\left( \left\langle T_{k}^{\prime },w_{\ge p},j-p\right\rangle \right) \right) \right) \\&=\underset{0\le p\le j}{\max }\left( \underset{1\le i\le n,1\le k\le m}{\max }\left( \left\langle T_{i},w,p\right\rangle +d_{w_{<p}}\left\langle T_{k}^{\prime },w_{\ge p},j-p\right\rangle \right) \right) \\&=\underset{1\le i\le n,1\le k\le m}{\max }\left( \underset{0\le p\le j}{\max }\left( \left\langle T_{i},w,p\right\rangle +d_{w_{<p}}\left\langle T_{k}^{\prime },w_{\ge p},j-p\right\rangle \right) \right) \\&=\underset{1\le i\le n,1\le k\le m}{\max }\left( \left\langle T_{i,k},w,j\right\rangle \right) \end{aligned}$$

for every $w\in A^{\omega },j\ge 0$.

Finally, let $L$ be a prefix-free set with bounded synchronization delay $k\ge 0$ satisfying the induction hypothesis. By Lemma 59, it suffices to consider the case $k\ge 1$. We will prove our claim for $L^{+}$. By Lemma 62, for $Y=A^{\omega }$, we get

$$\begin{aligned} 0_{L^{+}}+_{d}0_{A^{\omega }}&= \max \left( 0_{L}+_{d}0_{A^{\omega }},\ldots ,0_{L^{2k-1}}+_{d}0_{A^{\omega } },0_{L^{k}A^{\omega }}\right. \\&\qquad \quad \left. +\left( 0_{L^{k+1}A^{\omega }\cup \left( A^{\omega }{\setminus } L^{k}A^{\omega }\right) }U\left( 0_{L^{2k}}+_{d}0_{A^{\omega } }\right) \right) \right) . \end{aligned}$$

We denote $2k$ simply by $p$. By what we have shown above, the induction hypothesis, and same arguments with the ones used in the previous inductive step, we get that for every $1\le h\le p$ there exists an $n_{h}\in \mathbb {N},$ so that the following hold. For every $1\le i\le n_{h}$ there exist an $m_{i}\ge 0$ and a $T_{h,i}\in U_{m_{i}}$ with $\left( 0_{L^{h}},w_{<j}\right) ={\max \nolimits _{1\le i\le n_{h}}}\left( \left\langle T_{h,i},w,j\right\rangle \right)$, for every $w\in A^{\omega },j\ge 0$.

Let $\varphi ^{\prime },\widetilde{\varphi }\in bLTL \left( \mathbb {R}_{\max },A\right)$ with semantics $0_{L^{k}A^{\omega }},$ $0_{L^{k+1} A^{\omega }\cup \left( A^{\omega }\setminus L^{k}A^{\omega }\right) }$, respectively. We set $\overline{\varphi }=\varphi ^{\prime }$ if $\varphi ^{\prime }\in stLTL \left( \bigcirc ,0,\wedge \right)$ and $\overline{\varphi }=0\wedge \varphi ^{\prime }$, otherwise. Clearly, $\varphi ^{\prime }$ and $0\wedge \varphi ^{\prime }$ are equivalent and $0\wedge \varphi ^{\prime }\in stLTL \left( \bigcirc ,0,\wedge \right)$. We fix an $1\le i\le n_{p}$, and we denote for simplicity $T_{p,i},U_{m_{i}}$ (where $T_{p,i}\in U_{m_{i}}$) with $T,U_{m}$, respectively. Let

$$\begin{aligned} T=\left( \left( \psi _{0},l_{0}\right) ,\left( \varphi _{1},\psi _{1},l_{1}\right) ,\ldots ,\left( \varphi _{m},\psi _{m},l_{m}\right) \right) \end{aligned}$$

and define the tuple $T^{\prime }\in U_{m+1}$ by

$$\begin{aligned} T^{\prime }=\left( \left( \overline{\varphi },0\right) ,\left( \widetilde{\varphi },\psi _{0},l_{0}\right) ,\left( \varphi _{1},\psi _{1},l_{1}\right) ,\ldots ,\left( \varphi _{m},\psi _{m},l_{m}\right) \right) . \end{aligned}$$

Then, for every $w\in A^{\omega },j>l_{0}+\ldots +l_{m}$ we have

$$\begin{aligned}&\left\langle T^{\prime },w,j\right\rangle \nonumber \\&\quad =\underset{0\le q<j-(l_{0} +\ldots +l_{m})}{\max }\left( \left( \left\| \overline{\varphi }\right\| ,w\right) +\underset{0\le h<q}{ {\displaystyle \sum }}d_{w_{<h}}\left( \left\| \widetilde{\varphi }\right\| ,w_{\ge h}\right) +d_{w_{<q}}\left\langle T,w_{\ge q},j-q\right\rangle \right) \quad \quad \end{aligned}$$

(1)

and $\left\langle T^{\prime },w,j\right\rangle =-\infty$ for every $j\le l_{0}+\ldots +l_{m}.$ We repeat the same procedure for every $1\le i\le n_{p}$ and we get the corresponding $(m_{i}+1)$-tuple $T_{p,i}^{\prime }$.

Now we show that for every $w\in A^{\omega },j\ge 0$ we have

$$\begin{aligned} \left( 0_{L^{+}},w_{<j}\right) =\max \left( \underset{1\le h\le p-1}{\max }\left( \underset{1\le i\le n_{h}}{\max }\left( \left\langle T_{h,i},w,j\right\rangle \right) \right) ,\underset{1\le i\le n_{p}}{\max }\left( \left\langle T_{p,i}^{\prime },w,j\right\rangle \right) \right) . \end{aligned}$$

To this end, let $w_{<j}\in L^{+}$, hence either $w_{<j}\in \mathop {\bigcup }\nolimits _{1\le h\le p-1}L^{h},$ or $w_{<j}\in \mathop {\bigcup }\nolimits _{h\ge p}L^{h}.$ In the first case ${\max \nolimits _{1\le h\le p-1}}\left( \left( 0_{L^{h} },w_{<j}\right) \right) =0$ and so ${\max \nolimits _{1\le h\le p-1}}\left( \max \nolimits _{1\le i\le n_{h}}\left( \left\langle T_{h,i},w,j\right\rangle \right) \right) =0$. In the latter case, $\exists u\in L^{*},v\in L^{p}$ such that $w_{<j}=uv.$ Since $v=\left( w_{\ge \left| u\right| }\right) _{<\left| v\right| }$ and $\left( 0_{L^{p} },v\right) =0$, by induction hypothesis, we get that ${\max \nolimits _{1\le i\le n_{p}}}\left( \left\langle T_{p,i},w_{\ge \left| u\right| },\left| v\right| \right\rangle \right) ={\max \nolimits _{1\le i\le n_{p} }}\left( \left\langle T_{p,i},w_{\ge \left| u\right| },j-\left| u\right| \right\rangle \right) =0$. Then, by the proof of Lemma 6.12 (p. 372) in [24], we get that for every suffix $u^{\prime }$ of $u$ we have $u^{\prime }vw_{\ge j}\in L^{k+1}A^{\omega }\cup \left( A^{\omega }\setminus L^{k}A^{\omega }\right)$. Hence, $\left( \left\| \overline{\varphi }\right\| ,w\right) +{{\sum \nolimits _{0\le h<\left| u\right| }}}d_{w_{<h}}\left( \left\| \widetilde{\varphi }\right\| ,w_{\ge h}\right) +d_{w_{<\left| u\right| }}\left\langle T_{p,i} ,w_{\ge \left| u\right| },j-\left| u\right| \right\rangle =0$ for some $1\le i\le n_{p}.$ By this and relation (1), we conclude that ${\max \nolimits _{1\le i\le n_{p}}}\left( \left\langle T_{p,i}^{\prime },w,j\right\rangle \right) =0$. Therefore, $\left( 0_{L^{+}},w_{<j}\right) =0$ implies ${\max \nolimits _{1\le h\le p-1}}\left( \max \nolimits _{1\le i\le n_{h}}\left( \left\langle T_{h,i},w,j\right\rangle \right) \right) =0$ or ${\max \nolimits _{1\le i\le n_{p}}}\left( \left\langle T_{p,i}^{\prime },w,j\right\rangle \right) =0,$ as required.

Conversely, assume that ${\max \nolimits _{1\le h\le p-1}}\left( \max \nolimits _{1\le i\le n_{h}}\left( \left\langle T_{h,i} ,w,j\right\rangle \right) \right) =0$ or ${\max \nolimits _{1\le i\le n_{p}}}\left( \left\langle T_{p,i}^{\prime },w,j\right\rangle \right) =0.$ If the first one is true, then ${\max \nolimits _{1\le h\le p-1}}\left( \left( 0_{L^{h}},w_{<j}\right) \right) =0.$ Otherwise, if the latter case holds, then there is an $1\le i\le n_{p}$ such that $\left\langle T_{p,i}^{\prime },w,j\right\rangle =0$. This implies that $j>l_{0}+\ldots +l_{m_{i}},$ and by relation (1) we get

$$\begin{aligned}&\left\langle T_{p,i}^{\prime },w,j\right\rangle \\&\quad =\underset{0\le q<j-(l_{0} \!+\!\ldots +l_{m_{i}})}{\max }\left( \left( \left\| \overline{\varphi }\right\| ,w\right) \!+\!\underset{0\le h<q}{ {\displaystyle \sum }}d_{w_{<h}}\left( \left\| \widetilde{\varphi }\right\| ,w_{\ge h}\right) +d_{w_{<q}}\left\langle T_{p,i},w_{\ge q,}j-q\right\rangle \right) \!=\!0. \end{aligned}$$

Therefore, $\left( \left\| \overline{\varphi }\right\| ,w\right) =0$, and for some $0\le q<j-(l_{0}+\ldots +l_{m_{i}})$ we have $\left( \left\| \widetilde{\varphi }\right\| ,w_{\ge h}\right) =\left( 0_{L^{k+1} A^{\omega }\cup \left( A^{\omega }\setminus L^{k}A^{\omega }\right) },w_{\ge h}\right) =0$ for every $0\le h<q$, and $\left\langle T_{p,i},w_{\ge q,}j-q\right\rangle =\left( 0_{L^{p}},\left( w_{\ge q}\right) _{<j-q}\right) =0$. We set $u=w_{<q}$, and $v=\left( w_{\ge q}\right) _{<j-q}.$ Then $w=uvw_{\ge j}$ and the requirements of Lemma 60 fulfilled. We conclude that $w_{<j}=uv\in L^{+},$ i.e., $\left( 0_{L^{+} },w_{<j}\right) =0,$ and our proof is completed.$\square$

By the above inductive proof, we get that for every star-free language $L\subseteq A^{+}$ we can find a unique integer $n>0$ and a unique (up to formulas’ equivalence) set of tuples $\left( T_{i}\right) _{1\le i\le n}$, with $T_{i}\in U_{m_{i}}$ ($m_{i}\ge 0$) for every $1\le i\le n$, satisfying Lemma 63. More interestingly, we get that ${\max \nolimits _{1\le i\le n}}\left( \left\langle T_{i},w,j\right\rangle \right) ={\max \nolimits _{1\le i\le n}}\left( \left\langle T_{i},w^{\prime },j\right\rangle \right)$ for every $w,w^{\prime }\in A^{\omega }$ with $w_{<j}=w_{<j}^{\prime }$.

Example 64

Let $A=\left\{ a,b\right\}$ and $L=\left\{ ab\right\} .$ Clearly, $L$ is a prefix-free set with bounded synchronization delay $k=1.$ Following the inductive construction of the previous proof we get: $\varphi ^{\prime }=p_{a}\wedge \bigcirc p_{b},$ $\varphi _{L^{2}A^{\omega }} =p_{a}\wedge \bigcirc p_{b}\wedge \bigcirc ^{2}p_{a}\wedge \bigcirc ^{3}p_{b}$, $\varphi _{A^{\omega }\setminus LA^{\omega }}=\lnot \left( p_{a}\wedge \bigcirc p_{b}\right)$ and $\widetilde{\varphi }=\varphi _{L^{2}A^{\omega }}\vee \varphi _{A^{\omega }\setminus LA^{\omega }}.$ We set $T_{1}=\left( \varphi ^{\prime },1\right)$ and $T_{2}=\left( \left( 0\wedge \varphi ^{\prime },0\right) ,\left( \widetilde{\varphi },\varphi _{L^{2}A^{\omega } },3\right) \right) .$ Then, $\left( 0_{L^{+}},w_{<j}\right) =\max \left( \left\langle T_{1},w,j\right\rangle ,\left\langle T_{2},w,j\right\rangle \right)$ for every $w\in A^{\omega },\; j\ge 0.$ For instance, for every $w\in A^{\omega },\;\left\langle T_{1},w,j\right\rangle =0$ iff $\left( j=2\text { and }w_{<2}=ab\right) .$ Let now $w=abababu$ where $u\in A^{\omega }$. Then,

$$\begin{aligned} \left\langle T_{2},w,6\right\rangle&=\underset{0+i_{1}+3=5}{\underset{i_{1}\in \mathbb {N}}{\max }}\left( \left( \left\| \varphi ^{\prime }\right\| ,w\right) \!+\!\underset{0\le j_{1}<i_{1}}{\sum }d_{w_{<j_{1}}}\left( \left\| \widetilde{\varphi }\right\| ,w_{\ge j_{1}}\right) +d_{w_{<i_{1}}}\left( \left\| \varphi _{L^{2}A^{\omega }}\right\| ,w_{\ge i_{1}}\right) \right) \\&=\left( \left\| \varphi ^{\prime }\right\| ,w\right) +\left( \left\| \widetilde{\varphi }\right\| ,w\right) +d_{a}\left( \left\| \widetilde{\varphi }\right\| ,w_{\ge 1}\right) +d_{ab}\left( \left\| \varphi _{L^{2}A^{\omega }}\right\| ,w_{\ge 2}\right) =0\\&=\left( 0_{L^{+}},w_{<6}\right) . \end{aligned}$$

Similarly,

$$\begin{aligned} \left\langle T_{2},w,5\right\rangle&=\underset{0+i_{1}+3=4}{\underset{i_{1}\in \mathbb {N}}{\max }}\left( \left( \left\| \varphi ^{\prime }\right\| ,w\right) \!+\!\underset{0\le j_{1}<i_{1}}{\sum }d_{w_{<j_{1}}}\left( \left\| \widetilde{\varphi }\right\| ,w_{\ge j_{1}}\right) +d_{w_{<i_{1}}}\left( \left\| \varphi _{L^{2}A^{\omega }}\right\| ,w_{\ge i_{1}}\right) \right) \\&=\left( \left\| \varphi ^{\prime }\right\| ,w\right) +\left( \left\| \widetilde{\varphi }\right\| ,w\right) +d_{a}\left( \left\| \varphi _{L^{2}A^{\omega }}\right\| ,w_{\ge 1}\right) =-\infty \\&=\left( 0_{L^{+}},w_{<5}\right) . \end{aligned}$$

It is clear that the values obtained by the semantics of the formulas $\varphi ^{\prime },\widetilde{\varphi },\varphi _{L^{2}A^{\omega }}$ appearing in the computation of $\left\langle T_{2},w,6\right\rangle$ do not depend on the suffix $u=w_{\ge 6}$ of $w$, but only on the prefix $w_{<6}.$ This implies that $\left\langle T_{2},w^{\prime },6\right\rangle =\left\langle T_{2},w,6\right\rangle$ for $w^{\prime }= abababu ^{\prime }$ with $u^{\prime }\ne u$ ($u^{\prime }\in A^{\omega }$). A similar observation can be made for $\left\langle T_{2},w,5\right\rangle$.

Proposition 65

Let $L\subseteq A^{+}$ be a star-free language and $r\in \mathbb {R}_{\max }\left\langle \left\langle A^{*}\right\rangle \right\rangle$ be a letter-step series. Then, for every $\varphi \in ULTL \left( \mathbb {R}_{\max },A\right)$ the infinitary series $\left( 0_{L}+r^{+}\right) +_{d}\left\| \varphi \right\|$ is $\omega \hbox {-} ULTL \hbox {-}d$-definable.

Proof

Let $r=\max _{a\in A}\left( \left( k_{a}\right) _{a}\right)$ where $k_{a}\in \mathbb {R}_{\max }$ for every $a\in A$. We set $\zeta =\bigvee \nolimits _{a\in A}\left( k_{a}\wedge p_{a}\right)$. By the previous lemma there exist an $n>0$ and $T_{q}\in U_{m_{q}}$ ($m_{q}\ge 0$) for every $1\le q\le n$, such that for every $w\in A^{\omega },j\ge 0$ we have $\left( 0_{L},w_{<j}\right) ={\max \nolimits _{1\le q\le n}}\left( \left\langle T_{q},w,j\right\rangle \right)$. We fix a $1\le q\le n$ and let as assume that

$$\begin{aligned} T_{q}=\left( \left( \varphi _{0},k_{0}\right) ,\left( \xi _{1},\varphi _{1},k_{1}\right) ,\ldots ,\left( \xi _{m_{q}},\varphi _{m_{q}},k_{m_{q} }\right) \right) . \end{aligned}$$

We define the tuple $T_{q}^{\prime }\in U_{m_{q}}$ by

$$\begin{aligned} T_{q}^{\prime }=\left( \left( \varphi _{0}^{\prime },k_{0}\right) ,\left( \xi _{1}^{\prime },\varphi _{1}^{\prime },k_{1}\right) ,\ldots ,\left( \xi _{m_{q}}^{\prime },\varphi _{m_{q}}^{\prime },k_{m_{q}}\right) \right) \end{aligned}$$

as follows.

• If $m_{q}=0$, then $\varphi _{0}^{\prime }=\varphi _{0}\wedge \left( {{\bigwedge \nolimits _{0\le h\le k_{0}}}}\bigcirc ^{h}\zeta \right)$.

• If $m_{q}>0$, then $\xi _{l}^{\prime }=\xi _{l}\wedge \zeta$ for every $1\le l\le m_{q}.$ Moreover, for every $0\le l\le m_{q}-1$, if $k_{l} \ne 0,$ then we let $\varphi _{l}^{\prime }=\varphi _{l}\wedge \left( { {\bigwedge \nolimits _{0\le h\le k_{l}-1}}}\bigcirc ^{h}\zeta \right)$, otherwise $\varphi _{l}^{\prime }=\varphi _{l}.$ Finally, we set $\varphi _{m_{q}}^{\prime }=\varphi _{m_{q}}\wedge \left( {{\bigwedge \nolimits _{0\le h\le k_{m_{q}}}}}\bigcirc ^{h}\zeta \right)$.

We show that $\left\langle T_{q}^{\prime },w,j\right\rangle =\left\langle T_{q},w,j\right\rangle +\left( r^{+},w_{<j}\right)$ for every $w\in A^{\omega },j\ge 0.$ Indeed, assume firstly that $m_{q}=0$. Then, for every $j\ne k_{0}+1$ we get $\left\langle T_{q}^{\prime },w,j\right\rangle =\left\langle T_{q},w,j\right\rangle =-\infty$ which implies that $\left\langle T_{q}^{\prime },w,j\right\rangle =\left\langle T_{q} ,w,j\right\rangle +\left( r^{+},w_{<j}\right) .$ For $j=k_{0}+1$ we have

$$\begin{aligned} \left\langle T_{q}^{\prime },w,j\right\rangle&=\left( \left\| \varphi _{0}\wedge \left( \underset{0\le h\le k_{0}}{ {\displaystyle \bigwedge }}\bigcirc ^{h}\zeta \right) \right\| ,w\right) \\&=\left( \left\| \varphi _{0}\right\| ,w\right) +\left( \left\| \underset{0\le h\le k_{0}}{ {\displaystyle \bigwedge }}\bigcirc ^{h}\zeta \right\| ,w\right) \\&=\left\langle T_{q},w,j\right\rangle +\underset{0\le h\le k_{0}}{ {\displaystyle \sum }}d_{w_{<h}}\left( \max _{a\in A}\left( \left( k_{a}\right) _{a}\right) ,w\left( h\right) \right) \\&=\left\langle T_{q},w,j\right\rangle +\left( r^{+},w_{<j}\right) . \end{aligned}$$

Next let $m_{q}>0$. For every $j\le k_{0}+\ldots +k_{m_{q}}$ we have $\left\langle T_{q}^{\prime },w,j\right\rangle =\left\langle T_{q} ,w,j\right\rangle =-\infty$, i.e., $\left\langle T_{q}^{\prime } ,w,j\right\rangle =\left\langle T_{q},w,j\right\rangle +\left( r^{+},w_{<j}\right)$. Furthermore, for every $j>k_{0}+\ldots +k_{m_{q}}$ it holds

$$\begin{aligned} \left\langle T_{q}^{\prime },w,j\right\rangle =\underset{S_{m_{q}} =j-1}{\underset{i_{1},i_{2},\ldots ,i_{m_{q}}\in \mathbb {N}}{\max }}\left( \left( \left\| \varphi _{0}^{\prime }\right\| ,w\right) +\underset{1\le l\le m_{q}}{{\displaystyle \sum }}\left( \begin{array}{l} \underset{0\le j_{l}<i_{l}}{ {\displaystyle \sum }}d_{w_{<S_{l-1}+j_{l}}}\left( \left\| \xi _{l}^{\prime }\right\| ,w_{\ge S_{l-1}+j_{l}}\right) \\ +d_{w_{<S_{l-1}+i_{l}}}\left( \left\| \varphi _{l}^{\prime }\right\| ,w_{\ge S_{l-1}+i_{l}}\right) \end{array} \right) \right) . \end{aligned}$$

By definition we have

• $\left( \left\| \varphi _{0}^{\prime }\right\| ,w\right) =\left( \left\| \varphi _{0}\right\| ,w\right) +{{\sum \nolimits _{0\le h\le k_{0}-1}} }d_{w_{<h}}\left( r,w\left( h\right) \right)$,

• $\left( \left\| \xi _{l}^{\prime }\right\| ,w_{\ge S_{l-1}+j_{l}}\right) =\left( \left\| \xi _{l}\right\| ,w_{\ge S_{l-1}+j_{l}}\right) +\left( r,w\left( S_{l-1}+j_{l}\right) \right)$ for every $1\le l\le m_{q}$ and $0\le j_{l}<i_{l}$,

• $\left( \left\| \varphi _{l}^{\prime }\right\| ,w_{\ge S_{l-1}+i_{l}}\right) \!=\!\left( \left\| \varphi _{l}\right\| ,w_{\ge S_{l-1}+i_{l}}\right) +{{\sum \nolimits _{0\le h\le k_{l}-1}} }d_{\left( w_{\ge S_{l-1}+i_{l}}\right) _{<h}}\!\left( r,w\left( S_{l-1}+i_{l}+h\right) \right)$ for every $1\le l\le m_{q}-1$, and

• $\left( \left\| \varphi _{m_{q}}^{\prime }\right\| ,w_{\ge S_{m_{q}-1}+i_{m_{q}}}\right) =\left( \left\| \varphi _{m_{q}}\right\| ,w_{\ge S_{m_{q}-1}+i_{m_{q}}}\right) +{{\sum \nolimits _{0\le h\le k_{m_{q}}}}}d_{\left( w_{\ge S_{m_{q}-1} +i_{m_{q}}}\right) _{<h}}\left( r,w\left( S_{m_{q}-1}+i_{m_{q}}+h\right) \right)$.

Hence

$$\begin{aligned}&\left\langle T_{q}^{\prime },w,j\right\rangle \\&\quad =\underset{S_{m_{q}}=j-1}{\underset{i_{1},i_{2},\ldots ,i_{m_{q}}\in \mathbb {N}}{\max }}\left( \begin{array}{c} \left( \left\| \varphi _{0}\right\| ,w\right) +\underset{1\le l\le m_{q}}{{\displaystyle \sum } }\left( \begin{array}{l} \underset{0\le j_{l}<i_{l}}{ {\displaystyle \sum }}d_{w_{<S_{l-1}+j_{l}}}\left( \left\| \xi _{l}\right\| ,w_{\ge S_{l-1}+j_{l}}\right) \\ +d_{w_{<S_{l-1}+i_{l}}}\left( \left\| \varphi _{l}\right\| ,w_{\ge S_{l-1}+i_{l}}\right) \end{array} \right) \\ +\underset{0\le h\le S_{m_{q}}}{ {\displaystyle \sum }}d_{w_{<h}}\left( r,w\left( h\right) \right) \end{array} \right) \\&\quad =\underset{S_{m_{q}}=j-1}{\underset{i_{1},i_{2},\ldots ,i_{m_{q}}\in \mathbb {N}}{\max }}\left( \left( \left\| \varphi _{0}\right\| ,w\right) +\underset{1\le l\le m_{q}}{ {\displaystyle \sum }}\left( \begin{array}{l} \underset{0\le j_{l}<i_{l}}{ {\displaystyle \sum }}d_{w_{<S_{l-1}+j_{l}}}\left( \left\| \xi _{l}\right\| ,w_{\ge S_{l-1}+j_{l}}\right) \\ +d_{w_{<S_{l-1}+i_{l}}}\left( \left\| \varphi _{l}\right\| ,w_{\ge S_{l-1}+i_{l}}\right) \end{array} \right) \right) +\left( r^{+},w_{<j}\right) \\&\quad =\left\langle T_{q},w,j\right\rangle +\left( r^{+},w_{<j}\right) . \end{aligned}$$

Therefore, we get

$$\begin{aligned} \left( 0_{L},w_{<j}\right) +\left( r^{+},w_{<j}\right)&=\underset{1\le q\le n}{\max }\left( \left\langle T_{q},w,j\right\rangle \right) +\left( r^{+},w_{<j}\right) \\&=\underset{1\le q\le n}{\max }\left( \left\langle T_{q},w,j\right\rangle +\left( r^{+},w_{<j}\right) \right) \\&=\underset{1\le q\le n}{\max }\left( \left\langle T_{q}^{\prime },w,j\right\rangle \right) . \end{aligned}$$

Now, we define the formula $\zeta _{q}\in ULTL \left( \mathbb {R}_{\max },A\right)$ by

$$\begin{aligned} \zeta _{q}=\varphi _{0}^{\prime }\wedge \bigcirc ^{k_{0}}\left( \xi _{1}^{\prime }U\left( \varphi _{1}^{\prime }\wedge \bigcirc ^{k_{1}}\left( \xi _{2}^{\prime }U\left( \varphi _{2}^{\prime }\wedge \bigcirc ^{k_{2}}\left( \ldots U\left( \varphi _{m_{q}}^{\prime }\wedge \bigcirc ^{k_{m_{q}}+1}\varphi \right) \right) \right) \right) \right) \right) . \end{aligned}$$

By induction on $m_{q}$, with straightforward calculations, we can show that

$$\begin{aligned} \left( \left\| \zeta _{q}\right\| ,w\right) =\underset{j\ge 0}{\sup }\left( \left\langle T_{q}^{\prime },w,j\right\rangle +d_{w_{<j}}\left( \left\| \varphi \right\| ,w_{\ge j}\right) \right) \end{aligned}$$

for every $w\in A^{\omega }$. We repeat the same procedure for every $1\le q\le n$. We consider the formula ${ {\bigvee \nolimits _{1\le q\le n}}}\zeta _{q}\in ULTL \left( \mathbb {R}_{\max },A\right)$. Then for every $w\in A^{\omega }$ we get

$$\begin{aligned} \left( \left\| \underset{1\le q\le n}{ {\displaystyle \bigvee }}\zeta _{q}\right\| ,w\right)&=\left( \underset{1\le q\le n}{\max }\left( \left\| \zeta _{q}\right\| \right) ,w\right) \\&=\underset{1\le q\le n}{\max }\left( \underset{j\ge 0}{\sup }\left( \left\langle T_{q}^{\prime },w,j\right\rangle +d_{w_{<j}}\left( \left\| \varphi \right\| ,w_{\ge j}\right) \right) \right) \\&=\underset{j\ge 0}{\sup }\left( \underset{1\le q\le n}{\max }\left( \left\langle T_{q}^{\prime },w,j\right\rangle +d_{w_{<j}}\left( \left\| \varphi \right\| ,w_{\ge j}\right) \right) \right) \\&=\underset{j\ge 0}{\sup }\left( \underset{1\le q\le n}{\max }\left( \left\langle T_{q}^{\prime },w,j\right\rangle \right) +d_{w_{<j}}\left( \left\| \varphi \right\| ,w_{\ge j}\right) \right) \\&=\underset{j\ge 0}{\sup }\left( \left( 0_{L}+r^{+},w_{<j}\right) +d_{w_{<j}}\left( \left\| \varphi \right\| ,w_{\ge j}\right) \right) \\&=\left( \left( 0_{L}+r^{+}\right) +_{d}\left\| \varphi \right\| ,w\right) , \end{aligned}$$

and our proof is completed.$\square$

Our next result states that the almost simple $\omega \hbox {-}d$-counter-free series are $\omega \hbox {-}U$ LTL-$d$-definable, and in fact concludes our theory.

Theorem 66

$\omega \hbox {-} asCF (\mathbb {R}_{\max },A,d)\subseteq \omega$-$ULTL ( \mathbb {R}_{\max },A,d)$.

Proof

Clearly it suffices to show that whenever $\mathcal {A}_{1},\ldots ,\mathcal {A}_{n-1}$ are simple cfwa and $\mathcal {A}_{n}$ is a simple cfwBa over $A$ and $\mathbb {R}_{\max }$, then $\left\| \mathcal {A}_{1}\right\| +_{d}\ldots +_{d}\left\| \mathcal {A}_{n}\right\| \in \omega \hbox {-} ULTL ( \mathbb {R}_{\max },A,d)$. We let $r_{i}=\left\| \mathcal {A}_{i}\right\|$, and denote by $k_{i}$ the initial weight $\ne -\infty$ and $k_{a}^{(i)}$ the weight $\ne -\infty$ of the transitions of $\mathcal {A}_{i}\; (1\le i\le n)$ labelled by $a\in A$. Since $supp \left( r_{n}\right)$ is an $\omega$-counter-free language it is also $\omega$-LTL-definable hence, there is formula $\varphi \in bLTL (\mathbb {R}_{\max },A)$ with $\left\| \varphi \right\| =0_{ supp \left( r_{n}\right) }$. We let $\varphi _{n}=k_{n}\wedge \varphi \wedge \left( \left( {{\bigvee \nolimits _{a\in A}}}k_{a}^{(n)}\wedge p_{a}\right) U0\right)$ and we trivially get $r_{n}=\left\| \varphi _{n}\right\|$. By construction $\varphi _{n}\in ULTL \left( \mathbb {R}_{\max },A\right)$. Furthermore, for every $1\le i\le n-1$, the language $supp \left( r_{i}\right) \setminus \left\{ \varepsilon \right\} \subseteq A^{+}$ is counter-free hence, star-free. Since

$$\begin{aligned} r_{i}|_{A^{+}}=0_{ supp \left( r_{i}\right) \backslash \left\{ \varepsilon \right\} }+\left( k_{i}+\left( \max \limits _{a\in A}\left( \left( k_{a}^{(i)}\right) _{a}\right) \right) ^{+}\right) \end{aligned}$$

for every $1\le i\le n-1$, and

$$\begin{aligned} r_{n-1}|_{A^{+}}+_{d}r_{n}=k_{n-1}+\left( \left( 0_{ supp \left( r_{n-1}\right) \backslash \left\{ \varepsilon \right\} }+\left( \max \limits _{a\in A}\left( \left( k_{a}^{(n-1)}\right) _{a}\right) \right) ^{+}\right) +_{d}r_{n}\right) , \end{aligned}$$

by applying Proposition 65, we get that

$$\begin{aligned} \left( 0_{ supp \left( r_{n-1}\right) \backslash \left\{ \varepsilon \right\} }+\left( \max \limits _{a\in A}\left( \left( k_{a}^{(n-1)}\right) _{a}\right) \right) ^{+}\right) +_{d}r_{n}\in \omega \hbox {-} ULTL ( \mathbb {R}_{\max },A,d) \end{aligned}$$

which implies that there exists a $ULTL \left( \mathbb {R} _{\max },A\right)$ formula $\varphi _{n-1}^{+}$ such that

$$\begin{aligned} \left( 0_{ supp \left( r_{n-1}\right) \backslash \left\{ \varepsilon \right\} }+\left( \max \limits _{a\in A}\left( \left( k_{a}^{(n-1)}\right) _{a}\right) \right) ^{+}\right) +_{d}r_{n}=\left\| \varphi _{n-1} ^{+}\right\| . \end{aligned}$$

Hence, $r_{n-1}|_{A^{+}}+_{d}r_{n}=\left\| k_{n-1}\wedge \varphi _{n-1}^{+}\right\|$. We let $\varphi _{n-1}=\left( k_{n-1} \wedge \varphi _{n-1}^{+}\right) \vee \left( \left( r_{n-1},\varepsilon \right) \wedge \varphi _{n}\right) \in ULTL \left( \mathbb {R}_{\max },A\right)$ and we have $\left\| \varphi _{n-1}\right\| =r_{n-1}+_{d}r_{n}$. Thus $r_{n-1}+_{d}r_{n}\in \omega \hbox {-} ULTL ( \mathbb {R}_{\max },A,d)$. We proceed in the same way, and we show that $r_{i}+_{d} \ldots +_{d}r_{n}\in \omega \hbox {-} ULTL ( \mathbb {R}_{\max },A,d)$, for every $1\le i\le n-2$, which concludes our proof.$\square$

Now we are ready to state the equivalence of $\omega$-rLTL -$d$-definable, $\omega$-wqFO-$d$-definable, $\omega \hbox {-}d$-star-free, and almost simple $\omega \hbox {-}d$-counter-free series. More precisely, by Theorems 18, 45, 56, and 66 we get our main theorem.

Theorem 67

(Main theorem)

$$\begin{aligned} \omega \text {-} rLTL \left( \mathbb {R}_{\max },A,d\right) \!=\!\omega \text {-} wqFO ( \mathbb {R}_{\max },A,d)=\omega \text {-} SF ( \mathbb {R}_{\max },A,d)=\omega \text {-} asCF ( \mathbb {R}_{\max },A,d). \end{aligned}$$

8 Weighted MSO logic with discounting revisited

In this last section, we show that the consideration of the discounted existential quantification does not increase the power of the weighted MSO sentences which are expressively equivalent to $\omega$-recognizable series with discounting. In fact, we show that $\left\| \exists _{d}x\cdot \varphi \right\|$ is an $\omega \hbox {-}d$-recognizable series provided that $\left\| \varphi \right\|$ is an $\omega$-recognizable step function. This assumption is consistent with the definition of our weakly quantified FO logic fragment. For the definition of $\omega$-recognizable step functions we refer the reader to [13].

Proposition 68

Let $\varphi \in MSO ( \mathbb {R}_{\max },A)$ such that $\left\| \varphi \right\|$ is an $\omega$-recognizable step function. Then the series $\left\| \exists _{d}x\cdot \varphi \right\|$ is $\omega$-$d$-recognizable.

Proof

Let $\mathcal {W}= free (\varphi )\cup \{x\}$ and $\mathcal {V}= free (\exists _{d}x\cdot \varphi )=\mathcal {W}\setminus \{x\}.$ In case $x\notin free (\varphi ),$ by Proposition 28 in [13], we have $\left\| \varphi \right\| _{\mathcal {W}}={\max \nolimits _{1\le j\le n}}\left( k_{j}+0_{L_{j}}\right)$ with $\omega$-recognizable languages $L_{j}\subseteq A_{\mathcal {W}}^{\omega }\;(1\le j\le n)$. Moreover, $L_{j}\;\left( 1\le j\le n\right)$ can be considered to be a partition of $A_{\mathcal {W} }^{\omega }.$

Consider the alphabet $\widetilde{A}=A\times \{1,\ldots ,n\}$. Then, the elements of $\widetilde{A}_{\mathcal {V}}$ are triples of the form $\left( a,l,s\right) \in A\times \left\{ 1,\ldots ,n\right\} \times \left\{ 0,1\right\} ^{\mathcal {V}}$, and a word in $\widetilde{A}_{\mathcal {V} }^{\omega }$ can be written as a triple $(w,v,\sigma )$ where $(w,\sigma )\in A_{\mathcal {V}}^{\omega },$ and $v$ is a mapping from $\omega$ to $\{1,\ldots ,n\}.$ We fix a $1\le j\le n$ and let

$$\begin{aligned} \widetilde{L_{j}}=\{(w,v,\sigma )\in \widetilde{A}_{\mathcal {V}}^{\omega } \mid \exists i\ge 0\,\,\hbox {such that}\,v(i)=j\Longrightarrow (w,\sigma [x\rightarrow i])\in L_{j}\}. \end{aligned}$$

We show that $\widetilde{L_{j}}$ is $\omega$-recognizable. Let $\mathcal {A}_{j}=(Q,A_{\mathcal {W}},I,\Delta ,F)$ be a (nondeterministic) Büchi automaton accepting $L_{j}$. Without any loss we assume that for every $q_{1}\in Q,\;a\in A,$ and $s\in \left\{ 0,1\right\} ^{\mathcal {V}},$ there is a state $q_{2}\in Q$ such that $\left( q_{1},\left( a,\left[ s\rightarrow 0\right] \right) ,q_{2}\right) \in \Delta .$ We construct the Büchi automaton $\widetilde{\mathcal {A}_{j}}=\left( \widetilde{Q},\widetilde{A}_{\mathcal {V}},\widetilde{I},\widetilde{\Delta },\widetilde{F}\right)$ as follows. First we let $Q^{\prime }=\{q^{\prime }\mid q\in Q\}$ to be a copy of $Q$. Then we set $\widetilde{Q}=Q\times (Q\cup Q^{\prime }),$ $\widetilde{I}=\{(q,q)\mid q\in I\},$ and $\widetilde{F}=Q\times F^{\prime }$ where $F^{\prime }=\{q^{\prime }\mid q\in F\}$. The set of transitions $\widetilde{\Delta }$ is defined in the following way.

For every $\left( (q_{1},\overline{q}_{1}),(a,l,s),(q_{2},\overline{q}_{2})\right) \in \widetilde{Q}\times \widetilde{A}_{\mathcal {V}}\times \widetilde{Q}$, we let

$$\begin{aligned} \left( (q_{1},\overline{q}_{1}),(a,l,s),(q_{2},\overline{q}_{2})\right) \in \widetilde{\Delta }\text { \ iff\ \ }\left( q_{1},(a,s[x\rightarrow 0]),q_{2}\right) \in \Delta \end{aligned}$$

and

• $\overline{q}_{1}=q_{1}$ and $\overline{q}_{2}=q_{2},$ or

• $l=j,\;\overline{q}_{1}=q_{1},$ $\overline{q}_{2}=p^{\prime }\in Q^{\prime },$ and $\left( q_{1},(a,s[x\rightarrow 1]),p\right) \in \Delta$, or

• $\overline{q}_{1}=p^{\prime }\in Q^{\prime },$ $\overline{q} _{2}=r^{\prime }\in Q^{\prime },$ and $\left( p,(a,s[x\rightarrow 0]),r\right) \in \Delta$.

We show that $L\left( \widetilde{\mathcal {A}_{j}}\right) =\widetilde{L_{j}}$, where $L\left( \widetilde{\mathcal {A}_{j}}\right)$ stands for the behavior of $\widetilde{\mathcal {A}_{j}}.$ Let $(w,v,\sigma )\in \widetilde{L}_{j}$. Then, there exists an $i\ge 0$ such that $v(i)=j$ and $(w,\sigma [x\rightarrow i])\in L_{j},$ hence there exists a successful path $P_{(w,\sigma [x\rightarrow i])}$ of $\mathcal {A}_{j}$ over $(w,\sigma [x\rightarrow i])$. Let $P_{(w,\sigma [x\rightarrow i])}=\left( \left( q_{k},(a_{k},s_{k}[x\rightarrow l_{k}]),q_{k+1}\right) \right) _{k\ge 0}$ with $l_{k}=1$ if $k=i,$ and $l_{k}=0$ otherwise. Let $\widetilde{P}_{(w,v,\sigma )}=\left( \left( (\overline{q}_{k},\overline{\overline{q}}_{k}),(a_{k},v(k),s_{k}),(\overline{q}_{k+1},\overline{\overline{q}}_{k+1})\right) \right) _{k\ge 0}$ be a path of $\widetilde{\mathcal {A}_{j}}$ over $(w,v,\sigma )$ defined by

• $\overline{q}_{k}=\overline{\overline{q}}_{k}=q_{k}$ for every $0\le k\le i,$

• $\overline{q}_{k}=p_{k}\in Q$ for every $k>i,$ where $\left( q_{i},(a_{i},s_{i}[x\rightarrow 0]),p_{i+1}\right) ,\left( p_{k},(a_{k} ,s_{k}[x\rightarrow 0]),p_{k+1}\right) \in \Delta ,$ and

• $\overline{\overline{q}}_{k}=q_{k}^{\prime }$ for every $k>i.$

Since $P_{(w,\sigma [x\rightarrow i])}$ is successful, we get $In^{Q}\left( P_{(w,\sigma [x\rightarrow i])}\right) \cap F\ne \emptyset$ ⁶. Therefore, by construction of $\widetilde{P}_{(w,v,\sigma )}$, we have $In^{Q^{\prime }}\left( pr_{2}\left( \widetilde{P}_{(w,v,\sigma )}\right) \right) \cap F^{\prime }\ne \emptyset$ ($pr_{2}$ projects every state in $\widetilde{Q}$ to its second component) which implies that $In^{\widetilde{Q}}\left( \widetilde{P}_{(w,v,\sigma )}\right) \cap \widetilde{F}\ne \emptyset .$ We conclude $(w,v,\sigma )\in L\left( \widetilde{\mathcal {A}_{j}}\right) ,$ i.e., $\widetilde{L_{j}}\subseteq L\left( \widetilde{\mathcal {A}_{j}}\right)$.

Next, we show the converse inclusion. For this let $(w,v,\sigma )\in L\left( \widetilde{\mathcal {A}_{j}}\right) .$ There exists a successful path $\widetilde{P}_{(w,v,\sigma )}=\left( \left( (\overline{q}_{k},\overline{\overline{q}}_{k}),(a_{k},v(k),s_{k}),(\overline{q}_{k+1},\overline{\overline{q}}_{k+1})\right) \right) _{k\ge 0}$ of $\widetilde{\mathcal {A}_{j}}$ over $(w,v,\sigma ).$ We have $In^{\widetilde{Q}}\left( \widetilde{P}_{(w,v,\sigma )}\right) \cap \widetilde{F}\ne \emptyset$, i.e., $In^{Q^{\prime }}\left( pr_{2}\left( \widetilde{P}_{(w,v,\sigma )}\right) \right) \cap F^{\prime }\ne \emptyset$. This implies that there exists an $i\ge 0$ such that $v(i)=j$ and

• $\overline{q}_{k}=\overline{\overline{q}}_{k}=q_{k}$ for every $0\le k\le i$ and $\left( q_{k},(a_{k},s_{k}[x\rightarrow 0]),q_{k+1} \right) \in \Delta$ for every $1\le k<i$,

• $\overline{q}_{k}=p_{k}\in Q$ for every $k>i$ and $\left( q_{i},(a_{i},s_{i}[x\rightarrow 0]),p_{i+1}\right) ,\left( p_{k},(a_{k} ,s_{k}[x\rightarrow 0]),p_{k+1}\right) \in \Delta$, and

• $\overline{\overline{q}}_{k}=q_{k}^{\prime }$ for every $k>i$ and $\left( q_{i},(a_{i},s_{i}[x\rightarrow 1]),q_{i+1}\right) \in \Delta$ and $\left( q_{k},(a_{k},s_{k}[x\rightarrow 0]),q_{k+1}\right) \;\in \Delta$ for every $k>i+1$.

Consider the path $P_{(w,\sigma [x\rightarrow i])}=\left( \left( q_{k},(a_{k},s_{k}[x\rightarrow l_{k}]),q_{k+1}\right) \right) _{k\ge 0}$ of $\mathcal {A}_{j}$ over $(w,\sigma [x\rightarrow i])$ where $l_{k}=1$ if $k=i,$ and $l_{k}=0$ otherwise. Since $In^{Q^{\prime }}\left( pr_{2}\left( \widetilde{P}_{(w,v,\sigma )}\right) \right) \cap F^{\prime }\ne \emptyset$ we get $In^{Q}\left( P_{(w,\sigma [x\rightarrow i])}\right) \cap F\ne \emptyset$. Thus $P_{(w,\sigma [x\rightarrow i])}$ is successful, hence $(w,\sigma [x\rightarrow i])\in L_{j}.$ We conclude $(w,v,\sigma )\in \widetilde{L_{j}},$ as required.

Next we consider the weighted automaton $\overline{\mathcal {A}_{j} }=(\widetilde{Q},in, wt ,\widetilde{F})$ over $\widetilde{A}_{\mathcal {V}}$ and $\mathbb {R}_{\max }$ in the following way. For every $(q,\overline{q})\in \widetilde{Q}$ we let

$$\begin{aligned} in ((q,\overline{q}))=\left\{ \begin{array}{l@{\quad }l} 0 &{} \text {if }\overline{q}=q\in I\\ -\infty &{} \text {otherwise} \end{array} .\right. \end{aligned}$$

The weight assignment mapping $wt :\widetilde{Q}\times \widetilde{A}_{\mathcal {V}}\times \widetilde{Q}\rightarrow \mathbb {R}_{\max }$ is defined as follows. For every $t\in \left( \widetilde{Q} \times \widetilde{A}_{\mathcal {V}}\times \widetilde{Q}\right) \setminus \widetilde{\Delta }$ we let $wt (t)=-\infty ,$ whereas for every $\left( (q_{1},\overline{q}_{1}),(a,l,s),(q_{2},\overline{q}_{2})\right) \in \widetilde{\Delta }$ we set

$$\begin{aligned} wt \left( \left( (q_{1},\overline{q}_{1}),(a,l,s),(q_{2},\overline{q}_{2})\right) \right) =\left\{ \begin{array}{l@{\quad }l} 0 &{} \text {if }\overline{q}_{1}=q_{1}\text { and }\overline{q}_{2}=q_{2}\\ 0 &{} \text {if }\overline{q}_{1},\overline{q}_{2}\in Q^{\prime }\\ k_{j} &{} \text {if }\overline{q}_{1}=q_{1},l=j,\text { and }\overline{q}_{2}\in Q^{\prime }\\ -\infty &{} \text {otherwise.} \end{array}\right. \end{aligned}$$

Then for every $(w,v,\sigma )\in \widetilde{A}_{\mathcal {V}}^{\omega }$ we have⁷

$$\begin{aligned} \left( \left\| \overline{\mathcal {A}_{j}}\right\| ,(w,v,\sigma )\right) =\sup \left\{ d_{w_{<i}}\cdot k_{j}\mid i\ge 0,\;v(i)=j,\text { and }(w,\sigma [x\rightarrow i])\in L_{j}\right\} . \end{aligned}$$

Now, we let the weighted automaton $\overline{\mathcal {A}}$ to be the disjoint union of the weighted automata $\overline{\mathcal {A}_{j}}$ for all $1\le j\le n$. For every $(w,v,\sigma )\in \widetilde{A}_{\mathcal {V} }^{\omega }$ we have

$$\begin{aligned} \left( \left\| \overline{\mathcal {A}}\right\| ,(w,v,\sigma )\right)&=\underset{1\le j\le n}{\max }\left( \left( \left\| \overline{\mathcal {A}_{j}}\right\| ,(w,v,\sigma )\right) \right) \\&=\underset{1\le j\le n}{\max }\left( \sup \left\{ d_{w_{<i}}\cdot k_{j}\mid i\ge 0,\text { }v(i)=j,\text { and }(w,\sigma [x\rightarrow i])\in L_{j}\right\} \right) \end{aligned}$$

Let $h:\widetilde{A}_{\mathcal {V}}\rightarrow A_{\mathcal {V}}$ be the strict alphabetic epimorphism given by $h((a,l,s))=(a,s)$ for every $(a,l,s)\in \widetilde{A}_{\mathcal {V}}$. Then

$$\begin{aligned}&\left( h\left( \left\| \overline{\mathcal {A}}\right\| \right) ,(w,\sigma )\right) \\&\quad =\underset{v:\omega \rightarrow \{1,\ldots ,n\}}{\sup }\left( \left( \left\| \overline{\mathcal {A}}\right\| ,(w,v,\sigma )\right) \right) \\&\quad =\underset{v:\omega \rightarrow \{1,\ldots ,n\}}{\sup }\left( \underset{1\le j\le n}{\max }\left( \sup \left\{ d_{w_{<i}}\cdot k_{j}\mid i\ge 0,\text { }v(i)=j,\text { and }(w,\sigma [x\rightarrow i])\in L_{j}\right\} \right) \right) \\&\quad =\underset{1\le j\le n}{\max }\left( \underset{v:\omega \rightarrow \{1,\ldots ,n\}}{\sup }\left( \sup \left\{ d_{w_{<i}}\cdot k_{j}\mid i\ge 0,\text { }v(i)=j,\text { and }(w,\sigma [x\rightarrow i])\in L_{j}\right\} \right) \right) \\&\quad =\underset{1\le j\le n}{\max }\left( \underset{i\ge 0}{\sup }\left\{ d_{w_{<i}}\cdot k_{j}\mid (w,\sigma [x\rightarrow i])\in L_{j}\right\} \right) \\&\quad =\underset{i\ge 0}{\sup }\left( d_{w_{<i}}\cdot \underset{1\le j\le n}{\max }\left( \left( k_{j}+0_{L_{j}},(w,\sigma [x\rightarrow i])\right) \right) \right) \\&\quad =\underset{i\ge 0}{\sup }\left( d_{w_{<i}}\cdot \left( \left\| \varphi \right\| _{\mathcal {W}},(w,\sigma [x\rightarrow i])\right) \right) \\&\quad =\left( \left\| \exists _{d}x\cdot \varphi \right\| ,(w,\sigma )\right) \end{aligned}$$

for every $(w,\sigma )\in A_{\mathcal {V}}^{\omega }$. The argument above and Proposition 23(b) in [13] imply that the series $\left\| \exists _{d}x\cdot \varphi \right\|$ is $\omega \hbox {-}d$-recognizable and this completes our proof.$\square$

The proposition above implies that the expressive power of weighted restricted MSO sentences over $A$ and $\mathbb {R}_{\max }$ (cf. [13]) remains the same if we add the discounted existential first-order quantification applied to $\omega$-recognizable step functions.

Corollary 69

The class of $\omega \hbox {-}d$-definable series $($over $A$ and $\mathbb {R}_{\max })$ by weighted restricted MSO sentences coincides with the class of $\omega \hbox {-}d$-definable series $($over $A$ and $\mathbb {R}_{\max })$ by weighted restricted MSO sentences equipped with the discounted existential quantification which is applied to $\omega$-recognizable step functions.

9 Conclusion

We introduced a weighted LTL, a weighted FO logic, $\omega \hbox {-}d$-star-free series and counter-free weighted Büchi automata, over the max-plus semiring. We showed the equality of series definable in fragments of the weighted LTL and FO logic, $\omega \hbox {-}d$-star-free series, and almost simple $\omega \hbox {-}d$-counter-free series. In order to ensure the convergence of infinite sums in the max-plus semiring, we used the usual method of discounting. For the translation of an almost simple $\omega \hbox {-}d$-counter-free series to a weighted LTL definable series, we considered the corresponding boolean result of the translation of a counter-free Büchi automaton to an LTL formula. Our theory is applied as well into the min-plus semiring $\mathbb {R}_{\min }=(\mathbb {R}_{+}\cup \{\infty \},\min ,+,\infty ,0)$ by replacing max and sup with min and inf, respectively. Complexity results for our constructions form an interesting point for future research. In the literature, weighted logics have been investigated over arbitrary semirings; it is our intention to develop our theory in that framework. A first approach, to this direction, has been done in [23] for a restricted class of semirings. Recently, in [12], the authors considered weighted automata and weighted MSO logics over algebraic structures which are not semirings any more. Such structures, are important for concrete practical applications, and the development of our theory in that setup is a challenge.