# Reduction of Register Pushdown Systems with Freshness Property
to Pushdown Systems in LTL Model Checking111Funding: This work was partially
supported by JSPS KAKENHI Grant Numbers JP19H04083 and JP20K20625.

Yoshiaki Takata  Ryoma Senda  Hiroyuki Seki  Kochi University of Technology,
Tosayamada, Kami City, Kochi 782–8502, Japan  Nagoya University, Furo-cho,
Chikusa, Nagoya 464–8601, Japan

###### Abstract

Pushdown systems (PDS) are known as an abstract model of recursive programs,
and model checking methods for PDS have been studied. Register PDS (RPDS) are
PDS augmented by registers to deal with data values from an infinite domain in
a restricted way. A linear temporal logic (LTL) model checking method for RPDS
with regular valuations has been proposed; however, the method requires the
register automata (RA) used for representing a regular valuation to be
backward-deterministic. This paper proposes another approach to the same
problem, in which the model checking problem for RPDS is reduced to that
problem for PDS by constructing a PDS bisimulation equivalent to a given RPDS.
The construction in the proposed method is simpler than the previous model
checking method and does not require RAs deterministic or backward-
deterministic, and the bisimulation equivalence clearly guarantees the
correctness of this reduction. On the other hand, the proposed method requires
every RPDS (and RA) to have the freshness property, in which whenever the RPDS
updates a register with a data value not stored in any register or the stack
top, the value should be fresh. This paper also shows that this model checking
problem with regular valuations defined by general RA is undecidable, and thus
the freshness constraint is essential in the proposed method.

###### keywords:

model checking, register pushdown system, regular valuation

##  1 Introduction

A pushdown system (PDS) is a pushdown automaton without input and is well
known as an abstract model of recursive programs [1, 2]. The model checking
problem for a PDS $\mathcal{P}$, i.e. testing whether all runs of
$\mathcal{P}$ conforms to a given specification $\varphi$, has been studied
for various logics such as linear temporal logic (LTL) and branching-time
temporal logic [1, 2, 3]. In [4], the LTL model checking of PDS with regular
valuations was investigated and shown to be decidable. A valuation is a
function that labels each configuration in a run with a subset of atomic
propositions. A regular valuation is a valuation that labels each
configuration $c$ of a PDS with atomic propositions depending on whether the
stack contents in $c$ match a given regular pattern.

Although PDS is a natural model of recursive programs, it cannot deal with
data values directly. Register automata (RA) were introduced as an extension
of finite automata (FA) by adding the capability of dealing with data values
in a restricted way [5]. RA has attracted attention as a formal model of
navigational queries concerning data values to structured data such as XML
documents [6]. RA has also been considered as a formal model of software
systems with unbounded resources in e.g. runtime verification [7] and reactive
synthesis [8]. Similarly to extending FA to RA, PDS were extended to pushdown
register systems (PDRS) [9] and register pushdown systems (RPDS) [10], both of
them are equivalent each other, and the reachability problem for them has been
shown to be EXPTIME-complete.

In previous work [11], we have investigated the LTL model checking problem
with regular valuations for RPDS and proposed a method for solving the
problem. This method is a natural extension of the model checking method for
PDS in [4]. Similarly to the method in [4] that reduces the model checking
problem to the emptiness problem for Büchi pushdown systems, in [11] we
introduced Büchi register pushdown systems (BRPDS) and showed a reduction of
the model checking problem to the emptiness problem for BRPDS. Note that the
regular valuations in [11] were defined in terms of backward-deterministic RA,
in which every configuration has a unique predecessor configuration for each
input data value. This constraint is essential because unlike FA,
determinization is not possible for general RA.

In this paper, we work on the same problem in a different approach. We reduce
the model checking problem for RPDS to that problem for PDS by constructing a
PDS $\mathcal{P}^{\prime}$ bisimulation equivalent [12] to a given RPDS
$\mathcal{P}$. In the same way, we also construct an FA $\mathcal{A}^{\prime}$
bisimulation equivalent to an RA $\mathcal{A}$ used for a regular valuation.
The bisimulation equivalences between $\mathcal{P}$ and $\mathcal{P}^{\prime}$
and between $\mathcal{A}$ and $\mathcal{A}^{\prime}$ guarantee the correctness
of this reduction. The construction of a PDS bisimulation equivalent to an
RPDS is basically the same as the one used in our recent work [13] on reactive
synthesis from specifications given by deterministic register pushdown
automata (DRPDA). In [13], we construct a pushdown automaton (PDA) simulating
a DRPDA for reducing the realizability problem for DRPDA to the same problem
for PDA. The proposed method in this paper is an application of this
construction to the model checking problem, where not only RPDS but also RA
used for a regular valuation can be reduced to models without data values in a
uniform way, and the correctness of the reduction of the model checking
problem can be proved easily based on bisimulation equivalence.

Another feature of the proposed method is that it does not require RA used for
regular valuations to be deterministic or backward-deterministic. However, the
proposed method requires every RPDS (and RA) to have the freshness property
instead, in which whenever the RPDS updates a register with a data value not
stored in any register or the stack top, the value should be fresh, i.e. not
used before. This paper also shows that the LTL model checking problem for
RPDS with regular valuations defined by general RA is undecidable (Theorem 1),
and this fact compels the proposed method to require the freshness property
instead of requiring RA to be deterministic or backward-deterministic.

Advantages of the proposed method are summarized as follows: (i) The
construction in the proposed method is much simpler than the method in [11].
The bisimulation equivalence between an RPDS and a PDS clearly shows the
correctness of the reduction. We have proved this bisimulation equivalence
using a proof assistant software Coq [14]. (ii) By the proposed method, we can
apply existing model checking tools for PDS to solving the model checking
problem for RPDS. (iii) The method does not require RA used for regular
valuations to be deterministic or backward-deterministic, though it requires
the freshness property instead. Showing the undecidability of the model
checking problem in the general case is another contribution of the paper.

The rest of the paper is organized as follows. We define basic notions in
Section 2, RPDS and RA in Section 3, and the LTL model checking problem for
RPDS with regular valuations in Section 4. In Section 4, we also show that
this problem is undecidable in general. In Section 5, we introduce the
freshness property and redefine the semantics of RPDS so that every RPDS has
this property. In Section 6, we show the construction of a PDS bisimulation
equivalent to a given RPDS, which is the main part of the proposed method. We
conclude the paper in Section 7.

##  2 Preliminaries

Let $\mathbb{N}=\\{1,2,\ldots\\}$, $\mathbb{N}_{0}=\\{0\\}\cup\mathbb{N}$, and
$[n]=\\{1,2,\ldots,n\\}$ for $n\in\mathbb{N}$. We assume a countable set $D$
of _data values_. For a given $k\in\mathbb{N}_{0}$, a mapping $\theta:[k]\to
D$ is called an _assignment_ (of data values to $k$ registers). Let
$\Theta_{k}$ be the set of assignments to $k$ registers. Sometimes we consider
an assignment $\theta\in\Theta_{k}$ as the set of assigned data values; e.g.,
$d\in\theta$ means $d=\theta(i)$ for some $i\in[k]$.

For a set $A$, let $A^{*}$ and $A^{\omega}$ be the sets of finite and infinite
words over $A$, respectively. Let $A^{\infty}=A^{*}\cup A^{\omega}$. For a
word $\alpha\in A^{\infty}$, let $\alpha(i)\in A$ be the $i$-th element of
$\alpha$ and $\alpha(i\,{:})=\alpha(i)\alpha(i+1)\ldots$ for $i\geq 0$. Let
snd be the function over pairs that gives the second element of a pair; i.e.,
$\texttt{snd}((a,b))=b$. For a word $w=(a_{0},b_{0})(a_{1},b_{1})\ldots$ over
pairs, let $\texttt{snd}(w)=b_{0}b_{1}\ldots$ .

For a relation $\Rightarrow$, let $\Rightarrow^{*}$ be the reflexive
transitive closure of $\Rightarrow$.

###  2.1 Linear Temporal Logic (LTL)

The definition of LTL formulas we used is the same as [4]. Let $\mathit{At}$
be a finite set of _atomic propositions_ , and let $\Sigma=2^{\mathit{At}}$.
An _LTL formula_ over $\mathit{At}$ is given by the following syntax:

$\varphi::=\texttt{tt}\mid
A\mid\neg\varphi\mid\varphi_{1}\land\varphi_{2}\mid\mathbin{\mathcal{X}}\varphi\mid\varphi_{1}\mathbin{\mathcal{U}}\varphi_{2}$

where $A\in\mathit{At}$. For an infinite word $w\in\Sigma^{\omega}$, the
satisfaction relation $\models$ is defined as follows:

$\displaystyle w$ $\displaystyle\models\texttt{tt},$ $\displaystyle w$
$\displaystyle\models A$ $\displaystyle\iff\ $ $\displaystyle A\in w(0),$
$\displaystyle w$ $\displaystyle\models\neg\varphi$ $\displaystyle\iff\ $
$\displaystyle w\not\models\varphi,$ $\displaystyle w$
$\displaystyle\models\varphi_{1}\land\varphi_{2}$ $\displaystyle\iff\ $
$\displaystyle w\models\varphi_{1}\text{ and }w\models\varphi_{2},$
$\displaystyle w$ $\displaystyle\models\mathbin{\mathcal{X}}\varphi$
$\displaystyle\iff\ $ $\displaystyle w(1\,{:})\models\varphi,$ $\displaystyle
w$ $\displaystyle\models\varphi_{1}\mathbin{\mathcal{U}}\varphi_{2}\ $
$\displaystyle\iff\ $ $\displaystyle\exists j:(w(j\,{:})\models\varphi_{2})$
$\displaystyle{}\land(\forall i<j:w(i\,{:})\models\varphi_{1}).$

We also define $\Diamond\varphi=\texttt{tt}\mathbin{\mathcal{U}}\varphi$ and
$\Box\varphi=\neg\Diamond(\neg\varphi)$.

###  2.2 Pushdown systems and finite automata

For a finite set $\Gamma$, we define the set $\texttt{Com}(\Gamma)$ of
_commands_ over $\Gamma$ as
$\texttt{Com}(\Gamma)=\\{\texttt{pop},\texttt{skip}\\}\cup\\{\texttt{push}(\gamma)\mid\gamma\in\Gamma\\}$.

###### Definition 1

A _pushdown system_ (PDS) $\mathcal{P}$ over a stack alphabet $\Gamma$ is a
pair $(P,\Delta)$, where $P$ is a finite set of _states_ and $\Delta\subseteq
P\times\Gamma\times P\times\texttt{Com}(\Gamma)$ is a set of _transition
rules_. We write an element $(p,\gamma,q,\mathit{com})\in\Delta$ as
$(p,\gamma)\to(q,\mathit{com})$ for readability.

Let $\mathit{ID}_{\mathcal{P}}=P\times\Gamma^{*}$ and call each element of
$\mathit{ID}_{\mathcal{P}}$ an _instantaneous description_ (ID) of
$\mathcal{P}$. The transition relation $\Rightarrow_{\mathcal{P}}$ of
$\mathcal{P}$ is the smallest relation over $\mathit{ID}_{\mathcal{P}}$
satisfying the following inference rule, where $\texttt{upds}^{\prime}(\gamma
v,\mathit{com}^{\prime})=v$, $\gamma v$, or $\gamma^{\prime}\gamma v$ if
$\mathit{com}^{\prime}=\texttt{pop}$, skip, or
$\texttt{push}(\gamma^{\prime})$, respectively.

$\begin{array}[]{l}(p,\gamma)\to(q,\mathit{com}^{\prime})\in\Delta\\\
\hline\cr(p,\gamma
v)\Rightarrow_{\mathcal{P}^{\prime}}(q,\texttt{upds}^{\prime}(\gamma
v,\mathit{com}^{\prime}))\end{array}$

A _run_ of $\mathcal{P}$ is a sequence
$\rho\in\mathit{ID}_{\mathcal{P}}^{\omega}$ such that
$\rho(i)\Rightarrow_{\mathcal{P}}\rho(i+1)$ for $i\geq 0$.

We define nondeterministic finite automata as follows, which is used for
representing a (regular) subset of IDs of some PDS.

###### Definition 2

A _nondeterministic finite automaton_ (NFA) $\mathcal{A}$ over an alphabet
$\Gamma$ is a quadruple $(Q,I,F,\delta)$, where $(Q,\delta)$ is a PDS over
$\Gamma$ where $\delta$ consists of pop rules only, $I\subseteq Q$ is a set of
_initial states_ , and $F\subseteq Q$ is a set of _final states_. We call
$(Q,\delta)$ the _base PDS_ of $\mathcal{A}$. The set
$\mathit{ID}_{\\!\mathcal{A}}$ of IDs and the transition relation of
$\mathcal{A}$ are the same as those of its base PDS. We write the transition
relation of $\mathcal{A}$ as $\vdash_{\mathcal{A}}$. The _language_
$L(\mathcal{A})$ of $\mathcal{A}$ is a subset of
$\mathit{ID}_{\\!\mathcal{A}}$ defined as $L(\mathcal{A})=\\{(p,w)\in
I\times\Gamma^{*}\mid(p,w)\vdash_{\mathcal{A}}^{*}(q,\varepsilon)$ for some
$q\in F\\}$.

When we use an NFA $\mathcal{A}$ for representing a subset of IDs of a PDS
$\mathcal{P}=(P,\Delta)$, we let the set of the initial states of
$\mathcal{A}$ be $P$.

###### Definition 3

For a PDS $\mathcal{P}=(P,\Delta)$, we call a subset
$C\subseteq\mathit{ID}_{\mathcal{P}}$ _regular_ if there exists an NFA
$\mathcal{A}=(Q,P,F,\delta)$ that satisfies $C=L(\mathcal{A})$.

###  2.3 Equivalence relations over registers

Let $\Phi_{k}$ be the set of _equivalence relations_ over the set of $2k+1$
symbols
$X_{k}=\\{\mathtt{x}_{1},\ldots,\mathtt{x}_{k},\allowbreak\mathtt{x}^{\prime}_{1},\ldots,\mathtt{x}^{\prime}_{k},\allowbreak\mathtt{x}_{\texttt{top}}\\}$.
We write $a\equiv_{\phi}b$ and $a\not\equiv_{\phi}b$ to mean $(a,b)\in\phi$
and $(a,b)\notin\phi$, respectively, for $a,b\in X_{k}$ and $\phi\in\Phi_{k}$.
Intuitively, each $\phi\in\Phi_{k}$ represents the equality and inequality
among the data values in the registers and the stack top, as well as the
transfer of the values in the registers between two assignments. Two
assignments $\theta,\theta^{\prime}\in\Theta_{k}$ and a value $d$ at the stack
top satisfy $\phi$, denoted as $(\theta,d,\theta^{\prime})\models\phi$, iff
for $i,j\in[k]$,

$\displaystyle\mathtt{x}_{i}\equiv_{\phi}\mathtt{x}_{j}$
$\displaystyle\Leftrightarrow\theta(i)=\theta(j),$
$\displaystyle\mathtt{x}_{i}\equiv_{\phi}\mathtt{x}_{\texttt{top}}$
$\displaystyle\Leftrightarrow\theta(i)=d,$
$\displaystyle\mathtt{x}_{i}\equiv_{\phi}\mathtt{x}^{\prime}_{j}$
$\displaystyle\Leftrightarrow\theta(i)=\theta^{\prime}(j),\quad$
$\displaystyle\mathtt{x}^{\prime}_{j}\equiv_{\phi}\mathtt{x}_{\texttt{top}}$
$\displaystyle\Leftrightarrow\theta^{\prime}(j)=d,$
$\displaystyle\mathtt{x}^{\prime}_{i}\equiv_{\phi}\mathtt{x}^{\prime}_{j}$
$\displaystyle\Leftrightarrow\theta^{\prime}(i)=\theta^{\prime}(j).$

We will use elements of $\Phi_{k}$ to specify transition rules of a register
pushdown system with $k$ registers ($k$-RPDS), defined in the next section.

Let $\Phi^{\prime}_{k}$ be the set of equivalence relations over the $k$
symbols $\\{\mathtt{x}_{1},\ldots,\mathtt{x}_{k}\\}$. An assignment
$\theta\in\Theta_{k}$ satisfies $\phi^{\prime}\in\Phi^{\prime}_{k}$, denoted
as $\theta\models\phi^{\prime}$, iff for $i,j\in[k]$,
$\mathtt{x}_{i}\equiv_{\phi^{\prime}}\mathtt{x}_{j}\iff\theta(i)=\theta(j)$.
Elements of $\Phi^{\prime}_{k}$ will be used to specify accepting conditions
of a register automaton with $k$ registers ($k$-RA).

Let $\texttt{lat}:\Phi_{k}\to\Phi^{\prime}_{k}$ be the function defined as:
$\forall i,j\in[k]:\mathtt{x}_{i}\equiv_{\texttt{lat}(\phi)}\mathtt{x}_{j}$
iff $\mathtt{x}^{\prime}_{i}\equiv_{\phi}\mathtt{x}^{\prime}_{j}$.

##  3 Register pushdown systems and register automata

###### Definition 4

A _register pushdown system with $k$ registers_ ($k$-RPDS) $\mathcal{P}$ is a
pair $(P,\Delta)$, where $P$ is a finite set of _states_ and $\Delta\subseteq
P\times\Phi_{k}\times P\times\texttt{Com}([k])$ is a set of _transition
rules_. We write an element $(p,\phi,q,\mathit{com})\in\Delta$ as
$(p,\phi)\to(q,\mathit{com})$ for readability.

Let $\mathit{ID}_{\mathcal{P}}=P\times\Theta_{k}\times D^{*}$ and call each
element of $\mathit{ID}_{\mathcal{P}}$ an _instantaneous description_ (ID) of
$\mathcal{P}$. The transition relation $\Rightarrow_{\mathcal{P}}$ of
$\mathcal{P}$ is the smallest relation over $\mathit{ID}_{\mathcal{P}}$
satisfying the following inference rule, where
$\texttt{upds}(du,\theta^{\prime},\mathit{com})=u$, $du$, or
$\theta^{\prime}(j)du$ if $\mathit{com}=\texttt{pop}$, skip, or
$\texttt{push}(j)$, respectively.

$\begin{array}[]{l}(p,\phi)\to(q,\mathit{com})\in\Delta\quad(\theta,d,\theta^{\prime})\models\phi\\\
\hline\cr(p,\theta,du)\Rightarrow_{\mathcal{P}}(q,\theta^{\prime},\texttt{upds}(du,\theta^{\prime},\mathit{com}))\end{array}$

A _run_ of $\mathcal{P}$ is a sequence
$\rho\in\mathit{ID}_{\mathcal{P}}^{\omega}$ such that
$\rho(i)\Rightarrow_{\mathcal{P}}\rho(i+1)$ for $i\geq 0$.

###### Example 1

Let us consider 2-RPDS $\mathcal{P}=(\\{p_{0},p_{1},\allowbreak p_{2}\\}$,
$\\{r_{1},r_{2},r_{3},r_{4},r_{5}\\})$ where

$\displaystyle r_{1}$
$\displaystyle=(p_{0},\phi_{0})\to(p_{1},\texttt{push}(1)),$ $\displaystyle
r_{2}$ $\displaystyle=(p_{1},\phi_{1})\to(p_{1},\texttt{push}(1)),$
$\displaystyle r_{3}$ $\displaystyle=(p_{1},\phi_{1})\to(p_{1},\texttt{pop}),$
$\displaystyle r_{4}$ $\displaystyle=(p_{1},\phi_{2})\to(p_{1},\texttt{pop}),$
$\displaystyle r_{5}$
$\displaystyle=(p_{1},\phi_{3})\to(p_{2},\texttt{push}(2)),$

and $\phi_{0},\ldots,\phi_{3}\in\Phi_{2}$ are defined by the following
quotient sets:

$\displaystyle X_{2}/{\phi_{0}}$
$\displaystyle=\\{\\{\mathtt{x}_{1}\\},\\{\mathtt{x}_{2},\mathtt{x}^{\prime}_{2},\mathtt{x}_{\texttt{top}}\\},\\{\mathtt{x}^{\prime}_{1}\\}\\},$
$\displaystyle X_{2}/{\phi_{1}}$
$\displaystyle=\\{\\{\mathtt{x}_{1},\mathtt{x}_{\texttt{top}}\\},\\{\mathtt{x}_{2},\mathtt{x}^{\prime}_{2}\\},\\{\mathtt{x}^{\prime}_{1}\\}\\},$
$\displaystyle X_{2}/{\phi_{2}}$
$\displaystyle=\\{\\{\mathtt{x}_{1}\\},\\{\mathtt{x}_{2},\mathtt{x}^{\prime}_{2}\\},\\{\mathtt{x}^{\prime}_{1},\mathtt{x}_{\texttt{top}}\\}\\},$
$\displaystyle X_{2}/{\phi_{3}}$
$\displaystyle=\\{\\{\mathtt{x}_{1},\mathtt{x}^{\prime}_{1}\\},\\{\mathtt{x}_{2},\mathtt{x}_{\texttt{top}}\\},\\{\mathtt{x}^{\prime}_{2}\\}\\}.$

In this example, we let $[d_{1},d_{2}]$ for $d_{1},d_{2}\in D$ denote the
assignment $\theta\in\Theta_{2}$ such that $\theta(1)=d_{1}$ and
$\theta(2)=d_{2}$. Let $d_{0},d_{1},\ldots\in D$ represent distinct data
values. Figure 1 shows a transition sequence of $\mathcal{P}$ starting from an
ID $(p_{0},[d_{1},d_{0}],d_{0})$. For example, we can apply $r_{1}$ to this
starting ID and obtain $(p_{1},[d_{2},d_{0}],d_{2}d_{0})$, because $\phi_{0}$
requires that the value of the second register before the transition is the
same as the stack top, the second register is not changed by the transition,
and the value of the first register after the transition is not equal to the
value of any register before the transition.

stateregistersstack$p_{0}$$[d_{1},d_{0}]$$d_{0}$$p_{1}$$[d_{2},d_{0}]$$d_{2}\,d_{0}$$p_{1}$$[d_{3},d_{0}]$$d_{3}\,d_{2}\,d_{0}$$p_{1}$$[d_{4},d_{0}]$$d_{2}\,d_{0}$$p_{1}$$[d_{2},d_{0}]$$d_{0}$$p_{0}$$[d_{2},d_{5}]$$d_{5}\,d_{0}$$\Downarrow\,\phi_{0},\texttt{push}(1)$$\Downarrow\,\phi_{1},\texttt{push}(1)$$\Downarrow\,\phi_{1},\texttt{pop}$$\Downarrow\,\phi_{2},\texttt{pop}$$\Downarrow\,\phi_{3},\texttt{push}(2)$
Figure 1: A transition sequence of $\mathcal{P}$ from
$(p_{0},[d_{1},d_{0}],d_{0})$.

###### Definition 5

A _register automaton with $k$ registers_ ($k$-RA) $\mathcal{A}$ is a
quadruple $(Q,I,\xi,\delta)$, where $(Q,\delta)$ is a $k$-RPDS where $\delta$
consists of pop rules only, $I\subseteq Q$ is a set of _initial states_ , and
$\xi\subseteq Q\times\Phi^{\prime}_{k}$ is a set of _accepting conditions_. We
call $(Q,\delta)$ the _base RPDS_ of $\mathcal{A}$. The set
$\mathit{ID}_{\\!\mathcal{A}}$ of IDs and the transition relation of
$\mathcal{A}$ are the same as those of its base RPDS. We write the transition
relation of $\mathcal{A}$ as $\vdash_{\mathcal{A}}$. Let
$\mathit{Acc}_{\mathcal{A}}=\\{(p,\theta,\varepsilon)\in\mathit{ID}_{\\!\mathcal{A}}\mid$
$\theta\models\psi$ for some $(p,\psi)\in\xi\\}$. The _language_
$L(\mathcal{A})$ of $\mathcal{A}$ is a subset of
$\mathit{ID}_{\\!\mathcal{A}}$ defined as
$L(\mathcal{A})=\\{(p,\theta,w)\in\mathit{ID}_{\\!\mathcal{A}}\mid p\in I$ and
$(p,\theta,w)\vdash_{\mathcal{A}}^{*}(q,\theta^{\prime},\varepsilon)$ for some
$(q,\theta^{\prime},\varepsilon)\in\mathit{Acc}_{\mathcal{A}}\\}$.

We write a transition rule $(q_{1},\phi)\to(q_{2},\texttt{pop})$ of an RA as
$(q_{1},\phi)\to q_{2}$ for readability.

###### Definition 6

For a $k$-RPDS $\mathcal{P}=(P,\Delta)$, we call a subset
$C\subseteq\mathit{ID}_{\mathcal{P}}$ _regular_ if there exists a $k$-RA
$\mathcal{A}=(Q,P,\xi,\delta)$ that satisfies $C=L(\mathcal{A})$.

###### Example 2

Let us consider 2-RA $\mathcal{A}=(\\{p_{1},q_{1},\allowbreak q_{2}\\}$,
$\\{p_{1}\\}$, $\\{(q_{2},\psi)\\}$, $\\{r_{6},\allowbreak r_{7},r_{8}\\})$
where

$\displaystyle r_{6}$ $\displaystyle=(p_{1},\phi_{1})\to q_{1},\quad\ $
$\displaystyle r_{8}$ $\displaystyle=(q_{1},\phi_{3})\to q_{2},$
$\displaystyle r_{7}$ $\displaystyle=(q_{1},\phi_{4})\to q_{1},$

$\phi_{1}$ and $\phi_{3}$ are the same as Example 1, $\phi_{4}\in\Phi_{2}$ is
defined by the quotient set

$\displaystyle X_{2}/{\phi_{4}}$
$\displaystyle=\\{\\{\mathtt{x}_{1},\mathtt{x}^{\prime}_{1}\\},\\{\mathtt{x}_{2},\mathtt{x}^{\prime}_{2}\\},\\{\mathtt{x}_{\texttt{top}}\\}\\},$

and $\psi\in\Phi^{\prime}_{2}$ is the equivalence relation such that
$\mathtt{x}_{1}\not\equiv_{\psi}\mathtt{x}_{2}$. Figure 2 shows a transition
sequence of $\mathcal{A}$ starting from an ID
$(p_{1},[d_{3},d_{0}],d_{3}d_{2}d_{0})$. As shown in the figure,
$(p_{1},[d_{3},d_{0}],d_{3}d_{2}d_{0})\vdash_{\\!\mathcal{A}}^{*}(q_{2},[d_{4},d_{5}],\varepsilon)$.
Since $[d_{4},d_{5}]\models\psi$, $(p_{1},[d_{3},d_{0}],\allowbreak
d_{3}d_{2}d_{0})\in L(\mathcal{A})$.

stateregistersstack$p_{1}$$[d_{3},d_{0}]$$d_{3}\,d_{2}\,d_{0}$$q_{1}$$[d_{4},d_{0}]$$d_{2}\,d_{0}$$q_{1}$$[d_{4},d_{0}]$$d_{0}$$q_{2}$$[d_{4},d_{5}]$$\varepsilon$$\\!\rotatebox[origin={c}]{-90.0}{$\vdash$}\,\,\phi_{1}$$\\!\rotatebox[origin={c}]{-90.0}{$\vdash$}\,\,\phi_{4}$$\\!\rotatebox[origin={c}]{-90.0}{$\vdash$}\,\,\phi_{3}$
Figure 2: A transition sequence of $\mathcal{A}$ starting from an ID
$(p_{1},[d_{3},d_{0}],d_{3}d_{2}d_{0})$.

##  4 LTL model checking problem and valuations

We fix a finite set $\mathit{At}$ of atomic propositions, and let
$\Sigma=2^{\mathit{At}}$.

A _valuation_ for a $k$-RPDS $\mathcal{P}=(P,\Delta)$ is a function
$\Lambda:\mathit{ID}_{\mathcal{P}}\to\Sigma$, which labels each ID of
$\mathcal{P}$ with a subset of atomic propositions. We extend the domain of
$\Lambda$ to $(\mathit{ID}_{\mathcal{P}})^{\infty}$ in the usual way; i.e.,
$\Lambda(c_{0}c_{1}\ldots)=\Lambda(c_{0})\Lambda(c_{1})\ldots$ .

###### Definition 7

The _LTL model checking problem_ for RPDS is defined as:

Instance:

a $k$-RPDS $\mathcal{P}=(P,\Delta)$, an LTL formula $\varphi$ over
$\mathit{At}$, a valuation $\Lambda:\mathit{ID}_{\mathcal{P}}\to\Sigma$, and
an ID $c_{0}\in\mathit{ID}_{\mathcal{P}}$.

Question:

Does every run $\rho\in(\mathit{ID}_{\mathcal{P}})^{\omega}$ of $\mathcal{P}$
with $\rho(0)=c_{0}$ satisfy $\Lambda(\rho)\models\varphi$ ?

In the rest of the paper, we fix a $k$-RPDS $\mathcal{P}=(P,\Delta)$, a
valuation $\Lambda:\mathit{ID}_{\mathcal{P}}\to\Sigma$, and a starting ID
$c_{0}$.

###### Definition 8

We call $\Lambda:\mathit{ID}_{\mathcal{P}}\to\Sigma$ a _regular valuation_ if
the set $\\{c\in\mathit{ID}_{\mathcal{P}}\mid A\in\Lambda(c)\\}$ is regular
for every $A\in\mathit{At}$.

We assume that $\Lambda$ is a regular valuation and a $k$-RA
$\mathcal{A}_{A}=(Q_{A},P,\xi_{A},\delta_{A})$ for each $A\in\mathit{At}$
satisfying $L(\mathcal{A}_{A})=\\{c\in\mathit{ID}_{\mathcal{P}}\mid
A\in\Lambda(c)\\}$ is given.

We also define the model checking problem and regular valuations for PDS in
the same way. It is known that the LTL model checking problem with regular
valuations for PDS is decidable [4, Theorem 3]. The main objective of this
paper is to show a reduction of that problem for RPDS to the one for PDS.

However, that problem for RPDS is undecidable in general, as shown below.

###### Theorem 1

The LTL model checking problem with regular valuations for RPDS is
undecidable.

###### Proof 1

The universality problem for RA stated as follows is known to be undecidable
[15, Theorem 5.1]: _Instance_ : a $k$-RA $\mathcal{A}$, an initial state
$q_{0}$, and an initial assignment $\theta_{0}$. _Question_ : Does
$(q_{0},\theta_{0},w)\in L(\mathcal{A})$ for every $w\in D^{*}$? We can reduce
this problem to the model checking problem with regular valuations for RPDS;
for given $\mathcal{A}$, $q_{0}$, and $\theta_{0}$, we can construct a
$(k+1)$-RPDS $\mathcal{P}$ and a $(k+1)$-RA $\mathcal{A}^{\prime}$ that
satisfy the following: Let $\texttt{\$}\in D$ be an arbitrary data value,
which is used as the stack bottom. $\mathcal{P}$ has $q_{0}$ as its only
state. $\mathcal{P}$ does not alter the first $k$ registers, and in every
state transition, it loads an arbitrary data value to the $(k+1)$-th register
and pushes it into the stack. Therefore, from any starting ID
$(q_{0},\theta,\texttt{\$})$, $\mathcal{P}$ can reach an ID
$(q_{0},\theta^{\prime},w\texttt{\$})$ for every $w\in D^{*}$, where
$\theta^{\prime}(i)=\theta(i)$ for $i\in[k]$. $\mathcal{A}^{\prime}$ is a
modified version of $\mathcal{A}$ that does not use the $(k+1)$-th register
and satisfies for any $\theta^{\prime}_{0}$ with
$\theta^{\prime}_{0}(i)=\theta_{0}(i)$ for $i\in[k]$, $(q_{0},\theta_{0},w)\in
L(\mathcal{A})$ iff $(q_{0},\theta^{\prime}_{0},w\texttt{\$})\in
L(\mathcal{A}^{\prime})$. Let $\mathit{At}=\\{A\\}$ and $\Lambda$ be the
regular valuation such that $\Lambda(c)=\\{A\\}$ if $c\in
L(\mathcal{A}^{\prime})$ and $\Lambda(c)=\emptyset$ otherwise. Let
$c_{0}=(q_{0},\theta^{\prime}_{0},\texttt{\$})$ for some $\theta^{\prime}_{0}$
with $\theta^{\prime}_{0}(i)=\theta_{0}(i)$ for $i\in[k]$. Let $\varphi=\Box
A$. Then, the answer to the model checking problem on $\mathcal{P}$,
$\Lambda$, $\varphi$, and $c_{0}$ coincides with the answer to the
universality problem on $\mathcal{A}$, $q_{0}$, and $\theta_{0}$.

##  5 Freshness property

The method proposed in this paper requires that the transition relation
$\Rightarrow_{\mathcal{P}}$ of every $k$-RPDS (including $k$-RA) $\mathcal{P}$
should have the _freshness property_ stated as follows: If
$(p,\theta,du)\Rightarrow_{\mathcal{P}}(q,\theta^{\prime},u^{\prime})$ by a
rule $r$ and the updated assignment $\theta^{\prime}$ contains a data value
$d^{\prime}$ not in $\theta\cup\\{d\\}$, then $d^{\prime}$ must be “fresh”;
i.e., $d^{\prime}$ should have never appeared in the computation from a
starting configuration to $(p,\theta,du)$. Since the set $D$ of data values is
infinite, such a fresh data value $d^{\prime}$ always exists whenever the rule
$r$ can be applied to $(p,\theta,du)$ above.

To define the freshness property formally, we slightly modify the semantics of
$k$-RPDS so that each stack cell keeps the assignment at the time when the
cell is pushed into the stack. The assignments “saved” in the stack are used
only for choosing a fresh data value and do not affect the behavior of an RPDS
in other ways. We redefine the set $\mathit{ID}_{\mathcal{P}}$ of IDs of a
$k$-RPDS $\mathcal{P}=(P,\Delta)$ as

$\mathit{ID}_{\mathcal{P}}=P\times\Theta_{k}\times(D\times\Theta_{k})^{*}$

and the transition relation $\Rightarrow_{\mathcal{P}}$ as follows:

$\begin{array}[]{l}(p,\phi)\to(q,\mathit{com})\in\Delta\quad(\theta,d,\theta^{\prime})\models\phi\\\
\texttt{frsp}(\theta^{\prime};d,\theta;\theta^{\prime\prime}\texttt{snd}(u))\\\
\hline\cr(p,\theta,(d,\theta^{\prime\prime})u)\Rightarrow_{\mathcal{P}}(q,\theta^{\prime},\texttt{upds}((d,\theta^{\prime\prime})u,\theta^{\prime},\mathit{com}))\end{array}$

where
$\texttt{upds}((d,\theta^{\prime\prime})u,\theta^{\prime},\mathit{com})=u$,
$(d,\theta^{\prime\prime})u$, or
$(\theta^{\prime}(j),\theta^{\prime})(d,\theta^{\prime\prime})u$ if
$\mathit{com}=\texttt{pop}$, skip, or $\texttt{push}(j)$, respectively, and
$\texttt{frsp}(\theta^{\prime};d,\theta;\theta_{n}\ldots\theta_{1})$ is a
predicate that is true iff for each $i\in[k]$,
$\theta^{\prime}(i)\in\theta\cup\\{d\\}$ or
$\theta^{\prime}(i)\notin\theta_{1}\cup\ldots\cup\theta_{n}$. That is, each
value $\theta^{\prime}(i)$ in the updated assignment is either the value
$\theta(l)$ of some register, the value $d$ at the stack top, or a fresh value
that has not appeared in $\theta_{n}\ldots\theta_{1}$.

We say an ID
$(p,\theta_{n},(d_{n-1},\theta_{n-1})\allowbreak\ldots(d_{1},\theta_{1}))\in\mathit{ID}_{\mathcal{P}}$
is _proper_ if for $\forall i,j,l\in[n]$ with $i<j\leq l$,
$d_{i},\theta_{i},\theta_{j},\theta_{l}$ satisfy $d_{i}\in\theta_{i}$ and
$\bigl{(}\forall m\in[k]:\theta_{i}(m)\notin\theta_{j}$ implies
$\theta_{i}(m)\notin\theta_{l}\bigr{)}$ and $\bigl{(}d_{i}\notin\theta_{j}$
implies $d_{i}\notin\theta_{l}\bigr{)}$. Under the assumption of the freshness
property, every ID reachable from a proper starting ID is also proper. We
assume the starting ID $c_{0}$ given to the model checking problem is proper.

Note that RA with the freshness property is similar to session automata (SA)
[16], which is a special case of fresh-register automata (FRA) [17]. An SA has
the same structure as RA but requires an input data value to be either a value
stored in some register or a value not used before. On the other hand, RA in
this paper can update registers with data values not given as input but chosen
arbitrary from values satisfying a guard condition, and the freshness
constraint is imposed only on values not given as input.

##  6 PDS simulating RPDS

###  6.1 Bisimulation relation between an RPDS and a PDS

The bisimulation equivalence [12] is a basic notion to capture the equivalence
of behaviors of two state transition systems. We review the definition of the
notion in this subsection. We will show the construction of a PDS bisimulation
equivalent to a given RPDS in Section 6.3.

###### Definition 9

For an RPDS $\mathcal{P}=(P,\Delta)$ and a PDS
$\mathcal{P}^{\prime}=(P^{\prime},\Delta^{\prime})$, we call a relation
$R\subseteq\mathit{ID}_{\mathcal{P}}\times\mathit{ID}_{\mathcal{P}^{\prime}}$
a _bisimulation relation_ between $\mathcal{P}$ and $\mathcal{P}^{\prime}$ if
$R$ satisfies the following:

  1. (1)

For every $c_{1},c_{2}\in\mathit{ID}_{\mathcal{P}}$ and
$c^{\prime}_{1}\in\mathit{ID}_{\mathcal{P}^{\prime}}$, if
$c_{1}\Rightarrow_{\mathcal{P}}c_{2}$ and $(c_{1},c^{\prime}_{1})\in R$, then
$\exists
c^{\prime}_{2}\in\mathit{ID}_{\mathcal{P}^{\prime}}:c^{\prime}_{1}\Rightarrow_{\mathcal{P}^{\prime}}c^{\prime}_{2}$
and $(c_{2},c^{\prime}_{2})\in R$.

  2. (2)

For every $c_{1}\in\mathit{ID}_{\mathcal{P}}$ and
$c^{\prime}_{1},c^{\prime}_{2}\in\mathit{ID}_{\mathcal{P}^{\prime}}$, if
$c^{\prime}_{1}\Rightarrow_{\mathcal{P}^{\prime}}c^{\prime}_{2}$ and
$(c_{1},c^{\prime}_{1})\in R$, then $\exists
c_{2}\in\mathit{ID}_{\mathcal{P}}:c_{1}\Rightarrow_{\mathcal{P}}c_{2}$ and
$(c_{2},c^{\prime}_{2})\in R$.

For an RA $\mathcal{A}=(Q,I,\xi,\delta)$ and an NFA
$\mathcal{A}^{\prime}=(Q^{\prime},I^{\prime},F,\delta^{\prime})$, we call a
relation
$R\subseteq\mathit{ID}_{\\!\mathcal{A}}\times\mathit{ID}_{\\!\mathcal{A}^{\prime}}$
a bisimulation relation between $\mathcal{A}$ and $\mathcal{A}^{\prime}$ if
$R$ is a bisimulation relation between $(Q,\delta)$ and
$(Q^{\prime},\delta^{\prime})$ and also satisfies:

  1. (3)

If $(c,c^{\prime})\in R$, then $c\in\mathit{Acc}_{\mathcal{A}}$ iff
$c^{\prime}=(q,\varepsilon)$ and $q\in F$.

An RPDS $\mathcal{P}$ and a PDS $\mathcal{P}^{\prime}$ (or an RA $\mathcal{A}$
and an NFA $\mathcal{A}^{\prime}$) are _bisimulation equivalent_ if there is a
bisimulation relation between them.

By definition, we obtain the following propositions.

###### Proposition 2

If there is a bisimulation relation $R$ between an RA $\mathcal{A}$ and an NFA
$\mathcal{A}^{\prime}$, then for any pair $(c,c^{\prime})\in R$, $c\in
L(\mathcal{A})$ iff $c^{\prime}\in L(\mathcal{A}^{\prime})$.

###### Proposition 3

Let $\mathcal{P}$ be an RPDS and $\mathcal{P}^{\prime}$ be a PDS. Let
$\Lambda:\mathit{ID}_{\mathcal{P}}\to\Sigma$ and
$\Lambda^{\prime}:\mathit{ID}_{\mathcal{P}^{\prime}}\to\Sigma$ be their
valuations and $c_{0}\in\mathit{ID}_{\mathcal{P}}$ and
$c^{\prime}_{0}\in\mathit{ID}_{\mathcal{P}^{\prime}}$ be their IDs. If there
is a bisimulation relation $R$ between $\mathcal{P}$ and
$\mathcal{P}^{\prime}$ such that $(c_{0},c^{\prime}_{0})\in R$ and
$\Lambda(c)=\Lambda^{\prime}(c^{\prime})$ for every pair $(c,c^{\prime})\in
R$, then:

  1. (i)

For every run $\rho$ of $\mathcal{P}$ with $\rho(0)=c_{0}$, there exists a run
$\rho^{\prime}$ of $\mathcal{P}^{\prime}$ with
$\rho^{\prime}(0)=c^{\prime}_{0}$ such that
$\Lambda(\rho)=\Lambda^{\prime}(\rho^{\prime})$.

  2. (ii)

For every run $\rho^{\prime}$ of $\mathcal{P}^{\prime}$ with
$\rho^{\prime}(0)=c^{\prime}_{0}$, there exists a run $\rho$ of $\mathcal{P}$
with $\rho(0)=c_{0}$ such that
$\Lambda(\rho)=\Lambda^{\prime}(\rho^{\prime})$.

###  6.2 Composition of equivalence relations

Let $\odot$ and $\odot_{\mathtt{T}}$ be the binary predicates over $\Phi_{k}$
defined as:

$\displaystyle\phi_{1}\odot\phi_{2}\ $ $\displaystyle:\Leftrightarrow\
\bigl{(}\mathtt{x}^{\prime}_{i}\equiv_{\phi_{1}}\mathtt{x}^{\prime}_{j}\text{
iff }\mathtt{x}_{i}\equiv_{\phi_{2}}\mathtt{x}_{j}\ \text{for
}i,j\in[k]\bigr{)}.$ $\displaystyle\phi_{1}\odot_{\mathtt{T}}\phi_{2}\ $
$\displaystyle:\Leftrightarrow\ \bigl{(}\phi_{1}\odot\phi_{2}\ \text{and}$
$\displaystyle\quad\;(\mathtt{x}^{\prime}_{i}\equiv_{\phi_{1}}\mathtt{x}_{\texttt{top}}\text{
iff }\mathtt{x}_{i}\equiv_{\phi_{2}}\mathtt{x}_{\texttt{top}}\ \text{for
}i\in[k])\bigr{)}.$

Intuitively, $\phi_{1}\odot\phi_{2}$ represents the _composability_ of
$\phi_{1}$ and $\phi_{2}$; for $\phi_{1}$ and $\phi_{2}$ satisfying
$(\theta_{1},d_{1},\theta_{2})\models\phi_{1}$ and
$(\theta_{2},d_{2},\theta_{3})\models\phi_{2}$ for some
$\theta_{1},d_{1},\theta_{2},d_{2},\theta_{3}$, we will define (after Example
3) the composition $\phi_{1}\circ\phi_{2}$ that satisfies
$(\theta_{1},d_{1},\theta_{3})\models\phi_{1}\circ\phi_{2}$ (under the
assumption on the freshness property), and $\phi_{1}\odot\phi_{2}$ represents
the condition “$(\theta_{1},d_{1},\theta_{2})\models\phi_{1}$ and
$(\theta_{2},d_{2},\theta_{3})\models\phi_{2}$ for some
$\theta_{1},d_{1},\theta_{2},d_{2},\theta_{3}$.” Similarly,
$\phi_{1}\odot_{\mathtt{T}}\phi_{2}$ represents the condition
“$(\theta_{1},d,\theta_{2})\models\phi_{1}$ and
$(\theta_{2},d,\theta_{3})\models\phi_{2}$ for some
$\theta_{1},d,\theta_{2},\theta_{3}$.”

###### Example 3

The equivalence relations $\phi_{0}$ and $\phi_{1}$ shown in Example 1 satisfy
$\phi_{0}\odot\phi_{1}$ because
$\mathtt{x}^{\prime}_{1}\not\equiv_{\phi_{0}}\mathtt{x}^{\prime}_{2}$ and
$\mathtt{x}_{1}\not\equiv_{\phi_{1}}\mathtt{x}_{2}$. However,
$\phi_{0}\odot_{\mathtt{T}}\phi_{1}$ does not hold because
$\mathtt{x}^{\prime}_{2}\equiv_{\phi_{0}}\mathtt{x}_{\texttt{top}}$ but
$\mathtt{x}_{2}\not\equiv_{\phi_{1}}\mathtt{x}_{\texttt{top}}$. For $\phi_{2}$
and $\phi_{3}$ also shown in Example 1, both
$\phi_{0}\odot_{\mathtt{T}}\phi_{3}$ and $\phi_{1}\odot_{\mathtt{T}}\phi_{2}$
hold.

For $\phi_{1},\phi_{2}\in\Phi_{k}$ with $\phi_{1}\odot\phi_{2}$, the
_composition_ $\phi_{1}\circ\phi_{2}$ of them is the equivalence relation in
$\Phi_{k}$ that satisfies the following:

$\displaystyle\mathtt{x}_{i}\equiv_{\phi_{1}\circ\phi_{2}}\mathtt{x}_{j}:\Leftrightarrow{}$
$\displaystyle\mathtt{x}_{i}\equiv_{\phi_{1}}\mathtt{x}_{j}$
$\displaystyle\text{for }i,j\in[k]\cup\\{\texttt{top}\\},$ (1)
$\displaystyle\mathtt{x}^{\prime}_{i}\equiv_{\phi_{1}\circ\phi_{2}}\mathtt{x}^{\prime}_{j}:\Leftrightarrow{}$
$\displaystyle\mathtt{x}^{\prime}_{i}\equiv_{\phi_{2}}\mathtt{x}^{\prime}_{j}\quad\text{for
}i,j\in[k],$ (2)
$\displaystyle\mathtt{x}_{i}\equiv_{\phi_{1}\circ\phi_{2}}\mathtt{x}^{\prime}_{j}:\Leftrightarrow{}$
$\displaystyle(\exists
l\in[k]:{}\mathtt{x}_{i}\equiv_{\phi_{1}}\mathtt{x}^{\prime}_{l}\mathrel{\land}\mathtt{x}_{l}\equiv_{\phi_{2}}\mathtt{x}^{\prime}_{j})$
$\displaystyle\text{for }i\in[k]\cup\\{\texttt{top}\\},\ j\in[k].$ (3)

By definition, if an ID
$(p,\theta_{3},\allowbreak(d_{2},\theta_{2})\allowbreak(d_{1},\theta_{1})u)$
is proper, $(\theta_{1},d_{1},\theta_{2})\models\phi_{1}$ and
$(\theta_{2},d_{2},\theta_{3})\models\phi_{2}$, then
$(\theta_{1}\,d_{1},\theta_{3})\models\phi_{1}\circ\phi_{2}$. Guaranteeing
this property is the main purpose of the freshness property and the properness
of IDs: If the properness of the above ID is not assumed, and
$d_{1}\notin\theta_{2}$ and $\theta_{3}(j)\notin\theta_{2}\cup\\{d_{2}\\}$ for
some $j\in[k]$, then either $d_{1}=\theta_{3}(j)$ or $d_{1}\neq\theta_{3}(j)$
holds (and only the latter satisfies
$(\theta_{1}\,d_{1},\theta_{3})\models\phi_{1}\circ\phi_{2}$). This
uncertainty prevents a PDS from simulating an RPDS: When a PDS
$\mathcal{P}^{\prime}$ simulating an RPDS is popping off the stack top in an
ID corresponding to the above ID, without assuming the properness of the ID,
$\mathcal{P}^{\prime}$ cannot know whether or not the data value $d_{1}$ in
the new stack top of the RPDS is contained in the current register assignment
$\theta_{3}$.

Similarly to the composition $\circ$, for $\phi_{1},\phi_{2}\in\Phi_{k}$ with
$\phi_{1}\odot_{\mathtt{T}}\phi_{2}$, we define
$\phi_{1}\circ_{\mathtt{T}}\phi_{2}$ as the same as $\phi_{1}\circ\phi_{2}$
except that the Equation (3) is replaced with the following (4):

$\displaystyle\mathtt{x}_{i}\equiv_{\phi_{1}\circ_{\mathtt{T}}\phi_{2}}\mathtt{x}^{\prime}_{j}:\Leftrightarrow{}$
$\displaystyle(\exists
l\in[k]:{}\mathtt{x}_{i}\equiv_{\phi_{1}}\mathtt{x}^{\prime}_{l}\mathrel{\land}\mathtt{x}_{l}\equiv_{\phi_{2}}\mathtt{x}^{\prime}_{j})$
$\displaystyle\quad\>\lor{}(\mathtt{x}_{i}\equiv_{\phi_{1}}\mathtt{x}_{\texttt{top}}\mathrel{\land}\mathtt{x}_{\texttt{top}}\equiv_{\phi_{2}}\mathtt{x}^{\prime}_{j})$
$\displaystyle\text{for }i\in[k]\cup\\{\texttt{top}\\},\ j\in[k].$ (4)

By definition, $\circ$ and $\circ_{\mathtt{T}}$ are associative.

Let $({\phi})^{=}_{j}$ for $\phi\in\Phi_{k}$ and $j\in[k]$ be the equivalence
relation defined as follows: $\forall
i,l\in[k]:\bigl{(}\mathtt{x}_{i}\equiv_{({\phi})^{=}_{j}}\mathtt{x}_{l}$ iff
$\mathtt{x}^{\prime}_{i}\equiv_{\phi}\mathtt{x}^{\prime}_{l}\bigr{)}\land\bigl{(}\mathtt{x}_{i}\equiv_{({\phi})^{=}_{j}}\mathtt{x}_{\texttt{top}}$
iff
$\mathtt{x}^{\prime}_{i}\equiv_{\phi}\mathtt{x}^{\prime}_{j}\bigr{)}\allowbreak\land(\mathtt{x}_{i}\equiv_{({\phi})^{=}_{j}}\mathtt{x}^{\prime}_{i})$.
The intention of the above definition is to guarantee that
$(\theta^{\prime},\theta^{\prime}(j),\theta^{\prime})\models({\phi})^{=}_{j}$
whenever $(\theta,d,\theta^{\prime})\models\phi$.

###  6.3 Construction of PDS simulating RPDS

For a $k$-RPDS $\mathcal{P}=(P,\Delta)$, we construct a PDS
$\mathcal{P}^{\prime}=(P^{\prime},\Delta^{\prime})$ bisimulation equivalent to
$\mathcal{P}$. The set of states of $\mathcal{P}^{\prime}$ is
$P^{\prime}=P\times\Phi_{k}$, and the stack alphabet of $\mathcal{P}^{\prime}$
is $\Phi_{k}$. $\mathcal{P}^{\prime}$ must simulate $\mathcal{P}$ without
keeping data values in the stack. When popping off the stack top,
$\mathcal{P}^{\prime}$ must know whether or not the data value in the new
stack top of $\mathcal{P}$ equals the _current_ value of each register. For
this purpose, $\mathcal{P}^{\prime}$ keeps an abstract “history” of the
register assignments represented by a sequence of equivalence relations in the
stack, which tells whether each of the data values in the stack of
$\mathcal{P}$ equals the current value of each register. The second component
of each state of $\mathcal{P}^{\prime}$ is “the last element” of the abstract
history, which represents the accumulated updates since the current stack top
has been pushed into the stack. Because a PDS cannot replace the symbol at the
new stack top when pop or skip is performed, $\mathcal{P}^{\prime}$ keeps the
last element of the history in its finite state and updates it in every
transition.

For example, configuration
$(q,\theta_{2},(d_{1},\theta_{1})(d_{0},\theta_{0}))$ of $\mathcal{P}$ is
simulated by configuration $((q,\phi_{2}),\phi_{1}\phi_{0})$ of
$\mathcal{P}^{\prime}$, where $(\theta_{0},d_{0},\theta_{1})\models\phi_{1}$
and $(\theta_{1},d_{1},\theta_{2})\models\phi_{2}$. Equivalence relation
$\phi_{1}$ abstractly represents the updates of assignments between when
$d_{0}$ has been pushed and when $d_{1}$ has been pushed. Similarly,
$\phi_{2}$ represents the updates of assignments since $d_{1}$ has been
pushed.

The set $\Delta^{\prime}$ of transition rules of $\mathcal{P}^{\prime}$ is the
smallest set satisfying the following inference rules.

$\displaystyle\begin{array}[]{l}(q,\phi_{3})\to(q^{\prime},\texttt{skip})\in\Delta\quad\phi_{1}\odot\phi_{2}\quad\phi_{2}\odot_{\mathtt{T}}\phi_{3}\\\
\hline\cr((q,\phi_{2}),\phi_{1})\to((q^{\prime},\phi_{2}\circ_{\mathtt{T}}\phi_{3}),\texttt{skip})\in\Delta^{\prime}\end{array}$
$\displaystyle\begin{array}[]{l}(q,\phi_{3})\to(q^{\prime},\texttt{pop})\in\Delta\quad\phi_{1}\odot\phi_{2}\quad\phi_{2}\odot_{\mathtt{T}}\phi_{3}\\\
\hline\cr((q,\phi_{2}),\phi_{1})\to((q^{\prime},\phi_{1}\circ(\phi_{2}\circ_{\mathtt{T}}\phi_{3})),\texttt{pop})\in\Delta^{\prime}\end{array}$
$\displaystyle\begin{array}[]{l}(q,\phi_{3})\to(q^{\prime},\texttt{push}(j))\in\Delta\quad\phi_{1}\odot\phi_{2}\quad\phi_{2}\odot_{\mathtt{T}}\phi_{3}\\\
\hline\cr((q,\phi_{2}),\phi_{1})\to((q^{\prime},({\phi_{3}})^{=}_{j}),\texttt{push}(\phi_{2}\circ_{\mathtt{T}}\phi_{3}))\in\Delta^{\prime}\end{array}$

In the above inference rules, $\phi_{2}\circ_{\mathtt{T}}\phi_{3}$ represents
the accumulation of the update of registers by $\phi_{3}$ into $\phi_{2}$.
When pop is performed, $\phi_{1}$ at the stack top is composed into
$\phi_{2}\circ_{\mathtt{T}}\phi_{3}$, which then represents the accumulated
updates since the new stack top has been pushed into the stack. When push is
performed, $\phi_{2}\circ_{\mathtt{T}}\phi_{3}$ is pushed into the stack
because the current assignment is “the assignment when the stack top was
pushed into the stack.” In this case, $\mathcal{P}^{\prime}$ sets the second
component of the state to $({\phi_{3}})^{=}_{j}$, which represents the current
assignment (which is the result of the update by $\phi_{3}$) equals the
assignment saved in the stack top.

In the same way, we construct an NFA $\mathcal{A}^{\prime}_{A}$, as a PDS with
pop rules only, from $\mathcal{A}_{A}=(Q_{A},P,\allowbreak\xi_{A},\delta_{A})$
for each $A\in\mathit{At}$. Moreover, let the set of initial states and the
set of final states of $\mathcal{A}^{\prime}_{A}$ be $P\times\Phi_{k}$ and
$\\{(p,\phi)\mid(p,\texttt{lat}(\phi))\in\xi_{A}\\}$, respectively, for each
$A\in\mathit{At}$. Let
$\mathit{ID}_{\\!\mathcal{A}}=\bigcup_{A\in\mathit{At}}\mathit{ID}_{\\!\mathcal{A}_{A}}$
and
$\mathit{ID}_{\\!\mathcal{A}^{\prime}}=\bigcup_{A\in\mathit{At}}\mathit{ID}_{\\!\mathcal{A}^{\prime}_{A}}$.

We assume that the stack $u_{0}$ in the given starting ID
$c_{0}=(p_{0},\theta^{\prime}_{0},u_{0})$ is not empty, and let
$(d_{0},\theta_{0})$ be the last (bottom-most) element of $u_{0}$. Note that
the last element of the stack of _every_ ID reachable from $c_{0}$ equals
$(d_{0},\theta_{0})$, because an ID with empty stack has no successor and thus
any computation cannot alter the stack bottom.

Let
$R\subseteq\mathit{ID}_{\\!\mathcal{A}}\times\mathit{ID}_{\\!\mathcal{A}^{\prime}}$
be the smallest relation satisfying the following:
$((p,\theta_{n},u),\allowbreak((p,\phi_{n}),v))\in R$ for
$u=(d_{n-1},\theta_{n-1})\ldots(d_{1},\theta_{1})$ and
$v=\phi_{n-1}\ldots\phi_{1}$ iff $(p,\theta_{n},u)$ is proper,
$(d_{1},\theta_{1})=(d_{0},\theta_{0})$ (or $u=\varepsilon$), and $\forall
i\in[n]:(\theta_{i-1},d_{i-1},\theta_{i})\models\phi_{i}$. (Remember that
$(d_{0},\theta_{0})$ is the stack bottom in the starting ID $c_{0}$.)

By definition, $R$ is functional; that is, each
$(p,\theta_{n},u)\in\mathit{ID}_{\\!\mathcal{A}}$ has exactly one
$((p,\phi_{n}),v)\in\mathit{ID}_{\\!\mathcal{A}^{\prime}}$ that satisfies
$((p,\theta_{n},u),((p,\phi_{n}),v))\in R$. Let $R(c)$ for
$c\in\mathit{ID}_{\\!\mathcal{A}}$ denote the unique ID
$c^{\prime}\in\mathit{ID}_{\\!\mathcal{A}^{\prime}}$ that satisfies
$(c,c^{\prime})\in R$.

Let
$R_{\mathcal{P}}=R\cap(\mathit{ID}_{\mathcal{P}}\times\mathit{ID}_{\mathcal{P}^{\prime}})$
and
$R_{\mathcal{A}_{A}}=R\cap(\mathit{ID}_{\\!\mathcal{A}_{A}}\times\mathit{ID}_{\\!\mathcal{A}^{\prime}_{A}})$
for each $A\in\mathit{At}$. We have proved the following proposition using the
Coq proof assistant [14].222The proof scripts are available at
https://github.com/ytakata69/rpds-to-pds-proof.

###### Proposition 4

$R_{\mathcal{P}}$ is a bisimulation relation between $\mathcal{P}$ and
$\mathcal{P}^{\prime}$. $R_{\mathcal{A}_{A}}$ is a bisimulation relation
between $\mathcal{A}_{A}$ and $\mathcal{A}^{\prime}_{A}$ for each
$A\in\mathit{At}$.

The reduction is completed by letting $c^{\prime}_{0}=R(c_{0})$.

###### Example 4

Let $\mathcal{P}^{\prime}$ be the PDS obtained from the 2-RPDS $\mathcal{P}$
shown in Example 1. Let $\phi_{0},\ldots,\phi_{3}\in\Phi_{2}$ be the
equivalence relations also shown in Example 1. By the above inference rules,
$\mathcal{P}^{\prime}$ has rules
$((p_{1},\phi^{\prime\prime}),\phi^{\prime})\to((p_{1},({\phi_{1}})^{=}_{1}),\texttt{push}(\phi^{\prime\prime}\circ_{\mathtt{T}}\phi_{1}))$
(obtained from $r_{2}$) and
$((p_{1},\phi^{\prime\prime}),\phi^{\prime})\to((p_{1},\phi^{\prime}\circ(\phi^{\prime\prime}\circ_{\mathtt{T}}\phi_{1})),\texttt{pop})$
(obtained from $r_{3}$) for each $\phi^{\prime}$ and $\phi^{\prime\prime}$
such that $\phi^{\prime}\odot\phi^{\prime\prime}$ and
$\phi^{\prime\prime}\odot_{\mathtt{T}}\phi_{1}$. Let
$\phi_{5},\phi_{6}\in\Phi_{2}$ be the equivalence relations defined by the
following quotient sets:

$\displaystyle X_{2}/{\phi_{5}}$
$\displaystyle=\\{\\{\mathtt{x}_{1},\mathtt{x}^{\prime}_{1},\mathtt{x}_{\texttt{top}}\\},\\{\mathtt{x}_{2},\mathtt{x}^{\prime}_{2}\\}\\},$
$\displaystyle X_{2}/{\phi_{6}}$
$\displaystyle=\\{\\{\mathtt{x}_{1},\mathtt{x}^{\prime}_{1}\\},\\{\mathtt{x}_{2},\mathtt{x}^{\prime}_{2},\mathtt{x}_{\texttt{top}}\\}\\}.$

Because $\phi_{0}\odot\phi_{5}$, $\phi_{5}\odot_{\mathtt{T}}\phi_{1}$,
$\phi_{5}\circ_{\mathtt{T}}\phi_{1}=\phi_{1}$, and
$({\phi_{1}})^{=}_{1}=\phi_{5}$, $\mathcal{P}^{\prime}$ has rule
$r^{\prime}_{2}=((p_{1},\phi_{5}),\phi_{0})\to((p_{1},\phi_{5}),\texttt{push}(\phi_{1}))$.
Similarly, because $\phi_{1}\odot\phi_{5}$ and
$\phi_{1}\circ\phi_{1}=\phi_{1}$, $\mathcal{P}^{\prime}$ has rule
$r^{\prime}_{3}=((p_{1},\phi_{5}),\phi_{1})\to((p_{1},\phi_{1}),\texttt{pop})$.
By these two rules, $\mathcal{P}^{\prime}$ has the following transition
sequence:

$\displaystyle((p_{1},\phi_{5}),\phi_{0}\phi_{6})$
$\displaystyle\Rightarrow_{\mathcal{P}^{\prime}}((p_{1},\phi_{5}),\phi_{1}\phi_{0}\phi_{6})$
$\displaystyle\Rightarrow_{\mathcal{P}^{\prime}}((p_{1},\phi_{1}),\phi_{0}\phi_{6}).$
(5)

The following is a part of the transition sequence of $\mathcal{P}$ in Figure
1, in which each stack cell is augmented by the assignment at the time when
the cell has been pushed. (See Section 5.)

$\displaystyle(p_{1},[d_{2},d_{0}],(d_{2},[d_{2},d_{0}])(d_{0},[d_{1},d_{0}]))$
$\displaystyle\Rightarrow_{\mathcal{P}}(p_{1},[d_{3},d_{0}],(d_{3},[d_{3},d_{0}])(d_{2},[d_{2},d_{0}])(d_{0},[d_{1},d_{0}]))$
$\displaystyle\Rightarrow_{\mathcal{P}}(p_{1},[d_{4},d_{0}],(d_{2},[d_{2},d_{0}])(d_{0},[d_{1},d_{0}])).$
(6)

Let $c_{1},c_{2},c_{3}$ be the IDs in the sequence (6), respectively. We can
see that the IDs in the sequence (5) are $R(c_{1})$, $R(c_{2})$, and
$R(c_{3})$, respectively. (See the paragraphs before Proposition 4 for the
definition of $R$.)

###  6.4 Time complexity

Consider the LTL model checking problem on $\mathcal{P}=(P,\Delta)$,
$\varphi$, $\Lambda$, and $c_{0}$, where $\Lambda$ is a regular valuation and
is represented by $k$-RA $\mathcal{A}_{A}=(Q_{A},P,\xi_{A},\delta_{A})$ for
$A\in\mathit{At}$. Let $\mathcal{P}^{\prime}=(P^{\prime},\Delta^{\prime})$ and
$\mathcal{A}^{\prime}_{A}=(Q^{\prime}_{A},P^{\prime},F_{A},\delta^{\prime}_{A})$
be the PDS and NFA obtained from $\mathcal{P}$ and $\mathcal{A}_{A}$ in the
last subsection. Applying the LTL model checking method for PDS in [4] to
$\mathcal{P}^{\prime}$, we can solve the model checking problem on
$\mathcal{P},\varphi,\Lambda,c_{0}$ in
$O(|P^{\prime}|^{2}\cdot|\Delta^{\prime}|\cdot\prod_{A\in\mathit{At}}|Q^{\prime}_{A}|\cdot
2^{O(|\varphi|)})$ time, if $\mathcal{A}^{\prime}_{A}$ for each
$A\in\mathit{At}$ is backward-deterministic.333In [4], each FA for a regular
valuation is defined as the one that reads the _reverse_ of the stack
contents, and thus a deterministic FA in [4] is a backward-deterministic FA in
our settings. By the construction, $|P^{\prime}|=|P|\cdot|\Phi_{k}|$ and
$|Q^{\prime}_{A}|=|Q_{A}|\cdot|\Phi_{k}|$. Moreover,
$|\Delta^{\prime}|\leq|\Delta|\cdot|\Phi_{k}|^{2}$, because in the inference
rules defining $\Delta^{\prime}$, we choose two equivalence relations
$\phi_{1}$ and $\phi_{2}$ for each transition rule in $\Delta$. $|\Phi_{k}|$
equals the $(2k+1)$-th Bell number and thus $|\Phi_{k}|=2^{O(k\log k)}$. We
can assume that $|\mathit{At}|\leq|\varphi|$ and thus
$\prod_{A\in\mathit{At}}|Q^{\prime}_{A}|\leq\prod_{A\in\mathit{At}}|Q_{A}|\cdot|\Phi_{k}|^{|\varphi|}$.
Therefore the time complexity of the proposed method is exponential in $k$ and
$|\varphi|$ and polynomial in $|P|$ and $|\Delta|$ and
$\prod_{A\in\mathit{At}}|Q_{A}|$. Note that if the NFA
$\mathcal{A}^{\prime}_{A}$ for some $A\in\mathit{At}$ is not backward-
deterministic, we have to apply backward-determinization to
$\mathcal{A}^{\prime}_{A}$, which may increase the time complexity of the
proposed method. Also note that $\mathcal{A}^{\prime}_{A}$ is not necessarily
backward-deterministic even when $\mathcal{A}_{A}$ is backward-deterministic
in the sense defined in [11].

##  7 Conclusion

This paper proposed a method for solving the LTL model checking problem for
RPDS with regular valuations, in which the problem is reduced to the same
problem for PDS. In contrast to the method for the same problem proposed in
[11], the method in this paper does not require RA used for a regular
valuation to be deterministic or backward-deterministic. On the other hand,
the method in this paper requires every RPDS and RA has the freshness property
instead. This paper also showed that the LTL model checking problem for RPDS
with regular valuations defined by general RA is undecidable, and thus the
freshness constraint is essential in this method.

## References

  * [1] R. Alur, A. Bouajjani, J. Esparza, Model checking procedural programs, in: Handbook of Model Checking, Springer, 2018, Ch. 17, pp. 541–572.  doi:10.1007/978-3-319-10575-8_17.
  * [2] A. Bouajjani, J. Esparza, O. Maler, Reachability analysis of pushdown automata: Application to model-checking, in: 8th Int. Conf. on Concurrency Theory, CONCUR ’97, Vol. 1243 of Lecture Notes in Computer Science, Springer, 1997, pp. 135–150.  doi:10.1007/3-540-63141-0_10.
  * [3] I. Walukiewicz, Pushdown processes: Games and model checking, in: Computer Aided Verification, 8th Int. Conf., CAV ’96, Vol. 1102 of Lecture Notes in Computer Science, Springer, 1996, pp. 62–74.  doi:10.1007/3-540-61474-5_58.
  * [4] J. Esparza, A. Kučera, S. Schwoon, Model checking LTL with regular valuations for pushdown systems, Inf. Comput. 186 (2) (2003) 355–376.  doi:10.1016/S0890-5401(03)00139-1.
  * [5] M. Kaminski, N. Francez, Finite-memory automata, Theor. Comput. Sci. 134 (2) (1994) 329–363.  doi:10.1016/0304-3975(94)90242-9.
  * [6] L. Libkin, D. Vrgoč, Regular path queries on graphs with data, in: 15th Int. Conf. on Database Theory, ICDT ’12, ACM, 2012, pp. 74–85.  doi:10.1145/2274576.2274585.
  * [7] R. Grigore, D. Distefano, R. L. Petersen, N. Tzevelekos, Runtime verification based on register automata, in: TACAS 2013, Vol. 7795 of Lecture Notes in Computer Science, Springer, 2013, pp. 260–276.  doi:10.1007/978-3-642-36742-7_19.
  * [8] L. Exibard, E. Filiot, P. Reynier, Synthesis of data word transducers, Log. Methods Comput. Sci. 17 (1) (2021) .
URL https://lmcs.episciences.org/7279

  * [9] A. S. Murawski, S. J. Ramsay, N. Tzevelekos, Reachability in pushdown register automata, J. Comput. Syst. Sci. 87 (2017) 58–83.  doi:10.1016/j.jcss.2017.02.008.
  * [10] R. Senda, Y. Takata, H. Seki, Forward regularity preservation property of register pushdown systems, IEICE Trans. Inf. Syst. 104-D (3) (2021) 370–380.  doi:10.1587/transinf.2020FCP0008.
  * [11] R. Senda, Y. Takata, H. Seki, LTL model checking for register pushdown systems, IEICE Trans. Inf. Syst. 104-D (12) (2021) 2131–2144.  doi:10.1587/transinf.2020EDP7265.
  * [12] E. M. Clarke, O. Grumberg, D. Kroening, D. Peled, H. Veith, Model checking, 2nd Edition, MIT Press, 2018, Ch. 11, pp. 177–182.
  * [13] R. Senda, Y. Takata, H. Seki, Reactive synthesis from visibly register pushdown automata, in: ICTAC 2021, Vol. 12819 of Lecture Notes in Computer Science, Springer, 2021, pp. 334–353.  doi:10.1007/978-3-030-85315-0_19.
  * [14] Y. Bertot, P. Castéran, Interactive Theorem Proving and Program Development, Coq’Art: The Calculus of Inductive Constructions, Texts in Theoretical Computer Science. An EATCS Series, Springer, 2004.  doi:10.1007/978-3-662-07964-5.
  * [15] F. Neven, T. Schwentick, V. Vianu, Finite state machines for strings over infinite alphabets, ACM Trans. Comput. Log. 5 (3) (2004) 403–435.  doi:10.1145/1013560.1013562.
  * [16] B. Bollig, P. Habermehl, M. Leucker, B. Monmege, A robust class of data languages and an application to learning, Log. Methods Comput. Sci. 10 (4) (2014) 1–23.  doi:10.2168/LMCS-10(4:19)2014.
  * [17] N. Tzevelekos, Fresh-register automata, in: POPL ’11, ACM, 2011, pp. 295–306.  doi:10.1145/1926385.1926420.


# Study of polarization for even-denominator fractional quantum Hall states in
SU(4) Graphene

Moumita Indra1<EMAIL_ADDRESS>Dwipesh Majumder2<EMAIL_ADDRESS>1School of Basic Science, Swami Vivekananda University, Barrackpore, India
2Department of Physics, Indian Institute of Engineering Science and
Technology, Shibpur, Howrah, India

###### Abstract

We have focussed to study the even-denominator fractional quantum Hall (EDFQH)
states observed in monolayer graphene. In this letter, we have studied
polarization mainly for the two EDFQH states at filling fractions
$\nu=1/2,1/4$, which are observed in an experimental study [blue Nat. Phys.
14, 930 (2018)] a few years ago. We have applied Chern Simon’s gauge field
theory to explain the possible variational wave functions for different
polarized states and calculated their ground state energies using the Coulomb
potential. We have chosen the lowest energy states using suitable combinations
of flux attached with the electrons for different polarized states of those
EDFQH states.

##  I Introduction

Strongly correlated two-dimensional electron system (2DES) under a strong
perpendicular magnetic field shows a remarkable collective phenomenon, the
fractional quantum Hall effect (FQHE) Stormer ; Laughlin'83 . Composite
Fermion (CF) theory CF ; JainBook  beautifully explains the fractional quantum
Hall (FQH) states in detail qualitatively. CF is basically the bound state of
an electron and an even number ($2p$) of quantized vortices that produce a
Berry phase of $2n$ for a closed loop around it, such that the CFs obey the
same statistics as that of electrons. So the CFs experience a reduced amount
of magnetic field $B^{*}=B-2p\rho\phi_{0}$, where $\rho$ is the electron
density and $\phi_{0}$ is the flux quanta. The eigenstates of the Hamiltonian
of a CF are called $\Lambda$ levels, which are similar to the Landau levels
(LLs) with reduced degeneracy. $n$ number of filled $\Lambda$ levels of non-
interacting CFs system (integer quantum Hall effect of CF) describes the FQHE
of filling fraction $\nu=\frac{n}{2pn\pm 1}$ of a strongly interacting
electronic system. This is the beauty of this mean-field theory. For many
years, understanding the spin polarization of the various FQH states has
become a topic of great interest among experimentalists and theorists. In
sufficiently high magnetic fields, the low-energy states are of course fully
spin-polarized. The partially polarized and unpolarized states occur due to
the competition between the cyclotron energy and Zeeman energy. The magnetic
field (Zeeman energy) dependency of the polarization has been reported by
Kukushkin and co-authors Kukushkin  in detail. CF theory beautifully explains
most of the polarized states, except for some partially polarized states such
as $50\%$ polarized state of filling fraction $2/5,2/3$ and $25\%$, $75\%$
polarized state of filling fraction $4/7,4/9$ etc. Ganapathy Murthy explained
the partially polarized state of $2/5$ filling fraction as the density wave
ordered state of CF PRL80_1999 . The rest of the problem is explained later by
M. Indra et. al. PLA_MI .

Besides the two-dimensional (2D) semiconductor device, FQHE has been observed
in monolayer monolayer , and bilayer graphene bilayer . The effective low-
energy theory of the Graphene system can be described in terms of Dirac-like
quasi-particles RMP81_109 , which endows the electron wavefunctions with an
additional quantum number, termed valley isospin, that combined with the usual
electron spin, yields four-fold degenerate LLs Nat438 ; Zhang_2005 . This
additional symmetry adds up some new incompressible FQH states PRL96_2006 ;
PRB74_2006 ; Dean_Nat7 ; PRB77_2008  in graphene. In this SU(4) system CF
theory has been used to study the polarization TCJKJ2007  and collective
excitation TCJKJ2012  by the Jain group. Goerbig and Regnault Regnault2007
applied generalized Halperin’s wave function to study the ground state and
excited states of $\nu=2/3$ filling fraction in this SU(4) symmetric state. CF
theory is not sufficient to explain all the possible polarized states,
moreover, it can not explain the SU(4) polarized states of $\nu=n/(2pn\pm 1)$
with $n$ less than 3. In CF picture, it is not possible to obtain SU(4) states
of $1/3,2/5,3/7$ etc. SU(4) state has two types of Zeeman energies such as the
spin Zeeman energy and valley Zeeman energy. The polarization of the FQHE in
the SU(4) symmetric system has been addressed by Mandal and coworkers SM_SSM
using Chern Simon’s (CS) gauge field theory PRB44_1991 .

When graphene is placed in a strong perpendicular magnetic field, a plethora
of quantum Hall states are observed. Particularly notable is the recent
observation of incompressible even-denominator fractional quantum Hall (EDFQH)
states at $\nu=\pm 1/2$ and $\pm 1/4$ Zibrov_Nat14 . These EDFQH states were
not observed earlier in monolayer graphene, although EDFQH states have been
seen previously in higher LLs in single-component systems at $\nu=5/2$ in GaAs
PRL59_1987 , and at $\nu=3/2$ and $7/2$ in ZnO Falson_Nat11 . The most
discussed EDFQH state in the higher LL occurs at the filling fraction
$\nu=5/2$, thought to be described by the Moore Read Pfaffain Moore_Read
state. EDFQH states are observed for the lowest LLs both in double quantum
wells PRL68_1383  and wide single quantum wells at $\nu=1/2$ PRL68_1379 ;
PRL72_3405  and at $\nu=1/4$ PRL101_2008 ; PRL103_2009 . The $\nu=1/4$ state
may be interpreted as the pairing of CFs TCJKJ_2007  as described for
$\nu=1/2$ state in a thick 2DES PRB58_1998 . In literature, $\nu=1/2$ state
has been shown to have a large overlap with the so-called {3,3,1} wave
function PRB47_1993 ; RegnaultPRB77 , which was first introduced by Halperin
Halperin1983 . Beyond this {3,3,1} state this {m,m,n} model can be applied for
$\nu=1/4$ state considering two-component system. Possible wave function at
$\nu=1/4$ state is {5,5,3}, {6,6,2}, {7,7,1}. Since in monolayer graphene
there are 4-isospin configurations (two valleys and two spins) TChakrabarti ;
TCJKJ2006 ; PRB75_2007 ; TCJKJ2007 ; Ajit , we have many possibilities of
polarized states such as spin polarization, valley polarization, and a
combination of spin and valley polarization, which we call mixed polarization.
Four-fold states of Graphene are shown in figure 1. Golkmen et. al.
Golkmen2010  observed a marked contrast between the spin and valley degrees of
freedom. They found that an electron scattering from one valley to another
requires a large momentum transfer whereas an electron scattering from one
spin to another within the same valley requires a small momentum transfer. It
is also confirmed by another study by Papic Papic2010 . We are interested here
to study various possible wave functions for SU(4) graphene using CF or CS
theory of multicomponent FQH system. The various possibility of incompressible
EDFQH states in monolayer graphene was noted already in Ref. SM_SSM ;
PRB98_2018 . Following their work, we have investigated many more numerous
ways to realize different polarized states of the filling fractions
$\nu=1/2,1/4$ and then calculated the ground state energies of those states
using Coulomb potential. Although spin and valley energies are also important
factors for this kind of system but in our numerical study we only included
the usual Coulomb interactions between the electrons.

Figure 1: (Color online) Schematic diagram of four states of SU(4) Graphene in
lowest $\Lambda$-level, where $\uparrow,\downarrow(+,-)$ represents physical
spin (valley) states of the electron. Red-circled dot with arrow lines
represents CS-CF quasiparticles, electron (circular dot) with attached
magnetic flux (green arrow lines). Variation of the number of attached fluxes
to each of the four species gives rise to different polarized states.

##  II Calculation proccedure

Following the Chern-Simon’s gauge field theory in SU(4) system, we have seen
that the effective field depends on the quantum numbers (Spin and Valley)
carried by the quassiparticles. The quasiparticles in CS theory experiences a
mean effective magnetic field, $B^{*}_{\alpha}$

$B^{*}_{\alpha}=B-\phi_{0}{\cal{K}}_{\alpha\beta}\;\rho_{\beta}$ (1)

where $B$ is the applied actual magnetic filed, $\phi_{0}$ is the flux quanta.
We label the valley-spin configurations
$(+\uparrow),(+\downarrow),(-\uparrow),(-\downarrow)$ by $\alpha=1,2,3,4$
respectively as shown in fig 1. The indices $\alpha,\beta$ runs from $1$ to
$4$, i.e. ${\cal K}_{\alpha\beta}$ is $4\times 4$ matrix

$\cal{K}=\left(\begin{array}[]{llll}2k_{1}&m_{1}&n_{1}&n_{2}\\\
m_{1}&2k_{2}&n_{3}&n_{4}\\\ n_{1}&n_{2}&2k_{3}&m_{2}\\\
n_{3}&n_{4}&m_{2}&2k_{4}\end{array}\right),$ (2)

where $k$’s, $m$’s and $n$’s are positive integers including zero. In Ref.
SM_SSM  flux attachment scheme is represented schematically. As suggested by
them we have also simplified the flux attachment that
$k_{1}=k_{2},k_{3}=k_{4},n_{1}=n_{2}=n_{3}=n_{4}=n$. Considering mean-field
approximation, the electron filling factor $\nu$ and the effective filling
factor $\nu_{\alpha}$ of CS quasiparticles are related by,

$\rho_{\alpha}/\nu_{\alpha}=\rho/\nu-{\cal K}_{\alpha\beta}\rho_{\beta}\;.$
(3)

### Selection of number of particles::

We have considered that $N$ number of corelated electrons resides on the
spherical surface JainBook ; Fano's  in presence of radial magnetic field
created by a Dirac monopole at the center of the sphere with monopole strength
$Q$ and there are $N_{1}$, $N_{2}$, $N_{3}$, $N_{4}$ number of electrons in
species $1,2,3,4$ respectively.

$\displaystyle N$ $\displaystyle=$ $\displaystyle N_{1}+N_{2}+N_{3}+N_{4}$
$\displaystyle S$ $\displaystyle=$
$\displaystyle\frac{N_{1}+N_{3}-N_{2}-N_{4}}{N_{1}+N_{2}+N_{3}+N_{4}}$
$\displaystyle V$ $\displaystyle=$
$\displaystyle\frac{N_{1}+N_{2}-N_{3}-N_{4}}{N_{1}+N_{2}+N_{3}+N_{4}}$
$\displaystyle M$ $\displaystyle=$
$\displaystyle\frac{N_{1}+N_{4}-N_{2}-N_{3}}{N_{1}+N_{2}+N_{3}+N_{4}}$

We have chosen the values of $N_{1}$, $N_{2}$, $N_{3}$, $N_{4}$ such a way
that it will give the value of $S$, $V$, $M$ in the following tables. The
monopole strength corresponding to this field can be written as,

$2q_{\alpha}=2Q-\sum_{\beta}(N_{\beta}-\delta_{\alpha\beta})\cal{K}_{\alpha\beta}$
(4) $\displaystyle\sum_{\alpha}2q_{\alpha}$ $\displaystyle=$ $\displaystyle
8Q-\sum_{\alpha}\sum_{\beta}\left(N_{\alpha}-\delta_{\alpha\beta}\right)\cal{K}_{\alpha\beta}$
$\displaystyle\Rightarrow Q$ $\displaystyle=$
$\displaystyle\frac{1}{8}\left(\sum_{\alpha}2q_{\alpha}+\sum_{\alpha}{\cal
K}_{\alpha\alpha}(N_{\alpha}-1)\right)$ $\displaystyle+$
$\displaystyle\frac{1}{8}\left(m_{1}N_{1}+m_{1}N_{2}+m_{2}N_{3}+m_{2}N_{4}+2nN\right)$

2$Q\phi_{0}$ is the total flux through the spherical surface of radius $R$, if
$B$ is the corresponding magnetic filed then

$\displaystyle 2Q\phi_{0}=4\pi R^{2}B\Rightarrow
R^{2}=\frac{2Q}{4\pi}\frac{hc}{e}\frac{el^{2}}{\hbar c}=Q{l_{B}}^{2}$

So the radius of the sphere is $R=\sqrt{Q}$ in unit of magnetic length
$l_{B}$.

###  II.1 Wave function

Let us suppose that there are $\nu_{1}$ number of spin-up $(+)$ valley
$\Lambda$-level, $\nu_{2}$ number of spin-down $(+)$ valley $\Lambda$-level,
$\nu_{3}$ number of spin-up $(-)$ valley $\Lambda$-level, $\nu_{4}$ number of
spin-down $(-)$ valley $\Lambda$-level. Following the route proposed by Mandal
and co-workers the spin (S), the valley (V), and the mixed (M) polarization of
these quasi-particles in a given FQH states is defined as,

$\displaystyle S=(\rho_{1}+\rho_{3}-\rho_{2}-\rho_{4})/\rho,$ $\displaystyle
V=(\rho_{1}+\rho_{2}-\rho_{3}-\rho_{4})/\rho,$ $\displaystyle
M=(\rho_{1}+\rho_{4}-\rho_{2}-\rho_{3})/\rho,$ (5)

So, the above equation (3) relates total filling factor $\nu$ in terms of
those three polarization $S,V,M$ and the attached flux numbers k’s , m’s and
n’s.

$\displaystyle\gamma_{1}(2k_{1}+1/\nu_{1})+\gamma_{2}m_{1}+\eta_{1}2n=4/\nu$
$\displaystyle\gamma_{2}(2k_{1}+1/\nu_{2})+\gamma_{1}m_{1}+\eta_{1}2n=4/\nu$
$\displaystyle\gamma_{3}(2k_{3}+1/\nu_{3})+\gamma_{4}m_{2}+\eta_{2}2n=4/\nu$
$\displaystyle\gamma_{4}(2k_{3}+1/\nu_{4})+\gamma_{3}m_{2}+\eta_{2}2n=4/\nu$
(6)

where, $\eta_{1(2)}=1-(+)V$, $\delta_{1(2)}=S-(+)M$,
$\gamma_{1(2)}=\eta_{2}+(-)\delta_{2}$, and
$\gamma_{3(4)}=\eta_{1}+(-)\delta_{1}$.

The five indices $k_{1}$, $k_{3}$, $m_{1}$, $m_{2}$, $n$ represent the
interaction strength between different $\Lambda$-levels. From equation (6), it
is very clear that the polarization index $S$, $V$, $M$; four species
$\Lambda$-level filing fractions $\nu_{1},\nu_{2},\nu_{3},\nu_{4}$ and the
interaction parameters $k_{1}$, $k_{3}$, $m_{1}$, $m_{2}$, $n$ altogether
fixes the total filling fraction $\nu$ of the state. Here a particular state
with fixed interaction parameters between the four species is symbolized as
($k_{1}k_{3}m_{1}m_{2}n$) at a certain filling fraction $\nu$.

####  II.1.1 Meaning of $(k_{1}k_{3}m_{1}m_{2}n)$

i. $2k_{1}$ number of flux attachment of CF in the ($+\uparrow$) and
($+\downarrow$) $\Lambda$-levels.
ii. $2k_{3}$ number of flux attachment of CF in the ($-\uparrow$) and
($-\downarrow$) $\Lambda$-levels.
iii. $m_{1}$ flux attachment in the ($+\uparrow$) level seen by the CFs in
($+\downarrow$) $\Lambda$-level and vice versa.
iv. $m_{2}$ flux attachment in the ($-\uparrow$) level seen by the CFs in
($-\downarrow$) $\Lambda$-level and vice versa.
v. $n$ flux attachment in the ($+\uparrow\&\downarrow$) level seen by the CFs
in ($-\uparrow\&\downarrow$) $\Lambda$-levels and vice versa.

The variational wave function for the state is proposed by Mandal and coworker
SM_SSM  and is given by

$\displaystyle\Psi_{\\{\kappa_{\alpha\beta}\\}}$ $\displaystyle=$
$\displaystyle{\cal
P}_{L}\Phi_{\nu_{1}}(\Omega_{1}^{1},\cdots,\Omega_{N_{1}}^{1})\Phi_{\nu_{2}}(\Omega_{1}^{2},\cdots,\Omega_{N_{2}}^{2})$
$\displaystyle\times\Phi_{\nu_{3}}(\Omega_{1}^{3},\cdots,\Omega_{N_{3}}^{3})\Phi_{\nu_{4}}(\Omega_{1}^{4},\cdots,\Omega_{N_{4}}^{4})$
$\displaystyle\times
J_{11}\;J_{22}\;J_{33}\;J_{44}\;J_{12}\;J_{34}\;J_{13}\;J_{14}\;J_{23}\;J_{24}$

where, $\Phi_{\nu_{1}}$ is the Slater determinant of $\nu_{1}$ filled
$\Lambda$ level CFs, $\Omega_{1},\cdots\Omega_{N_{\alpha}}$ are the positions
of CFs on the spherical surface, upper index indicate the different species of
CFs and the Jastrow factor is given by

$\displaystyle J_{\alpha\beta}$ $\displaystyle=$
$\displaystyle\prod_{i,j}^{N_{\alpha},N_{\beta}}(u_{i}^{(\alpha)}v_{j}^{(\beta)}-u_{j}^{(\beta)}v_{i}^{(\alpha)})^{\kappa_{\alpha\beta}}\mbox{~{}~{}~{}~{}
if $\alpha\;\neq\beta$ }$ $\displaystyle J_{\alpha\alpha}$ $\displaystyle=$
$\displaystyle\prod_{i<j}^{N_{\alpha}}(u_{i}^{(\alpha)}v_{j}^{(\alpha)}-u_{j}^{(\alpha)}v_{i}^{(\alpha)})^{\kappa_{\alpha\alpha}}$

The prefix within bracket represent the CFs of different $\Lambda$ levels.
Here we have used the spinor coordinates

$\displaystyle u(\Omega)=cos(\theta/2)e^{-i\phi/2}\mbox{~{}~{}~{} and
~{}~{}~{}~{}}v(\Omega)=sin(\theta/2)e^{i\phi/2}$

Some of the above wave functions are identical with the wave function proposed
by Regnault and others using the plasma picture of the FQHE with internal
SU(4) symmetry PRB77_2008 . The ground state energy ($E_{g}$) per particle
corresponding to a particular state with flux attachment
($k_{1}k_{3}m_{1}m_{2}n$) can be calculated by the Monte Carlo method as

$\displaystyle E_{g}$ $\displaystyle=$ $\displaystyle\frac{E+E_{bg}}{N}$ (7)
$\displaystyle=$
$\displaystyle\left[\frac{<\Psi_{\\{\kappa_{\alpha\beta}\\}}|H|\Psi_{\\{\kappa_{\alpha\beta}\\}}>}{<\Psi_{\\{\kappa_{\alpha\beta}\\}}|\Psi_{\\{\kappa_{\alpha\beta}\\}}>}-\frac{N^{2}e^{2}}{2\epsilon
R}\right]/N\;$

Here, $H=\sum_{i<j}\frac{e^{2}}{r_{i,j}}$ is the Coulomb interaction, with
$r_{i,j}$ as the inter-electronic distance and
$E_{bg}=\frac{-N^{2}e^{2}}{2\epsilon R}$ term represents the background energy
i.e. the interaction between the electrons and the background positive ions
where $\epsilon$ is the dielectric constant of the background material. LL
mixing parameter is independent of the applied magnetic field in the graphene
system LLmixGraphene , so we do not need to include the LL mixing LLmix97 ;
LLmix2009  in our calculation.

Table 1: Possible polarized states for filling fraction $\nu=1/2$ and their ground state energies with different parameters $k_{1}$ | $k_{3}$ | $m_{1}$ | $m_{2}$ | $n$ | $V$ | $S$ | $M$ | $\nu_{1}$ | $\nu_{2}$ | $\nu_{3}$ | $\nu_{4}$ | $E_{g}(e^{2}/\epsilon l_{B})$
---|---|---|---|---|---|---|---|---|---|---|---|---
1 | 1 | 1 | 1 | 2 |  |  |  |  |  |  |  | -0.4677
1 | 1 | 3 | 3 | 1 | 0 | 0 | 0 | 1 | 1 | 1 | 1 | -0.46315
2 | 1 | 1 | 3 | 1 |  |  |  |  |  |  |  | -0.45576
2 | 2 | 1 | 1 | 1 |  |  |  |  |  |  |  | -0.44983
1 | 1 | 1 | 1 | 2 |  |  |  | 1 | 1 | 1 | 1 | -0.46742
1 | 2 | 2 | 3 | 1 |  |  |  |  |  |  |  | -0.46351
1 | 3 | 2 | 1 | 1 | 1/3 | 0 | 0 | 1 | 1 | 1 | 1 | -0.46012
1 | 1 | 2 | 5 | 1 |  |  |  |  |  |  |  | -0.45653
|  |  |  |  |  |  |  | 1 | 1 | 0 | 0 | -0.46321
|  |  |  |  | 1 | 0 | 0 | 1 | 1 | 1 | 0 | -0.46303
|  |  |  |  |  |  |  | 1 | 1 | 0 | 1 | -0.46298
1 | 1 | 1 | 1 | 2 | -1 | 0 | 0 | 0 | 0 | 1 | 1 | -0.46223
|  |  |  |  | 1/4 | 0 | 0 | 1 | 1 | 1 | 1 | -0.46759
|  |  |  |  | 1/2 | 0 | 0 | 1 | 1 | 1 | 1 | -0.46671
|  |  |  |  | 2/3 | 0 | 0 | 1 | 1 | 1 | 1 | -0.46567
1 | 1 | 1 | 1 | 3 | 1 | 0 | 0 | 1 | 1 | 0 | 0 | -0.46321
|  |  |  |  | -1 | 0 | 0 | 0 | 0 | 1 | 1 | -0.46223
1 | 2 | 1 | 1 | 1 | 1 | 0 | 0 | 1 | 1 | 0 | 0 | -0.53459
2 | 1 | 1 | 1 | 1 | -1 | 0 | 0 | 0 | 0 | 1 | 1 | -0.53353
1 | 2 | 1 | 1 | 2 | 1 | 0 | 0 | 1 | 1 | 0 | 0 | -0.46302
2 | 1 | 1 | 1 | 2 | -1 | 0 | 0 | 0 | 0 | 1 | 1 | -0.46186
|  |  |  |  | 0 | 1 | 0 | 1 | 0 | 1 | 0 | -0.51384
|  |  |  |  | 0 | -1 | 0 | 0 | 1 | 0 | 1 | -0.51289
1 | 1 | 1 | 2 | 1 | 0 | 0 | 1 | 1 | 0 | 0 | 1 | -0.51381
|  |  |  |  | 0 | 0 | -1 | 0 | 1 | 1 | 0 | -0.51282
|  |  |  |  | 0 | 1 | 0 | 1 | 0 | 1 | 0 | -0.49495
|  |  |  |  | 0 | -1 | 0 | 0 | 1 | 0 | 1 | -0.49391
1 | 1 | 2 | 2 | 1 | 0 | 0 | 1 | 1 | 0 | 0 | 1 | -0.49514
|  |  |  |  | 0 | 0 | -1 | 0 | 1 | 1 | 0 | -0.49398
|  |  |  |  | 0 | 1 | 0 | 1 | 0 | 1 | 0 | -0.49501
|  |  |  |  | 0 | -1 | 0 | 0 | 1 | 0 | 1 | -0.49400
1 | 1 | 1 | 3 | 1 | 0 | 0 | 1 | 1 | 0 | 0 | 1 | -0.49492
|  |  |  |  | 0 | 0 | -1 | 0 | 1 | 1 | 0 | -0.49407
Figure 2: (Color online) Ground state energy per particle for different combinations of ($k_{1}k_{3}m_{1}m_{2}n$) with different values of polarization indices $V,S,M$ at filling fraction $\nu=1/2$. Table 2: Lowest energy states with different polarization indices for $\nu=1/2$ $k_{1}$ | $k_{3}$ | $m_{1}$ | $m_{2}$ | $n$ | $V$ | $S$ | $M$ | $\nu_{1}$ | $\nu_{2}$ | $\nu_{3}$ | $\nu_{4}$
---|---|---|---|---|---|---|---|---|---|---|---
1 | 1 | 1 | 1 | 2 | 0 | 0 | 0 | 1 | 1 | 1 | 1
|  |  |  |  | 1/3 | 0 | 0 | 1 | 1 | 1 | 1
1 | 2 | 1 | 1 | 1 | 1 | 0 | 0 | 1 | 1 | 0 | 0
2 | 1 | 1 | 1 | 1 | -1 | 0 | 0 | 0 | 0 | 1 | 1
|  |  |  |  | 0 | 1 | 0 | 1 | 0 | 1 | 0
1 | 1 | 1 | 2 | 1 | 0 | -1 | 0 | 0 | 1 | 0 | 1
|  |  |  |  | 0 | 0 | 1 | 1 | 0 | 0 | 1
|  |  |  |  | 0 | 0 | -1 | 0 | 1 | 1 | 0
Table 3: Possible polarized states of filling fraction $\nu=1/4$ and their ground state energies with different parameters $k_{1}$ | $k_{3}$ | $m_{1}$ | $m_{2}$ | $n$ | $V$ | $S$ | $M$ | $\nu_{1}$ | $\nu_{2}$ | $\nu_{3}$ | $\nu_{4}$ | $E_{g}(e^{2}/\epsilon l_{B})$
---|---|---|---|---|---|---|---|---|---|---|---|---
1 | 1 | 3 | 3 | 5 |  |  |  | 1 | 1 | 1 | 1 | -0.21142
2 | 2 | 1 | 1 | 5 |  |  |  | 1 | 1 | 1 | 1 | -0.17752
2 | 2 | 3 | 3 | 4 | 0 | 0 | 0 | 1 | 1 | 1 | 1 | -0.35856
2 | 2 | 5 | 5 | 3 |  |  |  | 1 | 1 | 1 | 1 | -0.35749
3 | 3 | 1 | 1 | 4 |  |  |  | 1 | 1 | 1 | 1 | -0.33227
2 | 1 | 3 | 1 | 1 | 1 | 0 | 0 | 1 | 1 | 0 | 0 | -0.45215
2 | 2 | 3 | 1 | 1 | 1 | 0 | 0 | 1 | 1 | 0 | 0 | -0.45217
1 | 2 | 1 | 3 | 1 | -1 | 0 | 0 | 0 | 0 | 1 | 1 | -0.45178
2 | 2 | 1 | 3 | 1 | -1 | 0 | 0 | 0 | 0 | 1 | 1 | -0.45183
2 | 2 | 3 | 3 | 1 | 1 | 0 | 0 | 1 | 1 | 0 | 0 | -0.45221
|  |  |  |  | -1 | 0 | 0 | 0 | 0 | 1 | 1 | -0.45196
2 | 2 | 3 | 3 | 2 | 1 | 0 | 0 | 1 | 1 | 0 | 0 | -0.41279
|  |  |  |  | -1 | 0 | 0 | 0 | 0 | 1 | 1 | -0.41257
3 | 1 | 1 | 1 | 1 | 1 | 0 | 0 | 1 | 1 | 0 | 0 | -0.42212
2 | 3 | 1 | 1 | 1 | -1 | 0 | 0 | 0 | 0 | 1 | 1 | -0.42164
|  |  |  |  | 0 | 1 | 0 | 1 | 0 | 1 | 0 | -0.41283
2 | 2 | 1 | 1 | 3 | 0 | -1 | 0 | 0 | 1 | 0 | 1 | -0.4125
|  |  |  |  | 0 | 0 | 1 | 1 | 0 | 0 | 1 | -0.41277
|  |  |  |  | 0 | 0 | -1 | 0 | 1 | 1 | 0 | -0.41253
|  |  |  |  | 0 | 1 | 0 | 1 | 0 | 1 | 0 | -0.40453
2 | 2 | 1 | 2 | 3 | 0 | -1 | 0 | 0 | 1 | 0 | 1 | -0.40423
|  |  |  |  | 0 | 0 | 1 | 1 | 0 | 0 | 1 | -0.40439
|  |  |  |  | 0 | 0 | -1 | 0 | 1 | 1 | 0 | -0.40407
|  |  |  |  | 0 | 1 | 0 | 1 | 0 | 1 | 0 | -0.40445
2 | 2 | 2 | 1 | 3 | 0 | -1 | 0 | 0 | 1 | 0 | 1 | -0.40423
|  |  |  |  | 0 | 0 | 1 | 1 | 0 | 0 | 1 | -0.40444
|  |  |  |  | 0 | 0 | -1 | 0 | 1 | 1 | 0 | -0.40433
|  |  |  |  | 0 | 1 | 0 | 1 | 0 | 1 | 0 | -0.39658
2 | 2 | 2 | 2 | 3 | 0 | -1 | 0 | 0 | 1 | 0 | 1 | -0.39634
|  |  |  |  | 0 | 0 | 1 | 1 | 0 | 0 | 1 | -0.39654
|  |  |  |  | 0 | 0 | -1 | 0 | 1 | 1 | 0 | -0.39646
Figure 3: (Color online) Ground state energy per particle for different combinations of ($k_{1}k_{3}m_{1}m_{2}n$) with different values of polarization indices $V,S,M$ at filling fraction $\nu=1/4$. Table 4: Lowest energy states of different polarization indices for $\nu=1/4$ $k_{1}$ | $k_{3}$ | $m_{1}$ | $m_{2}$ | $n$ | $V$ | $S$ | $M$ | $\nu_{1}$ | $\nu_{2}$ | $\nu_{3}$ | $\nu_{4}$
---|---|---|---|---|---|---|---|---|---|---|---
2 | 2 | 3 | 3 | 4 | 0 | 0 | 0 | 1 | 1 | 1 | 1
2 | 2 | 5 | 5 | 3 |  |  |  |  |  |  |
2 | 1 | 3 | 1 | 1 |  |  |  |  |  |  |
2 | 2 | 3 | 1 | 1 | 1 | 0 | 0 | 1 | 1 | 0 | 0
2 | 2 | 3 | 3 | 1 |  |  |  |  |  |  |
1 | 2 | 1 | 3 | 1 |  |  |  |  |  |  |
2 | 2 | 1 | 3 | 1 | -1 | 0 | 0 | 0 | 0 | 1 | 1
2 | 2 | 3 | 3 | 1 |  |  |  |  |  |  |
|  |  |  |  | 0 | 1 | 0 | 1 | 0 | 1 | 0
2 | 2 | 1 | 1 | 3 | 0 | -1 | 0 | 0 | 1 | 0 | 1
|  |  |  |  | 0 | 0 | 1 | 1 | 0 | 0 | 1
|  |  |  |  | 0 | 0 | -1 | 0 | 1 | 1 | 0

##  III Results & Conclusion

We observed that the EDFQH states do not correspond to the Fermi sea of CFs.
Zibrov et. al. Zibrov_Nat14  proposed that the EDFQH states are associated
with a phase transition from a partial sublattice polarized PSP  to a canted
antiferromagnet phase CAF . With this idea, Sujit et. al. PRB98_2018
concluded that there is a phase transition from a state with $V\neq 0,S=0,M=0$
to one with $V=0$ and either $S$ or $M\neq 0$. They have noted also that the
flux attachments for the state at $\nu=1/4$ are related to those found for
$\nu=1/2$ by $j\rightarrow j+1$ for $j=k_{1},k_{3},m_{1},m_{2},n$ which agrees
with our result too. In this article, we have accumulated all possible wave-
functions for the recently observed EDFQH states at $\nu=1/2,1/4$ and
calculated their ground state energies which help us to find out the befitted
wave functions for those states. An understanding of the suitable ground state
wave function for those two EDFQH states awaits future theoretical
developments.

We have studied here the possible polarizations for the two EDFQH states
($\nu=1/2,1/4$). We have considered different combinations of flux attachment
$(k_{1}k_{3}m_{1}m_{2}n)$ between the four species of electrons and calculated
their ground state energies using the Coulomb potential for a finite number of
particles. To get the thermodynamic limit, we have extrapolated the result in
the $1/N\rightarrow 0$ region. The energy values for the filling fraction
$\nu=1/2$ and $1/4$ are listed in TABLE 1 and TABLE 3. Energy has been
expressed in natural unit $e^{2}/\epsilon l_{B}$ with respect to the spin and
valley Zeeman energy. The error of the Monte-Carlo integration is less than
the symbol size.
We have observed that different interaction strength between the four species
can lead to different polarization. We can have the unpolarized state of
$\nu=1/2$ for different combinations of flux attachment i.e. different
interaction parameters; keeping the four $\Lambda$-level filling fractions
unity ($\nu_{1}=\nu_{2}=\nu_{3}=\nu_{4}=1$). The ground state energies differ
in each of the cases. We found that the state with interaction $(11112)$ has
the lowest energy (see FIG. 2 (a)). So this is the most stable state for the
unpolarized condition. Other states having interaction parameters $(11331)$,
$(21131)$, $(22111)$ have higher energy compared to that. These states can be
thought of as next stable states. By a slight change in the interaction
parameters the system can suffer transition from one state to another. After
that, we have considered different valley polarized states. We have observed
that also for $V=1/3$ polarized state, with other two polarization index zero
($S$, $M=0$), the state with interaction $(11112)$ has the lowest energy (Fig.
2 (b)). Then we have checked the energies for different valley polarizations
for the combination $(11112)$ keeping the spin and mixed polarization zero
($S=M=0$). Energies of those valley polarized states ($V=0,1/4,1/3,1/2,2/3,\pm
1$) are slightly differ from each other. So there is a high chance for the
phase transition depending upon the Zeeman energies between the four
$\Lambda$-levels. We have noted that $V=0$ state has the lowest energy and
$V=\pm 1$ state has the highest energy and intermediate states lie in between.
Besides, we have checked whether there is any other state having lower energy
for $V=\pm 1$ polarization with other two polarization index ($S,M$) zero. We
found that the states $(12111)$ and $(21111)$ have the lowest energy for the
valley polarization $V=1$ and $V=-1$ respectively; with other two polarization
index $S$, $M$ zero for both the two cases (see FIG. 2 (c)). Next, we
calculated the same taking the polarization $S$ (or $M$) as $\pm 1$ and the
other two polarization indices $V$, $M$ (or $V$, $S$) as zero, as suggested by
Sujit et. al. PRB98_2018 . We observed that for the interaction $(11121)$ we
get the lowest energy when the polarization $S$ (or, $M$) is $\pm 1$ and the
energy values are almost equal (see FIG. 2 (d)). All the results for the
filling fraction $\nu=1/2$ are shown in TABLE 2.

Similarly, we have checked all the above possibilities for the filling
fraction $\nu=1/4$, the results are shown in Fig. 3 and in TABLE 3. For the
unpolarized state ($V=S=M=0$), we have found that $(22334)$, $(22553)$ states
have almost the same energy which is the lowest for this polarization (see
FIG. 3 (a)). So the unpolarized state is doubly degenerate for $\nu=1/4$. We
have found that for $V=1$ polarized state with other two polarization zero
($S$, $M=0$); $(21311)$, $(22311)$ and $(22331)$ states have the same energy
value (see FIG. 3 (c)). That is those three states are degenerate metastable
states; so the system can change any one of those. For the valley polarization
$V=-1$ with $S$, $M=0$; there are also three degenerate metastable states,
which are $(12131)$, $(22131)$, and $(22331)$ (see FIG. 3 (d)). We have found
that $(22113)$ has the lowest energy when spin or mixed polarization $S$ (or,
$M$) is $\pm 1$ and valley polarization is zero (see Fig. 3 (b)). We also
noticed that for same interaction parameters ($22113$), change in Zeeman
energies between four $\Lambda$-levels can lead to different polarization
$S=\pm 1$, $M=\pm 1$ states, those states have same energies i.e. those are
the degenerate states for the filling fraction $\nu=1/4$. The energy values
for the different polarized states of filling fraction $\nu=1/4$ are enlisted
in TABLE 4.

##  IV acknowledgement

Moumita thanks Dr. Debashis Das for the preliminary idea to start this work.
She is thankful to the Department of Physics, IIEST Shibpur for providing her
with the computing facility. Both of the two authors like to acknowledge Prof.
Sudhansu Sekhar Mandal (IIT Kharagpur) for some fruitful discussions.

## References

  * (1) D. C. Tsui, H. L. Stormer, and A. C. Gossard, Phys. Rev. Lett. 48, 1559 (1982).
  * (2) Laughlin, R. B., Phys. Rev. Lett. 50, 1395-1398 (1983).
  * (3) J. K. Jain, Phys. Rev. Lett. 63, 199 (1989).
  * (4) Composite Fermions, J. K. Jain (Cambridge University Press), http://www.cambridge.org/9780521862325.
  * (5) I. V. Kukushkin, K. v. Klitzing and K. Eber, Phys. Rev. Lett. 82, 3665 (1999).
  * (6) Ganpathy Murthy, Phys. Rev. Lett. 80, 350 (1999).
  * (7) M. Indra, D. Das, D. Majumder; Phys. Lett. A 382 (2018), 2984–2988.
  * (8) K. I. Bolotin, F. Ghahari, M. D. Shulman, H. L. Stormer, and P. Kim, Nature (London) 462, 196 (2009); X. Du, I. Skachko, F. Duerr, A. Luican, and E. Y. Andrei, Nature (London) 462, 192 (2009); D. A. Abanin, I. Skachko, X. Du, E. Y. Andrei, and L. S. Levitov, Phys. Rev. B 81, 115410 (2010); F. Ghahari, Y. Zhao, P. Cadden-Zimansky, K. Bolotin, and P. Kim, Phys. Rev. Lett. 106, 046801 (2011);
  * (9) C. Pan, Y. Wu, B. Cheng, S. Che, T. Taniguchi, K. Watanabe, C. N. Lau, and M. Bock-rath, Nano Lett. 17 (6), pp 34163420 (2017); A. Kou, B. E. Feldman, A. J. Levin, B. I. Halperin, K. Watanabe, T. Taniguchi, and A. Yacoby Science 345, 55 (2014); Dong-Keun Ki, Vladimir I. Falko, Dmitry A. Abanin, and Alberto F. Morpurgo Nano Lett. 14, 2135 (2014).
  * (10) A. H. Castro Neto, F. Guinea, N. M. R. Peres, K. S. Novoselov, and A. K. Geim, Rev. Mod. Phys. 81, 109 (2009).
  * (11) K. Novoselov et. al., Nature 438, 197-200 (2005).
  * (12) Zhang, Y., Tan, Y., Stormer, H. & Kim, P., Nature 438, 201-204 (2005).
  * (13) Nomura, K. & MacDonald, A. H., Phys. Rev. Lett. 96, 256602 (2006).
  * (14) Yang, K., Das Sarma, S. & MacDonald, A. H., Phys. Rev. B 74, 075423 (2006).
  * (15) Dean, C. R., Young A. F., Cadden-Zimansky, P., Watanabe, K., Taniguchi, T., Kim, P., Hone, J., Shepard, K. L., Nature Physics 7, 693, (2011).
  * (16) Shibata, N. & Nomura, K. Phys. Rev. B 77, 235426 (2008).
  * (17) Csaba Toke, Jainendra K. Jain, Phys. Rev. B 75, 245440 (2007).
  * (18) C Toke and J K Jain, J. Phys. Condens. Matter 24 (2012) 235601.
  * (19) M. O. Goerbig and N. Regnault, Phys. Rev. B 75, 241405 R (2007).
  * (20) Sanchita Modak, Sudhansu S. Mandal, and K. Sengupta, Phys. Rev. B 84, 165118 (2011).
  * (21) A. Lopez, E. Fradkin, Phys. Rev. B 44 (1991) 5246.
  * (22) A. A. Zibrov, E. M. Spanton, H. Zhou, C. Kometter, T. Taniguchi, K. Watanabe, and A. F. Young, Nat. Phys. 14, 930 (2018).
  * (23) R. Willett, J. P. Eisenstein, H. L. Störmer, D. C. Tsui, A. C. Gossard, and J. H. English, Phys. Rev. Lett. 59, 1776 (1987).
  * (24) J. Falson, D. Maryenko, B. Friess, D. Zhang, Y. Kozuka, A. Tsukazaki, J. H. Smet, and M. Kawasaki, Nat. Phys. 11, 347 (2015).
  * (25) G. Moore and N. Read, Nucl. Phys. B 360, 362 (1991).
  * (26) J. P. Eisenstein, G. S. Boebinger, L. N. Pfeiffer, K. W. West, and Song He, Phys. Rev. Lett. 68, 1383 (1992).
  * (27) Y. W. Suen, L. W. Engel, M. B. Santos, M. Shayegan, and D. C. Tsui Phys. Rev. Lett. 68, 1379 (1992).
  * (28) Y. W. Suen, H. C. Manoharan, X. Ying, M. B. Santos, and M. Shayegan, Phys. Rev. Lett. 72, 3405 (1994).
  * (29) D. R. Luhman, W. Pan, D. C. Tsui, L. N. Pfeiffer, K. W. Baldwin, and K. W. West, Phys. Rev. Lett. 101, 266804 (2008).
  * (30) J. Shabani, T. Gokmen, Y. T. Chiu, and M. Shayegan, Phys. Rev. Lett. 103, 256802 (2009).
  * (31) C Toke and J K Jain, Phys. Rev. B 76, 081403(R) (2007).
  * (32) K. Park, V. Melik-Alaverdian, N. E. Bonesteel, and J. K. Jain, Phys. Rev. B 58, R10167 (1998).
  * (33) Song He, S. Das Sarma, and X. C. Xie, Phys. Rev. B 47, 4394 (1993).
  * (34) R. de Gail, N. Regnault, and M. O. Goerbig, Phys. Rev. B 77, 165310 (2008).
  * (35) B. I. Halperin, Helv. Phys. Acta 56, 75 (1983).
  * (36) V. M. Apalkov and T. Chakraborty, Phys. Rev. Lett. 97, 126801 (2006).
  * (37) Csaba Tőke, Paul E. Lammert, Vincent H. Crespi, and Jainendra K. Jain, Phys. Rev. B 74, 235417 (2006).
  * (38) D. V. Khveshchenko, Phys. Rev. B 75, 153405 (2007).
  * (39) Ajit C. Balram, Csaba Toke, A. Wojs, and J. K. Jain, Phys. Rev. B 92, 075410 (2015).
  * (40) T. Gokmen, Medini Padmanabhan, and M. Shayegan, Phys. Rev. B 81, 235305 (2010).
  * (41) Z. Papic, M. O. Goerbig, and N. Regnault Phys. Rev. Lett. 105 176802 (2010).
  * (42) Sujit Narayanan, Bitan Roy and Malcolm P. Kennett, Phys. Rev. B 98, 235411 (2018).
  * (43) G. Fano, F. Ortolani and E. Colombo, Phys. Rev. B 34, 2670 (1986).
  * (44) Michael R. Peterson and Chetan Nayak, Phys. Rev. Lett. 113, 086401 (2014).
  * (45) V. Melik-Alaverdian and N. E. Bonesteel, Phys. Rev. Lett. 79, 5286 (1997).
  * (46) Waheb Bishara and Chetan Nayak, Phys. Rev. B 80, 121302(R) (2009).
  * (47) Kentaro Nomura, Shinsei Ryu, and Dung-Hai Lee, Phys. Rev. Lett. 103, 216801, (2009).
  * (48) Igor F. Herbut, Phys. Rev. B 75, 165411, (2007).