inequality relation $\mathsf{R}\in\\{<,>,\leq,\geq,=,\neq\\}$, and a threshold
value $v\in\mathbb{Q}$ the DS comparison language with upper bound $\mu$,
relation $\mathsf{R}$, discount factor $d$ and threshold value $v$ is a
language of infinite words over the alphabet $\Sigma=\\{-\mu,\dots,\mu\\}$
that accepts $A\in\Sigma^{\omega}$ iff $\mathit{DS}({A},{d})$ $\mathsf{R}$ $v$
holds.

######  Definition 8.3 (DS comparator automata with threshold
$v\in\mathbb{Q}$)

For an integer upper bound $\mu>0$, discount factor $d>1$, equality or
inequality relation $\mathsf{R}\in\\{<,>,\leq,\geq,=,\neq\\}$, and a threshold
value $v\in\mathbb{Q}$ the DS comparator automata with upper bound $\mu$,
relation $\mathsf{R}$, discount factor $d$ and threshold value $v$ is an
automaton that accepts the DS comparison language with upper bound $\mu$,
relation $\mathsf{R}$, discount factor $d$ and threshold value $v$.

For sake of succinctness, we refer to the DS comparison language and DS
comparator automata by comparison language and comparator, respectively.

###### Safety and co-safety of DS comparison languages

Our finding here is all DS comparison languages are either safety langauges or
co-safety langagues. More interestingly, the only parameter that decides
whether a comparison langauge is safety/co-safety is the equality or
inequality relation $\mathsf{inc}$. The values of the discount factor and
threshold have no implication on this property.

These observations are formally proven next: Recall definitions of safety/co-
safety languages and bad-prefixes from Chapter 6.

###### Theorem 8.4

Let $\mu>1$ be the integer upper bound. For arbitrary discount factor $d>1$
and threshold value $v$

  1. 1.

DS comparison languages are safety languages for relations
$R\in\\{\leq,\geq,=\\}$.

  2. 2.

DS comparison language are co-safety languages for relations
$R\in\\{<,>,\neq\\}$.

###### Proof 81

Due to duality of safety/co-safety languages, it is sufficient to show that
DS-comparison language with $\leq$ is a safety language.

Let us assume that DS-comparison language with $\leq$ is not a safety
language. Let $W$ be a weight-sequence in the complement of DS-comparison
language with $\leq$ such that it does not have a bad prefix.

Since $W$ is in the complement of DS-comparison language with $\leq$,
$\mathit{DS}({W},{d})>v$. By assumption, every $i$-length prefix $W[i]$ of $W$
can be extended to a bounded weight-sequence $W[i]\cdot Y^{i}$ such that
$\mathit{DS}({W[i]\cdot Y^{i}},{d})\leq v$.

Note that $\mathit{DS}({W},{d})=\mathit{DS}({{\rm
Phys.~{}Rev.~{}E}{W}{i}},{d})+\frac{1}{d^{i}}\cdot\mathit{DS}({W[i\dots]},{d})$,
and $\mathit{DS}({{\rm Phys.~{}Rev.~{}E}{W}{i}\cdot
Y^{i}},{d})=\mathit{DS}({{\rm
Phys.~{}Rev.~{}E}{W}{i}},{d})+\frac{1}{d^{i}}\cdot\mathit{DS}({Y^{i}},{d})$.
The contribution of tail sequences $W[i\dots]$ and $Y^{i}$ to the discounted-
sum of $W$ and ${\rm Phys.~{}Rev.~{}E}{W}{i}\cdot Y^{i}$, respectively
diminishes exponentially as the value of $i$ increases. In addition, since and
$W$ and ${\rm Phys.~{}Rev.~{}E}{W}{i}\cdot Y^{i}$ share a common $i$-length
prefix ${\rm Phys.~{}Rev.~{}E}{W}{i}$, their discounted-sum values must
converge to each other. The discounted sum of $W$ is fixed and greater than
$v$, due to convergence there must be a $k\geq 0$ such that $\mathit{DS}({{\rm
Phys.~{}Rev.~{}E}{W}{k}\cdot Y^{k}},{d})>v$. Contradiction. Therefore, DS-
comparison language with $\leq$ is a safety language.

The above intuition is formalized below:

Since $\mathit{DS}({W},{d})>v$ and $\mathit{DS}({{\rm
Phys.~{}Rev.~{}E}{W}{i}\cdot Y^{i}},{d})\leq v$, the difference
$\mathit{DS}({W},{d})-\mathit{DS}({{\rm Phys.~{}Rev.~{}E}{W}{i}\cdot
Y^{i}},{d})>0$.

By expansion of each term, we get $\mathit{DS}({W},{d})-\mathit{DS}({{\rm
Phys.~{}Rev.~{}E}{W}{i}\cdot
Y^{i}},{d})=\frac{1}{d^{i}}(\mathit{DS}({W[i\dots]},{d})-\mathit{DS}({Y^{i}},{d}))\leq\frac{1}{d^{i}}\cdot(\mod{\mathit{DS}({W[i\dots]},{d})}+\mod{\mathit{DS}({Y^{i}},{d})})$.
Since the maximum value of discounted-sum of sequences bounded by $\mu$ is
$\frac{\mu\cdot d}{d-1}$, we also get that
$\mathit{DS}({W},{d})-\mathit{DS}({{\rm Phys.~{}Rev.~{}E}{W}{i}\cdot
Y^{i}},{d})\leq 2\cdot\frac{1}{d^{i}}\mod{\frac{\mu\cdot d}{d-1}}$.

Putting it all together, for all $i\geq 0$ we get

$0<\mathit{DS}({W},{d})-\mathit{DS}({W[i]\cdot Y^{i}},{d})\leq
2\cdot\frac{1}{d^{i}}\mod{\frac{\mu\cdot d}{d-1}}$

As $i\rightarrow\infty$,
$2\cdot\mod{\frac{1}{d^{i-1}}\cdot\frac{\mu}{d-1}}\rightarrow 0$. So,
$\text{lim}_{{}_{\rightarrow}i\rightarrow\infty}(\mathit{DS}({W},{d})-\mathit{DS}({W[i]\cdot
Y^{i}},{d}))=0$. Since $\mathit{DS}({W},{d})$ is fixed,
$\text{lim}_{{}_{\rightarrow}i\rightarrow\infty}\mathit{DS}({W[i]\cdot
Y^{i}},{d})=\mathit{DS}({W},{d})$.

By definition of convergence, there exists an index $k\geq 0$ such that
$\mathit{DS}({W[k]\cdot Y^{k}},{d})$ falls within the
$\frac{\mod{\mathit{DS}({W},{d})}}{2}$ neighborhood of $\mathit{DS}({W},{d})$.
Finally since $\mathit{DS}({W},{d})>0$, $\mathit{DS}({W[k]\cdot Y^{k}},{d})>0$
as well. But this contradicts our assumption that for all $i\geq 0$,
$\mathit{DS}({W[i]\cdot Y^{i}},{d})\leq 0$.

Therefore, DS-comparator with $\leq$ is a safety comparator.

∎

######  $\omega$-regularity of DS comparison languages

Next, we determine $\omega$-regularity of comparison languages with threshold
value $v\in\mathbb{Q}$. The critical parameter in this case is the discount
factor $d>1$. We observe that a comparison language is $\omega$-regular iff
the discount factor is an integer. Finally, while the threshold value does not
affect the $\omega$-regularity of a comparison language, it impacts the size
of the $\omega$-regular comparator automata (when discount factor $d>1$ is an
integer).

First, we introduce notation. Since $v\in\mathbb{Q}$, w.l.o.g. let us assume
that the threshold value is represented by the regular expression
$v=v[0]v[1]\dots v[m](v[m+1]v[m+2]\dots v[n])^{\omega}$. By abuse of notation,
we denote both the regular expression $v[0]v[1]\dots v[m](v[m+1]v[m+2]\dots
v[n])^{\omega}$ and the value $\mathit{DS}({v},{d})$ by $v$.

Our first result is that a comparison language with $v\in\mathbb{Q}$ is not
$\omega$-regular if the discount factor is not an integer. The result follows
immediately from prior work as it is known that comparison language with $v=0$
is not $\omega$-regular if the discount factor is not an integer [26].
Therefore:

###### Theorem 8.5

Let $\mu>0$ be the integer upper bound, $v\in\mathbb{Q}$ be the threshold
value, and $\mathsf{inc}\in\\{<,>,\leq,\geq,=,\neq\\}$ be an equality or
inequality relation. Let the discount factor $d>1$ be a non-integer. Then, the
DS comparison language with $\mu$, $d$, $\mathsf{inc}$, and $v$ is not
$\omega$-regular.

Next, we prove that DS comparison languages are $\omega$-regular if the
discount factor $d>1$ is an integer. To prove this, we construct the Büchi
automaton corresponding to the language. Since Büchi automata are closed under
complementation, intersection and union, it is sufficient to construct the
(Büchi) comparator automata for one equality or inequality relation
$\mathsf{inc}$. We do so for the relation $\leq$. The construction technique
resembles the construction of comparator automata for threshold $v=0$ for
inequality relation $\leq$ presented in [28]. Due to space constraints, we
present critical lemma statements, theorem statement and high-level intuition.
Please refer to [28] or the supplemental material for details.

Since we know that the comparison language for $\leq$ is a safety language, we
begin by characterizing the bad-prefixes of the comparison language with
threshold $v\in\mathbb{Q}$ and relation $\leq$. For this, we introduce
notation. Let $W$ be a finite weight-sequence. By abuse of notation, the
discounted-sum of finite-sequence $W$ with discount-factor $d$ is defined as
$\mathit{DS}({W},{d})=\mathit{DS}({W\cdot 0^{\omega}},{d})$. The recoverable-
gap of a finite weight-sequences $W$ with discount factor $d$, denoted
$\mathsf{gap}(W,d)$, is its normalized discounted-sum: If $W=\varepsilon$ (the
empty sequence), $\mathsf{gap}(\varepsilon,d)=0$, and
$\mathsf{gap}(W,d)=d^{|W|-1}\cdot\mathit{DS}({W},{d})$ otherwise [31].

###### Lemma 8.6

Let $\mu>0$ be the integer upper bound, $d>1$ be an integer discount factor,
and the relation $\mathsf{inc}$ be the inequality $\leq$. Let $v\in\mathbb{Q}$
be the threshold value such that $v=v[0]v[1]\dots v[m](v[m+1]v[m+2]\dots
v[n])^{\omega}$. Let $W$ be a non-empty, bounded, finite weight-sequence.
Then, weight sequence $W$ is a bad-prefix of the DS comparison language with
$\mu$, $d$, $\leq$ and $v$ iff $\mathsf{gap}(W-{\rm
Phys.~{}Rev.~{}E}{v}{|W|},d)>\frac{1}{d}\cdot\mathit{DS}({\mathsf{post}_{v}(|W|)},{d})+\frac{\mu}{d-1}$.

###### Proof 82

Let $W$ be a bad prefix. Then for all infinite length, bounded weight sequence
$Y$ we get that $\mathit{DS}({W\cdot
Y},{d})>v\implies\mathit{DS}({W},{d})+\frac{1}{d^{|W|}}\cdot\mathit{DS}({Y},{d})\geq\mathit{DS}({{\rm
Phys.~{}Rev.~{}E}{v}{|W|}\cdot\mathsf{post}_{v}(|W|)},{d})\implies\mathit{DS}({W},{d})-\mathit{DS}({{\rm
Phys.~{}Rev.~{}E}{v}{|W|}},{d})>\frac{1}{d^{|W|}}\cdot(\mathit{DS}({\mathsf{post}_{v}(|W|)},{d})-\mathit{DS}({Y},{d}))\implies\mathsf{gap}(W-{\rm
Phys.~{}Rev.~{}E}{v}{|W|},d)>\frac{1}{d}(\mathit{DS}({\mathsf{post}_{v}(|W|)},{d})+\frac{\mu\cdot
d}{d-1})$.

Next, we prove that if a finite weight sequence $W$ is such that, the W is a
bad prefix. Let $Y$ be an arbitrary infinite but bounded weight sequence. Then
$\mathit{DS}({W\cdot
Y},{d})=\mathit{DS}({W},{d})+\frac{1}{d^{|W|}}\cdot\mathit{DS}({Y},{d})=\frac{1}{d^{|W|-1}}\cdot\mathsf{gap}(W,d)+\frac{1}{d^{|W|}}\cdot\mathit{DS}({Y},{d})=\frac{1}{d^{|W|-1}}\cdot\mathsf{gap}(W,d)+\frac{1}{d^{|W|}}\cdot\mathit{DS}({Y},{d})+\frac{1}{d^{|W|-1}}\cdot(\mathsf{gap}({\rm
Phys.~{}Rev.~{}E}{v}{|W|},d)-\mathsf{gap}({\rm Phys.~{}Rev.~{}E}{v}{|W|},d))$.
By re-arrangement of terms we get that $\mathit{DS}({W\cdot
Y},{d})=\frac{1}{d^{|W|-1}}\cdot\mathsf{gap}(W-{\rm
Phys.~{}Rev.~{}E}{v}{|W|},d)+\frac{1}{d^{|W|}}\cdot\mathit{DS}({Y},{d})+\frac{1}{d^{|W|-1}}\cdot\mathsf{gap}({\rm
Phys.~{}Rev.~{}E}{v}{|W|},d)$. Since $\mathsf{gap}(W-{\rm
Phys.~{}Rev.~{}E}{v}{|W|},d)>\frac{1}{d}\cdot(\mathit{DS}({\mathsf{post}_{v}(|W|)},{d})+\frac{\mu\cdot
d}{d-1})$ holds, we get that $\mathit{DS}({W\cdot
Y},{d})>\frac{1}{d^{|W|}}\cdot(\mathit{DS}({\mathsf{post}_{v}(|W|)},{d})+\frac{\mu\cdot
d}{d-1})+\frac{1}{d^{|W|}}\cdot\mathit{DS}({Y},{d})+\frac{1}{d^{|W|-1}}\cdot\mathsf{gap}({\rm
Phys.~{}Rev.~{}E}{v}{|W|},d)$. Since minimal value of
$\mathit{DS}({Y},{d})is\frac{-\mu\cdot d}{d-1}$, the inequality simplifies to
$\mathit{DS}({W\cdot Y},{d})>\frac{1}{d^{|W|-1}}\cdot\mathsf{gap}({\rm
Phys.~{}Rev.~{}E}{v}{|W|},d)+\frac{1}{d^{|W|}}\cdot\mathit{DS}({\mathsf{post}_{v}(|W|)},{d})\implies\mathit{DS}({W\cdot
Y},{d})>\mathit{DS}({v},{d})=v$. Therefore, $W$ is a bad prefix. ∎

Intuitively, Lemma 8.6 says that if an infinite length weight sequence $A$ has
a finite prefix for which its recoverable gap is too large, then the sequence
$A$ will not be present in the coveted language. This way, if we track the
recoverable gap value of finite-prefixes of $A$, Lemma 8.6 gives a handle for
when to reject $A$ from the coveted language. It also says that if the
recoverable gap of a finite-prefix exceeds the bounds in the lemma statement,
then there is no need to track the recoverable gap of other finite-prefixes
any further.

Similarly, we define very-good prefixes for the comparison language with
$\mu$, $d$, $\leq$ and $v$ as follows: A finite and bounded weight-sequence
$W$ is a very good prefix for the aformentioned language if for all infinite,
bounded extensions of $W$ by $Y$, $\mathit{DS}({W\cdot Y},{d})\leq v$. A proof
similar to Lemma 8.6 proves an upper bound for the recoverable gap of very-
good prefixes of the language:

###### Lemma 8.7

Let $\mu>0$ be the integer upper bound, $d>1$ be an integer discount factor,
and the relation $\mathsf{inc}$ be the inequality $\leq$. Let $v\in\mathbb{Q}$
be the threshold value such that $v=v[0]v[1]\dots v[m](v[m+1]v[m+2]\dots
v[n])^{\omega}$. Let $W$ be a non-empty, bounded, finite weight-sequence.
Weight sequence $W$ is a very good-prefix of DS comparison language with
$\mu$, $d$, $\leq$ and $v$ iff $\mathsf{gap}(W-{\rm
Phys.~{}Rev.~{}E}{v}{|W|},d)\leq\frac{1}{d}\cdot\mathit{DS}({\mathsf{post}_{v}(|W|)},{d})-\frac{\mu}{d-1}$.

###### Proof 83

Let $W$ be a very good prefix. Then for all infinite, bounded sequences $Y$,
we get that $\mathit{DS}({W\cdot Y},{d})\leq
v\implies\mathit{DS}({W},{d})+\frac{1}{d^{|W|}}\cdot\mathit{DS}({Y},{d})\leq
v$. By re-arrangement of terms, we get that $\mathsf{gap}(W-{\rm
Phys.~{}Rev.~{}E}{v}{|W|},d)\leq\frac{1}{d}\cdot\mathit{DS}({\mathsf{post}_{v}(|W|)},{d})-\frac{1}{d}\cdot\mathit{DS}({Y},{d})$.
Since maximal value of $\mathit{DS}({Y},{d})=\frac{\mu\cdot d}{d-1}$, we get
that $\mathsf{gap}(W-{\rm
Phys.~{}Rev.~{}E}{v}{|W|},d)\leq\frac{1}{d}\cdot\mathit{DS}({\mathsf{post}_{v}(|W|)},{d})-\frac{\mu}{d-1}$.

Next, we prove the converse. We know $\mathit{DS}({W\cdot
Y},{d})=\mathit{DS}({W},{d})+\frac{1}{d^{|W|}}\cdot\mathit{DS}({Y},{d})=\frac{1}{d^{|W|-1}}\cdot\mathsf{gap}(W,d)+\frac{1}{d^{|W|}}\cdot\mathit{DS}({Y},{d})=\frac{1}{d^{|W|-1}}\cdot\mathsf{gap}(W,d)+\frac{1}{d^{|W|}}\cdot\mathit{DS}({Y},{d})+\frac{1}{d^{|W|-1}}\cdot(\mathsf{gap}({\rm
Phys.~{}Rev.~{}E}{v}{|W|},d)-\mathsf{gap}({\rm Phys.~{}Rev.~{}E}{v}{|W|},d))$.
By re-arrangement of terms we get that

$\mathit{DS}({W\cdot Y},{d})=\frac{1}{d^{|W|-1}}\cdot\mathsf{gap}(W-{\rm
Phys.~{}Rev.~{}E}{v}{|W|},d)+\frac{1}{d^{|W|}}\cdot\mathit{DS}({Y},{d})+\frac{1}{d^{|W|-1}}\cdot\mathsf{gap}({\rm
Phys.~{}Rev.~{}E}{v}{|W|},d)$. From assumption we derive that
$\mathit{DS}({W\cdot
Y},{d})\leq\frac{1}{d^{|W|}}\cdot\mathit{DS}({\mathsf{post}_{v}(|W|)},{d})-\frac{\mu}{d-1}+\frac{1}{d^{|W|}}\cdot\mathit{DS}({Y},{d})+\mathit{DS}({{\rm
Phys.~{}Rev.~{}E}{v}{|W|}},{d})$. Since maximal value of
$\mathit{DS}({Y},{d})$ is $\frac{\mu}{d-1}$, we get that $\mathit{DS}({W\cdot
Y},{d})\leq v$. Therefore, $W$ is a very good prefix. ∎

Intuitively, Lemma 8.7 says that if an infinite-length weight sequence $A$ has
a finite-prefix for which the recoverable gap is too small, $A$ is present in
the coveted language. This condition gives a handle on when to accept the
weight sequence $A$ by tracking on the recoverable gap of its finite prefixes.
It also says that if the recoverable gap of a finite-prefix falls below the
bound in Lemma 8.7, there is no need to track recoverable gaps of finite-
prefixes of $A$ any further.

The question we need to answer to obtain the targeted Büchi automata is how to
track the recoverable gaps of finite-prefixes using a finite amount of memory
(or states). We already know that there are upper and lower bounds on which
recoverable gaps are interesting: If a recoverable gap is too large (Lemma
8.6) or too small (Lemma 8.7), the recoverable gap value does not need to be
tracked any more. Now note that since the discount factor is an integer, in
our case the recoverable gap value is always an integer (from definition of
recoverable gap). Therefore, between the upper and lower bounds for
recoverable established by Lemma 8.6 and Lemma 8.7, there are only finitely
many candidate values of recoverable gaps. These finitely many values will
form the states of the automata.

The final question is how to determine the transition function of the
automata. For this, observe that the recoverable-gap has an inductive
definition i.e. $\mathsf{gap}(\varepsilon,d)=0$, where $\varepsilon$ is the
empty weight-sequence, and $\mathsf{gap}(W\cdot
w,d)=d\cdot\mathsf{gap}(W,d)+w$, where $w\in\\{-\mu,\dots,\mu\\}$. Therefore,
transitions between states are established by mimicking the inductive
definition.

Therefore, the formal construction of the Büchi automata for comparison
language with threshold $v$ with relation $\leq$ is given as follows:

###### Theorem 8.6

Let $\mu>0$ be the integer upper bound, $d>1$ be an integer discount factor,
and the relation $\mathsf{inc}$ be the inequality $\leq$. Let $v\in\mathbb{Q}$
be the threshold value such that $v=v[0]v[1]\dots v[m](v[m+1]v[m+2]\dots
v[n])^{\omega}$. Then the DS comparison language for with $\mu$, $d$, $\leq$
and $v$ is $\omega$-regular.

###### Proof 84

The ideas described above are formalized to construct the desired Büchi
automaton as follows:

For $i\in\\{0,\dots,n\\}$, let
$\mathsf{U}_{i}=\frac{1}{d}\cdot\mathit{DS}({\mathsf{post}_{v}(i)},{d})+\frac{\mu}{d-1}$
(from Lemma 8.6).

For $i\in\\{0,\dots,n\\}$, let
$\mathsf{L}_{i}=\frac{1}{d}\cdot\mathit{DS}({\mathsf{post}_{v}(i)},{d})-\frac{\mu}{d-1}$
(from Lemma 8.7).

The Büchi automata $\mathcal{A}=(S,s_{I},\Sigma,\delta,\mathcal{F})$ is
defined as follows:

  * •

States $S=\bigcup_{i=0}^{n}S_{i}\cup\\{\mathsf{bad},\mathsf{veryGood}\\}$
where
$S_{i}=\\{(s,i)|s\in\\{\lfloor\mathsf{L}_{i}\rfloor+1,\dots,\lfloor\mathsf{U}_{i}\rfloor\\}\\}$

  * •

Initial state $s_{I}=(0,0)$, Accepting states
$\mathcal{F}=S\setminus\\{\mathsf{bad}\\}$

  * •

Alphabet $\Sigma=\\{-\mu,-\mu+1,\dots,\mu-1,\mu\\}$

  * •

Transition function $\delta\subseteq S\times\Sigma\rightarrow S$ where
$(s,a,t)\in\delta$ then:

    1. 1.

If $s\in\\{\mathsf{bad},\mathsf{veryGood}\\}$, then $t=s$ for all $a\in\Sigma$

    2. 2.

If $s$ is of the form $(p,i)$, and $a\in\Sigma$

      1. (a)

If $d\cdot p+a-v[i]>\lfloor\mathsf{U}_{i}\rfloor$, then $t=\mathsf{bad}$

      2. (b)

If $d\cdot p+a-v[i]\leq\lfloor\mathsf{L}_{i}\rfloor$, then
$t=\mathsf{veryGood}$

      3. (c)

If $\lfloor\mathsf{L}_{i}\rfloor<d\cdot
p+a-v[i]\leq\lfloor\mathsf{U}_{i}\rfloor$,

        1. i.

If $i==n$, then $t=(d\cdot p+a-v[i],m+1)$

        2. ii.

Else, $t=(d\cdot p+a-v[i],i+1)$

∎

###### Corollary 8.3

Let $\mu>0$ be the integer upper bound, $d>1$ be an integer discount factor,
and $\mathsf{inc}$ be the equality or inequality relation. Let
$v\in\mathbb{Q}$ be the threshold value such that $v=v[0]v[1]\dots
v[m](v[m+1]v[m+2]\dots v[n])^{\omega}$. Then the DS comparator automata with
with $\mu$, $d$, $\leq$ and $v$ is a safety or co-safety automata with
$\mathcal{O}(\frac{\mu\cdot n}{d-1})$ states.

Note that the (deterministic) Büchi automaton constructed in Theorem 8.6 is a
safety automaton [63]. Safety/Co-safety automata for all other relations can
be constructed by simple modifications to the one constructed above. Further,
note that the number of states depends on the value $v$ (number $n$). Lastly,
this construction is tight, since prior work shows that when $v=0$, the
automaton constructed above is the minimal automata for its language [28].

#####  8.3.2 Reduction of satisficing to solving safety or reachability games

We arrive at the core result of this section. We show that when the discount
factor is an integer, satisficing is reduced to solving a safety or
reachability game. This method is linear in size of the game graph, as opposed
to the higher polynomial solutions of optimization via VI. Hence, satisficing
is more efficient and scalable alternative to analyze quantitative graph games
for integer discount factors.

The key idea behind this reduction is as follows: Recall, the satisficing
problem is to determine whether player $P_{1}$ has a strategy that can
guarantee that all resulting plays will have cost less than (or less than or
equal to) a given threshold value $v\in\mathbb{Q}$. When the discount factor
is an integer, the criteria for satisficing to hold is the same as ensuring
that every resulting play is accepted by the safety/co-safety comparator
automata with the same discount factor inequality relation, and threshold
value. This lets us show that when the discount factor is an integer, the
satisficing problem reduces to solving a new game obtained by taking the
product of the quantitative graph game with the appropriate comparator.
Finally, the resulting new game will be safety or reachability depending on
whether the comparator is safety or co-safety, respectively.

The formal reduction is as follows: Let $G=(V=V_{0}\uplus
V_{1},v_{\mathit{init}},E,\gamma)$ be a quantitative graph game. Let the
maximum weight on the graph game be the integer $\mu>0$. Let $d>1$ be the
integer discount factor. Suppose, $v=v_{0}v_{1}\cdot v_{m}(v_{m+1}\cdots
v_{n})^{\omega}$ is the rational threshold value for the satisficing problem,
and suppose the inequality in the problem is $\mathsf{inc}\in\\{<,\leq\\}$.

Then, first construct the $\omega$-regular comparator automaton for $\mu$,
$d$, $\mathsf{inc}$ and $v$. Let us denote it by
$\mathcal{A}=(S,s_{I},\Sigma,\delta,\mathcal{F})$. From Corollary 8.3 we know
that $\mathcal{A}$ is a deterministic safety or co-safety automaton. Next,
construct structure $\mathsf{GA}=(W=W_{0}\cup
W_{1},s_{0}\times\mathsf{init},\delta_{W},\mathcal{F}_{W})$ from $G$ and
$\mathcal{A}$ as follows:

  * •

$W=V\times S$. Specifically $W_{0}=V_{0}\times S$ and $W_{1}=V_{1}\times S$.

Since $V_{0}$ and $V_{1}$ are disjoint, $W_{0}$ and $W_{1}$ are disjoint too.
Let sets of states $W_{0}$ and $W_{1}$ belong to players $P_{0}$ and $P_{1}$
in $\mathsf{GA}$.

  * •

Let $s_{0}\times\mathsf{init}$ be the initial state of $\mathsf{GA}$.

  * •

Transition relation $\delta_{W}=W\times W$ is defined such that transition
$(w,w^{\prime})\in\delta_{W}$ where $w=(v,s)$ and
$w^{\prime}=(v^{\prime},s^{\prime})$ if

    * –

transition $(v,v^{\prime})\in\delta$,

    * –

$n=\gamma((v,v^{\prime}))$, i.e., $n$ is the cost of the transition in $G$,
and

    * –

$(s,n,s^{\prime})\in\delta_{C}$ is a transition in the comparator automata.

  * •

$\mathcal{F}_{W}=V\times\mathcal{F}$

Finally, let $\mathsf{GA}$ be a reachability game if the comparator
$\mathcal{A}$ is a co-safety automaton, and let $\mathsf{GA}$ be a safety game
otherwise. Correspondingly, $\mathcal{F}_{W}$ will be referred to as accepting
states or rejecting states.

Let us call a play in the quantitative graph game $G$ to be winning play for
$P_{1}$ if its cost relates to threshold $v$ by $\mathsf{inc}$. Recall, the
definition of winning plays in reachability and safety games (Chapter 2).
Then, it is easy to show the following correspondence by relating plays in
$\mathcal{G}$ and those in $\mathsf{GA}$, since $\mathcal{A}$ is
deterministic:

###### Lemma 8.8

There is a one-one correspondence between plays in $G$ and plays in
$\mathsf{GA}$. This correspondence preserves the winning condition.

###### Proof 85

(One-one correspondence) Let $\rho=v_{0}v_{1}\dots$ be a play in $G$ with cost
sequence $w_{0}w_{1}\dots$. Let $s_{0}s_{1}\dots$ be the run of weight cost of
$w_{0}w_{1}\dots$ in the DS comparator. Note, that since the comparator is
deterministic, there is a unique run for each finite/infinite cost sequence.
Then, play $\rho=v_{1}v_{2}\dots$ in $G$ and corresponds to play
$(v_{0},s_{0})(v_{1},s_{1})\dots$ in $\mathsf{GA}$. Similarly, one can prove
that for each play $(v_{0},s_{0})(v_{1},s_{1})\dots$ in $\mathsf{GA}$ uniquely
corresponds to play $v_{0}v_{1}\dots$ in $G$, where the correspondence is
defined by the weight sequence shared by the run $s_{0}s_{1}\dots$ in the
comparator and play $v_{0}v_{1}\dots$ in $G$.

(Winning-condition preservation) A play $\rho=v_{0}v_{1}v_{2}\dots$ is a
winning run for player $P_{1}$ in $G$ iff its cost relates to threshold value
$v$ by $\mathsf{inc}$. So, let $n_{1}n_{2}\dots$ be the cost sequence of
$\rho$ in G, then $\mathit{DS}({n_{1}n_{2}\dots},{d})$ $\mathsf{inc}$ $v$
holds. Let the run of weight sequence $n_{0}n_{1}\dots$ be
$s_{0}s_{1}s_{2}\dots$ in comparator automata $\mathcal{A}$. Then, run
$s_{0}s_{1}s_{2}\dots$ is an accepting run in $\mathcal{A}$. As a result, the
corresponding play in $\mathsf{GA}$, i.e. $s_{0}s_{1}s_{2}\dots$ must be a
winning run in $G$.

∎

Next, let us call a strategy of player $P_{1}$ a winning strategy for $P_{1}$
in $G$ if the strategy guarantees that all resulting plays in $\mathsf{GA}$
are winning for $P_{1}$. Then, it is easy to see that the winning play
preserving, one-one correspondence between plays in $\mathsf{GA}$ and $G$
obtained in Lemma 8.8 can be lifted to winning strategies between both games.
As a result, we get the following:

###### Lemma 8.9

Let $G$ be a quantitative graph game, and $d>1$ be an integer discount factor.
Then player $P_{1}$ has a winning strategy for the satisficing problem with
threshold $v\in Q$ and relation $\mathsf{inc}\in\\{<,\leq\\}$ iff player
$P_{1}$ has a winning strategy in the reachability or safety game
$\mathsf{GA}$ constructed as above.

###### Proof 86

The proof lifts Lemma 8.8 from plays to strategies. The same idea of winning
runs-preserving one-one correspondence is lifted to complete this proof. Due
to the similarities, we skip the proof here. ∎

Then, the final statement for our reduction is:

###### Theorem 8.7

Let $G=(V,v_{\mathit{init}},E,\gamma)$ be a quantitative graph game. Let
$\mu>0$ be the maximum of the absolute value of costs on transitions in $G$.
Let $d>1$ be an integer discount factor $v=v[0]v[1]\cdots v[m](v[m+1]\cdots
v[n])^{\omega}$ be the rational threshold value, and
$\mathsf{inc}\in\\{\leq,<\\}$ be the inequality relation. Then, the complexity
of satisficing on $G$ with threshold $v$ and inequality $\mathsf{inc}$ is
$\mathcal{O}((V+E)\cdot\mu\cdot n)$.

###### Proof 87

From Lemma 8.9 we know satisficing $G$ is equivalent to solving the
reachability/safety game $\mathsf{GA}$ In order to determine its complexity of
solving $\mathsf{GA}$, we need to know its number of states and edges.
Clearly, there are $\mathcal{O}(|V|\cdot\mu\cdot n)$ states in $\mathsf{GA}$,
since the comparator $\mathcal{A}$ has $\mathcal{O}(\mu\cdot n)$ states. We
claim that $\mathsf{GA}$ has $\mathcal{O}(|E|\cdot\mu\cdot v)$ edges. For
this, we observe that a state $(v,s)$ in $\mathsf{GA}$ has the same number of
outgoing edges as state $v$ in $G$, as comparator $\mathcal{A}$ is
deterministic. Since there are $\mathcal{O}(\mu\cdot n)$ copies of each state
$v$ in $\mathsf{GA}$, there are $\mathcal{O}(|E|\cdot\mu\cdot n)$ edges in
$\mathsf{GA}$. Therefore, the solving the reachability/safety game is
$\mathcal{O}((|V|+|E|)\cdot\mu\cdot n)$. ∎

Therefore, we observe that when the discount factor is an integer, our
comparator-based solution for satisficing is more efficient than optimization
via VI by degrees of magnitude in size of the game graph.

####  8.4 Satisficing via value iteration

So far, we have observed that for integer discount factors, comparator-based
satisficing is more efficient than VI-based optimization. However, a crucial
question still remains unanswered: Does the complexity improvement between VI
for optimization to comparators for satisficing arise from (a) solving the
decision problem of satisficing instead of optimization, or (b) adopting the
comparator approach instead of numerical methods? To answer this, we design
and analyze a VI based algorithm for satisficing: If this algorithm shows
improvement over VI for optimization, then the complexity gain would have
occurred from solving satisficing. Otherwise, if this algorithm does not
reflect any improvement, then the gain should have come from adhering to
comparator based methods.

The VI based algorithm for satisficing is described as follows: Perform VI as
was done for optimization in §3.1. Terminate the algorithm after whichever of
the following two occurs first: (a) VI has performed the number of iterations
as shown in Theorem 8.1, or (b): In the $k$-th iteration, the threshold value
$v$ falls outside of the interval defined in Lemma 8.1. In either case, one
can determine how the threshold value relates to the optimal value, and hence
determines satisficing.

Clearly, termination by condition (a). results in the same number of
iterations as optimization itself (Theorem 8.1). We show that condition (b)
does not reduce the number of iterations either. On the contrary, it
introduces non-robustness to the algorithm’s performance (See § 8.1). The
reason is that the number of iterations is based on the distance between the
threshold value and the optimal value. So, if this distance is large, few
iterations will be required since the interval length in Lemma 8.1 declines
exponentially. But if the distance is small (say close to 0), then it will
take as many iterations as taken by optimization itself. Formally,

###### Theorem 8.8

Let $d>1$ be an integer discount factor. Let $G$ be a quantitative graph game
with state set $V$. Let $W$ be the optimal cost, and $v\in\mathbb{Q}$ be the
threshold value. Then number of iterations taken by VI for satisfaction is
$\min\\{O(|V|^{2}),\log{\frac{\mu}{|W|-v}}\\}$.

Hence, VI for satisficing does not improve upon VI for optimization. This
indicates comparator-based methods may be responsible for the improvement.

####  8.5 Implementation and Empirical Evaluation

The goal of the empirical analysis is to determine whether the practical
performance of these algorithms resonate with our theoretical discoveries.

###### Implementation details

We implement three algorithms: (a) $\mathsf{VIOptimal}$: Optimization tool
based on the value-iteration, (b). $\mathsf{CompSatisfice}$: Satisfying tool
implementing our comparator-based method, and (c)$\mathsf{VISatisfice}$:
Satisficing tool based on value iteration. All tools have been implemented in
C++. To overcome floating-point errors in $\mathsf{VIOptimal}$ and
$\mathsf{VISatisfice}$, the tools invoke open-source arbitrary precision
arithmetic library GMP (GNU Multi-Precision) [3]. Arithmetic operations in
$\mathsf{CompSatisfice}$ are contained within integers only. Therefore,
$\mathsf{CompSatisfice}$ does not call the GMP library.

###### Design and setup for experiments

Figure 8.2: Cactus plot. $\mu=5,v=3$. Total benchmarks = 291

Figure 8.3: Single counter scalable benchmark. $\mu=5,v=3$. Timeout = 500s.

Since empirical evaluations and applications of synthesis with quantitative
constraints is an emerging area of research, there exist too few benchmarks of
quantitative game graphs to generate a substantial amount of data to make
inferences on algorithm performance. To this end, our benchmarks are derived
from specification used in synthesis from the temporal specifications. We
obtain (non-quantitative) graph games by converting temporal specifications to
their automaton/game form. Then, we randomly assign an integer weight between
$-\mu$ and $\mu$ (for a given $\mu>0$) over all transitions. In this way, the
benchmarks we create retain the structural aspects of a game graph, and hence
are a better fit than randomly generated graph games.

In all, we create 291 benchmarks. We use temporal specifications used in prior
literature in synthesis from temporal specifications [36, 92]. The state-of-
the-art logic-to-automaton conversion tool $\mathsf{Lisa}$ [27] has been
deployed to obtain the automaton/graph game. The number of states in our
benchmark set ranges from 3 to 50000+. Discount factor $d=2$, threshold $v$
ranges in 0-10. All experiments were run on 8 CPU cores at 2.4GHz, 16GB RAM on
a 64-bit Linux machine.

###### Observations and Inferences

######  $\mathsf{CompSatisfice}$ outperforms $\mathsf{VIOptimal}$

111Figures are best viewed online and in color

in runtime and consequently in number of benchmarks solved The cactus plot in
Fig 8.3 clearly indicates that $\mathsf{CompSatisfice}$ is more efficient than
$\mathsf{VIOptimal}$. In fact, a closer look reveals that all benchmarks
solved by $\mathsf{VIOptimal}$ have fewer than 200 states. In contrast,
$\mathsf{CompSatisfice}$ solves all but two benchmarks. Thus solving
benchmarks with many thousands of states.

To test scalability, we plot runtime of both tools on a set of scalable
benchmarks. For integer parameter $i>0$, the $i$-th scalable benchmark has
$3\cdot 2^{i}$ states. Fig 8.3 plots the observations in $\log$-$\log$ scale.
Thus, the slope of the straight line indicates the degree of polynomial (in
practice). We see that in practice $\mathsf{CompSatisfice}$ exhibits linear
behavior (slope $\sim$1), whereas $\mathsf{VIOptimal}$ is much more expensive
(slope $>>1$) even for small values of weights and threshold.

######  $\mathsf{CompSatisfice}$ is more robust than $\mathsf{VISatisfice}$.

Figure 8.4: Robustness. Fix benchmark, vary $v$. $\mu=5$. Timeout = 500s.

We compare $\mathsf{CompSatisfice}$ and $\mathsf{VISatisfice}$ as the
threshold value changes. This experiment is chosen due to Theorem 8.8 which
proves that $\mathsf{VISatisfice}$ is non-robust. The goal is to see how
$\mathsf{VISatisfice}$ fluctuates in practice, while $\mathsf{CompSatisfice}$
maintains steady performance owning to its low complexity. These are shown in
Fig 8.4.

####  8.6 Quantitative games with temporally extended goals

In several synthesis tasks, the objective is to solve a quantitative game
while also satisfying a given temporal goal. So, the goal is to ensure that
the system has a strategy that also ensures that the temporal objective is met
along all possible plays resulting from the game. However, prior works have
proven that optimal strategies may not exist under extension with temporal
goals, rendering analysis by optimization incompatible with temporal goals
[41]. In this section, we show that our comparator-based solution for
satisficing can extend to all kinds of temporal goals.

Intuitively, a quantitative game with temporal goals appends a quantitative
game with a labeling function that assigns states to atomic propositions.
Therefore, each play of the game is associated with the sequence of atomic
propositions. It is over this sequence of atomic propositions that the given
temporal goal is evaluated. In this section, we show that our comparator-based
approach to solve satisficing on quantitative games can be extended to all
temporal goals expressed by linear temporal logic (LTL) [77]. More generally,
our approach extends to all $\omega$-regular goals. This is in sharp contrast
to existing work based on VI which extends to a limited subclass of temporal
goals only, namely safety objectives [91], since optimal solutions are not
known to exist with $\omega$-regular objectives [41].

Formally, a quantitative game with temporal goals, denoted by
$\mathcal{G}_{\mathsf{T}}$, is the tuple $(G,\mathit{AP},\mathcal{L},\varphi)$
where $G$ is a quantitative game, $\mathit{AP}$ is a finite set of atomic
propositions, $\mathcal{L}:V\rightarrow 2^{\mathit{AP}}$ is a labeling
function, and $\varphi$ is an LTL formula over propositions $\mathit{AP}$.
Plays, cost-sequences, cost and strategies are defined as earlier for
quantitative games. The difference is that plays in a quantitative game with
temporal goals are also accompanied with a sequence of propositions. If
$\rho=v_{0}v_{1}v_{2}\dots$ is a play in game $\mathcal{G}_{\mathsf{T}}$, then
$\rho_{\mathit{AP}}=A_{0}A_{1}A_{2}\dots$ is the proposition sequence where
$A_{i}=\mathcal{L}(v_{i})\subseteq\mathit{AP}$ for all $i\geq 0$. Given an LTL
formula $\varphi$ over $\mathit{AP}$, we say that a play $\rho$ satisfies
$\varphi$ if its corresponding proposition sequence $\rho_{\mathit{AP}}$
satisfies $\varphi$.

Let us assume that the objectives of $P_{0}$ and $P_{1}$ are to maximize and
minimize the cost of plays, respectively. Given threshold value
$v\in\mathbb{Q}$ and inequality relation $\mathsf{inc}\in\\{\leq,<\\}$, a
strategy for $P_{1}$ is said to be winning in a quantitative game with
temporal goals $\mathcal{G}_{\mathsf{T}}$, threshold $v$ and relation
$\mathsf{inc}$ if the strategy is winning for $P_{1}$ in quantitative game $G$
with threshold $v$ and relation $\mathsf{inc}$, and every resulting play in
the game satisfies $\varphi$.

The satisficing problem with temporal goals is defined as follows:

######  Definition 8.4 (Satisficing problem with temporal goals)

Given a quantitative game with temporal goals
$\mathcal{G}_{\mathsf{T}}=(G,\mathit{AP},\mathcal{L},\varphi)$, a threshold
value $v\in\mathbb{Q}$, and an inequality relation
$\mathsf{R}\in\\{\leq,<\\}$, the satisficing problem with temporal goals is to
determine whether $P_{1}$ has a winning strategy in $\mathcal{G}_{\mathsf{T}}$
with threshold $v$ and relation $\mathsf{inc}$, assuming that the objectives
of $P_{0}$ and $P_{1}$ are to maximize and minimize the cost of plays,
respectively.

We show that solving the satisficing problem with temporal goals reduces to
solving a parity game. The key insight behind this is that when the discount
factor is an integer then both the satisficing criteria and the temporal goal
are represented by NBAs. As a result of which the criteria for the player to
win a satisficing problem with temporal goals can be represented by a single
NBA that refers to the combination of both conditions. Thus, leading to a
parity game.

###### Theorem 8.9

Let $\mathcal{G}_{\mathsf{T}}=(G,\mathit{AP},\mathcal{L},\varphi)$ be a
quantitative game with temporal goals. Let $V$ and $E$ refer to the set of
states and edges in game $G$, and $\mu$ be the maximum of the absolute value
of weights along transitions in $G$. Let $d>1$ be an integer discount factor,
and $v=v[0]v[1]\cdots v[m](v[m+1]\cdots v[n])^{\omega}$ be the rational
threshold value

  * •

Solving the satisficing problem with temporal goals reduces to solving a
parity game. The size of the parity game is linear in $|V|$, $\mu$, $n$ and
double exponential in $|\varphi|$.

  * •

If $\varphi$ can be represented by a (deterministic) safety/co-safety automata
$\mathcal{A}$, then solving the satisficing problem with temporal goals is
$\mathcal{O}((|V|+|E|)\cdot\mu\cdot n\cdot|\mathcal{A}|)$, where
$|\mathcal{A}|=2^{2^{\mathcal{O}(|\varphi|)}}$.

###### Proof 88

This reduction can be carried out in two steps. In the first step, we reduce
the quantitative graph game $G$ to a reachability/safety game $\mathsf{GA}$ by
means of the comparator automata for DS with integer discount factor, as done
in Section 8.3.2. There is one key difference in constructing $\mathsf{GA}$.
The labelling function of $\mathcal{G}_{\mathsf{T}}$ is extended to states in
$\mathsf{GA}$ so that the label of state $(v,s)$ in $\mathsf{GA}$ is identical
to the label of state $v$ in $\mathcal{G}_{\mathsf{T}}$. In the second step,
we incorporate the temporal goal into the safety/reachability game
$\mathsf{GA}$. For this, first the temporal goal $\varphi$ is converted into
its equivalent deterministic parity automaton (DPA) [87]. Next, take the
product of the game $\mathsf{GA}$ with the DFA by synchronizing the labeling
function of $\mathsf{GA}$ with transitions in the DPA. This follows standard
operations for product constructions. The end result will be a parity game
that is linear in the size of $\mathsf{GA}$ and the DPA for $\varphi$. Recall
from Section 8.3.2, size of $\mathsf{GA}$ is linear in size of $G$, $\mu$ and
$n$. Further, note that the DPA is double exponential in size of $\varphi$.
Therefore, the final product game has size linear in $|V|$ and $\mu$, and
double exponential in $|\varphi|$.

Finally, in the special case where the DPA for $\varphi$ is actually a
deterministic safety/co-safety automaton, the resulting product game can be
solved in time linear in the size of the final product game. The reason behind
this is that the final DPA will be a weak Büchi automata generated from the
union of safety/co-safety automaton from the comparator, and a safety/co-
safety autoamton from the temporal property (Theorem 6.1). Games with weak
Büchi winning conditions can be solved in size linear to the underlying graph
game.

Finally, the proof of correctness is identical to that of Lemma 8.9. ∎

####  8.7 Chapter summary

This work introduced the notion of satisficing for quantitative games with
discounted-sum aggregation function. This is proposed as a decision variant of
the optimization problem. Following a thorough analysis of both problems, we
show that satisficing theoretical, empirical and practical advantages over the
optimization problem. In particular, we show that when the discount factor is
an integer, then the satisficing problem can be solved by automata-based
solutions. Not only is our automata-based solution for satisficing more
efficient than existing solutions for optimization in size of the game graph,
our solutions perform more scalablely and robustly in empirical evaluations.
Furthermore, the practical applicability of quantitative games with temporal
goals can be handled naturally with our automata-based solution for
satisficing as opposed to the non-existence of optimal solutions with temporal
goals. This works yet again presents the benefits of automata-based approaches
in quantitative reasoning over traditional numerical approaches.

While this chapter explored the automata-based solution for an integer
discount factor only, in theory these results could be extended to non-integer
discount factors as well as done in Chapter 7. This may come at the cost of a
small approximation factor, but we can envision solving approximate
satisficing using the approximate comparators for non-integer discount
factors. Of course, the critical question here is to investigate the impact of
the approximation in practical usage.

###  Chapter 9 Conclusion

####  9.1 Concluding remarks

This thesis introduces comparator automata, a novel technique based on
automata for quantitative reasoning. The use of automata for quantitative
reasoning is unique in its own, and infact counterintuitive as far as earlier
work is concerned.

The challenges of lack of genralizability and separation-of-techniques
adversely affect the practical viability of quantitative reasoning, and also
prevent a clear understanding of similarities and dissimilarities across
aggregate functions. The motivation behind the development of comparator
automata is to addresses these challenges. Our investigations on quantitative
inclusion and quantitative games, especially an in-depth examination of the
discounted-sum aggregation function, have established key theoretical results,
improved upon the state-of-the-art in empirical performance, and indicated
promise of approach in applications.

An undercurrent in the progress of comparator-based approaches is that they
have bridged quantitative reasoning to qualitative reasoning. This is in stark
contrast to separation-of-techniques in prior work where the two are
segregated from one another. As demonstrated in this thesis, this digression
will prove to be of immense importance in the long run, since it allows
quantitative reasoning to leverage the advances in the theory, practice and
applications of qualitative reasoning. To the best of our knowledge, this
thesis is the first work to do so.

####  9.2 Future work

##### Theory: Building on the foundations.

$\omega$-regular comparators advocate for the treatment of quantitative
properties as any other $\omega$-regular property. As a result, it is likely
that problems that have found success with an $\omega$-regular property, such
as a temporal logic [77], could do so with $\omega$-regular comparators as
well. The study of quantitative games with imperfect information gives a
glimpse of the hypothesis. One avenue of interest are probabilistic systems.
So far, probabilistic verification and synthesis involves techniques from
linear programming, optimization, solving sets of equalities and inequalities,
and so on. Whether comparator-based approaches can substitute some of these
operations is an open question.

Another line of research is to identify necessary and sufficient conditions
for aggregate functions to have $\omega$-regular comparators. So far,
aggregate functions have been studied on a case-by-case basis. The broadest
classification we have currently is that it is sufficient if an aggregate
function is $\omega$-regular. A better understanding of necessary and
sufficient conditions could contribute to clearer understanding of aggregate
functions.

##### Practice: Scaling further and beyond.

Symbolic methods have been gaining in popularity in qualitative reasoning due
to their scalability and efficiency advantages over explicit methods[35]. In
symbol methods, the state space is typically represented with a logarithmic
number of bits. Following this success, the symbolic reasoning has been
adopted in quantitative reasoning. In most cases, however, the symbolic
structures extend their qualitative counterparts. For example, Binary Decision
Diagram (BDDs) [34] are a popular symbolic data-structure in qualitative
domains. These have been extended to MTBDDs and ADDs to reason about
quantitative properties. Since the development of quantitative symbolic data-
structures and their algorithms are still in nascent stages, relative to their
qualitative counterparts, their full impact is yet to be discovered.

While investigations on quantitative symbolic methods are underway,
comparators offer an alternate perspective. Since comparators are automata,
existing symbolic methods such as BDD, SAT and SMT can be applied. Albeit
promising, only a comparative analysis can reveal the strengths and weakness
of quantitative and comparator-based qualitative symbolic methods, and expose
areas for improvement.

##### Application: White-boxing RL engines.

Owing to the unprecedented rise of machine learning algorithms, reinforcement
learning (RL) has come to the forefront in the design of controllers for
robotics, autonomous vehicles, and several control-related domestic
appliances. Due to their safety-critical nature of these applications, it has
become crucial to white-box the underlying RL algorithms. In response, the
formal methods community has begun looking into the quantitative and
qualitative aspects of RL algorithms.

This direction is particularly exciting for comparator automata. First of all,
several RL engines make use of discounted-sum. Secondly, with comparators we
can combine quantitative and qualitative properties with rigorous guarantees,
as demonstrated in this thesis. Having said that, the capabilities of
comparators will have to be extended further to be applicable to the domain.
For example, RL algorithms have to work under the assumption that the reward
function is known partially only. To address this, comparators will have to be
effective at verification and synthesis under partial information. Similarly,
one could identify numerous ways in which automata-theoretic reasoning could
be of use in the space of white-boxing RL engines.

######

In all, this thesis has introduced a novel framework for the formal analysis
of quantitative systems. The evidence collected throughout the thesis
indicates promise of our approach. The scope in future directions of research
spreads across the wide spectrum from theoretical results to current
applications. In all we believe that this thesis has managed to work at the
tip of automata-based reasoning of quantitative systems. The iceberg is yet to
be discovered.

###  Appendix A Appendix of miscellaneous results

####  A.1 Discounted-sum is an $\omega$-regular function

We use the $\omega$-regular comparator for DS-aggregate function for integer
discount-factor to prove that discounted-sum with integer discount-factors is
an $\omega$-regular aggregate function.

###### Theorem A.1

Let $d>1$ be a non-integer, rational discount-factor. The discounted-sum
aggregate function with discount factor $d$ is not $\omega$-regular.

###### Proof 89

Immediate from Lemma 4.1 and Theorem 4.9.

###### Theorem A.2

Let $d>1$ be an integer discount-factor. The discounted-sum aggregate function
with discount-factor $d$ is $\omega$-regular under base $d$.

###### Proof 90

We define the discounted-sum aggregate function automaton (DS-function
automaton, in short): For integer $\mu>0$, let $\Sigma=\\{0,1,\dots\mu\\}$ be
the input alphabet of DS-function, and $d>1$ be its integer base. Büchi
automaton $\mathcal{A}^{\mu}_{d}$ over alphabet
$\Sigma\times\mathsf{AlphaRep}(d)$ is a DS-function automaton of type
$\Sigma^{\omega}\rightarrow\mathbb{R}$ if for all $A\in\Sigma^{\omega}$,
$(A,\mathsf{rep}(\mathit{DS}({A},{d})),d)\in\mathcal{A}^{\mu}_{d}$. Here we
prove that such a $\mathcal{A}_{d}^{\mu}$ exists.

Let $\mu>0$ be the integer upper-bound. Let $\mathcal{A}^{=}_{d}$ be the DS-
comparator for integer discount-factor $d>1$ for relation $=$. Intersect
$\mathcal{A}^{=}_{d}$ with the Büchi automata consisting of all infinite words
from alphabet $\\{0,1\dots\mu\\}\times\\{0,\dots,d-1\\}$. The resulting
automaton $\mathcal{B}$ accepts $(A,B)$ for $A\in\\{0,\dots,\mu\\}^{\omega}$
and $B\in\\{0,\dots,d-1\\}^{\omega}$ iff
$\mathit{DS}({A},{d})=\mathit{DS}({B},{d})$.

Since all elements of $B$ are bounded by $d-1$, $\mathit{DS}({B},{d})$ can be
represented as an $\omega$-word as follows: Let $B=B[0],B[1]\dots$, then its
$\omega$-word representation in base $d$ is given by
$+\cdot(\mathsf{Int}(\mathit{DS}({B},{d}),d),\mathsf{Frac}(\mathit{DS}({B},{d}),d))$
where $\mathsf{Int}(\mathit{DS}({B},{d}),d)=B[0]\cdot 0^{\omega}$ and
$\mathsf{Frac}(\mathit{DS}({B},{d}),d)=B[1],B[2]\dots$. This transformation of
integer sequence $B$ into its $\omega$-regular word form in base $d$ can be
achieved with a simple transducer $\mathcal{T}$.

Therefore, application of transducer $\mathcal{T}$ to Büchi automaton
$\mathcal{B}$ will result in a Büchi automaton over the alphabet
$\Sigma\times\mathsf{AlphaRep}(d)$ such that for all $A\in\Sigma^{\omega}$ the
automaton accepts $(A,\mathsf{rep}(\mathit{DS}({A},{d}),d))$. This is exactly
the DS-function automaton over input alphabet $\Sigma$ and integer base $d>1$.
Therefore, the discounted-sum aggregate function with integer discount-factors
in $\omega$-regular. ∎

Recall, this proof works only for the discounted-sum aggregate function with
integer discount-factor. In general, there is no known procedure to derive a
function automaton from an $\omega$-regular comparator (Conjecture 4.1).

####  A.2 Connection between discounted-sum and sum

###### Theorem A.3

Let integer $\mu>0$ be the upper-bound. Let $d=1+2^{-k}$ be the discount-
factor for rational-number $k>0$. Let $A$ be a non-empty, bounded, finite,
weight-sequence. Then
$\mod{\mathsf{Sum}({A})-\mathit{DS}({A},{d})}<2^{-k}\cdot\mu\cdot|A|^{2}$

###### Proof 91

We prove the desired bound on the difference between discounted-sum and sum.
Let $n>0$ be the length of $A$, and $\varepsilon=2^{-k}$.

$\displaystyle|{\mathsf{Sum}({A})-\mathit{DS}({A},{d})}|$
$\displaystyle=\mod{\Sigma_{i=0}^{n-1}A_{i}-\frac{A_{i}}{d^{i}}}$
$\displaystyle\leq\Sigma_{i=0}^{n-1}\mod{A_{i}}\cdot\mod{1-\frac{1}{d^{i}}}$
By Cauchy-Schwarz inequality, we get
$\displaystyle\leq\sqrt{(\Sigma_{i=0}^{n-1}A_{i}^{2})\cdot(\Sigma_{i=0}^{n-1}(1-\frac{1}{d^{i}})^{2})}$
$\displaystyle\text{ Since }A\text{ is bounded by }\mu$
$\displaystyle\leq\sqrt{n\cdot\mu^{2}\cdot(\Sigma_{i=0}^{n-1}(1-\frac{1}{d^{i}})^{2})}=\sqrt{n\cdot\mu^{2}\cdot(\Sigma_{i=0}^{n-1}(1-\frac{1}{(1+\varepsilon)^{i}})^{2})}$
$\displaystyle\leq\sqrt{n\cdot\mu^{2}\cdot(\Sigma_{i=0}^{n-1}(1-\frac{1}{(1+\varepsilon)^{(\frac{1}{\varepsilon})\cdot\varepsilon\cdot
i}})^{2})}$ $\displaystyle\text{ Since }(1+x)^{\frac{1}{x}}<e^{x}\text{, for
all }0<x\leq 1$
$\displaystyle<\sqrt{n\cdot\mu^{2}\cdot(\Sigma_{i=0}^{n-1}(1-\frac{1}{e^{\varepsilon\cdot
i}})^{2})}$
$\displaystyle\leq\sqrt{n\cdot\mu^{2}\cdot(\Sigma_{i=0}^{n-1}(1-e^{-\varepsilon\cdot
i})^{2})}$ $\displaystyle\leq\sqrt{n\cdot\mu^{2}\cdot
n\cdot(1-e^{-\varepsilon\cdot n})^{2})}\text{ as }i<n$ $\displaystyle\text{
Since }1-x<e^{-x}\text{ holds for all }x>0$
$\displaystyle<\sqrt{n\cdot\mu^{2}\cdot n\cdot(\varepsilon\cdot
n)^{2})}=\varepsilon\cdot\mu\cdot n^{2}$

∎

The bound above is simply an upper bound. It will be good to tighten the bound
to $\mathcal{O}(\varepsilon\cdot\mu\cdot n)$.

### References

  * [1] Satisficing.  https://en.wikipedia.org/wiki/Satisficing.
  * [2] GLPK.  https://www.gnu.org/software/glpk/.
  * [3] GMP.  https://gmplib.org/.
  * [4] GOAL.  http://goal.im.ntu.edu.tw/wiki/.
  * [5] Rabit-Reduce.  http://www.languageinclusion.org/.
  * [6] P. A Abdulla, Y. Chen, L. Clemente, L. Holík, Chih-Duo Hong, R. Mayr, and T. Vojnar.  Simulation subsumption in ramsey-based büchi automata universality and inclusion testing.  In Proc. of CAV, pages 132–147. Springer, 2010.
  * [7] Parosh Aziz Abdulla, Yu-Fang Chen, Lorenzo Clemente, Lukás Holík, Chih-Duo Hong, Richard Mayr, and Tomas Vojnar.  Advanced ramsey-based büchi automata inclusion testing.  In Proc. of CONCUR, volume 11, pages 187–202. Springer, 2011.
  * [8] Dilip Abreu.  On the theory of infinitely repeated games with discounting.  Econometrica, pages 383–396, 1988.
  * [9] Umair Z Ahmed, Sumit Gulwani, and Amey Karkare.  Automatically generating problems and solutions for natural deduction.  In Proc. of IJCAI, 2013.
  * [10] S. Akiyama, C. Frougny, and J. Sakarovitch.  On the representation of numbers in a rational base.  Proc. of Word, pages 47–64, 2005.
  * [11] S. Almagor, U. Boker, and O. Kupferman.  Whatś decidable about weighted automata?  In Proc. of ATVA, pages 482–491. Springer, 2011.
  * [12] Shaull Almagor, Udi Boker, and Orna Kupferman.  Formalizing and reasoning about quality.  In In Proc. of ICALP, pages 15–27. Springer, 2013.
  * [13] B. Alpern and F. B. Schneider.  Recognizing safety and liveness.  Distributed computing, 2(3):117–126, 1987.
  * [14] R. Alur and K. Mamouras.  An introduction to the streamqre language.  Dependable Software Systems Engineering, 50:1, 2017.
  * [15] Rajeev Alur, Aldric Degorre, Oded Maler, and Gera Weiss.  On omega-languages defined by mean-payoff conditions.  In Proc. of FOSSACS, pages 333–347. Springer, 2009.
  * [16] Benjamin Aminof, Orna Kupferman, and Robby Lampert.  Reasoning about online algorithms with weighted automata.  Transactions on Algorithms, 6(2):28, 2010.
  * [17] Garrett Andersen and Vincent Conitzer.  Fast equilibrium computation for infinitely repeated games.  In Proc. of AAAI, pages 53–59, 2013.
  * [18] D. Andersson.  An improved algorithm for discounted payoff games.  In ESSLLI Student Session, pages 91–98, 2006.
  * [19] C. Baier.  Probabilistic model checking.  In Dependable Software Systems Engineering, pages 1–23. 2016.
  * [20] Christel Baier, Luca de Alfaro, Vojtěch Forejt, and Marta Kwiatkowska.  Model checking probabilistic systems.  In Handbook of Model Checking, pages 963–999. Springer, 2018.
  * [21] Christel Baier, Joost-Pieter Katoen, et al.  Principles of model checking.  MIT press Cambridge, 2008.
  * [22] Teodora Baluta, Shiqi Shen, Shweta Shinde, Kuldeep S Meel, and Prateek Saxena.  Quantitative verification of neural networks and its security applications.  arXiv preprint arXiv:1906.10395, 2019.
  * [23] S. Bansal.  Algorithmic analysis of regular repeated games.  Master’s thesis, Rice University, 2016.
  * [24] S. Bansal, S. Chaudhuri, and M. Y. Vardi.  Automata vs linear-programming discounted-sum inclusion.  In Proc. of CAV, 2018.
  * [25] S. Bansal, S. Chaudhuri, and M. Y. Vardi.  Comparator automata in quantitative verification.  In Proc. of FOSSACS, 2018.
  * [26] S. Bansal, S. Chaudhuri, and M. Y. Vardi.  Comparator automata in quantitative verification (full version).  CoRR, abs/1812.06569, 2018.
  * [27] S. Bansal, Y. Li, L.M. Tabajara, and M. Y. Vardi.  Hybrid compositional reasoning for reactive synthesis from finite-horizon specifications.  In Proc. of AAAI, 2020.
  * [28] S. Bansal and M. Y. Vardi.  Safety and co-safety comparator automata for discounted-sum inclusion.  In Proc. of CAV, 2019.
  * [29] Roderick Bloem, Krishnendu Chatterjee, Thomas A Henzinger, and Barbara Jobstmann.  Better quality in synthesis through quantitative objectives.  In Proc. of CAV, pages 140–156. Springer, 2009.
  * [30] Roderick Bloem, Krishnendu Chatterjee, and Barbara Jobstmann.  Graph games and reactive synthesis.  In Handbook of Model Checking, pages 921–962. Springer, 2018.
  * [31] U. Boker and T. A. Henzinger.  Exact and approximate determinization of discounted-sum automata.  LMCS, 10(1), 2014.
  * [32] U. Boker, T. A. Henzinger, and J. Otop.  The target discounted-sum problem.  In Proc. of LICS, pages 750–761, 2015.
  * [33] Lubos Brim, Jakub Chaloupka, Laurent Doyen, Raffaella Gentilini, and Jean-François Raskin.  Faster algorithms for mean-payoff games.  Formal methods in system design, 38(2):97–118, 2011.
  * [34] R. E. Bryant.  Graph-based algorithms for boolean function manipulation.  Computers, IEEE Transactions on, 100(8):677–691, 1986.
  * [35] Jerry R Burch, Edmund M Clarke, Kenneth L McMillan, David L Dill, and Lain-Jinn Hwang.  Symbolic model checking: 1020 states and beyond.  Information and computation, 98(2):142–170, 1992.
  * [36] Alberto Camacho, Jorge A Baier, Christian Muise, and Sheila A McIlraith.  Finite LTL synthesis as planning.  In ICAPS, pages 29–38. AAAI Press, 2018.
  * [37] A. Chakrabarti, K. Chatterjee, T.A. Henzinger, O. Kupferman, and R. Majumdar.  Verifying quantitative properties using bound functions.  In Advanced Research Working Conference on Correct Hardware Design and Verification Methods, pages 50–64. Springer, 2005.
  * [38] K. Chatterjee, L. Doyen, and T. A. Henzinger.  Expressiveness and closure properties for quantitative languages.  In Proc. of LICS, pages 199–208. IEEE, 2009.
  * [39] K. Chatterjee, L. Doyen, and T. A. Henzinger.  Quantitative languages.  Transactions on Computational Logic, 11(4):23, 2010.
  * [40] Krishnendu Chatterjee, Thomas A Henzinger, and Marcin Jurdzinski.  Mean-payoff parity games.  In Proc. of LICS, pages 178–187. IEEE, 2005.
  * [41] Krishnendu Chatterjee, Thomas A Henzinger, Jan Otop, and Yaron Velner.  Quantitative fair simulation games.  Information and Computation, 254:143–166, 2017.
  * [42] Swarat Chaudhuri, Sriram Sankaranarayanan, and Moshe Y. Vardi.  Regular real analysis.  In Proc. of LICS, pages 509–518, 2013.
  * [43] David Clark, Sebastian Hunt, and Pasquale Malacaria.  A static analysis for quantifying information flow in a simple imperative language.  Journal of Computer Security, 15(3):321–371, 2007.
  * [44] Edmund M. Clarke, E Allen Emerson, and A Prasad Sistla.  Automatic verification of finite-state concurrent systems using temporal logic specifications.  ACM Transactions on Programming Languages and Systems (TOPLAS), 8(2):244–263, 1986.
  * [45] Rina S Cohen and Arie Y Gold.  Theory of $\omega$-languages: Characterizations of $\omega$-context-free languages.  Journal of Computer and System Sciences, 15(2):169–184, 1977.
  * [46] L. De Alfaro, M. Faella, T.A. Henzinger, R. Majumdar, and M. Stoelinga.  Model checking discounted temporal properties.  In Proc. of TACAS, pages 77–92. Springer, 2004.
  * [47] L. De Alfaro, M. Faella, and M Stoelinga.  Linear and branching metrics for quantitative transition systems.  In In Proc. of ICALP, pages 97–109. Springer, 2004.
  * [48] L. De Alfaro, T.A. Henzinger, and R. Majumdar.  Discounting the future in systems theory.  In ICALP, pages 1022–1037. Springer, 2003.
  * [49] T.L. Dean and M.S. Boddy.  An analysis of time-dependent planning.  In Proc. of AAAI, volume 88, pages 49–54, 1988.
  * [50] Aldric Degorre, Laurent Doyen, Raffaella Gentilini, Jean-François Raskin, and Szymon Toruńczyk.  Energy and mean-payoff games with imperfect information.  In International Workshop on Computer Science Logic, pages 260–274. Springer, 2010.
  * [51] Laurent Doyen and Jean-François Raskin.  Antichain algorithms for finite automata.  In Proc. of TACAS, pages 2–22. Springer, 2010.
  * [52] Manfred Droste, Werner Kuich, and Heiko Vogler.  Handbook of weighted automata.  Springer, 2009.
  * [53] Loris D’Antoni, Roopsha Samanta, and Rishabh Singh.  Qlose: Program repair with quantitative objectives.  In Proc. of CAV, pages 383–401. Springer, 2016.
  * [54] Rüdiger Ehlers.  Minimising deterministic büchi automata precisely using sat solving.  In International Conference on SAT, pages 326–332. Springer, 2010\.
  * [55] Emmanuel Filiot, Raffaella Gentilini, and Jean-François Raskin.  Quantitative languages defined by functional automata.  In Proc. of CONCUR, pages 132–146. Springer, 2012.
  * [56] Bernd Finkbeiner, Christopher Hahn, and Hazem Torfah.  Model checking quantitative hyperproperties.  In Proc. of CAV, pages 144–163. Springer, 2018.
  * [57] Thomas Dueholm Hansen, Peter Bro Miltersen, and Uri Zwick.  Strategy iteration is strongly polynomial for 2-player turn-based stochastic games with a constant discount factor.  Journal of the ACM (JACM), 60(1):1–16, 2013.
  * [58] K. He, M. Lahijanian, L.E. Kavraki, and M.Y. Vardi.  Reactive synthesis for finite tasks under resource constraints.  In Intelligent Robots and Systems (IROS), 2017 IEEE/RSJ International Conference on, pages 5326–5332. IEEE, 2017.
  * [59] John E Hopcroft and Jeffrey D Ullman.  Formal languages and their relation to automata.  1969\.
  * [60] L. Hu, Q.and D’Antoni.  Syntax-guided synthesis with quantitative syntactic objectives.  In Proc. of CAV, pages 386–403. Springer, 2018.
  * [61] R. M. Karp.  A characterization of the minimum cycle mean in a digraph.  Discrete mathematics, 23(3):309–311, 1978.
  * [62] Daniel Krob.  The equality problem for rational series with multiplicities in the tropical semiring is undecidable.  In International Colloquium on Automata, Languages, and Programming, pages 101–112. Springer, 1992.
  * [63] O. Kupferman and M. Y. Vardi.  Model checking of safety properties.  In Proc. of CAV, pages 172–183. Springer, 1999.
  * [64] O. Kupferman and M. Y. Vardi.  Weak alternating automata are not that weak.  Transactions on Computational Logic, 2(3):408–429, 2001.
  * [65] Orna Kupfermant and Moshe Y Vardit.  Synthesis with incomplete informatio.  In Advances in temporal logic, pages 109–127. Springer, 2000.
  * [66] M. Kwiatkowska.  Quantitative verification: Models, techniques and tools.  In Proc. 6th joint meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering (ESEC/FSE), pages 449–458. ACM Press, September 2007.
  * [67] M. Kwiatkowska, G. Norman, and D. Parker.  Probabilistic symbolic model checking with PRISM: A hybrid approach.  International Journal on Software Tools for Technology Transfer (STTT), 6(2):128–142, 2004.
  * [68] Marta Kwiatkowska, Gethin Norman, and David Parker.  Advances and challenges of probabilistic model checking.  In 2010 48th Annual Allerton Conference on Communication, Control, and Computing (Allerton), pages 1691–1698. IEEE, 2010.
  * [69] M. Lahijanian, S. Almagor, D. Fried, L.E. Kavraki, and M.Y. Vardi.  This time the robot settles for a cost: A quantitative approach to temporal logic planning with partial satisfaction.  In AAAI, pages 3664–3671, 2015.
  * [70] Christof Löding.  Efficient minimization of deterministic weak $\omega$-automata.  volume 79, pages 105–109. Elsevier, 2001.
  * [71] R. Mayr and L. Clemente.  Advanced automata minimization.  ACM SIGPLAN Notices, 48(1):63–74, 2013.
  * [72] M. Mohri.  Weighted automata algorithms.  In Handbook of weighted automata, pages 213–254. Springer, 2009\.
  * [73] Mehryar Mohri, Fernando Pereira, and Michael Riley.  Weighted finite-state transducers in speech recognition.  Computer Speech & Language, 16(1):69–88, 2002.
  * [74] Anil Nerode.  Linear automaton transformations.  Proceedings of the American Mathematical Society, 9(4):541–544, 1958.
  * [75] M.J. Osborne and A. Rubinstein.  A course in game theory.  MIT press, 1994.
  * [76] D. Parker.  Implementation of Symbolic Model Checking for Probabilistic Systems.  PhD thesis, University of Birmingham, 2002.
  * [77] Amir Pnueli.  The temporal logic of programs.  In Proc. of FOCS, pages 46–57. IEEE, 1977.
  * [78] M.L. Puterman.  Markov decision processes.  Handbooks in operations research and management science, 2:331–434, 1990.
  * [79] Walter Rudin.  Principles of mathematical analysis, volume 3.  McGraw-Hill New York, 1964.
  * [80] S. Safra.  On the complexity of $\omega$-automata.  In Proc. of FOCS, pages 319–327. IEEE, 1988.
  * [81] Walter J Savitch.  Relationships between nondeterministic and deterministic tape complexities.  Journal of Computer and System Sciences, 4(2):177–192, 1970.
  * [82] Sanjit A Seshia, Ankush Desai, Tommaso Dreossi, Daniel J Fremont, Shromona Ghosh, Edward Kim, Sumukh Shivakumar, Marcell Vazquez-Chanlatte, and Xiangyu Yue.  Formal specification for deep neural networks.  In Proc. of ATVA, pages 20–34. Springer, 2018.
  * [83] Lloyd S Shapley.  Stochastic games.  Proceedings of the National Academy of Sciences of the United States of America, 39(10):1095, 1953.
  * [84] Rishabh Singh, Sumit Gulwani, and Armando Solar-Lezama.  Automated feedback generation for introductory programming assignments.  In Proceedings of the 34th ACM SIGPLAN conference on Programming language design and implementation, pages 15–26, 2013.
  * [85] R.S. Sutton and A.G. Barto.  Introduction to reinforcement learning, volume 135.  MIT press Cambridge, 1998.
  * [86] D. Tabakov and M. Y. Vardi.  Experimental evaluation of classical automata constructions.  In Proc. of LPAR, pages 396–411. Springer, 2005.
  * [87] W. Thomas, T. Wilke, et al.  Automata, logics, and infinite games: A guide to current research, volume 2500.  Springer Science & Business Media, 2002.
  * [88] M. Y Vardi.  The büchi complementation saga.  In Annual Symposium on Theoretical Aspects of Computer Science, pages 12–22. Springer, 2007.
  * [89] Moshe Y Vardi and Pierre Wolper.  An automata-theoretic approach to automatic program verification.  In 1st Symposium in Logic in Computer Science (LICS). IEEE Computer Society, 1986.
  * [90] Amol Wakankar, Paritosh K Pandya, and Raj Mohan Matteplackel.  Dcsynth: Guided reactive synthesis with soft requirements.  In Working Conference on Verified Software: Theories, Tools, and Experiments, pages 124–142. Springer, 2019.
  * [91] Min Wen, Rüdiger Ehlers, and Ufuk Topcu.  Correct-by-synthesis reinforcement learning with temporal logic constraints.  In 2015 IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS), pages 4983–4990. IEEE, 2015.
  * [92] S. Zhu, L. M. Tabajara, J. Li, G. Pu, and M. Y Vardi.  A symbolic approach to safety ltl synthesis.  In Haifa Verification Conference, pages 147–162. Springer, 2017\.
  * [93] Uri Zwick and Mike Paterson.  The complexity of mean payoff games on graphs.  Theoretical Computer Science, 158(1):343–359, 1996.


# Modulational instability of dust-ion-acoustic mode and associated rogue
waves in a non-extensive plasma medium

N. K. Tamanna∗,1, J. Akter∗∗,1, N. A. Chowdhury†,2, and A. A. Mamun‡,1,3
1Department of Physics, Jahangirnagar University, Savar, Dhaka-1342,
Bangladesh
2Plasma Physics Division, Atomic Energy Centre, Dhaka-1000, Bangladesh
3Wazed miah science research centre, Jahangirnagar University, Savar,
Dhaka-1342, Bangladesh
e-mail<EMAIL_ADDRESS><EMAIL_ADDRESS>
<EMAIL_ADDRESS><EMAIL_ADDRESS>
###### Abstract

The modulational instability of dust-ion-acoustic (DIA) mode and associated
rogue waves in a three component dusty plasma system (containing inertial warm
ion and negatively charged dust fluids along with inertialess $q$-distributed
electrons) has been theoretically investigated. A nonlinear Schrödinger
equation (NLSE) has been derived by employing the reductive perturbation
method. It is observed that the dusty plasma system under consideration
supports the fast and slow DIA modes, and that the dispersion and nonlinear
coefficients of the NLSE determine the parametric regimes not only for the
modulationally stable and unstable fast DIA mode, but also for the formation
of the DIA rogue waves. The parametric regimes for the modulational
instability of the fast DIA mode, and the criterion for the formation of the
DIA rogue waves have been found to be significantly modified by the effects of
the relevant plasma parameters, particularly, mass and charge state of ion and
dust species, number density of the plasma species, and non-extensive
parameter $q$, etc. It is found that the modulationally stable parametric
regime decreases (increases) with the increase in the value of positive
(negative) $q$. The numerical analysis has also shown that the nonlinearity as
well as the amplitude and width of the rogue waves increases (decreases) with
the mass of positive ion (negative dust grains) while decreases (increases)
with the charge state of the positive ion (negative dust). The applications of
our present work in space (viz., Earth ionosphere, magnetosphere, molecular
clouds, interstellar medium, cometary tails, and planetary rings, etc.) and
laboratory plasmas have been pinpointed.

###### keywords:

NLSE , Modulational instability , Dust-ion-acoustic waves , Rogue waves.

††journal: “Heliyon”

##  1 Introduction

The presence of highly charged massive dust grains in a three component dusty
plasma medium (DPM) along with electron and ion in space plasmas (viz., Earth
ionosphere [1], asteroid zones [2], magnetosphere [1], protostellar disks [2],
molecular clouds [2], interstellar medium [1], cometary tails [2], and
planetary rings [1], etc.) as well as laboratory plasmas [3, 4, 5] not only
change the dynamics of the plasma medium but also change the characteristic of
the various kinds of nonlinear electrostatic disturbance, viz., dust-acoustic
(DA) waves (DAWs) [6, 7, 8], DA solitary waves (DASWs) [6], DA shock waves
(DASHWs) [6, 7], DA double layers (DADLs) [8], dust-ion-acoustic (DIA) waves
(DIAWs) [1, 2], DIA solitary waves (DIASWs) [1, 2], DIA shock waves (DIASHWs),
DIA double layers (DIADLs), DIA cnoidal waves (DIACWs), and has also
mesmerized many plasma physicists to examine the propagation of nonlinear
electrostatic perturbation.

A number of authors have considered non-extensive $q$-distribution in
describing non-equilibrium plasma species (due to the existence of long range
interactions like gravitational and coulomb interactions) in the long tail
space environments such as asteroid zones [9, 10, 11, 12, 13, 14, 15, 16],
Earth ionosphere [14, 15, 16], and interstellar medium [14, 15, 16], etc. In
the $q$-distribution, the parameter $q$ describes the non-extensivity of the
species, and the species are to be considered super-extensive species for the
limit $q<1$ while the species are to be considered sub-extensive species for
the limit $q>1$ [14, 15, 16, 17]. El-Labany et al. [1] examined DIA multi-
solitons in three components DPM. Sahu and Tribeche [6] investigated the
nonlinear properties of the DASWs and DASHWs in presence of the non-extensive
plasma species. Akter et al. [15] theoretically and numerically analyzed the
nonlinear propagation of the ion-acoustic waves in a plasma having non-
extensive plasma species, and reported that the saturation of the curve for
the low and high frequency is totally depend on the non-extensive parameter of
the plasma species. Bacha et al. [16] considered inertial ions, inertialess
electrons, and immobile dust grains to study DIASWs in a three components DPM,
and found that the profile becomes narrower with $q$ for sub-extensive limit
of $q$ while wider with $q$ for super-extensive limit of $q$.

The nonlinear Schrödinger equation (NLSE) [18, 19, 20, 21, 22, 23], which can
solve the puzzle of nature, and associated rogue waves (RWs) are the most
interesting theory in plasma physics, and are employed by a number of authors
to investigate the modulational instability (MI) of the DAWs [24, 25, 26] and
DIAWs [27, 28] in nonlinear and dispersive plasma medium. Moslem et al. [25]
considered inertial massive dust grains and inertialess non-extensive
electrons and ions to analyze numerically the condition of the MI of DAWs in
presence of non-extensive plasma species, and observed that the critical wave
number $k_{c}$ increases or decreases according to the sign and magnitude of
the $q$. Bains et al. [26] demonstrated the MI of the DAWs in a plasma having
non-extensive electrons and ions. Pakzad et al. [28] studied the stability
criterion of the DIAWs in a three component DPM by considering inertial ions,
inertialess electrons and immobile massive dust grains.

In DAWs, the moment of inertia is provided by the dust grains and restoring
force is provided by the thermal pressure of the ions and electrons. On the
other hand in DIAWs, the moment of inertia is provided by the ions and
restoring force is provided by the thermal pressure of the electrons in
presence of immobile dust grains. The mass and charge of the dust grains are
considerably larger than the ions while the mass and charge of the ion are
considerably larger than the electron. It may be noted here that in the DIAWs,
if anyone consider the pressure term of the ions then it is important to be
considered the moment of inertia of the ions along with the dust grains in
presence of inertialess electrons. This means that the consideration of the
pressure term of the ions highly contributes to the moment of inertia along
with inertial dust grains to generate DIAWs in a DPM having inertialess
electrons. In the present work, we are interested to investigate the nonlinear
propagation of DIA RWs (DIARWs) in which the moment of inertia is provided by
the inertial warm ions and negatively charged dust grains and the restoring
force is provided by the thermal pressure of the inertialess electrons in a
three component DPM by using the standard NLSE.

##  2 Model Equations

We consider a three component DPM comprising of inertial positively charged
warm ion (charge $q_{i}=Z_{i}e$ and mass $m_{i}$) and inertial negatively
charged dust grains (charge $q_{d}=-Z_{d}e$ and mass $m_{d}$) as well as
inertialess non-extensive electron (charge $q_{e}=-e$; mass $m_{e}$); where
$Z_{i}$ ($Z_{d}$) is the number of protons (electrons) residing onto the ion
(dust grains) surface, and $e$ is the magnitude of the charge of an electron.
Overall, the charge neutrality condition for our plasma model can be written
as $Z_{i}n_{i0}=Z_{d}n_{d0}+n_{e0}$. Now, the normalized governing equations
of the DIAWs can be written as

$\displaystyle\frac{\partial n_{d}}{\partial t}+\frac{\partial}{\partial
x}(n_{d}u_{d})=0,$ (1) $\displaystyle\frac{\partial u_{d}}{\partial
t}+u_{d}\frac{\partial u_{d}}{\partial
x}=\alpha_{1}\frac{\partial\phi}{\partial x},$ (2)
$\displaystyle\frac{\partial n_{i}}{\partial t}+\frac{\partial}{\partial
x}(n_{i}u_{i})=0,$ (3) $\displaystyle\frac{\partial u_{i}}{\partial
t}+u_{i}\frac{\partial u_{i}}{\partial x}+\alpha_{2}n_{i}\frac{\partial
n_{i}}{\partial x}=-\frac{\partial\phi}{\partial x},$ (4)
$\displaystyle\frac{\partial^{2}\phi}{\partial
x^{2}}+n_{i}=\alpha_{3}n_{e}+(1-\alpha_{3})n_{d},$ (5)

where $n_{d}$ $(n_{i})$ is the dust (ion) number density normalized by its
equilibrium value $n_{d0}$ $(n_{i0})$; $u_{d}$ $(u_{i})$ is the dust (ion)
fluid speed normalized by the ion-acoustic wave speed
$C_{i}=(Z_{i}k_{B}T_{e}/m_{i})^{1/2}$ with $T_{e}$ being the non-extensive
electron temperature, and $k_{B}$ being the Boltzmann constant; $\phi$ is the
electrostatic wave potential normalized by $k_{B}T_{e}/e$; the time and space
variables are normalized by
${\omega^{-1}_{pi}}=(m_{i}/4\pi{Z_{i}}^{2}e^{2}n_{i0})^{1/2}$ and
$\lambda_{Di}=(k_{B}T_{e}/4\pi Z_{i}e^{2}n_{i0})^{1/2}$, respectively. The
pressure term of the ion is recognized as
$P_{i}=P_{i0}(N_{i}/n_{i0})^{\gamma}$ with $P_{i0}=n_{i0}k_{B}T_{i}$ being the
equilibrium pressure of the ion, and $T_{i}$ being the temperature of warm
ion, and $\gamma=(N+2)/N$ (where $N$ is the degree of freedom and for one-
dimensional case $N=1$, then $\gamma=3$). Other plasma parameters are
$\alpha_{1}=\mu\nu$, $\mu=m_{i}/m_{d}$, $\nu=Z_{d}/Z_{i}$,
$\alpha_{2}=3T_{i}/Z_{i}T_{e}$, and $\alpha_{3}=n_{e0}/Z_{i}n_{i0}$, etc. Now,
the expression for the number density of non-extensive electrons following the
non-extensive distribution [15, 16] can be written as

$\displaystyle n_{e}=\left[1+(q-1)\phi\right]^{\frac{(q+1)}{2(q-1)}},\ $ (6)

where the parameter $q$ (known as entropic index) quantifies the degree of
non-extensivity. Now, by substituting Eq. (6) into Eq. (5), and expanding up
to third order of $\phi$, we get

$\displaystyle\frac{\partial^{2}\phi}{\partial
x^{2}}+n_{i}=\alpha_{3}+(1-\alpha_{3})n_{d}+M_{1}\phi+M_{2}\phi^{2}+M_{3}\phi^{3}+\cdot\cdot\cdot,$
(7)

where

$\displaystyle M_{1}=\alpha_{3}(1+q)/2,$ $\displaystyle
M_{2}=\alpha_{3}(1+q)(3-q)/8,$ $\displaystyle
M_{3}=\alpha_{3}(1+q)(q-3)(3q-5)/48.\ $

It may be noted here that the terms containing $M_{1}$, $M_{2}$, and $M_{3}$
in the right hand side of Eq. (7) are the contribution of $q$-distributed
electrons.

##  3 Derivation of NLSE

To study the MI of the DIAWs, we want to derive the NLSE by employing the
reductive perturbation method, and for that case, first we can write the
stretched co-ordinates in the following form [24, 25, 26, 27, 28]

$\displaystyle\xi={\epsilon}(x-v_{g}t),$ (8)
$\displaystyle\tau={\epsilon}^{2}t,$ (9)

where $v_{g}$ is the group speed and $\epsilon$ is a small parameter. Then we
can write the dependent variables [24, 25, 26, 27, 28] as

$\displaystyle
n_{d}=1+\sum_{m=1}^{\infty}\epsilon^{m}\sum_{l=-\infty}^{\infty}n_{dl}^{(m)}(\xi,\tau)~{}\mbox{exp}[il(kx-\omega
t)],$ (10) $\displaystyle
u_{d}=\sum_{m=1}^{\infty}\epsilon^{m}\sum_{l=-\infty}^{\infty}u_{dl}^{(m)}(\xi,\tau)~{}\mbox{exp}[il(kx-\omega
t)],$ (11) $\displaystyle
n_{i}=1+\sum_{m=1}^{\infty}\epsilon^{m}\sum_{l=-\infty}^{\infty}n_{il}^{(m)}(\xi,\tau)~{}\mbox{exp}[il(kx-\omega
t)],$ (12) $\displaystyle
u_{i}=\sum_{m=1}^{\infty}\epsilon^{m}\sum_{l=-\infty}^{\infty}u_{il}^{(m)}(\xi,\tau)~{}\mbox{exp}[il(kx-\omega
t)],$ (13)
$\displaystyle\phi=\sum_{m=1}^{\infty}\epsilon^{m}\sum_{l=-\infty}^{\infty}\phi_{l}^{(m)}(\xi,\tau)~{}\mbox{exp}[il(kx-\omega
t)],$ (14)

where $k$ and $\omega$ are real variables representing the carrier wave number
and frequency, respectively. The derivative operators in the above equations
are treated as follows:

$\displaystyle\frac{\partial}{\partial x}\rightarrow\frac{\partial}{\partial
x}+\epsilon\frac{\partial}{\partial\xi},$ (15)
$\displaystyle\frac{\partial}{\partial t}\rightarrow\frac{\partial}{\partial
t}-\epsilon
v_{g}\frac{\partial}{\partial\xi}+\epsilon^{2}\frac{\partial}{\partial\tau}.$
(16)

Now, by substituting Eqs. (8)-(16) into Eqs. (1)-(4), and (7), and collecting
the terms containing $\epsilon$, the first order ($m=1$ with $l=1$) reduced
equations can be written as

$\displaystyle
n_{d1}^{(1)}=-\frac{k^{2}\alpha_{1}}{\omega^{2}}\phi_{1}^{(1)},$ (17)
$\displaystyle u_{d1}^{(1)}=-\frac{k\alpha_{1}}{\omega}\phi_{1}^{(1)},$ (18)
$\displaystyle
n_{i1}^{(1)}=\frac{k^{2}}{\omega^{2}-\alpha_{2}k^{2}}\phi_{1}^{(1)},$ (19)
$\displaystyle u_{i1}^{(1)}=\frac{\omega
k}{\omega^{2}-\alpha_{2}k^{2}}\phi_{1}^{(1)},$ (20) $\displaystyle
n_{i1}^{(1)}=k^{2}\phi_{1}^{(1)}+M_{1}\phi_{1}^{(1)}+(1-\alpha_{3})n_{d1}^{(1)},\
$ (21)

these relations provide the dispersion relation of DIAWs

$\displaystyle\omega^{2}=\frac{k^{2}D_{1}\pm
k^{2}\sqrt{D_{1}^{2}-4D_{2}D_{3}}}{2D_{2}},\ $ (22)

where
$D_{1}=1+\alpha_{1}-\alpha_{1}\alpha_{3}+\alpha_{2}k^{2}+\alpha_{2}M_{1}$,
$D_{2}=k^{2}+M_{1}$, and
$D_{3}=\alpha_{1}\alpha_{2}-\alpha_{1}\alpha_{2}\alpha_{3}$. In Eq. (22), to
get real and positive values of $\omega$, the condition
$D_{1}^{2}>4D_{2}D_{3}$ should be satisfied. The positive and negative signs
in Eq. (22) corresponds to the fast ($\omega_{f}$) and slow ($\omega_{s}$) DIA
modes. The fast DIA mode corresponds to the case in which both inertial dust
and ion components oscillate in phase with the inertialess electrons. On the
other hand, the slow DIA mode corresponds to the case in which only one of the
inertial components oscillates in phase with inertialess electrons, but the
other inertial component oscillates in anti-phase with them [34]. The second-
order ($m=2$ with $l=1$) equations are given by

$\displaystyle
n_{d1}^{(2)}=-\frac{k^{2}\alpha_{1}}{\omega^{2}}\phi_{1}^{(2)}-\frac{2ik\alpha_{1}(v_{g}k-\omega)}{\omega^{3}}\frac{\partial\phi_{1}^{(1)}}{\partial\xi},$
(23) $\displaystyle
u_{d1}^{(2)}=-\frac{k\alpha_{1}}{\omega}\phi_{1}^{(2)}-\frac{i\alpha_{1}(v_{g}k-\omega)}{\omega^{2}}\frac{\partial\phi_{1}^{(1)}}{\partial\xi},$
(24) $\displaystyle
n_{i1}^{(2)}=\frac{k^{2}}{\omega^{2}-\alpha_{2}k^{2}}\phi_{1}^{(2)}+\frac{2i\omega
k(v_{g}k-\omega)}{(\omega^{2}-\alpha_{2}k^{2})^{2}}\frac{\partial\phi_{1}^{(1)}}{\partial\xi},$
(25) $\displaystyle u_{i1}^{(2)}=\frac{\omega
k}{\omega^{2}-\alpha_{2}k^{2}}\phi_{1}^{(2)}+\frac{i(v_{g}k-\omega)(\omega^{2}+\alpha_{2}k^{2})}{i(\omega^{2}-\alpha_{2}k^{2})^{2}}\frac{\partial\phi_{1}^{(1)}}{\partial\xi},\
$ (26)

with the compatibility condition

$\displaystyle
v_{g}=\frac{\alpha_{1}\alpha_{3}\omega^{5}-\alpha_{1}\omega^{5}+2\alpha_{1}\alpha_{2}\omega^{3}k^{2}-D_{4}}{\alpha_{1}\alpha_{3}\omega^{4}k-\alpha_{1}\omega^{4}k+2\alpha_{1}\alpha_{2}\omega^{2}k^{3}-D_{5}},$
(27)

where

$\displaystyle
D_{4}=\alpha_{1}\alpha_{2}^{2}k^{4}\omega-\alpha_{1}\alpha_{2}^{2}\alpha_{3}k^{4}\omega-\alpha_{2}^{2}\omega^{3}k^{4}$
$\displaystyle-\omega^{7}+2\alpha_{2}\omega^{5}k^{2}+\omega^{5}+2\alpha_{1}\alpha_{2}\alpha_{3}\omega^{3}k^{2},$
$\displaystyle
D_{5}=2\alpha_{1}\alpha_{2}\alpha_{3}\omega^{2}k^{3}+\alpha_{1}\alpha_{2}^{2}k^{5}-\alpha_{1}\alpha_{2}^{2}\alpha_{3}k^{5}+\omega^{4}k.\
$

The coefficients of $\epsilon$ for $m=2$ with $l=2$ provide the second order
harmonic amplitudes which are found to be proportional to
$|\phi_{1}^{(1)}|^{2}$

$\displaystyle n_{d2}^{(2)}=M_{4}|\phi_{1}^{(1)}|^{2},$ (28) $\displaystyle
u_{d2}^{(2)}=M_{5}|\phi_{1}^{(1)}|^{2},$ (29) $\displaystyle
n_{i2}^{(2)}=M_{6}|\phi_{1}^{(1)}|^{2},$ (30) $\displaystyle
u_{i2}^{(2)}=M_{7}|\phi_{1}^{(1)}|^{2},$ (31)
$\displaystyle\phi_{2}^{(2)}=M_{8}|\phi_{1}^{(1)}|^{2},\ $ (32)

where

$\displaystyle
M_{4}=\frac{3k^{4}\alpha_{1}^{2}-2k^{2}\alpha_{1}\omega^{2}M_{8}}{2\omega^{4}},$
$\displaystyle
M_{5}=\frac{k^{3}\alpha_{1}^{2}-2k\omega^{2}\alpha_{1}M_{8}}{2\omega^{3}},$
$\displaystyle
M_{6}=\frac{2k^{2}M_{8}(\omega^{2}-\alpha_{2}k^{2})^{2}+k^{4}(\alpha_{2}k^{2}+3\omega^{2})}{2(\omega^{2}-\alpha_{2}k^{2})^{3}},$
$\displaystyle M_{7}=\frac{\omega^{3}M_{6}-\alpha_{2}\omega k^{2}M_{6}-\omega
k^{4}}{k(\omega^{2}-\alpha_{2}k^{2})^{2}},$ $\displaystyle
M_{8}=\frac{D_{6}-2\omega^{4}M_{2}(\omega^{2}-\alpha_{2}k^{2})^{3}}{6k^{2}\omega^{4}(\omega^{2}-\alpha_{2}k^{2})^{3}},\
$

where
$D_{6}=k^{4}\omega^{4}(3\omega^{2}+\alpha_{2}k^{2})-3\alpha_{1}^{2}k^{4}(\omega^{2}-\alpha_{2}k^{2})^{3}$.
Now, we consider the expression for ($m=3$ with $l=0$) and ($m=2$ with $l=0$),
which leads the zeroth harmonic modes. Thus, we obtain

$\displaystyle n_{d0}^{(2)}=M_{9}|\phi_{1}^{(1)}|^{2},$ (33) $\displaystyle
u_{d0}^{(2)}=M_{10}|\phi_{1}^{(1)}|^{2},$ (34) $\displaystyle
n_{i0}^{(2)}=M_{11}|\phi_{1}^{(1)}|^{2},$ (35) $\displaystyle
u_{i0}^{(2)}=M_{12}|\phi_{1}^{(1)}|^{2},$ (36)
$\displaystyle\phi_{0}^{(2)}=M_{13}|\phi_{1}^{(1)}|^{2},\ $ (37)

where

$\displaystyle
M_{9}=\frac{2v_{g}\alpha_{1}^{2}k^{3}+\alpha_{1}^{2}k^{2}\omega-\alpha_{1}\omega^{3}M_{13}}{v_{g}^{2}\omega^{3}},$
$\displaystyle
M_{10}=\frac{\alpha_{1}^{2}k^{2}-\alpha_{1}\omega^{2}M_{13}}{v_{g}\omega^{2}},$
$\displaystyle
M_{11}=-\frac{M_{13}(\omega^{2}-\alpha_{2}k^{2})^{2}+k^{2}(\alpha_{2}k^{2}+\omega^{2}+2\omega
v_{g}k)}{(\alpha_{2}-v_{g}^{2})(\omega^{2}-\alpha_{2}k^{2})^{2}},$
$\displaystyle
M_{12}=\frac{v_{g}M_{11}(\omega^{2}-\alpha_{2}k^{2})^{2}-2\omega
k^{3}}{(\omega^{2}-\alpha_{2}k^{2})^{2}},$ $\displaystyle
M_{13}=\frac{2M_{2}v_{g}^{2}\omega^{3}(\alpha_{2}-v_{g}^{2})(\omega^{2}-\alpha_{2}k^{2})^{2}+D_{7}}{\omega^{3}\times
D_{8}\times(\omega^{2}-\alpha_{2}k^{2})^{2}},\ $

where

$\displaystyle
D_{7}=(1-\alpha_{3})(\alpha_{2}-v_{g}^{2})(\omega^{2}-\alpha_{2}k^{2})(\alpha_{1}^{2}k^{2}\omega+2v_{g}\alpha_{1}^{2}k^{3})$
$\displaystyle+k^{2}v_{g}^{2}\omega^{3}(\alpha_{2}k^{2}+\omega^{2}+2\omega
v_{g}k),$ $\displaystyle
D_{8}=[\alpha_{1}(1-\alpha_{3})(\alpha_{2}-v_{g}^{2})-v_{g}^{2}-v_{g}^{2}M_{1}(\alpha_{2}-v_{g}^{2})].\
$

Finally, the third harmonic modes ($m=3$) and ($l=1$) with the help of Eqs.
(17)$-$(37), give a set of equations, which can be reduced to the following
NLSE:

$\displaystyle
i\frac{\partial\Phi}{\partial\tau}+P\frac{\partial^{2}\Phi}{\partial\xi^{2}}+Q|\Phi|^{2}\Phi=0,$
(38)

where $\Phi=\phi_{1}^{(1)}$ for simplicity. In Eq. (38), $P$ is the dispersive
coefficient which can be written as

$\displaystyle P=\frac{\omega^{4}(\omega-
v_{g}k)^{2}(\omega^{2}+\alpha_{2}k^{2})-D_{9}}{\omega(\omega^{2}-\alpha_{2}k^{2})[2\omega^{4}k^{2}+2\alpha_{1}k^{2}(1-\alpha_{3})(\omega^{2}-\alpha_{2}k^{2})^{2}]},\
$

where

$\displaystyle D_{9}=2\omega^{5}kv_{g}(\omega-v_{g}k)(\omega
v_{g}-\alpha_{2}k)+\omega^{4}(\omega^{2}-\alpha_{2}k^{2})^{3}$
$\displaystyle+\alpha_{1}(1-\alpha_{3})(\omega-
v_{g}k)(3v_{g}k-\omega)(\omega^{2}-\alpha_{2}k^{2})^{3},\ $

and also $Q$ is the nonlinear coefficient which can be written as

$\displaystyle
Q=\frac{\omega^{3}(\omega^{2}-\alpha_{2}k^{2})^{2}[3M_{3}+2M_{2}(M_{8}+M_{13})]-D_{10}}{2\omega^{4}k^{2}+2\alpha_{1}k^{2}(1-\alpha_{3})(\omega^{2}-\alpha_{2}k^{2})^{2}},\
$

where

$\displaystyle D_{10}=\alpha_{1}\omega
k^{2}(1-\alpha_{3})(\omega^{2}-\alpha_{2}k^{2})^{2}(M_{4}+M_{9})$
$\displaystyle+2\alpha_{1}k^{3}(1-\alpha_{3})(\omega^{2}-\alpha_{2}k^{2})^{2}(M_{5}+M_{10})$
$\displaystyle+\omega^{3}(\omega^{2}k^{2}+\alpha_{2}k^{4})(M_{6}+M_{11})+2\omega^{4}k^{3}(M_{7}+M_{12}).\
$

The space and time evolution of the DIAWs in DPM are directly governed by the
coefficients $P$ and $Q$, and indirectly governed by different plasma
parameters such as $\mu$, $\nu$, $\alpha_{2}$, $\alpha_{3}$, $q$, and $k$.
Thus, these plasma parameters significantly affect the stability conditions of
the DIAWs.

##  4 Modulational instability and Rogue waves

The stable and unstable parametric regimes of the DIAWs are organized by the
sign of $P$ and $Q$ of the standard NLSE (38) [24, 25, 26, 27, 28, 29, 30, 31,
32]. When $P$ and $Q$ have same sign (i.e., $P/Q>0$), the evolution of the
DIAWs amplitude is modulationally unstable in presence of the external
perturbations. On the other hand, when $P$ and $Q$ have opposite sign (i.e.,
$P/Q<0$), the DIAWs are modulationally stable in presence of the external
perturbations. The plot of $P/Q$ against $k$ yields stable and unstable
parametric regimes of the DIAWs. The point, at which transition of $P/Q$ curve
intersect with $k$-axis, is known as threshold or critical wave number $k$
($=k_{c}$). The governing equation of the highly energetic DIARWs in the
unstable parametric regime (i.e., $P/Q>0$) can be written as [33]

$\displaystyle\Phi(\xi,\tau)=\sqrt{\frac{2P}{Q}}\Big{[}\frac{4+16i\tau
P}{1+4\xi^{2}+16\tau^{2}P^{2}}-1\Big{]}\mbox{exp}(2i\tau P),$ (39)

Figure 1: Plot of $P/Q$ vs $k$ for different values of positive $q$ when other
plasma parameters are $\mu=2\times 10^{-6}$, $\nu=3\times 10^{5}$,
$\alpha_{2}=0.5$, $\alpha_{3}=0.2$, and $\omega_{f}$.

Figure 2: Plot of $P/Q$ vs $k$ for different values of negative $q$ when other
plasma parameters are $\mu=2\times 10^{-6}$, $\nu=3\times 10^{5}$,
$\alpha_{2}=0.5$, $\alpha_{3}=0.2$, and $\omega_{f}$. Figure 3: Plot of $P/Q$
vs $k$ for different values of positive $\alpha_{3}$ when other plasma
parameters are $q=1.5$ $\mu=2\times 10^{-6}$, $\nu=3\times 10^{5}$,
$\alpha_{2}=0.5$, and $\omega_{f}$. Figure 4: Plot of $Re(\Phi)$ vs $\xi$ for
different values of $\mu$ when $k=0.3$, $\tau=0.0$, $q=1.5$, $\nu=3\times
10^{5}$, $\alpha_{2}=0.5$, $\alpha_{3}=0.2$, and $\omega_{f}$. Figure 5: Plot
of $Re(\Phi)$ vs $\xi$ for different values of $\nu$ when $k=0.3$, $\tau=0.0$,
$q=1.5$, $\mu=2\times 10^{-6}$, $\alpha_{2}=0.5$, $\alpha_{3}=0.2$, and
$\omega_{f}$.

Equation (39) describes that a large amount of wave energy, which causes due
to the nonlinear characteristics of the medium, is localized into a
comparatively small area in space.

##  5 Results and discussion

Now, we would like to numerically analyze the stability conditions of the
DIAWs in presence of the non-extensive electrons. The mass and charge state of
the plasma species even their number density are important factors in
recognizing the stability conditions of the DIAWs in DPM [34, 35, 36, 37, 38,
39]. The mass of the dust grains is comparable to the mass of proton. In
general picture of the DPM, dust grains are massive (millions to billions
times heavier than the protons) and their sizes range from nanometres to
millimetres. Dust grains may be metallic, conducting, or made of ice
particulate. The size and shape of dust grains will be different, unless they
are man-made. The dust grains are millions to billions times heavier than the
protons, and typically, a dust grain acquires one thousand to several hundred
thousand elementary charges [34, 35, 36, 37, 38, 39]. In this article, we
consider three components dusty plasma model having inertial warm positive
ions and negative dust grains, and interialess non-thermal non-extensive
electrons. It may be noted here that in the DIAWs, if anyone consider the
pressure term of the ions then it is important to be considered the moment of
inertia of the ions along with the dust grains in presence of inertialess
electrons. This means that the consideration of the pressure term of the ions
highly contributes to the moment of inertia along with inertial dust grains to
generate DIAWs in a DPM having inertialess electrons. In our present analysis,
we have considered that $m_{d}=10^{6}m_{i}$, $Z_{d}=(10^{3}\thicksim
10^{5})Z_{i}$, and $T_{e}=10T_{i}$.

The detail picture of the non-extensive parameter (for both sub-extensive and
super-extensive limits) in recognizing stable and unstable parametric regimes
of the DIAWs can be observed in Figs. 2 and 2 for $\omega_{f}$ only, and it is
obvious from this two figures that (a) both modulationally stable (i.e.,
$P/Q<0$) and unstable (i.e., $P/Q>0$) parametric regimes of the DIAWs can be
obtained for sub-extensive (i.e., $q>1$) and super-extensive (i.e., $q<1$)
limits of $q$; (b) the $k_{c}$ decreases with the increase in the value of $q$
within the limit of sub-extensive (i.e., $q>1$) but the $k_{c}$ increases with
the increase in the value of $q$ within the limit of super-extensive (i.e.,
$q<1$); (c) so, the direction of the variation of $k_{c}$ totally depends on
the sign of the $q$.

The influence of the charge state of positive ion, and the number density of
the warm ions and electrons on the possible unstable and stable parametric
regimes of DIAWs can be seen from Fig. 3 in which the variation of the $P/Q$
with $k$ for different values of $\alpha_{3}$ is shown when other plasma
parameters are remain constant. It is clear from this figure that (a) when the
parameter $\alpha_{3}$ is $0.1$, $0.2$, and $0.3$, then the corresponding
$k_{c}$ is almost $0.21$, $0.20$, and $0.13$; (b) so, the stable window as
well as the $k_{c}$ decreases with increasing $\alpha_{3}$; (c) the presence
of excess number of non-extensive electrons dictates the DIAWs to be unstable
as well allows to generate DIARWs for small wave number while the presence of
excess number of warm ions dictates the DIAWs to be unstable as well allows to
generate DIARWs for large wave number for a constant value of ion charge state
(via $\alpha_{3}$).

The effects of inertial warm positive ion mass to inertial negatively charged
massive dust grains mass (via $\mu$) on the formation of the DIARWs can be
observed from Fig. 4, and it can be highlighted from this figure that (a) the
increase in the value of $\mu$ does not only cause to change the nonlinearity
of the plasma medium but also causes to increase the amplitude and width of
the DIARWs; (b) physically, the nonlinearity of the plasma medium as well as
the amplitude and width of the DIARWs increases (decreases) with the increase
of positive ion mass (negative dust mass). Figure 5 demonstrates the influence
of the ratio of the charge state of negative dust grains to the charge state
of positive ion in recognizing the shape of the DIARWs in a nonlinear and
dispersive plasma medium (via $\nu$). The amplitude and width of the DIARWs
associated with modulationally unstable parametric regime decreases (due to
the decrease of the nonlinearity of plasma medium) with positive ion charge
state while increases (due to the increase of the nonlinearity of plasma
medium) with negative dust grains charge state (via $\nu$).

##  6 Conclusion

In this paper, we have considered a dusty plasma model having inertial warm
positive ions and negative dust grains, and inertialess non-extensive
electrons to investigate the stability criteria, which determines by the sign
of $P$ and $Q$ of NLSE, of the DIAWs according to the variation of plasma
parameters, and have also observed the formation of DIARWs in the
modulationally unstable parametric regime. The variation of the mass and
charge state of the positive ion and negative dust grains has dictated a
rigourous change in the configuration of DIARWs associated with DIAWs in the
modulationally unstable parametric regime. The results from this brief study
are to be applicable in explaining the formation of nonlinear electrostatic
DIARWs in space (viz., Earth ionosphere [1], asteroid zones [2], magnetosphere
[1], protostellar disks [2], molecular clouds [2], interstellar medium [1],
cometary tails [2], and planetary rings [1], etc.) and laboratory plasmas.

## References

  * [1] S. K. El-Labany, et al., Phys. Plasmas 25, 013701 (2018).
  * [2] P. Eslami, et al., IEEE Trans. Plasma Sci.  41, 3589 (2013).
  * [3] P. Bandyopadhyay, et al., Phys. Rev. Lett. 101, 065006 (2008).
  * [4] J. Heinrich, et al., Phys. Rev. Lett. 103, 115002 (2009).
  * [5] S. I. Popel, et al., JETP Lett. 74, 362 (2001).
  * [6] B. Sahu and M. Tribeche, Astrophys. Space Sci. 338, 259 (2012).
  * [7] M. Ferdousi, et al., Eur. Phys. J. D 71, 102 (2017).
  * [8] B. Sahu and M. Tribeche, Astrophys. Space Sci. 341, 573 (2012).
  * [9] N. A. Chowdhury, et al., Chaos 27, 093105 (2017).
  * [10] N. A. Chowdhury, et al., Phys. plasmas 24, 113701 (2017).
  * [11] M. H. Rahman, et al., Chinese J. Phys. 56, 2061 (2018).
  * [12] M. H. Rahman, et al., Phys. Plasmas 25, 102118 (2018).
  * [13] N. A. Chowdhury, et al., Vacuum 147, 31 (2018).
  * [14] C. Tsallis, J. Stat. Phys. 52, 479 (1988).
  * [15] N. Akter, et al., J. Plasma Phys. 81, 905810518 (2015).
  * [16] M. Bacha, et al., Phys. Rev. E 85, 056413 (2012).
  * [17] A. Renyi, Acta Math. Acad. Sci. Hung. 6, 285 (1955).
  * [18] N. A. Chowdhury, et al., Contrib. Plasma Phys. 58, 870 (2018).
  * [19] N. Ahmed, et al., Chaos 28, 123107 (2018).
  * [20] R. K. Shikha, et al., Eur. Phys. J. D 73, 177 (2019).
  * [21] S. Jahan, et al., Commun. Theor. Phys. 71, 327 (2019).
  * [22] M. Hassan, et al., Commun. Theor. Phys. 71, 1017 (2019).
  * [23] N. A. Chowdhury, et al., Plasma Phys. Rep. 45, 459 (2019).
  * [24] I. Kourakis and P.K. Shukla, Phys. Plasmas. 10, 3459 (2003).
  * [25] W. M. Moslem, et al., Phys. Rev. E 84, 066402 (2011).
  * [26] A. S. Bains, et al., Astrophys. Space Sci. 343, 621 (2013).
  * [27] X. Jukui and L. He, Phys. Plasmas 10, (2003) 339.
  * [28] H. R. Pakzad, et al., Astrophys. Space Sci. 353, 543 (2014).
  * [29] C. Li, et al., Smart Mater. Struct. 20, 0152023 (2011).
  * [30] C. Li, et al., Compos. Part B-Eng. 116, 153 (2017).
  * [31] J. J. Liu, et al., J. Vib. Control 23, 3327 (2016).
  * [32] J. J. Liu, et al., Appl. Math. Model 45, 65 (2017).
  * [33] A. Ankiewicz, et al., Phys. Lett. A 373, 3997 (2009).
  * [34] E. Saberiana, et al., Plasma Phys. Rep. 43, 83 (2017).
  * [35] R. L. Merlino, J. Plasma Phys. 80, 773 (2014).
  * [36] P. K. Shukla and B. Eliasson, Phys. Rev. E 86, 046402 (2012).
  * [37] A. A. Mamun and P.K. Shukla, Phys. Scripta T98, 107 (2002).
  * [38] M. Shalaby, et al., Phys. Plasmas 16, 123706 (2009).
  * [39] P. K. Shukla and A.A. Mamun, Introduction to Dusty Plasma Physics (IOP, London, 2002).