17415 LABEL:LastPageDec. 01, 2020Dec. 02, 2021 [a] [a] [b]

# A Probabilistic Higher-order Fixpoint Logic

Yo Mitani  The University of Tokyo, Tokyo, Japan  ,  Naoki Kobayashi  and
Takeshi Tsukada  Chiba University, Chiba, Japan

###### Abstract.

We introduce PHFL, a probabilistic extension of higher-order fixpoint logic,
which can also be regarded as a higher-order extension of probabilistic
temporal logics such as PCTL and the $\mu^{p}$-calculus. We show that PHFL is
strictly more expressive than the $\mu^{p}$-calculus, and that the PHFL model-
checking problem for finite Markov chains is undecidable even for the
$\mu$-only, order-$1$ fragment of PHFL. Furthermore the full PHFL is far more
expressive: we give a translation from Lubarsky’s $\mu$-arithmetic to PHFL,
which implies that PHFL model checking is $\Pi^{1}_{1}$-hard and
$\Sigma^{1}_{1}$-hard. As a positive result, we characterize a decidable
fragment of the PHFL model-checking problems using a novel type system.

###### Key words and phrases:

probabilistic logic, probabilistic model checking, higher-order fixpoint logic

###### Key words and phrases:

Probabilistic logics, higher-order fixpoint logic, model checking

##  1\. Introduction

Temporal logics such as CTL and CTL* have been playing important roles in
system verification. Among the most expressive temporal logics is the _higher-
order fixpoint logic_ (_HFL_ for short) proposed by Viswanathan and
Viswanathan [VV04], which is a higher-order extension of the _modal
$\mu$-calculus_ [Koz83]. HFL is known to be strictly more expressive than the
modal $\mu$-calculus but the model-checking problem against finite models is
still decidable.

In view of the increasing importance of probabilistic systems, temporal logics
for probabilistic systems (such as PCTL [HJ94]) and their model-checking
problems have been studied and applied to verification and analysis of
probabilistic systems and randomized distributed algorithms [KNP11]. Recently
Castro et al. [CKP15] have proposed a probabilistic extension of the modal
$\mu$-calculus, called the _$\mu^{p}$ -calculus_. They showed that the
$\mu^{p}$-calculus is strictly more expressive than PCTL and that the model-
checking problem for the $\mu^{p}$-calculus belongs to NP $\cap$ co-NP.

In the present paper, we introduce PHFL, a probabilistic higher-order fixpoint
logic, and studies the model checking problem. PHFL can be regarded as a
probabilistic extension of HFL and as a higher-order extension of the
$\mu^{p}$-calculus. PHFL strictly subsumes the $\mu^{p}$-calculus [CKP15],
which coincides with order-$0$ PHFL.

We prove that PHFL model checking for finite Markov chains is undecidable even
for the order-1 fragment of PHFL without fixpoint alternations, by giving a
reduction from the _value problem_ of probabilistic automata [Rab63, Paz71].
In the presence of fixpoint alternations (i.e., with both least and greatest
fixpoint operators), PHFL model checking is even harder: the order-1 PHFL
model-checking problem is $\Pi^{1}_{1}$-hard and $\Sigma^{1}_{1}$-hard. The
proof is by a reduction from the validity checking problem for
$\mu$-arithmetic [Lub89] to PHFL model checking. This may be surprising,
because both order-0 PHFL model checking (i.e. $\mu^{p}$-calculus model
checking) for finite Markov chains [CKP15] and HFL model checking for finite
state systems [VV04] are decidable. The combination of probabilities and
higher-order predicates suddenly makes the model-checking problem highly
undecidable.

As a positive result, we identify a decidable subclass of PHFL model-checking
problems. To characterize the subclass, we introduce a type system for PHFL
formulas, which is parameterized by a Markov chain $M$. We show that the
model-checking problem $M\models\varphi$ is decidable provided that $\varphi$
is typable in the type system for $M$, by giving a decision procedure using
the decidability of existential theories of reals. The decidable subclass is
reasonably expressive: the problem of computing termination probabilities of
_recursive Markov chains_ [EY09] can be reduced to the subclass.

The rest of this article is organized as follows. Section 2 introduces PHFL
and shows that it is strictly more expressive than the $\mu^{p}$-calculus.
Section 3 proves undecidability of the model-checking problem for $\mu$-only
and order-$1$ PHFL. Section 4 proves that the PHFL model-checking problem is
both $\Pi^{1}_{1}$-hard and $\Sigma^{1}_{1}$-hard. Section 5 introduces a
decidable subclass of PHFL model-checking problems, and shows that the
subclass is reasonably large. Section 6 discusses related work, and Section 7
concludes the paper. A preliminary summary of this article has been published
in Proceedings of FSCD 2020 [MKT20]. This article contains details omitted in
the preliminary summary, and also significantly extends the decidable fragment
of PHFL in Section 5.

##  2\. PHFL: Probabilistic Higher-order Fixpoint Logic

This section introduces PHFL, a probabilistic extension of HFL [VV04]. PHFL is
a logic used for describing properties of Markov chains. We define its syntax
and semantics and show that it is more expressive than the $\mu^{p}$-calculus
[CKP15].

###  2.1. Markov Chains

We first recall the standard notion of Markov chains. Our definitions follow
those in [CKP15].

######  Definition .

Let $\mathit{AP}$ be a set of atomic propositions. A _Markov chain_ over
$\mathit{AP}$ is a tuple $(S,P,\rho_{\mathit{AP}},s_{\text{in}})$, where:

  * •

$S$ is a finite set of states,

  * •

$P:S\times S\to[0,1]$ satisfying $\sum_{s^{\prime}\in S}P(s,s^{\prime})=1$ for
every $s\in S$, describes transition probabilities,

  * •

$\rho_{\mathit{AP}}:\mathit{AP}\to 2^{S}$ is a labeling function, and

  * •

$s_{\text{in}}\in S$ is an initial state.

For a Markov chain $M=(S,P,\rho_{\mathit{AP}},s_{\text{in}})$, its _embedded
Kripke structure_ is $K=(S,R,\rho_{\mathit{AP}},s_{\text{in}})$ where
$R\subseteq S\times S$ is a relation such that
$R=\\{(s,s^{\prime})|P(s,s^{\prime})>0\\}$.

Intuitively, $P(s,s^{\prime})$ denotes the probability that the state $s$
transits to the state $s^{\prime}$, and $\rho_{\mathit{AP}}(p)$ gives the set
of states where $p$ is true. Throughout the paper, we assume that the set
$\mathit{AP}$ of atomic propositions is closed under negations, in the sense
that for any $p\in\mathit{AP}$, there exists $\overline{p}\in\mathit{AP}$ such
that $\rho_{\mathit{AP}}(\overline{p})=S\setminus\rho_{\mathit{AP}}(p)$.

Given a Markov chain $M$, we often write
$S_{M},P_{M},\rho_{\mathit{AP},M},s_{\text{in},M}$ for its components; we omit
the subscript $M$ when it is clear from the context.

###  2.2. Syntax of PHFL Formulas

As in HFL [VV04, KLB17], we need the notion of types to define the syntax of
PHFL formulas.

The set of types, ranged over by $\tau$, is given by:

$\tau::=\mathit{Prop}\,|\,\tau_{1}\rightarrow\tau_{2}.$

The type $\mathit{Prop}$ describes _quantitative_ propositions, whose values
range over $[0,1]$. Intuitively, the value of a quantitative proposition
represents the _probability_ that the proposition holds. The type
$\tau_{1}\to\tau_{2}$ is for functions from $\tau_{1}$ to $\tau_{2}$. For
example, $(\mathit{Prop}\to\mathit{Prop})\to\mathit{Prop}$ represents the type
of (higher-order, quantitative) predicates on unary predicates.

######  Remark .

In the $\mu^{p}{}$-calculus [CKP15] and the previous version of this paper
[MKT20], two kinds of propositions were considered: _quantitative_
propositions, which take values in $[0,1]$, and _qualitative_ propositions,
which take truth values. In the present paper, we consider only quantitative
propositions for the sake of simplicity, and regard qualitative propositions
as a special case of the former by treating $0$ and $1$ as the truth values
“false” and “true” respectively.

We assume a countably infinite set $\mathit{Var}$ of variables, ranged over by
$X_{1},X_{2},\dots$. The set of PHFL (pre-)formulas, ranged over by $\phi$, is
given by:

$\phi::=p\,|\,X\,|\,\phi_{1}\lor\phi_{2}\,|\,\phi_{1}\land\phi_{2}\,|\,[\phi]_{J}\,|\,\square\phi\,|\,\lozenge\phi\,|\,\mathbin{\bigcirc}\phi\,|\,\mu
X.\phi\,|\,\nu X.\phi\,|\,\lambda X.\phi\,|\,\phi_{1}\,\phi_{2}.$

Here, $p$ ranges over the set $\mathit{AP}$ of atomic propositions (of the
underlying Markov chains; we thus assume that $\mathit{AP}$ is closed under
negations). The subscript $J$ of $[\phi]_{J}$ is either “$>r$” or “$\geq r$”
for some rational number $r\in[0,1]$. We often identify $J$ with an interval:
for example, “$>r$” is regarded as $(r,1]=\\{\,x\mid r<x\leq 1\,\\}$. Given a
quantitative proposition $\phi$, the formula $[\phi]_{>r}$ (resp.
$[\phi]_{\geq r}$) is a qualitative formula, which is true just if the
probability that $\phi$ holds is greater than $r$ (resp. no less than $r$). We
exclude trivial bounds “$>1$” and “$\geq 0$”; note that $[\phi]_{>1}$ and
$[\phi]_{\geq 0}$ are equivalent to false and true respectively. The formulas
$\square\phi$, $\lozenge\phi$, and $\mathbin{\bigcirc}\phi$ respectively mean
the minimum, maximum, and average probabilities that $\phi$ holds after a one-
step transition. The formulas $\mu X.\phi$ and $\nu X.\phi$ respectively
denote the least and greatest fixpoints of $\lambda X.\phi$. Note that $\phi$
may denote higher-order predicates, as in HFL [VV04] (but unlike in the modal
$\mu$-calculus and its probabilistic variants [CKP15, MS13, MM97], where
fixpoints are restricted to propositions). We have also $\lambda$-abstractions
and applications, which are used for manipulating higher-order predicates. The
prefixes $\mu X$, $\nu X$ and $\lambda X$ bind the variable $X$. As usual, we
identify formulas up to the renaming of bound variables and implicitly apply
$\alpha$-conversions. We write $[\phi_{1}/X]$ for the capture-avoiding
substitution of $\phi_{1}$ for $X$, and $[\phi_{1}/X]\phi_{2}$ for the formula
obtained by applying the substitution $[\phi_{1}/X]$ to $\phi_{2}$.

In order to exclude out ill-formed formulas like $(p_{1}\lor p_{2})(\phi)$, we
restrict the shape of formulas using a simple type system. A _type
environment_ is a map from a finite set of variables to the set of types. A
_type judgment_ is of the form $\Gamma\vdash\phi:\tau$. The typing rules are
shown in Figure 1. A formula $\phi$ is _well-typed_ if $\Gamma\vdash\phi:\tau$
is derivable for some $\Gamma$ and $\tau$. Henceforth, we consider only well-
typed formulas.

######  Example 2.1.

For a proposition $p\in\mathit{AP}$, the formula $\phi=(\mu F.\lambda X.X\lor
F(\mathbin{\bigcirc}X))p$ is a well-typed formula of type $\mathit{Prop}$. By
unfolding the fixpoint formula (i.e., replacing $\mu X.\phi$ with $[\mu
X.\phi/X]\phi$, which will be justified by the semantics introduced later) and
applying $\beta$-reductions, we obtain:

$\displaystyle\phi$ $\displaystyle\equiv(\lambda X.X\lor(\mu F.\lambda X.X\lor
F(\mathbin{\bigcirc}X))(\mathbin{\bigcirc}X)){p}$
$\displaystyle\equiv{p}\lor(\mu F.\lambda X.X\lor
F(\mathbin{\bigcirc}X))(\mathbin{\bigcirc}{p})$
$\displaystyle\equiv{p}\lor\mathbin{\bigcirc}{p}\lor(\mu F.\lambda X.X\lor
F(\mathbin{\bigcirc}X))(\mathbin{\bigcirc}\mathbin{\bigcirc}{p})$
$\displaystyle\equiv{p}\lor\mathbin{\bigcirc}{p}\lor\mathbin{\bigcirc}\mathbin{\bigcirc}{p}\lor\cdots$

Thus, intuitively, the formula represents the function that maps the current
state $s$ to the value $\sup_{k\geq 0}q_{k}$ where $q_{k}$ is the probability
that a $k$-step transition sequence starting from the state $s$ ends in a
state satisfying $p$. ∎

######  Remark 2.2.

Following the definition of HFL by Kobayashi et al. [KLB17], we have excluded
out negations. By a transformation similar to that in [Loz15] and our
assumption that the set of atomic propositions is closed under negations, any
closed ground-type formula of PHFL extended with negations can be transformed
to an equivalent negation-free formula (as long as the occurrences of
negations are restricted as in the original HFL [VV04] so that fixpoint
operators are applied to only monotonic functions). ∎

$\Gamma\vdash p:\mathit{Prop}$

$\Gamma,X\mathbin{:}\tau\vdash X:\tau$

$\Gamma\vdash\phi:\mathit{Prop}$ $\Gamma\vdash[\phi]_{J}:\mathit{Prop}$

$\Gamma\vdash\phi_{1}:\mathit{Prop}$ $\Gamma\vdash\phi_{2}:\mathit{Prop}$
$\Gamma\vdash\phi_{1}\lor\phi_{2}:\mathit{Prop}$

$\Gamma\vdash\phi_{1}:\mathit{Prop}$ $\Gamma\vdash\phi_{2}:\mathit{Prop}$
$\Gamma\vdash\phi_{1}\land\phi_{2}:\mathit{Prop}$

$\Gamma\vdash\phi:\mathit{Prop}$ $\Gamma\vdash\square\phi:\mathit{Prop}$

$\Gamma\vdash\phi:\mathit{Prop}$ $\Gamma\vdash\lozenge\phi:\mathit{Prop}$

$\Gamma\vdash\phi:\mathit{Prop}$
$\Gamma\vdash\mathbin{\bigcirc}\phi:\mathit{Prop}$

$\Gamma,X:\tau\vdash\phi:\tau$ $\Gamma\vdash\mu X.\phi:\tau$

$\Gamma,X:\tau\vdash\phi:\tau$ $\Gamma\vdash\nu X.\phi:\tau$

$\Gamma,X:\tau_{1}\vdash\phi:\tau_{2}$ $\Gamma\vdash\lambda
X.\phi:\tau_{1}\to\tau_{2}$

$\Gamma\vdash\phi:\tau_{1}\to\tau_{2}$ $\Gamma\vdash\psi:\tau_{1}$
$\Gamma\vdash\phi\,\psi:\tau_{2}$

Figure 1. Typing rules for PHFL formulas.

We define the _order_ of a type $\tau$ by:

$\mathit{order}(\mathit{Prop})=0\qquad\mathit{order}(\tau_{1}\rightarrow\tau_{2})=\max(\mathit{order}(\tau_{1})+1,\mathit{order}(\tau_{2})).$

The order of a formula $\phi$ such that $\Gamma\vdash\phi:\tau$ is the largest
order of types used in the derivation of $\Gamma\vdash\phi:\tau$. The _order-
$k$ PHFL_ is the fragment of PHFL consisting of formulas of order up to $k$.
Order-$0$ PHFL coincides with the $\mu^{p}$-calculus [CKP15].

###  2.3. Semantics

We first give the semantics of types. We write $\leq_{\mathbb{R}}$ for the
natural order over the set $\mathbb{R}$ of real numbers, and often omit the
subscript when there is no danger of confusion. For a map $f$, we write
$\mathit{dom}(f)$ for the domain of $f$.

######  Definition 2.3 (Semantics of Types).

Let $M$ be a Markov chain. For each $\tau$, we define a partially ordered set
$\llbracket\tau\rrbracket_{M}=(D_{\tau},\sqsubseteq_{\tau})$ inductively by:

$\begin{array}[]{l}D_{\mathit{Prop}}=S_{M}\to[0,1]\qquad
f\sqsubseteq_{\mathit{Prop}}g\,\overset{\text{def}}{\Longleftrightarrow}\,\forall
s\in S_{M}.f(s)\leq g(s)\\\ D_{\tau_{1}\rightarrow\tau_{2}}=\\{f\in
D_{\tau_{1}}\rightarrow D_{\tau_{2}}\mid\forall x,y\in
D_{\tau_{1}}.x\sqsubseteq_{\tau_{1}}y\implies
f(x)\sqsubseteq_{\tau_{2}}f(y)\\}\\\
f\sqsubseteq_{\tau_{1}\rightarrow\tau_{2}}g\,\overset{\text{def}}{\Longleftrightarrow}\,\forall
x\in D_{\tau_{1}}.f(x)\sqsubseteq_{\tau_{2}}g(x).\end{array}$

For a type environment $\Gamma$, we write $\llbracket\Gamma\rrbracket_{M}$ for
the set of maps $f$ such that $\mathit{dom}(f)=\mathit{dom}(\Gamma)$ and
$f(x)\in D_{\Gamma(x)}$ for every $x\in\mathit{dom}(\Gamma)$.

We omit the subscript $M$ below. Note that $\llbracket\tau\rrbracket$ forms a
complete lattice for each $\tau$. We write $\bot_{\tau}$ for the least element
of $\llbracket\tau\rrbracket$, and for a set $V\subseteq D_{\tau}$, we write
$\mathbin{\textstyle{\bigsqcup_{\tau}}}V$ ($\textstyle{\bigsqcap_{\tau}}V$,
resp.) for the least upper bound (greatest lower bound, resp.) of $V$ with
respect to $\sqsubseteq_{\tau}$; we often omit the subscript $\tau$ if it is
clear from the context. Note also that for every functional type
$\tau_{1}\to\tau_{2}$, every element of $D_{\tau_{1}\to\tau_{2}}$ is
monotonic. Thus, for every type $\tau$ and every function $f\in
D_{\tau\rightarrow\tau}$, there exist the least and greatest fixed points of
$f$, which we write $\mathit{LFP}(f)$ and $\mathit{GFP}(f)$ respectively. They
are given by:

$\mathit{LFP}(f)=\textstyle{\bigsqcap_{\tau}}\\{x\in D_{\tau}\mid
f\,x\sqsubseteq_{\tau}x\\}\qquad\mathit{GFP}(f)=\mathbin{\textstyle{\bigsqcup_{\tau}}}\\{x\in
D_{\tau}\mid x\sqsubseteq_{\tau}f\,x\\}.$

We now define the semantics of formulas. Since the meaning of a formula
depends on its type environment, we actually define the semantics
$\llbracket\Gamma\vdash\phi:\tau\rrbracket_{M}$ for each type judgment
$\Gamma\vdash\phi:\tau$. Here, the subscript $M$ denotes the underlying Markov
chain, which is often omitted.

######  Definition 2.4 (Semantics of Type Judgement).

Let $M$ be a Markov chain and assume that $\Gamma\vdash\phi:\tau$ is
derivable. Then its semantics
$\llbracket\Gamma\vdash\phi:\tau\rrbracket_{M}\in\llbracket\Gamma\rrbracket\to\llbracket\tau\rrbracket$
is defined by induction on the (unique) derivation of
${\Gamma\vdash\phi:\tau}$ by:

$\displaystyle\llbracket\Gamma\vdash p:{\mathit{Prop}}\rrbracket_{M}(\rho)$
$\displaystyle=$ $\displaystyle\lambda s\in S_{M}.\text{if
$s\in\rho_{\mathit{AP},M}(p)$ then $1$ else $0$}$
$\displaystyle\llbracket\Gamma\vdash X:\tau\rrbracket_{M}(\rho)$
$\displaystyle=$ $\displaystyle\rho(X)$
$\displaystyle\llbracket\Gamma\vdash\phi_{1}\land\phi_{2}:\mathit{Prop}\rrbracket_{M}(\rho)$
$\displaystyle=$ $\displaystyle\lambda s\in
S_{M}.\min_{i\in\\{1,2\\}}\llbracket\Gamma\vdash\phi_{i}:\mathit{Prop}\rrbracket_{M}(\rho)(s)$
$\displaystyle\llbracket\Gamma\vdash\phi_{1}\lor\phi_{2}:\mathit{Prop}\rrbracket_{M}(\rho)$
$\displaystyle=$ $\displaystyle\lambda s\in
S_{M}.\max_{i\in\\{1,2\\}}\llbracket\Gamma\vdash\phi_{i}:\mathit{Prop}\rrbracket_{M}(\rho)(s)$
$\displaystyle\llbracket\Gamma\vdash[\phi]_{J}:{\mathit{Prop}}\rrbracket_{M}(\rho)$
$\displaystyle=$ $\displaystyle\lambda s\in S_{M}.\text{if
$\llbracket\Gamma\vdash\phi:\mathit{Prop}\rrbracket_{M}(\rho)(s)\in J$ then
$1$ else $0$}$
$\displaystyle\llbracket\Gamma\vdash\square\phi:\mathit{Prop}\rrbracket_{M}(\rho)$
$\displaystyle=$ $\displaystyle\lambda s\in
S_{M}.\min_{s^{\prime}:P_{M}(s,s^{\prime})>0}\llbracket\Gamma\vdash\phi:\mathit{Prop}\rrbracket_{M}(\rho)(s^{\prime})$
$\displaystyle\llbracket\Gamma\vdash\lozenge\phi:\mathit{Prop}\rrbracket_{M}(\rho)$
$\displaystyle=$ $\displaystyle\lambda s\in
S_{M}.\max_{s^{\prime}:P_{M}(s,s^{\prime})>0}\llbracket\Gamma\vdash\phi:\mathit{Prop}\rrbracket_{M}(\rho)(s^{\prime})$
$\displaystyle\llbracket\Gamma\vdash\mathbin{\bigcirc}\phi:\mathit{Prop}\rrbracket_{M}(\rho)$
$\displaystyle=$ $\displaystyle\lambda s\in S_{M}.\sum_{s^{\prime}\in
S_{M}}\big{(}P_{M}(s,s^{\prime})\cdot\llbracket\Gamma\vdash\phi:\mathit{Prop}\rrbracket_{M}(\rho)(s^{\prime})\big{)}$
$\displaystyle\llbracket\Gamma\vdash\mu X.\phi:\tau\rrbracket_{M}(\rho)$
$\displaystyle=$ $\displaystyle\mathit{LFP}(\lambda v\in
D_{\tau}.\llbracket\Gamma,X:\tau\vdash\phi:\tau\rrbracket_{M}(\rho[X\mapsto
v]))$ $\displaystyle\llbracket\Gamma\vdash\nu X.\phi:\tau\rrbracket_{M}(\rho)$
$\displaystyle=$ $\displaystyle\mathit{GFP}(\lambda v\in
D_{\tau}.\llbracket\Gamma,X:\tau\vdash\phi:\tau\rrbracket_{M}(\rho[X\mapsto
v]))$ $\displaystyle\llbracket\Gamma\vdash\lambda
X.\phi:\tau_{1}\to\tau_{2}\rrbracket_{M}(\rho)$ $\displaystyle=$
$\displaystyle\lambda v\in
D_{\tau_{1}}.\llbracket\Gamma,X:\tau_{1}\vdash\phi:\tau_{2}\rrbracket_{M}(\rho[X\mapsto
v])$
$\displaystyle\llbracket\Gamma\vdash\phi_{1}\,\phi_{2}:\tau\rrbracket_{M}(\rho)$
$\displaystyle=$
$\displaystyle\llbracket\Gamma\vdash\phi_{1}:\tau_{2}\to\tau\rrbracket_{M}(\rho)\,(\llbracket\Gamma\vdash\phi_{2}:\tau_{2}\rrbracket_{M}(\rho))$

In the last equality, $\tau_{2}$ is uniquely determined from $\Gamma$ and
$\phi_{2}$. In the definitions of the semantics of $\square\phi$ and
$\lozenge\phi$, the set $\\{s^{\prime}\in S_{M}|P(s,s^{\prime})>0\\}$ is non-
empty and finite, because $\sum_{s^{\prime}\in S_{M}}P(s,s^{\prime})=1$ and
$S_{M}$ is finite by the definition of Markov chains. Thus the max/min
operations are well-defined. We also note that
$\llbracket\Gamma\vdash\phi:\tau\rrbracket$ is a monotone function from
$\llbracket\Gamma\rrbracket$ to $\llbracket\tau\rrbracket$ (where
$\llbracket\Gamma\rrbracket$ is ordered by the component-wise ordering; note
also Remark 2.5 below). This ensures the well-definedness of the semantics of
$\mu X.\phi$, $\nu X.\phi$, and $\lambda X.\phi$.

######  Remark 2.5.

Recall that in a formula $[\phi]_{J}$, we allow the predicate $J$ to be “$>r$”
or “$\geq r$” (where $r\in[0,1]$), but neither “$<r$” nor “$\leq r$”. Allowing
“$<r$” would break the monotonicity of the semantics of a formula. For
example, $\llbracket\emptyset\vdash\lambda
X.[X]_{<1}:\mathit{Prop}\to{\mathit{Prop}}\rrbracket=\lambda v\in
D_{\mathit{Prop}}.\lambda s\in S.(\mbox{if $v(s)<1$ then $1$ else $0$})$ is
not monotonic. ∎

We often omit $M$, the type of the formula, and the type environment, and just
write $\llbracket\phi\rrbracket$ or $\llbracket\Gamma\vdash\phi\rrbracket$ for
$\llbracket\Gamma\vdash\phi:\tau\rrbracket_{M}$ when there is no danger of
confusion. For a Markov chain $M=(S,P,\rho_{\mathit{AP}},s_{\text{in}})$ and a
closed PHFL formula $\phi$ of type ${\mathit{Prop}}$, we write $M\models\phi$
if $\llbracket\phi\rrbracket(s_{\text{in}})=1$.

######  Example 2.6.

Recall the PHFL formula $\phi=\psi\,{p}$ where $\psi=\mu F.\lambda X.X\lor
F(\mathbin{\bigcirc}X)$ in Example 2.1. We have:

$\displaystyle\llbracket\psi\rrbracket$
$\displaystyle=\mathit{LFP}\Big{(}\lambda v\in
D_{\mathit{Prop}\to\mathit{Prop}}.\lambda x\in D_{\mathit{Prop}}.\lambda s\in
S.$ $\displaystyle\hphantom{\lambda v\in
D_{\mathit{Prop}\to\mathit{Prop}}.\lambda x\in
D_{\mathit{Prop}}}\max\Big{(}x\,s,v\,(\lambda s^{\prime}\in
S.\sum_{s^{\prime\prime}}P(s^{\prime},s^{\prime\prime})\cdot(xs^{\prime\prime}))\,s\Big{)}\Big{)}$
$\displaystyle\geq\Big{(}\lambda v.\lambda x.\lambda
s.\max\Big{(}x\,s,v\,(\lambda s^{\prime}\in
S.\sum_{s^{\prime\prime}}P(s^{\prime},s^{\prime\prime})\cdot(xs^{\prime\prime}))\,s\Big{)}\Big{)}^{n+1}(\bot_{\mathit{Prop}\to\mathit{Prop}})$
$\displaystyle=\lambda x.\lambda s.\max_{0\leq k\leq n}\sum_{s_{0}s_{1}\dots
s_{k}\in S^{k+1},s_{0}=s}\big{(}x(s_{k})\cdot\prod_{0\leq j\leq
k-1}P(s_{j},s_{j+1})\big{)}$

for every $n\geq 0$. Thus, we have:

$\llbracket\psi\rrbracket\geq\lambda x.\lambda s\in S.\sup_{k\geq
0}\sum_{s_{0}s_{1}\dots s_{k}\in
S^{k+1},s_{0}=s}\big{(}x(s_{k})\cdot\prod_{0\leq j\leq
k-1}P(s_{j},s_{j+1})\big{)}.$

Actually, the equality holds, because the righthand side is a fixpoint of

$\lambda v\in D_{\mathit{Prop}\to\mathit{Prop}}.\lambda x\in
D_{\mathit{Prop}}.\lambda s\in S.\max(x\,s,v(\lambda s\in
S.\sum_{s^{\prime}}P(s,s^{\prime})\cdot(xs^{\prime}))).$

The semantics of $\phi$ is, therefore, given by

$\llbracket\phi\rrbracket=\lambda s\in S.\sup_{k\geq 0}\sum_{s_{0}s_{1}\dots
s_{k}\in S^{k+1},s_{0}=s,s_{k}\in\rho_{\mathit{AP}}(p)}\prod_{0\leq j\leq
k-1}P(s_{j},s_{j+1}).$

###  2.4. Expressive Power

PHFL obviously subsumes the $\mu^{p}$-calculus [CKP15], which coincides with
order-$0$ PHFL. Hence PHFL also subsumes PCTL [HJ94], since the
$\mu^{p}$-calculus subsumes PCTL [CKP15].

PHFL is _strictly_ more expressive than the $\mu^{p}$-calculus.

######  Theorem 2.6.

Order-1 PHFL is strictly more expressive than the $\mu^{p}$-calculus, i.e.,
there exists an order-1 PHFL proposition $\phi$ such that $\phi$ is not
equivalent to any $\mu^{p}$-formula.

######  Proof 2.7.

Let $\mathcal{M}$ be the set of Markov chains
$M=(S,P,\rho_{\mathit{AP}},s_{\text{in}})$ that satisfy the following
conditions.

  * •

$S=\\{s_{0},s_{1},\dots,s_{n}\\}$ for a positive integer $n$,

  * •

$P(s_{i},s_{i+1})=1$ ($0\leq i\leq n-1$), $P(s_{n},s_{n})=1$ and
$P(s_{i},s_{j})=0$ otherwise.

  * •

There are three atomic propositions $a,b,c$ with
$\rho_{\mathit{AP}}(a)\cup\rho_{\mathit{AP}}(b)=\\{s_{0},s_{1},\dots,s_{n-1}\\}$,
$\rho_{\mathit{AP}}(a)\cap\rho_{\mathit{AP}}(b)=\emptyset$ and
$\rho_{\mathit{AP}}(c)=\\{s_{n}\\}$.

  * •

The initial state is $s_{\text{in}}=s_{0}$.

Let $\phi$ be the order-1 PHFL formula of type ${\mathit{Prop}}$:

$(\mu F.\lambda X.a\land\lozenge(X\lor F(b\land\lozenge X)))(b\land\lozenge
c).$

Note that, for $M\in\mathcal{M}$, $M\models\phi$ holds just if $n$ is even,
$\rho_{\mathit{AP}}(a)=\\{s_{0},s_{1},\dots,s_{\frac{n}{2}-1}\\}$ and
$\rho_{\mathit{AP}}(b)=\\{s_{\frac{n}{2}},s_{\frac{n}{2}+1},\dots,s_{n-1}\\}$.

We show that there is no $\mu^{p}$-formula equivalent to $\phi$. Suppose that
a $\mu^{p}$-formula $\phi^{\prime}$ _were_ equivalent to $\phi$, which would
imply that $M\models\phi$ if and only if $M\models\phi^{\prime}$ for any
$M\in\mathcal{M}$. For $M\in\mathcal{M}$, let us write $K_{M}$ for the
embedded Kripke structure of $M$. Since all the transitions in ${M}$ are
deterministic, there exists a modal $\mu$-calculus formula
$\phi^{\prime\prime}$ such that $M\models\phi^{\prime}$ if and only if
$K_{M}\models\phi^{\prime\prime}$ (note that $\phi^{\prime\prime}$ is obtained
by replacing $\mathbin{\bigcirc}$ with $\lozenge$, and replacing
$[\phi_{1}]_{J}$ with true if $J$ is “$\geq 0$” and with $\phi_{1}$
otherwise). That would imply that $K_{M}\models\phi^{\prime\prime}$ for
$M\in\mathcal{M}$, just if $n$ is even and $\rho_{\mathit{AP}}$ satisfies
$\rho_{\mathit{AP}}(a)=\\{s_{0},s_{1},\dots,s_{\frac{n}{2}-1}\\}$ and
$\rho_{\mathit{AP}}(b)=\\{s_{\frac{n}{2}},s_{\frac{n}{2}+1},\dots,s_{n-1}\\}$.
But then $\phi^{\prime\prime}$ would describe the non-regular language
$\\{a^{m}b^{m}\mid m\geq 1\\}$, which contradicts the fact that the modal
$\mu$-calculus can express only regular properties.

######  Remark 2.8.

For non-probabilistic logics, HFL was known to be strictly more expressive
than the modal $\mu$-calculus [VV04]. The above proof can be easily adapted to
show that fact.

##  3\. Undecidability of PHFL Model Checking

In this section we prove the undecidability of the following problem.

######  Definition 3.1 (PHFL Model Checking).

The _PHFL model-checking problem_ for finite Markov chains is the problem of
deciding whether $M\models\phi$, given a (finite) Markov chain $M$ and a
closed PHFL formula $\phi$ of type ${\mathit{Prop}}$ as input.

We prove that the problem is undecidable even for the order-1 fragment of PHFL
without fixpoint alternations, by a reduction from the undecidability of the
value-1 problem [GO10] for probabilistic automata [Rab63]. In contrast to the
undecidability of PHFL model checking, the corresponding model-checking
problems are _decidable_ for the full fragments of the $\mu^{p}$-calculus
[CKP15] and (non-probabilistic) HFL [VV04], with fixpoint alternations. Thus,
the combination of probabilities and higher-order predicates introduces a new
difficulty.

In Section 3.1, we review the definition of probabilistic automata and the
value-1 problem. Section 3.2 shows the reduction from the value-1 problem to
the PHFL model-checking problem.

###  3.1. Probabilistic Automata

We review probabilistic automata [Rab63] and the undecidability of the value-1
problem. Our definition follows [Fij17].

######  Definition 3.2 (Probabilistic Automata).

A _probabilistic automaton_ $A$ is a quintuple $(Q,\Sigma,q_{I},\Delta,F)$
where

  * •

$Q$ is a finite set of states,

  * •

$\Sigma$ is a finite set of input symbols,

  * •

$q_{I}\in Q$ is an initial state,

  * •

$\Delta:Q\times\Sigma\to D(Q)$, where $D(Q):=\\{\,f\colon
Q\to[0,1]\mid\sum_{q\in Q}f(q)=1\,\\}$ is the set of probabilistic
distributions over the set $Q$, represents transition probabilities, and

  * •

$F\subseteq Q$ is a set of accepting states.

For a word $w=w_{1}\cdots w_{n}\in\Sigma^{n}$, the probability that $w$ is
accepted by $A=(Q,\Sigma,q_{I},\Delta,F)$, written $A(w)$, is defined by:

$A(w):=\sum_{\begin{subarray}{c}q_{0},\dots,q_{n-1}\in Q,q_{n}\in F\\\
\mathit{s.t.}\ q_{0}=q_{I}\end{subarray}}\,\prod_{1\leq i\leq
n}\Delta(q_{i-1},w_{i})(q_{i}).$

The _value_ of a probabilistic automaton $A$, denoted by $\text{val}(A)$, is
defined by

$\text{val}(A):=\sup_{w\in\Sigma^{\ast}}A(w).$

The problem of deciding whether $\text{val}(A)=1$, called the _value-1
problem_ , is known to be undecidable.

######  Theorem 3.2 (Undecidability of The Value-1 Problem [GO10]).

Given a probabilistic automaton $A$, whether $\text{val}(A)=1$ is undecidable.

###  3.2. The Undecidability Result

Let $A=(Q,\Sigma,q_{I},\Delta,F)$ be a probabilistic automaton, where
$\Sigma=\\{c_{1},\ldots,c_{|\Sigma|}\\}$ with $|\Sigma|>0$. We shall construct
a Markov chain $M_{A}$ and a PHFL formula $\phi_{A}$, so that
$\text{val}(A)=1$ if and only if $M_{A}\models\phi_{A}$. The undecidability of
PHFL model checking then follows immediately from Theorem 2.

We first construct the Markov chain $M_{A}$. The set $\mathit{AP}$ of atomic
propositions is $\\{\,p_{c}\mid c\in\Sigma\,\\}\uplus\\{\,p_{F}\,\\}$. The
Markov chain $M_{A}=(S,P,\rho_{\mathit{AP}},s_{\text{in}})$ is defined as
follows.

  * •

The set $S$ of states is $Q\uplus(Q\times\Sigma)$.

  * •

The transition probability $P$ is given by:

$\displaystyle P((q,c),q^{\prime})$ $\displaystyle=\Delta(q,c)(q^{\prime})$
($c\in\Sigma$ and $q,q^{\prime}\in Q$) $\displaystyle P(q,(q,c))$
$\displaystyle=\frac{1}{|\Sigma|}$ ($c\in\Sigma$ and $q\in Q$) $\displaystyle
P(s,s^{\prime})$ $\displaystyle=0$ (otherwise)

The first transition (from $(q,c)$ to $q^{\prime}$) is used to simulate the
transition of $A$ from $q$ to $q^{\prime}$ for the input symbol $c$. The
second transition (from $q$ to $(q,c)$) is used to choose the next input
symbol to be supplied to the automaton; the probability is not important, and
replacing $1/|\Sigma|$ with any non-zero probability does not affect the
arguments below.

  * •

$\rho_{\mathit{AP}}$ is defined by:

$\displaystyle\rho_{\mathit{AP}}(p_{c})$ $\displaystyle=\\{\,(q,c)\mid q\in
Q\,\\}$ $\displaystyle\rho_{\mathit{AP}}(p_{F})$ $\displaystyle=\\{\,q\mid
q\in F\,\\}.$

  * •

The initial state is $s_{\text{in}}=q_{I}$.

Intuitively, the Markov chain $M_{A}$ simulates the behavior of $A$. The
atomic proposition $p_{c}$ means that $A$ is currently reading the symbol $c$,
and $p_{F}$ means that $A$ is in a final state.

Based on this intuition, we now construct the PHFL formula $\phi_{A}$. For
each $c\in\Sigma$, we define a formula $f_{c}$ of type
$\mathit{Prop}\to\mathit{Prop}$ by:

$f_{c}:=\lambda X.\lozenge({p_{c}}\land\bigcirc X).$

Intuitively $f_{c}(\phi)$ denotes the probability that the automaton transits
to a state satisfying $\phi$ given $c$ as the next input. Given a word
$w=w_{1}w_{2}\dots w_{n}\in\Sigma^{*}$, we define the formula $g_{w}$ by

$g_{w}:=f_{w_{1}}(f_{w_{2}}(\dots(f_{w_{n}}{p_{F}})\dots)).$

We write $A_{q}$ for the automaton obtained from $A$ by replacing the initial
state with $q$. The following lemma states that $g_{w}$ represents the
probability that $w$ is accepted by the automaton from the current state $q$.

######  Lemma 3.3.

$A_{q}(w)=\llbracket g_{w}\rrbracket_{M_{A}}(q)$ for every $q\in Q$.

######  Proof 3.4.

Let $A=(Q,\Sigma,q_{I},\Delta,F)$. The proof proceeds by induction on the
length $|w|$ of $w$.

  * •

Case where $|w|=0$, i.e., $w=\epsilon$: By the definition of $A_{q}$,
$A_{q}(\epsilon)=1$ if $q\in F$ and $0$ otherwise. We have the required
result, as $g_{\epsilon}={p_{F}}$.

  * •

Case where $|w|>0$: Let $w=w_{1}\cdots w_{n}=w_{1}w^{\prime}$. We have:

$\displaystyle A_{q}(w)$
$\displaystyle=\sum_{\begin{subarray}{c}q_{0},\dots,q_{n-1}\in Q,q_{n}\in
F\;\mathit{s.t.}\ q_{0}=q\end{subarray}}\,\prod_{1\leq i\leq
n}\Delta(q_{i-1},w_{i})(q_{i})$ $\displaystyle=\sum_{q^{\prime}\in
Q}\Delta(q,w_{1})(q^{\prime})\cdot(\sum_{\begin{subarray}{c}q_{1}\dots,q_{n-1}\in
Q,q_{n}\in F\;\mathit{s.t.}\ q_{1}=q^{\prime}\end{subarray}}\,\prod_{2\leq
i\leq n}\Delta(q_{i-1},w_{i})(q_{i}))$ $\displaystyle=\sum_{q^{\prime}\in
Q}\Delta(q,w_{1})(q^{\prime})\cdot A_{q^{\prime}}(w^{\prime}).$

Since $g_{w}=f_{w_{1}}(g_{w^{\prime}})\equiv\lozenge({p_{w_{1}}}\land\bigcirc
g_{w^{\prime}})$, we have:

$\displaystyle\llbracket g_{w}\rrbracket_{M_{A}}(q)$
$\displaystyle=\max_{c\in\Sigma}\llbracket{p_{w_{1}}}\land\bigcirc
g_{w^{\prime}}\rrbracket(q,c)$ $\displaystyle=\llbracket\bigcirc
g_{w^{\prime}}\rrbracket(q,w_{1})$ $\displaystyle=\sum_{q^{\prime}\in
Q}\Delta(q,w_{1})(q^{\prime})\cdot\llbracket
g_{w^{\prime}}\rrbracket(q^{\prime})$

By the induction hypothesis, we have $A_{q^{\prime}}(w^{\prime})=\llbracket
g_{w^{\prime}}\rrbracket(q^{\prime})$, which implies the the required result.

Using Lemma 3.3, we obtain
$\text{val}(A)=\sup_{n\in\omega}\llbracket\bigvee_{w\in\Sigma^{\leq
n}}g_{w}\rrbracket_{M_{A}}(q_{I})$, where $\Sigma^{\leq n}$ is the set of
words of length up to $n$. This can be expressed by using the least fixpoint
operator.

######  Theorem 3.4.

Let $\theta_{A}$ be the formula of type
$\mathit{Prop}\rightarrow\mathit{Prop}$ defined by:

$\theta_{A}:=\mu F.\big{(}\lambda
X.X\lor\bigvee_{c\in\Sigma}F\,(f_{c}\,X)\big{)}.$

Then $\text{val}(A)=\llbracket\theta_{A}\,{p_{F}}\rrbracket_{M_{A}}(q_{I})$.
Therefore $M_{A}\models\phi_{A}$ if and only if $\text{val}(A)=1$, for
$\phi_{A}:=[\theta_{A}\,{p_{F}}]_{\geq 1}$.

######  Proof 3.5.

Let

$\xi:=\lambda F.\lambda X.X\vee\bigvee_{c\in\Sigma}F\,(f_{c}\,X).$

Then, we have

$\llbracket\theta_{A}\rrbracket_{M}\quad=\quad\llbracket\mu
F.\xi\,F\rrbracket_{M}\quad=\quad\mathbin{\textstyle{\bigsqcup_{\mathit{Prop}\to\mathit{Prop}}}}\\{\llbracket\xi^{n}(\bot)\rrbracket\mid
n\in\omega\\}$

where $\bot:=\lambda Z.\mu U.U$ is the formula of type
$\mathit{Prop}\to\mathit{Prop}$, and $\xi^{n}(x)$ denotes $n$-times
applications of $\xi$ to $x$. In fact,
$\mathbin{\textstyle{\bigsqcup_{\mathit{Prop}\to\mathit{Prop}}}}\\{\llbracket\xi^{n}(\bot)\rrbracket\mid
n\in\omega\\}$ is a fixpoint of $\llbracket\xi\rrbracket$, because:

$\displaystyle\llbracket\xi\rrbracket(\mathbin{\textstyle{\bigsqcup_{\mathit{Prop}\to\mathit{Prop}}}}\\{\llbracket\xi^{n}(\bot)\rrbracket\mid
n\in\omega\\})$ $\displaystyle=\lambda x\in
D_{\mathit{Prop}}.x\mathbin{\textstyle{\bigsqcup_{\mathit{Prop}}}}\big{(}\mathbin{\textstyle{\bigsqcup}}_{c\in\Sigma}(\mathbin{\textstyle{\bigsqcup_{\mathit{Prop}\to\mathit{Prop}}}}\\{\llbracket\xi^{n}(\bot)\rrbracket\mid
n\in\omega\\})(\llbracket f_{c}\rrbracket\;x)\big{)}$ $\displaystyle=\lambda
x\in
D_{\mathit{Prop}}.x\mathbin{\textstyle{\bigsqcup_{\mathit{Prop}}}}\big{(}\mathbin{\textstyle{\bigsqcup}}_{c\in\Sigma}(\mathbin{\textstyle{\bigsqcup_{\mathit{Prop}}}}\\{\llbracket\xi^{n}(\bot)\rrbracket(\llbracket
f_{c}\rrbracket\;x)\mid n\in\omega\\})\big{)}$ $\displaystyle=\lambda x\in
D_{\mathit{Prop}}.\mathbin{\textstyle{\bigsqcup_{\mathit{Prop}}}}\\{x\mathbin{\textstyle{\bigsqcup_{\mathit{Prop}}}}\big{(}\mathbin{\textstyle{\bigsqcup}}_{c\in\Sigma}\llbracket\xi^{n}(\bot)\rrbracket(\llbracket
f_{c}\rrbracket\;x)\big{)}\mid n\in\omega\\}$
$\displaystyle=\mathbin{\textstyle{\bigsqcup_{\mathit{Prop}\to\mathit{Prop}}}}\\{\llbracket\xi^{n+1}(\bot)\rrbracket\mid
n\in\omega\\}.$

Since $\llbracket\xi\rrbracket$ is monotonic and $\llbracket\bot\rrbracket$ is
the least element, we also have:

$\llbracket\mu F.\xi\,F\rrbracket_{M}=\llbracket\xi^{n}(\mu
F.\xi\,F)\rrbracket\sqsupseteq\llbracket\xi^{n}(\bot)\rrbracket$

for any $n\in\omega$ hence also

$\llbracket\mu
F.\xi\,F\rrbracket_{M}\sqsupseteq\mathbin{\textstyle{\bigsqcup_{\mathit{Prop}\to\mathit{Prop}}}}\\{\llbracket\xi^{n}(\bot)\rrbracket\mid
n\in\omega\\}.$

Thus, we have the equality.

By a straightforward induction on $n$, we also have:
$\llbracket\xi^{n+1}(\bot)\,{p_{F}}\rrbracket_{M}=\llbracket\bigvee_{w\in\Sigma^{\leq
n}}g_{w}\rrbracket_{M}$. Therefore, by using also Lemma 3.3, we obtain:

$\text{val}(A)\quad=\quad\sup_{n}(\llbracket\bigvee_{w\in\Sigma^{\leq
n}}g_{w}\rrbracket_{M_{A}}(q_{I}))\quad=\quad\sup_{n}(\llbracket\xi^{n+1}(\bot){p_{F}}\rrbracket(q_{I}))\quad=\quad\llbracket\theta_{A}\,{p_{F}}\rrbracket_{M_{A}}(q_{I}),$

which implies the required result.

The following is an immediate corollary of Theorems 2 and 3.

######  Corollary 3.6 (Undecidability of PHFL Model-Checking Problem).

There is no algorithm that, given a Markov chain $M$ and a closed order-1
formula $\phi$ of type ${\mathit{Prop}}$, decides whether $M\models\phi$.

We close this section with some remarks.111We would like to thank an anonymous
reviewer of our FSCD 2020 submission for pointing them out.

######  Remark 3.7.

Note that the value $\text{val}(A)$ of a probabilistic automaton cannot even
be approximately computed [Fij17]: there is no algorithm that outputs “Yes” if
$\text{val}(A)=1$ and “No” if $\text{val}(A)\leq\frac{1}{2}$. Thus, the proof
of Theorem 3 (in particular, the result
$\text{val}(A)=\llbracket\theta_{A}\,{p_{F}}\rrbracket_{M_{A}}(q_{I})$) also
implies that for a qualitative formula of PHFL $\psi$,
$\llbracket\psi\rrbracket$ is not approximately computable in general.

######  Remark 3.8.

It would be interesting to study a converse encoding, i.e., to find an
encoding of some fragment of the PHFL model checking problem into the value-1
problem. Such an encoding may help us find a decidable class of the PHFL model
checking problem, based on decidable subclasses for the value-1 problem, such
as the one studied in [FGKO15].

##  4\. Hardness of the PHFL Model-Checking Problem

In the previous section, we have seen that PHFL model checking is undecidable
even for the fragment of PHFL without fixpoint alternations. In this section,
we give a lower bound of the hardness of the PHFL model-checking problem in
the presence of fixpoint alternations. The following theorem states the main
result of this section.

######  Theorem 4.0.

The order-1 PHFL model-checking problem is $\Pi^{1}_{1}$-hard and
$\Sigma^{1}_{1}$-hard.

Note that $\Pi^{1}_{1}$ and $\Sigma^{1}_{1}$, defined in terms of the second-
order arithmetic, contain very hard problems. For example, those classes
contain the problem of deciding whether a given first-order Peano arithmetic
formula is true.

We prove this theorem by reducing the validity checking problem of the
$\mu$-arithmetic [Lub89] to the PHFL model-checking problem. Even the validity
checking problem of a higher-order extension of the $\mu$-arithmetic can be
reduced to the PHFL model-checking problem. The key in the proof is a
representation of natural numbers as quantitative propositions such that all
the operations on natural numbers in the $\mu$-arithmetic are expressible in
PHFL.

This section is structured as follows. Section 4.1 reviews the basic notions
of the $\mu$-arithmetic. Section 4.2 describes the reduction and proves the
theorem above.

###  4.1. Higher-Order Fixpoint Arithmetic

The $\mu$-arithmetic [Lub89] is a first-order arithmetic with fixpoint
operators. This section briefly reviews its higher-order extension, studied by
Kobayashi et al. [KTW18].

As in PHFL, we first define the types of $\mu$-arithmetic formulas. The set of
_types_ , ranged over by $A$, is given by:

$\displaystyle A$ $\displaystyle::=N\,|\,T$ $\displaystyle T$
$\displaystyle::=\Omega\,|\,A\to T.$

The type $N$ is for natural numbers, $\Omega$ for (qualitative) propositions,
and $A\to T$ for functions. We do not allow functions to return values of type
$N$. We define the order of types of the $\mu$-arithmetic similarly to the
PHFL types, by: $\mathit{order}(N)=\mathit{order}(\Omega)=0$ and
$\mathit{order}(A\to T)=\max(\mathit{order}(A)+1,\mathit{order}(T))$.

Assume a countably infinite set $\mathit{Var}$ of variables ranged over by
$X$. The set of formulas, ranged over by $\varphi$, is given by the following
grammar.

$\displaystyle s$ $\displaystyle::=X\,|\,Z\,|\,Ss$ $\displaystyle\varphi$
$\displaystyle::=s\,|\,s_{1}\leq
s_{2}\,|\,\varphi_{1}\land\varphi_{2}\,|\,\varphi_{1}\lor\varphi_{2}\,|\,\lambda
X.\varphi\,|\,\varphi_{1}\,\varphi_{2}\,|\,\mu X.\varphi\,|\,\nu X.\varphi.$

Here, $Z$ and $S$ respectively denote the constant $0$ and the successor
function on natural numbers.

$\Gamma,X\mathbin{:}A\vdash_{\mu}X:A$

$\Gamma\vdash_{\mu}Z:N$

$\Gamma\vdash_{\mu}s:N$ $\Gamma\vdash_{\mu}S\,s:N$

$\Gamma\vdash_{\mu}s:N$ $\Gamma\vdash_{\mu}t:N$ $\Gamma\vdash_{\mu}s\leq
t:\Omega$

$\Gamma\vdash_{\mu}\varphi_{1}:\Omega$ $\Gamma\vdash_{\mu}\varphi_{2}:\Omega$
$\Gamma\vdash_{\mu}\varphi_{1}\land\varphi_{2}:\Omega$

$\Gamma\vdash_{\mu}\varphi_{1}:\Omega$ $\Gamma\vdash_{\mu}\varphi_{2}:\Omega$
$\Gamma\vdash_{\mu}\varphi_{1}\lor\varphi_{2}:\Omega$

$\Gamma,X:A\vdash_{\mu}\varphi:T$ $\Gamma\vdash_{\mu}\lambda
X.\varphi:A\rightarrow T$

$\Gamma\vdash_{\mu}\varphi_{1}:A\rightarrow T$
$\Gamma\vdash_{\mu}\varphi_{2}:A$ $\Gamma\vdash_{\mu}\varphi\,\varphi_{2}:T$

$\Gamma,X:T\vdash_{\mu}\varphi:T$ $\Gamma\vdash_{\mu}\mu X.\varphi:T$

$\Gamma,X:T\vdash_{\mu}\varphi:T$ $\Gamma\vdash_{\mu}\nu x.\varphi:T$

Figure 2. Typing Rules for the Higher-order Fixpoint Arithmetic.

The typing rules are shown in Fig. 2; they are just standard typing rules for
the simply-typed $\lambda$-calculus, with several constructors such as
$Z\mathbin{:}N$, $S\mathbin{:}N\to N$, and $\land:\Omega\to\Omega$. We shall
consider only well-typed formulas. We define the _order_ of a formula as the
largest order of the types of its subformulas.

######  Definition 4.1 (Semantics of Types).

The semantics of a type $A$ is a partially ordered set $\llbracket
A\rrbracket_{\mu}=(D_{A},\sqsubseteq_{A})$ defined inductively on the
structure of $A$ as follows.

  1. (1)

The semantics of $N$ and $\Omega$:

$\displaystyle D_{N}$ $\displaystyle=\mathbb{N}$ $\displaystyle
n\sqsubseteq_{N}m$ $\displaystyle\overset{\text{def}}{\Longleftrightarrow}n=m$
$\displaystyle D_{\Omega}$ $\displaystyle=\\{0,1\\}$ $\displaystyle
p\sqsubseteq_{\Omega}q$
$\displaystyle\overset{\text{def}}{\Longleftrightarrow}p\leq q$

  2. (2)

The semantics of $A\to T$:

$\displaystyle D_{A\to T}$ $\displaystyle=\\{\,f:D_{A}\to D_{T}\mid\forall
u,v\in D_{A}.u\sqsubseteq_{A}v\implies f(u)\sqsubseteq_{T}f(v)\,\\}$
$\displaystyle f\sqsubseteq_{A\to T}g$
$\displaystyle\overset{\text{def}}{\Longleftrightarrow}\forall v\in
D_{A}.f(v)\sqsubseteq_{T}g(v)$

The semantics $\llbracket T\rrbracket_{\mu}$ of a type $T$ forms a complete
lattice (while $\llbracket N\rrbracket_{\mu}$ is not); we write
$\mathbin{\textstyle{\bigsqcup_{T}}}$ (resp. $\textstyle{\bigsqcap_{T}}$) for
the least upper bound (resp. greatest lower bound) operation, and $\bot_{T}$
for the least element.

The interpretation $\llbracket\Gamma\rrbracket_{\mu}$ of a type environment
$\Gamma$ is the set of functions $\theta$ such that
$\mathit{dom}(\theta)=\mathit{dom}(\Gamma)$ and that
$\theta(X)\in\llbracket\Gamma(X)\rrbracket_{\mu}$ for every
$X\in\mathit{dom}(\Gamma)$. It is ordered by the point-wise ordering.

######  Definition 4.2 (Semantics of Formulas).

The semantics of a formula $\varphi$ with judgment
$\Gamma\vdash_{\mu}\varphi:A$ is a monotone map from
$\llbracket\Gamma\rrbracket_{\mu}$ to $\llbracket A\rrbracket_{\mu}$, defined
as follows.

$\displaystyle\llbracket\Gamma\vdash_{\mu}X:A\rrbracket_{\mu}(\theta)$
$\displaystyle:=\theta(X)$
$\displaystyle\llbracket\Gamma\vdash_{\mu}Z:N\rrbracket_{\mu}(\theta)$
$\displaystyle:=0$
$\displaystyle\llbracket\Gamma\vdash_{\mu}Ss:N\rrbracket_{\mu}(\theta)$
$\displaystyle:=\llbracket\Gamma\vdash_{\mu}s:N\rrbracket_{\mu}(\theta)+1$
$\displaystyle\llbracket\Gamma\vdash_{\mu}s\leq
t:\Omega\rrbracket_{\mu}(\theta)$ $\displaystyle:=\begin{cases}1&\mbox{(if
$\llbracket\Gamma\vdash_{\mu}s:N\rrbracket_{\mu}(\theta)\leq\llbracket\Gamma\vdash_{\mu}t:N\rrbracket_{\mu}(\theta)$)}\\\
0&\mbox{(if
$\llbracket\Gamma\vdash_{\mu}s:N\rrbracket_{\mu}(\theta)>\llbracket\Gamma\vdash_{\mu}t:N\rrbracket_{\mu}(\theta)$)}\end{cases}$
$\displaystyle\llbracket\Gamma\vdash_{\mu}\varphi_{1}\land\varphi_{2}:\Omega\rrbracket_{\mu}(\theta)$
$\displaystyle:=\llbracket\Gamma\vdash_{\mu}\varphi_{1}:\Omega\rrbracket_{\mu}(\theta)\mathbin{\textstyle{\bigsqcup_{\Omega}}}\llbracket\Gamma\vdash_{\mu}\varphi_{2}:\Omega\rrbracket_{\mu}(\theta)$
$\displaystyle\llbracket\Gamma\vdash_{\mu}\varphi_{1}\lor\varphi_{2}:\Omega\rrbracket_{\mu}(\theta)$
$\displaystyle:=\llbracket\Gamma\vdash_{\mu}\varphi_{1}:\Omega\rrbracket_{\mu}(\theta)\textstyle{\bigsqcap_{\Omega}}\llbracket\Gamma\vdash_{\mu}\varphi_{2}:\Omega\rrbracket_{\mu}(\theta)$
$\displaystyle\llbracket\Gamma\vdash_{\mu}\lambda X.\varphi:A\to
T\rrbracket_{\mu}(\theta)$ $\displaystyle:=\lambda v\in\llbracket
A\rrbracket_{\mu}.\llbracket\Gamma,X:A\vdash_{\mu}\varphi:T\rrbracket_{\mu}(\theta[X\mapsto
v])$
$\displaystyle\llbracket\Gamma\vdash_{\mu}\varphi_{1}\,\varphi_{2}:T\rrbracket_{\mu}(\theta)$
$\displaystyle:=\llbracket\Gamma\vdash_{\mu}\varphi_{1}:A\to
T\rrbracket_{\mu}(\theta)\,(\llbracket\Gamma\vdash_{\mu}\varphi_{2}:A\rrbracket_{\mu}(\theta))$
$\displaystyle\llbracket\Gamma\vdash_{\mu}\mu
X.\varphi:T\rrbracket_{\mu}(\theta)$ $\displaystyle:=\mathit{LFP}(\lambda v\in
D_{T}.\llbracket\Gamma,X:T\vdash_{\mu}\varphi:T\rrbracket(\theta[X\mapsto
v]))$ $\displaystyle\llbracket\Gamma\vdash_{\mu}\nu
X.\varphi:T\rrbracket_{\mu}(\theta)$ $\displaystyle:=\mathit{GFP}(\lambda v\in
D_{T}.\llbracket\Gamma,X:T\vdash_{\mu}\varphi:T\rrbracket(\theta[X\mapsto
v]))$

As in the case of PHFL, we write $\llbracket\varphi\rrbracket_{\mu}(\theta)$
for $\llbracket\Gamma\vdash_{\mu}\varphi:A\rrbracket_{\mu}(\theta)$ and just
$\llbracket\varphi\rrbracket_{\mu}$ for
$\llbracket\varphi\rrbracket_{\mu}(\emptyset)$ when there is no confusion.

######  Example 4.3.

Let $\varphi=\mu F.\lambda X.(X=100\lor F(S(S\,X)))$ where $100$ is an
abbreviation of the term $\underbrace{S(S(\dots S}_{100}\,Z)\dots)$. The
semantics $\llbracket\varphi\rrbracket_{\mu}$ is a function
$f:\mathbb{N}\to\\{0,1\\}$ where $f(n)=1$ just if $n$ is an even number no
greater than $100$.

The _validity checking problem_ of the higher-order fixpoint arithmetic is the
problem of, given a closed formula $\varphi$ of type $\Omega$, deciding
whether $\llbracket\varphi\rrbracket_{\mu}=1$. The following result is
probably folklore, which follows from the well-known fact that the _fair
termination problem for programs_ is $\Pi^{1}_{1}$-complete (see, e.g., Harel
[Har86]), and the fact that the fair termination of a program can be reduced
to the validity of a first-order fixpoint arithmetic formula (see, e.g.,
[KTW18] for the reduction).

######  Theorem 4.3.

The validity checking problem of the first-order fixpoint arithmetic is
$\Pi^{1}_{1}$-hard and $\Sigma^{1}_{1}$-hard.

######  Remark 4.4.

As for an upper bound, Lubarsky [Lub89] has shown that predicates on natural
numbers definable by $\mu$-arithmetic formulas belong to $\Delta^{1}_{2}$. One
can prove that the validity problem for the $\mu$-arithmetic is
$\Delta^{1}_{2}$ as well.

###  4.2. Hardness of PHFL Model Checking

We give a reduction from the validity checking problem of the higher-order
fixpoint arithmetic to the PHFL model-checking problem. The main theorem of
this section (Theorem 4) is an immediate consequence of this reduction and
Theorem 5.

Given a formula $\varphi$ of the higher-order fixpoint arithmetic, we need to
effectively construct a pair $(\phi,M)$ of a formula of PHFL and a Markov
chain such that $\varphi$ is true if and only if $M\models\phi$. The Markov
chain $M$ is independent of the formula $\varphi$. We first define the Markov
chain and then explain the intuition of the translation of formulas.

The Markov chain $M=(S,P,\rho_{\mathit{AP}},s_{\text{in}})$ is shown in Figure
3. It is defined as follows.

  * •

The set of states is $S=\\{s_{0},s^{\prime}_{0},s_{1},s_{1}^{\prime}\\}$.

  * •

The transition probability satisfies
$P(s_{0},s_{1})=P(s_{0},s^{\prime}_{0})=P(s^{\prime}_{0},s_{0})=P(s^{\prime}_{0},s_{1}^{\prime})=\frac{1}{2}$,
$P(s_{1},s_{0})=P(s_{1}^{\prime},s^{\prime}_{0})=1$ and $P(s_{i},s_{j})=0$ for
all other pairs of states.

  * •

There are four atomic propositions $p_{0},p_{0}^{\prime},p_{1}$, and
$p_{1}^{\prime}$, representing each state (e.g.
$\rho_{\mathit{AP}}(p_{0})=\\{s_{0}\\}$).

  * •

The initial state $s_{\text{in}}$ is $s_{0}$.

$s^{\prime}_{0}$$s_{0}$$s_{1}^{\prime}$$s_{1}$$0.5$$0.5$$0.5$$1$$0.5$$1$
Figure 3. The Markov Chain for Reduction from Higher-order Fixpoint Arithmetic
to PHFL.

For notational convenience, we write
$v\in\llbracket\mathit{Prop}\rrbracket_{M}$ as a tuple
$(v(s_{0}),v(s^{\prime}_{0}),v(s_{1}),v(s_{1}^{\prime}))$.

As mentioned at the beginning of this section, the key of the reduction is the
representation of natural numbers, as well as operations on natural numbers.
We encode a propositional formula $\varphi$ into a quantitative propositional
formula $\phi$ such that
$\llbracket\phi\rrbracket_{M}=(\llbracket\varphi\rrbracket_{\mu},\\_,\\_,\\_)$,
and encode a natural number $n$ into a quantitative propositional formula
$\psi$ such that
$\llbracket\phi\rrbracket_{M}=(\frac{1}{2^{n}},1-\frac{1}{2^{n}},\\_,\\_)$.
Here, $\\_$ denotes a “don’t care” value. We implement primitives on natural
numbers $Z$, $S$ and $\leq$, as follows.

The constant $Z$ can be represented by ${p_{0}}$. Indeed,
$\llbracket{p_{0}}\rrbracket_{M}=(1,0,0,0)=(1/2^{0},1-(1/2^{0}),0,0)$ as
expected.

Assuming that $\phi$ represents $n$ (i.e.
$\llbracket\phi\rrbracket_{M}=(1/2^{n},1-(1/2^{n}),\\_,\\_)$), the successor
$n+1$ can be represented by

$\phi^{\prime}\quad:=\quad\bigcirc((\bigcirc\phi\land(p_{1}\lor
p_{1}^{\prime}))\lor p_{0}).$

Indeed, we have:

$\displaystyle\llbracket\bigcirc\phi\rrbracket_{M}$
$\displaystyle=(\\_,\\_,\frac{1}{2^{n}},1-\frac{1}{2^{n}})$
$\displaystyle\llbracket\bigcirc\phi\land(p_{1}\lor
p_{1}^{\prime})\rrbracket_{M}$
$\displaystyle=(0,0,\frac{1}{2^{n}},1-\frac{1}{2^{n}})$
$\displaystyle\llbracket(\bigcirc\phi\land(p_{1}\lor p_{1}^{\prime}))\lor
p_{0}\rrbracket_{M}$ $\displaystyle=(1,0,\frac{1}{2^{n}},1-\frac{1}{2^{n}})$
$\displaystyle\llbracket\bigcirc((\bigcirc\phi\land(p_{1}\lor
p_{1}^{\prime}))\lor p_{0})\rrbracket_{M}$
$\displaystyle=(\frac{1}{2}\times\frac{1}{2^{n}},\frac{1}{2}+\frac{1}{2}\times(1-\frac{1}{2^{n}}),\\_,\\_)$
$\displaystyle=(\frac{1}{2^{n+1}},1-\frac{1}{2^{n+1}},\\_,\\_).$

It remains to encode $\leq$. We use the fact that, for any natural numbers $n$
and $m$,

$n\leq
m\quad\Leftrightarrow\quad\frac{1}{2^{n}}\geq\frac{1}{2^{m}}\quad\Leftrightarrow\quad\frac{1}{2^{n}}+(1-\frac{1}{2^{m}})\geq
1.$

The $s_{0}^{\prime}$-component of the representation of a natural number plays
an important role below. Assume that $\phi$ and $\chi$ represent $n$ and $m$
respectively. Then we have

$\llbracket\bigcirc\phi\land
p_{1}\rrbracket_{M}=(0,0,\frac{1}{2^{n}},0)\qquad\llbracket\chi\land
p_{0}^{\prime}\rrbracket_{M}=(0,1-\frac{1}{2^{m}},0,0)$

and thus

$\llbracket(\bigcirc\phi\land p_{1})\lor(\chi\land
p_{0}^{\prime})\rrbracket_{M}=(0,1-\frac{1}{2^{m}},\frac{1}{2^{n}},0).$

Therefore

$\llbracket\bigcirc((\bigcirc\phi\land p_{1})\lor(\chi\land
p_{0}^{\prime}))\rrbracket_{M}=(\frac{1}{2}\times\big{(}\frac{1}{2^{n}}+(1-\frac{1}{2^{m}})\big{)},\\_,\\_,\\_).$

Thus, $n\leq m$ if and only if the $s_{0}$-component of the above formula is
$\geq\frac{1}{2}$. In other words, $n\leq m$ just if:

$\llbracket[\bigcirc((\bigcirc\phi\land p_{1})\lor(\chi\land
p_{0}^{\prime}))]_{\frac{1}{2}}\rrbracket_{M}=(1,\\_,\\_,\\_).$

Let us formalize the above argument. We first give the translation of types:

$\displaystyle\textit{tr}(N)$ $\displaystyle=\mathit{Prop}$
$\displaystyle\textit{tr}(\Omega)$ $\displaystyle={\mathit{Prop}}$
$\displaystyle\textit{tr}(A\to T)$
$\displaystyle=\textit{tr}(A)\to\textit{tr}(T).$

The translation can be naturally extended to type environments. Following the
above discussion, the translation of formulas of type $N$ is given by

$\textit{tr}(Z)={p_{0}}\qquad\mbox{and}\qquad\textit{tr}(S\,s)=\bigcirc((\bigcirc\textit{tr}(s)\land(p_{1}\lor
p_{1}^{\prime}))\lor p_{0}).$

The comparison operator can be translated as follows:

$\textit{tr}(s\leq t)=[\bigcirc((\bigcirc\textit{tr}(s)\land
p_{1})\lor(\textit{tr}(t)\land p_{0}^{\prime}))]_{\geq\frac{1}{2}}.$

The translation of other connectives is straightforward:

$\displaystyle\textit{tr}(\varphi_{1}\land\varphi_{2})=\textit{tr}(\varphi_{1})\land\textit{tr}(\varphi_{2})\qquad\textit{tr}(\varphi_{1}\lor\varphi_{2})=\textit{tr}(\varphi_{1})\lor\textit{tr}(\varphi_{2})\qquad\textit{tr}(\lambda
X.\varphi)=\lambda X.\textit{tr}(\varphi)$
$\displaystyle\textit{tr}(X)=X\qquad\textit{tr}(\varphi_{1}\,\varphi_{2})=\textit{tr}(\varphi_{1})\,\textit{tr}(\varphi_{2})\qquad\textit{tr}(\mu
X.\varphi)=\mu X.\textit{tr}(\varphi)\qquad\textit{tr}(\nu X.\varphi)=\nu
X.\textit{tr}(\varphi).$

The following lemma states that the translation preserves types.

######  Lemma 4.5.

If $\Gamma\vdash_{\mu}\varphi:A$, then
$\textit{tr}(\Gamma)\vdash\textit{tr}(\varphi):\textit{tr}(A)$.

######  Proof 4.6.

This follows by straightforward induction on the derivation of
$\Gamma\vdash_{\mu}\varphi:A$.

We prove the correctness of the translation. For each type $A$ of the higher-
order fixpoint arithmetic, we define a relation
$({\sim_{A}})\subseteq\llbracket
A\rrbracket_{\mu}\times\llbracket\textit{tr}(A)\rrbracket_{M}$ by induction on
$A$ as follows:

$\displaystyle n\sim_{N}(r_{0},r_{0}^{\prime},r_{1},r_{1}^{\prime})$
$\displaystyle\quad\overset{\text{def}}{\Longleftrightarrow}\quad
r_{0}=\frac{1}{2^{n}}\mbox{ and }r_{0}^{\prime}=1-\frac{1}{2^{n}}$
$\displaystyle b\sim_{\Omega}(r_{0},r_{0}^{\prime},r_{1},r_{1}^{\prime})$
$\displaystyle\quad\overset{\text{def}}{\Longleftrightarrow}\quad b=r_{0}$
$\displaystyle f\sim_{A\to T}g$
$\displaystyle\quad\overset{\text{def}}{\Longleftrightarrow}\quad\forall
x\in\llbracket A\rrbracket_{\mu}.\forall
y\in\llbracket\textit{tr}(A)\rrbracket_{M}.\;x\sim_{A}y\implies
f\,x\sim_{T}g\,y.$

This relation can be naturally extended to the interpretations of type
environments: given a type environment $\Gamma$ of the $\mu$-arithmetic, the
relation
$({\sim_{\Gamma}})\subseteq\llbracket\Gamma\rrbracket_{\mu}\times\llbracket\textit{tr}(\Gamma)\rrbracket_{M}$
is defined by

$\theta\sim_{\Gamma}\rho\quad\overset{\text{def}}{\Longleftrightarrow}\quad\forall
X\in\mathit{dom}(\Gamma).\;\theta(X)\sim_{\Gamma(X)}\rho(X).$

The following theorem states the correspondence between the source and the
target of the translation. A proof is provided in Appendix A.

######  Theorem 4.6.

Let $\Gamma\vdash_{\mu}\varphi:A$ be a formula of the higher-order fixpoint
arithmetic. Assume $\theta\in\llbracket\Gamma\rrbracket_{\mu}$ and
$\rho\in\llbracket\textit{tr}(\Gamma)\rrbracket$. If
$\theta\sim_{\Gamma}\rho$, then
$\llbracket\Gamma\vdash_{\mu}\varphi:A\rrbracket_{\mu}(\theta)\sim_{A}\llbracket\textit{tr}(\Gamma)\vdash\textit{tr}(\varphi):\textit{tr}(A)\rrbracket_{M}(\rho)$.

######  Corollary 4.7.

The validity problem of the order-$k$ fixpoint arithmetic is reducible to the
order-$k$ PHFL model-checking problem.

######  Proof 4.8.

Assume $\emptyset\vdash_{\mu}\varphi:\Omega$. By Theorem 6,
$\llbracket\varphi\rrbracket_{\mu}\sim_{\Omega}\llbracket\textit{tr}(\varphi)\rrbracket_{M}$.
Therefore, $\llbracket\varphi\rrbracket_{\mu}=1$ if and only if
$\llbracket\textit{tr}(\varphi)\rrbracket_{M}(s_{0})=1$, i.e.
$M\models\textit{tr}(\varphi)$. The mapping
$\varphi\mapsto(\textit{tr}(\varphi),M)$ is obviously effective, and preserves
the order.

Theorem 4 is an immediate consequence of Theorem 5 and Corollary 4.7.

##  5\. Decidable Subclass of Order-1 PHFL Model Checking

As we have seen in Section 3, PHFL model checking is undecidable, even for
order 1. In this section, we identify a decidable subclass of the order-1 PHFL
model-checking problems (i.e., a set of pairs $(\phi,M)$ such that whether
$M{\models}\phi$ is decidable). We identify the subclass by using a type
system: we define a type system $\mathcal{T}_{M}$ for PHFL formulas,
parameterized by $M$, so that if $\phi$ is a proposition well-typed in
$\mathcal{T}_{M}$, then $M{\models}\phi$ is decidable.

This section is structured as follows. In Section 5.1, we introduce the type
system $\mathcal{T}_{M}$, and prove that the semantics of any order-1 well-
typed formula is an affine function. Section 5.2 introduces a matrix
representation of affine functions and shows the decidability of
$M{\models}\phi$ by appealing to the decidability of the first-order theory of
reals [Tar51]. Section 5.3 shows that the restricted fragment is reasonably
expressive, by giving an encoding of the termination problem for recursive
Markov chains into the restricted fragment of PHFL model checking.

###  5.1. Type-based Restriction of Order-1 PHFL

We first explain the idea of the restriction imposed by our type system. By
definition, the semantics of a (closed) order-$1$ PHFL formula $\phi$ of type
$\mathit{Prop}\to\mathit{Prop}$ with respect to the Markov chain $M$ is a map
$f_{\phi}$ from the set of functions $S\to[0,1]$ to the same set, where $S$ is
the set of states of $M$. Thus, if $S=\\{s_{1},s_{2},\dots,s_{n}\\}$ is fixed,
$f_{\phi}$ can be regarded as a function from $[0,1]^{n}$ to $[0,1]^{n}$. Now,
if the function $f_{\phi}$ were affine, i.e., if there are functions
$f_{1},f_{2},\dots,f_{n}$ such that
$f_{\phi}(r_{1},r_{2},\dots,r_{n})=(f_{1}(r_{1},r_{2},\dots,r_{n}),\dots,f_{n}(r_{1},r_{2},\dots,r_{n}))$,
where $f_{i}(r_{1},r_{2},\dots,r_{n})=c_{i,0}+c_{i,1}r_{1}+\dots+c_{i,n}r_{n}$
for some real numbers $c_{i,j}$, then the function $f_{\phi}$ would be
representable by a finite number of reals $c_{i,j}$. The semantics of a
fixpoint formula would then be given as a solution of a fixpoint equation on
the coefficients, which is solvable by appealing to the decidability of first-
order theories of reals [Tar51].

Based on the observation above, we introduce a type system to restrict the
formulas so that the semantics of every well-typed order-$1$ formula is
affine. The conjunction $\phi_{1}\land\phi_{2}$ is one of the problematic
logical connectives that may make the semantics of an order-$1$ formula non-
affine: recall that the $\min$ operator was used to define the semantics of
conjunction. We require that for every subformula of the form
$\phi_{1}\land\phi_{2}$ and for each state $s\in S$, one of the values
$\llbracket\phi_{1}\rrbracket(s)$ and $\llbracket\phi_{2}\rrbracket(s)$ is the
constant $0$ or $1$. We can then remove the $\min$ operator, since we have
$\min(0,x)=0$ and $\min(1,x)=x$ for every $x\in[0,1]$.

We parameterize the type system by the Markov chain $M$, since it often
depends on $M$ whether the semantics of an order-$1$ formula is affine. For
example, the semantics of $(p\land\phi_{1})\lor(q\land\phi_{2})$ is affine if
the semantics of $\phi_{1}$ and $\phi_{2}$ are affine _and if_ $p$ and $q$
cannot be simultaneously true (i.e., if
$\rho_{\mathit{AP},M}(p)\cap\rho_{\mathit{AP},M}(q)=\emptyset$). Without the
parameterization, the resulting type system would be too conservative.

The discussion above motivates us to refine the type $\mathit{Prop}$ of
propositions to $\mathit{Prop}^{T,U}$ where $T,U\subseteq S$ and $T\cap
U=\emptyset$. Intuitively, the type $\mathit{Prop}^{T,U}$ describes
propositions $\phi\in\mathit{Prop}$ such that $\llbracket\phi\rrbracket(s)=0$
for all $s\in T$ and $\llbracket\phi\rrbracket(s)=1$ for all $s\in U$; there
is no guarantee on the value of $\llbracket\phi\rrbracket(s)$ for $s\in
S\setminus(T\cup U)$. The syntax of _refined types_ is given by:

$\displaystyle\kappa$
$\displaystyle::=\mathit{Prop}^{T,U}\,|\,\mathit{Prop}^{T,U}\to\kappa$

where $T$ and $U$ range over the set of subsets of $S$ satisfying $T\cap
U=\emptyset$. Note that each type $\kappa$ can be expressed as
$\mathit{Prop}^{T_{1},U_{1}}\to\mathit{Prop}^{T_{2},U_{2}}\to\dots\to\mathit{Prop}^{T_{k},U_{k}}\to\mathit{Prop}^{T,U}$
where $k\geq 0$.

We define the translation from the set of refined types to the set of types in
PHFL by

$\displaystyle\textit{tr}(\mathit{Prop}^{T,U})$ $\displaystyle=\mathit{Prop}$
$\displaystyle\textit{tr}(\kappa_{1}\to\kappa_{2})$
$\displaystyle=\textit{tr}(\kappa_{1})\to\textit{tr}(\kappa_{2})$

and the translation of type environment $\mathcal{K}$ by
$(\textit{tr}(\mathcal{K}))(x)=\textit{tr}(\mathcal{K}(x))$. The semantics of
refined types is defined as follows. As explained above, the values of
function types are restricted to affine functions.

######  Definition 5.1.

For each refined type $\kappa$, we define the subset
$\llbracket\kappa\rrbracket\subseteq\llbracket\textit{tr}(\kappa)\rrbracket$
as follows.

$\begin{array}[]{l}\llbracket\mathit{Prop}^{T,U}\rrbracket=\\{v\in
D_{\mathit{Prop}}\mid\forall s\in T.v(s)=0,\forall s\in U.v(s)=1\\}\\\
\llbracket\mathit{Prop}^{T_{1},U_{1}}\to\dots\mathit{Prop}^{T_{k},U_{k}}\to\mathit{Prop}^{T,U}\rrbracket=\\\
\qquad\\{f\in\llbracket\mathit{Prop}^{k}\to\mathit{Prop}\rrbracket\mid\\\
\qquad\qquad f\mbox{ is affine on
$\llbracket\mathit{Prop}^{T_{1},U_{1}}\rrbracket\times\dots\times\llbracket\mathit{Prop}^{T_{k},U_{k}}\rrbracket$,
and}\\\ \qquad\qquad\forall
v_{1}\in\llbracket\mathit{Prop}^{T_{1},U_{1}}\rrbracket,\dots,v_{k}\in\llbracket\mathit{Prop}^{T_{k},U_{k}}\rrbracket.f\,v_{1}\,\cdots\,v_{k}\in\llbracket\mathit{Prop}^{T,U}\rrbracket\\}\end{array}$

In the definition above, by “$f$ is affine on $D_{1}\times\dots\times D_{k}$”,
we mean that, for each state $s_{\ell}\in S$, there exist some coefficients
$c^{\ell}_{0},c^{\ell}_{1,1},\ldots,c^{\ell}_{k,n}$ such that, for every
$(v_{1},\dots,v_{k})\in D_{1}\times\dots\times D_{k}$,

$f\,v_{1}\,\cdots\,v_{k}\,s_{\ell}=c^{\ell}_{0}+\sum_{i\in\\{1,\ldots,k\\},j\in\\{1,\ldots,n\\}}c^{\ell}_{i,j}v_{i}(s_{j}).$

######  Remark 5.2.

Note that $\llbracket\kappa\rrbracket$ is not closed under various operations.
For example, the greatest lower bound of affine functions $\lambda(x,y).x$ and
$\lambda(x,y).y\in[0,1]^{2}\to[0,1]$ is $\lambda(x,y).\min(x,y)$, which is not
affine. This means that the conjunction does not preserve affinity, as
mentioned above. A similar observation applies to fixpoints: for a monotone
function $h$ on $\llbracket\textit{tr}(\kappa)\rrbracket$, even if
$h\,x\in\llbracket\kappa\rrbracket$ for every
$x\in\llbracket\kappa\rrbracket$, it is not necessarily the case that
$\mathit{LFP}(h)\in\llbracket\kappa\rrbracket$. For example, let $S=\\{s\\}$,
$\kappa=\mathit{Prop}^{\emptyset,\emptyset}\to\mathit{Prop}^{\emptyset,\\{s\\}}$,
and $h(f)=\lambda v.\lambda s.\max(f(v)(s),v(s)^{2})$. For any
$f\in\llbracket\kappa\rrbracket$ and
$v\in\mathit{Prop}^{\emptyset,\emptyset}$,
$h(f)(v)(s)=\max(f(v)(s),v(s)^{2})=\max(1,v(s)^{2})=1$, hence
$h(f)\in\llbracket\kappa\rrbracket$. However, $\mathit{LFP}(h)=\lambda
v.\lambda s.v(s)^{2}\not\in\llbracket\kappa\rrbracket$.

We restrict PHFL formulas by a type system parameterized by a Markov chain
$M$. We consider a type judgment of the form:
$\mathcal{K};\Delta\vdash_{M}\phi:\kappa$. Here, $\mathcal{K}$ is a type
environment of the form
$X_{1}\mathbin{:}\kappa_{1},\ldots,X_{k}\mathbin{:}\kappa_{k}$; it is for
fixpoint variables, i.e., those bound by $\mu$ or $\nu$. The other type
environment $\Delta$ is of the form
$Y_{1}\mathbin{:}\mathit{Prop}^{T_{1},U_{1}},\ldots,Y_{m}\mathbin{:}\mathit{Prop}^{T_{\ell},U_{\ell}}$;
it is for variables bound by $\lambda$. We require that the domains of
$\mathcal{K}$ and $\Delta$ are disjoint. The intended meaning of the judgment
$\mathcal{K};\Delta\vdash_{M}\phi:\kappa$, where
$\Delta=Y_{1}\mathbin{:}\mathit{Prop}^{T_{1},U_{1}},\ldots,Y_{\ell}\mathbin{:}\mathit{Prop}^{T_{\ell},U_{\ell}}$
and
$\kappa=\mathit{Prop}^{T_{\ell+1},U_{\ell+1}}\to\cdots\to\mathit{Prop}^{T_{\ell+m},U_{\ell+m}}\to\mathit{Prop}^{T,U}$
is as follows. Assume: (i) each fixpoint variable $X$ is bound to an affine
function as described by $\mathcal{K}(X)$, (ii) each $Y_{i}\;(1\leq
i\leq\ell+m)$ is bound to a value $(x_{i,1},\ldots,x_{i,n})$ described by
$\mathit{Prop}^{T_{i},U_{i}}$. Then the value of
$\phi\,Y_{\ell+1}\,\cdots\,Y_{\ell+m}$ is an affine function on $x_{i,j}$.
Note that the value of $\phi\,Y_{\ell+1}\,\cdots\,Y_{\ell+m}$ need not be
affine on the values of fixpoint variables. Below $\Delta$ is treated as a
_sequence_ of type bindings, while $\mathcal{K}$ is treated as a _set_.

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\mathcal{K};\Delta\vdash_{M}\phi:\mathit{Prop}^{T,U}\\\
T^{\prime}\subseteq T\quad\quad U^{\prime}\subseteq
U\end{array}}{\begin{array}[]{@{}c@{}}\mathcal{K};\Delta\vdash_{M}\phi:\mathit{Prop}^{T^{\prime},U^{\prime}}\end{array}}$
(T-WeakTU)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\mathcal{K};\Delta\vdash_{M}\phi:\kappa\end{array}}{\begin{array}[]{@{}c@{}}\mathcal{K};X\mathbin{:}\mathit{Prop}^{T,U},\Delta\vdash_{M}\phi:\kappa\end{array}}$
(T-Weak)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\end{array}}{\begin{array}[]{@{}c@{}}\mathcal{K};\emptyset\vdash_{M}p:\mathit{Prop}^{\overline{\rho_{\mathit{AP}}(p)},\rho_{\mathit{AP}}(p)}\end{array}}$
(T-AP)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\end{array}}{\begin{array}[]{@{}c@{}}\mathcal{K},X\mathbin{:}\kappa;\emptyset\vdash_{M}X:\kappa\end{array}}$
(T-FVar)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\end{array}}{\begin{array}[]{@{}c@{}}\mathcal{K};X\mathbin{:}\mathit{Prop}^{T,U}\vdash_{M}X:\mathit{Prop}^{T,U}\end{array}}$
(T-Var)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\mathcal{K},X\mathbin{:}\kappa;\emptyset\vdash_{M}\phi:\kappa\\\
\mbox{$\kappa$ is of the form
$\cdots\to\mathit{Prop}^{T,\emptyset}$}\end{array}}{\begin{array}[]{@{}c@{}}\mathcal{K};\emptyset\vdash_{M}\mu
X.\phi:\kappa\end{array}}$ (T-Mu)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\mathcal{K},X\mathbin{:}\kappa;\emptyset\vdash_{M}\phi:\kappa\\\
\mbox{$\kappa$ is of the form
$\cdots\to\mathit{Prop}^{\emptyset,U}$}\end{array}}{\begin{array}[]{@{}c@{}}\mathcal{K};\emptyset\vdash_{M}\nu
X.\phi:\kappa\end{array}}$ (T-Nu)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\mathcal{K};\Delta,X\mathbin{:}\mathit{Prop}^{T,U}\vdash_{M}\phi:\kappa\end{array}}{\begin{array}[]{@{}c@{}}\mathcal{K};\Delta\vdash_{M}\lambda
X.\phi:\mathit{Prop}^{T,U}\to\kappa\end{array}}$ (T-Abs)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\mathcal{K};\Delta\vdash_{M}\phi_{1}:\mathit{Prop}^{T,U}\to\kappa\\\
\mathcal{K};\Delta\vdash_{M}\phi_{2}:\mathit{Prop}^{T,U}\end{array}}{\begin{array}[]{@{}c@{}}\mathcal{K};\Delta\vdash_{M}\phi_{1}\phi_{2}:\kappa\end{array}}$
(T-App)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\mathcal{K};\Delta_{1},X\mathbin{:}\mathit{Prop}^{T,U},Y\mathbin{:}\mathit{Prop}^{T^{\prime},U^{\prime}},\Delta_{2}\vdash_{M}\phi:\kappa\end{array}}{\begin{array}[]{@{}c@{}}\mathcal{K};\Delta_{1},Y\mathbin{:}\mathit{Prop}^{T^{\prime},U^{\prime}},X\mathbin{:}\mathit{Prop}^{T,U},\Delta_{2}\vdash_{M}\phi:\kappa\end{array}}$
(T-Ex)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\mathcal{K};\Delta\vdash_{M}\phi_{1}:\mathit{Prop}^{T_{1},U_{1}}\quad\quad\mathcal{K};\Delta\vdash_{M}\phi_{2}:\mathit{Prop}^{T_{2},U_{2}}\\\
\Delta\neq\emptyset\Rightarrow T_{1}\cup U_{1}\cup T_{2}\cup
U_{2}=S_{M}\end{array}}{\begin{array}[]{@{}c@{}}\mathcal{K};\Delta\vdash_{M}\phi_{1}\land\phi_{2}:\mathit{Prop}^{(T_{1}\cup
T_{2}),(U_{1}\cap U_{2})}\end{array}}$ (T-Conj)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\mathcal{K};\Delta\vdash_{M}\phi_{1}:\mathit{Prop}^{T_{1},U_{1}}\quad\quad\mathcal{K};\Delta\vdash_{M}\phi_{2}:\mathit{Prop}^{T_{2},U_{2}}\\\
\Delta\neq\emptyset\Rightarrow T_{1}\cup U_{1}\cup T_{2}\cup
U_{2}=S_{M}\end{array}}{\begin{array}[]{@{}c@{}}\mathcal{K};\Delta\vdash_{M}\phi_{1}\lor\phi_{2}:\mathit{Prop}^{(T_{1}\cap
T_{2}),(U_{1}\cup U_{2})}\end{array}}$ (T-Disj)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\mathcal{K};\emptyset\vdash_{M}\phi:\mathit{Prop}^{T,U}\end{array}}{\begin{array}[]{@{}c@{}}\mathcal{K};\emptyset\vdash_{M}[\phi]_{J}:\mathit{Prop}^{T,U}\end{array}}$
(T-J)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\mathcal{K};\emptyset\vdash_{M}\phi:\mathit{Prop}^{T,U}\\\
T^{\prime}=\\{s\in S_{M}\mid\exists s^{\prime}\in
T.P_{M}(s,s^{\prime})>0\\}\\\ U^{\prime}=\\{s\in S_{M}\mid\forall
s^{\prime}\in S_{M}.P_{M}(s,s^{\prime})>0\Rightarrow s^{\prime}\in
U\\}\end{array}}{\begin{array}[]{@{}c@{}}\mathcal{K};\emptyset\vdash_{M}\square\phi:\mathit{Prop}^{T^{\prime},U^{\prime}}\end{array}}$
(T-Min)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\mathcal{K};\emptyset\vdash_{M}\phi:\mathit{Prop}^{T,U}\\\
T^{\prime}=\\{s\in S_{M}\mid\forall s^{\prime}\in
S_{M}.P_{M}(s,s^{\prime})>0\Rightarrow s^{\prime}\in T\\}\\\
U^{\prime}=\\{s\in S_{M}\mid\exists s^{\prime}\in
U.P_{M}(s,s^{\prime})>0\\}\end{array}}{\begin{array}[]{@{}c@{}}\mathcal{K};\emptyset\vdash_{M}\lozenge\phi:\mathit{Prop}^{T^{\prime},U^{\prime}}\end{array}}$
(T-Max)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\mathcal{K};\Delta\vdash_{M}\phi:\mathit{Prop}^{T,U}\\\
T^{\prime}=\\{s\in S_{M}\mid\forall s^{\prime}\in
S_{M}.P_{M}(s,s^{\prime})>0\Rightarrow s^{\prime}\in T\\}\\\
U^{\prime}=\\{s\in S_{M}\mid\forall s^{\prime}\in
S_{M}.P_{M}(s,s^{\prime})>0\Rightarrow s^{\prime}\in
U\\}\end{array}}{\begin{array}[]{@{}c@{}}\mathcal{K};\Delta\vdash_{M}\mathbin{\bigcirc}\phi:\mathit{Prop}^{T^{\prime},U^{\prime}}\end{array}}$
(T-Avg)

Figure 4. Typing Rules for the Decidable Fragment

The typing rules are given in Figure 4. We explain key rules below. The rule
T-WeakTU is for weakening the information represented by $T$ and $U$; this
rule is required, for example, for adjusting the types between a function and
its argument. The rule T-Weak is a usual weakening rule for adding type
bindings to $\Delta$. The rule T-AP is for atomic propositions; recall that
$\rho_{\mathit{AP}}(p)$ denotes the set of states where $p$ holds with
probability $1$. The rule T-Mu is for least fixpoint formulas. The second
premise means that $\kappa$ is of the form
$\mathit{Prop}^{T_{1},U_{1}}\to\dots\to\mathit{Prop}^{T_{k},U_{k}}\to\mathit{Prop}^{T,U}$,
where $U=\emptyset$.222The condition $U=\emptyset$ is sometimes too
restrictive. For example, consider the formula $\mu X.\text{true}$. We can
only assign $\mathit{Prop}^{\emptyset,\emptyset}$, although
$\mathit{Prop}^{\emptyset,S_{M}}$ can be assigned to the equivalent formula
true. To remedy this problem, it suffices to add the rule for unfolding:
$\displaystyle\frac{\begin{array}[]{@{}c@{}}\mathcal{K};\Delta\vdash_{M}[\mu
X.\phi/X]\phi:\kappa\end{array}}{\begin{array}[]{@{}c@{}}\mathcal{K};\Delta\vdash_{M}\mu
X.\phi:\kappa\end{array}}$ For the sake of simplicity, we do not consider this
rule. Without this restriction, the value of
$\phi\,\phi_{1}\,\cdots\,\phi_{k}$ at a state in $U$ may be wrongly estimated
to be $1$. For example, consider the case where $\phi=X$ and the simple type
of $X$ is $\mathit{Prop}$. Then, the value of $\mu X.X$ should be the map $f$
such that $f(s)=0$ for every state. Without the restriction, however, we could
wrongly derive $\mu X.X:\mathit{Prop}^{\emptyset,S_{M}}$. Note also that
$\Delta$ is empty in T-Mu; this is just for technical convenience, and is not
a fundamental restriction. Indeed, if $\mu X.\phi$ contains a free variable
$Y$ of type $\mathit{Prop}^{T,U}$, then we can replace it with $(\mu
X^{\prime}.\lambda Y.[X^{\prime}\,Y/X]\phi)Y$, without changing the semantics.
Analogous conditions are imposed in the rule T-Nu for greatest fixpoint
formulas. In the rule T-Conj for conjunctions, the first two premises imply
that the value of $\phi_{i}$ at a state in $T_{i}$ is $0$; therefore, the
value of $\phi_{1}\land\phi_{2}$ at a state in $T_{1}\cup T_{2}$ is $0$, which
explains $T_{1}\cup T_{2}$ in the conclusion. Similarly for $U_{1}\cap U_{2}$.
The third premise (on the second line) ensures that the value of
$\phi_{1}\land\phi_{2}$ is an affine function on the value of the variables in
$\Delta$. That is guaranteed if $\Delta=\emptyset$. Otherwise, we require
$T_{1}\cup U_{1}\cup T_{2}\cup U_{2}=S_{M}$; recall the earlier discussion on
a sufficient condition for the semantics of an order-1 formula to be affine.
The rule T-Disj for disjunctions is analogous. In the rules T-J, T-Min, and
T-Max, we require that the type environment $\Delta$ for $\lambda$-bound
variables be empty, since the operators $[\cdot]_{J},\square$, and $\lozenge$
break the affinity. The sets $T^{\prime}$ and $U^{\prime}$ in the conclusions
of those rules are conservatively approximated. In T-J, recall that we have
excluded out trivial bounds such as $>1$ and $\geq 0$; thus, the value of
$[\phi]_{J}$ is $0$ ($1$, resp.) if the value of $\phi$ is $0$ ($1$, resp.).
In the rule T-Avg, we need not require $\Delta$ to be empty, as the average of
affine functions is again affine.

######  Example 5.3.

Let $M$ be an element of $\mathcal{M}$ in the proof of Theorem 1, i.e., a
Markov chain $(S,P,\rho_{\mathit{AP}},s_{\text{in}})$ that satisfies the
following conditions.

  * •

$S=\\{s_{0},s_{1},\dots,s_{n}\\}$ for a positive integer $n$,

  * •

$P(s_{i},s_{i+1})=1$ ($0\leq i\leq n-1$), $P(s_{n},s_{n})=1$ and
$P(s_{i},s_{j})=0$ otherwise.

  * •

There are three atomic propositions $a,b,c$ with
$\rho_{\mathit{AP}}(a)\cup\rho_{\mathit{AP}}(b)=\\{s_{0},s_{1},\dots,s_{n-1}\\}$,
$\rho_{\mathit{AP}}(a)\cap\rho_{\mathit{AP}}(b)=\emptyset$ and
$\rho_{\mathit{AP}}(c)=\\{s_{n}\\}$.

  * •

The initial state is $s_{\text{in}}=s_{0}$.

Let $\phi_{1}$ be the formula:

$(\mu F.\lambda X.a\land\mathbin{\bigcirc}(X\lor
F(b\land\mathbin{\bigcirc}X)))(b\land\lozenge c),$

which is a variation of the formula $\phi$ considered in the proof, obtained
by replacing two occurrences of $\lozenge$ with $\mathbin{\bigcirc}$. Since
$M$ has only deterministic transitions, $\phi_{1}$ has the same value as
$\phi$. Let
$\mathcal{K}=F\mathbin{:}\mathit{Prop}^{\rho_{\mathit{AP}}(a),\emptyset}\to\mathit{Prop}^{\rho_{\mathit{AP}}(b)\cup\rho_{\mathit{AP}}(c),\emptyset}$
and $\Delta=X\mathbin{:}\mathit{Prop}^{\rho_{\mathit{AP}}(a),\emptyset}$.
Then, we have:

$\footnotesize\infers{\mathcal{K};\Delta\vdash_{M}a\land\mathbin{\bigcirc}(X\lor
F(b\land\mathbin{\bigcirc}X)):\mathit{Prop}^{\rho_{\mathit{AP}}(b)\cup\rho_{\mathit{AP}}(c),\emptyset}}{\mathcal{K};\Delta\vdash_{M}a:\mathit{Prop}^{\rho_{\mathit{AP}}(b)\cup\rho_{\mathit{AP}}(c),\rho_{\mathit{AP}}(a)}&\infers{\mathcal{K};\Delta\vdash_{M}\mathbin{\bigcirc}(X\lor
F(b\land\mathbin{\bigcirc}X)):\mathit{Prop}^{\emptyset,\emptyset}}{\infers{\mathcal{K};\Delta\vdash_{M}X\lor
F(b\land\mathbin{\bigcirc}X):\mathit{Prop}^{\emptyset,\emptyset}}{\infers{\mathcal{K};\Delta\vdash_{M}X:\mathit{Prop}^{\rho_{\mathit{AP}}(a),\emptyset}}{}\infers{\mathcal{K};\Delta\vdash_{M}F(b\land\mathbin{\bigcirc}X):\mathit{Prop}^{\rho_{\mathit{AP}}(b)\cup\rho_{\mathit{AP}}(c),\emptyset}}{\cdots}}}}$

Here,
$\mathcal{K};\Delta\vdash_{M}F(b\land\mathbin{\bigcirc}X):\mathit{Prop}^{\rho_{\mathit{AP}}(b)\cup\rho_{\mathit{AP}}(c),\emptyset}$
is derived as follows.

$\footnotesize\infers{\mathcal{K};\Delta\vdash_{M}F(b\land\mathbin{\bigcirc}X):\mathit{Prop}^{\rho_{\mathit{AP}}(b)\cup\rho_{\mathit{AP}}(c),\emptyset}}{\mathcal{K};\Delta\vdash_{M}F:\mathit{Prop}^{\rho_{\mathit{AP}}(a),\emptyset}\to\mathit{Prop}^{\rho_{\mathit{AP}}(b)\cup\rho_{\mathit{AP}}(c),\emptyset}&\infers{\mathcal{K};\Delta\vdash_{M}b\land\mathbin{\bigcirc}X:\mathit{Prop}^{\rho_{\mathit{AP}}(a),\emptyset}}{\infers{\mathcal{K};\Delta\vdash_{M}b\land\mathbin{\bigcirc}X:\mathit{Prop}^{\rho_{\mathit{AP}}(a)\cup\rho_{\mathit{AP}}(c),\emptyset}}{\mathcal{K};\Delta\vdash_{M}b:\mathit{Prop}^{\rho_{\mathit{AP}}(a)\cup\rho_{\mathit{AP}}(c),\rho_{\mathit{AP}}(b)}\infers{\mathcal{K};\Delta\vdash_{M}\mathbin{\bigcirc}X:\mathit{Prop}^{\emptyset,\emptyset}}{\mathcal{K};\Delta\vdash_{M}X:\mathit{Prop}^{\rho_{\mathit{AP}}(a),\emptyset}}}}}$

We can thus obtain

$\emptyset;\emptyset\vdash_{M}(\mu F.\lambda X.a\land\mathbin{\bigcirc}(X\lor
F(b\land\mathbin{\bigcirc}X)))(b\land\lozenge
c):\mathit{Prop}^{\rho_{\mathit{AP}}(b)\cup\rho_{\mathit{AP}}(c),\emptyset}.$

Note that, by the same argument as the proof of Theorem 1, there exists no
$\mu^{p}$-calculus formula equivalent to $\phi_{1}$. ∎

The following lemma states that a formula that is well-typed in
$\mathcal{T}_{M}$ is also well-typed in the original PHFL type system.

######  Lemma 5.4.

Let $\phi$ be a PHFL formula such that
$\mathcal{K};\Delta\vdash_{M}\phi:\kappa$. Then we have
$\textit{tr}(\mathcal{K},\Delta)\vdash\phi:\textit{tr}(\sigma)$.

######  Proof 5.5.

This follows by a straightforward induction on the derivation of
$\mathcal{K};\Delta\vdash_{M}\phi:\kappa$.

The following lemma states that the refined type system does not impose any
restriction on the order-0 fragment of PHFL. Thus, together with the
observation in Example 5.3, the lemma implies that our decidable fragment is
strictly more expressive than the $\mu^{p}$-calculus.

######  Lemma 5.6.

If $\Gamma\vdash\phi:\tau$, and $\phi$ is an order-0 formula, then
$\mathcal{K};\emptyset\vdash_{M}\phi:\mathit{Prop}^{\emptyset,\emptyset}$
where $\mathcal{K}$ is the type environment such that
$\mathit{dom}(\mathcal{K})=\mathit{dom}(\Gamma)$ and
$\mathcal{K}(X)=\mathit{Prop}^{\emptyset,\emptyset}$ for every
$X\in\mathit{dom}(\mathcal{K})$.

######  Proof 5.7.

This follows by a straightforward induction on the derivation of
$\Gamma\vdash\phi:\tau$. Note that since $\Delta$ is always empty, the
condition $T_{1}\cup U_{1}\cup T_{2}\cup U_{2}$ in T-Conj and T-Disj is
irrelevant.

In the rest of this subsection, we prove the following properties.

  1. (1)

The type system is sound in the sense that the semantics of any formula $\phi$
of type $\kappa$ indeed belongs to $\llbracket\kappa\rrbracket$; see Theorem 7
for the precise statement.

  2. (2)

The calculation of the semantics of a well-typed formula (especially, the
least/greatest fixpoint computation) can be performed up to the equivalence
relation $\sim_{\kappa}$, where
$f\sim_{\mathit{Prop}^{T_{1},U_{1}}\to\dots\to\mathit{Prop}^{T_{m},U_{m}}\to\mathit{Prop}^{T,U}}g$
just if $f$ and $g$ are equivalent on the intended domain, i.e., if
$f\,v_{1}\,\cdots\,v_{m}=g\,v_{1}\,\cdots\,v_{m}$ for any
$v_{1}\in\llbracket\mathit{Prop}^{T_{1},U_{1}}\rrbracket,\ldots,v_{m}\in\llbracket\mathit{Prop}^{T_{m},U_{m}}\rrbracket$;
see Lemmas 5.15 and 5.17.

The reason why the type system ensures affinity has been intuitively explained
already, except for the fixpoints. Here we show (in Lemma 5.10) that the
fixpoint of a typable fixpoint operator is indeed affine. The key observation
is that
$\llbracket\kappa\rrbracket\subseteq\llbracket\textit{tr}(\kappa)\rrbracket$
is closed under the limit of chains, as stated in the following lemma.

######  Lemma 5.8.

Let $\kappa$ be a refined type and $\gamma$ be an ordinal number. For every
increasing chain $(f_{\alpha})_{\alpha<\gamma}$ of elements in
$\llbracket\kappa\rrbracket$, the limit $\bigsqcup_{\alpha<\gamma}f_{\alpha}$
in $\llbracket\textit{tr}(\kappa)\rrbracket$ belongs to
$\llbracket\kappa\rrbracket$. Similarly, for every decreasing chain
$(f_{\alpha})_{\alpha<\gamma}$, the limit
$\bigsqcap_{\alpha<\gamma}x_{\alpha}$ is in $\llbracket\kappa\rrbracket$.

######  Proof 5.9.

We prove the former. Assume
$\kappa=\mathit{Prop}^{T_{1},U_{1}}\to\dots\to\mathit{Prop}^{T_{k},U_{k}}\to\mathit{Prop}^{T,U}$.

We first give an alternative characterization of affinity. For each $i\leq k$,
given $v_{i}\in\llbracket\mathit{Prop}^{T_{i},U_{i}}\rrbracket$ and
$r\in[0,1]$, we define $r\cdot v_{i}$ by $(r\cdot v_{i})(s)=r(v_{i}(s))$. Note
that $r\cdot v_{i}$ may not be a member of
$\llbracket\mathit{Prop}^{T_{i},U_{i}}\rrbracket$, but $r\cdot
v_{i}+(1-r)\cdot
v_{i}^{\prime}\in\llbracket\mathit{Prop}^{T_{i},U_{i}}\rrbracket$ for every
$v_{i},v_{i}^{\prime}\in\llbracket\mathit{Prop}^{T_{i},U_{i}}\rrbracket$ and
$r\in[0,1]$ (here the sum is the point-wise sum on reals). Then
$f\in\llbracket\mathit{Prop}^{k}\to\mathit{Prop}\rrbracket$ is affine on
$\llbracket\mathit{Prop}^{T_{1},U_{1}}\rrbracket\times\dots\times\llbracket\mathit{Prop}^{T_{k},U_{k}}\rrbracket$
if and only if, for every
$(v_{1},\dots,v_{k}),(v^{\prime}_{1},\dots,v^{\prime}_{k})\in\llbracket\mathit{Prop}^{T_{1},U_{1}}\rrbracket\times\dots\times\llbracket\mathit{Prop}^{T_{k},U_{k}}\rrbracket$
and $r\in[0,1]$,

$f(r\cdot v_{1}+(1-r)\cdot v_{1}^{\prime})\dots(r\cdot v_{k}+(1-r)\cdot
v_{k}^{\prime})=r(f\,v_{1}\,\dots\,v_{k})+(1-r)(f\,v_{1}^{\prime}\,\dots\,v_{k}^{\prime}).$

Let $(f_{\alpha})_{\alpha<\gamma}$ be an increasing chain and
$f=\bigsqcup_{\alpha<\gamma}f_{\alpha}$. Then $f$ can be characterized in
terms of the limits in real numbers as
$f\,y_{1}\,\dots\,y_{k}=\lim_{\alpha<\gamma}(f_{\alpha}\,y_{1}\,\dots\,y_{k})$
for every $y_{1},\dots,y_{k}\in\llbracket\mathit{Prop}\rrbracket$. Since
$\lim_{\alpha<\gamma}$ commutes with linear operations, for every
$(v_{1},\dots,v_{k})$,
$(v^{\prime}_{1},\dots,v^{\prime}_{k})\in\llbracket\mathit{Prop}^{T_{1},U_{1}}\rrbracket\times\dots\times\llbracket\mathit{Prop}^{T_{k},U_{k}}\rrbracket$
and $r\in[0,1]$, we have:

$\displaystyle f\,(r\cdot v_{1}+(1-r)\cdot v^{\prime}_{1})\dots(r\cdot
v_{k}+(1-r)\cdot v^{\prime}_{k})$
$\displaystyle=\lim_{\alpha<\gamma}(f_{\alpha}\,(r\cdot v_{1}+(1-r)\cdot
v^{\prime}_{1})\dots(r\cdot v_{k}+(1-r)\cdot v^{\prime}_{k})$
$\displaystyle=\lim_{\alpha<\gamma}\big{(}r(f_{\alpha}\,v_{1}\dots
v_{k})+(1-r)(f_{\alpha}\,v^{\prime}_{1}\,\dots\,v^{\prime}_{k})\big{)}$
$\displaystyle=r\big{(}\lim_{\alpha<\gamma}(f_{\alpha}\,v_{1}\,\dots
v_{k})\big{)}+(1-r)\big{(}\lim_{\alpha<\gamma}(f_{\alpha}\,v^{\prime}_{1}\,\dots\,v^{\prime}_{k})\big{)}$
$\displaystyle=r(f\,v_{1}\,\dots\,v_{k})+(1-r)(f\,v_{1}^{\prime}\,\dots\,v_{k}^{\prime}).$

The latter is the dual of the former, and can be proved in the same manner, by
just replacing $\bigsqcup$ with $\bigsqcap$.

######  Lemma 5.10.

Let
$\kappa=\mathit{Prop}^{T_{1},U_{1}}\to\dots\to\mathit{Prop}^{T_{k},U_{k}}\to\mathit{Prop}^{T,U}$
be a refined type and $h$ be a monotone function on $\textit{tr}(\kappa)$ such
that $x\in\llbracket\kappa\rrbracket$ implies
$h\,x\in\llbracket\kappa\rrbracket$.

  * •

If $U=\emptyset$, then $\mathit{LFP}(h)\in\llbracket\kappa\rrbracket$.

  * •

If $T=\emptyset$, then $\mathit{GFP}(h)\in\llbracket\kappa\rrbracket$.

Here $\mathit{LFP}$ and $\mathit{GFP}$ are taken in
$\llbracket\textit{tr}(\kappa)\rrbracket$.

######  Proof 5.11.

We prove the former; the latter can be proved similarly. We define
$h^{\alpha}(\bot)$ for ordinals $\alpha$ as follows:

$\displaystyle
h^{\alpha}(\bot)=\begin{cases}\bot_{\textit{tr}(\kappa)}&\mbox{if
$\alpha=0$}\\\ h(h^{\beta}(\bot))&\mbox{if $\alpha=\beta+1$}\\\
\bigsqcup_{\beta<\alpha}h^{\beta}(\bot)&\mbox{if $\alpha$ is a limit
ordinal}.\end{cases}$

Then $\mathit{LFP}(h)=h^{\alpha}(\bot)$ for some sufficiently large $\alpha$.

It suffices to show that $h^{\alpha}(\bot)\in\llbracket\kappa\rrbracket$ for
every $\alpha$. We prove this claim by transfinite induction. For $\alpha=0$,
$\bot_{\textit{tr}(\kappa)}\in\llbracket\kappa\rrbracket$ since $U=\emptyset$.
For $\alpha=\beta+1$, we have
$h(h^{\beta}(\bot))\in\llbracket\kappa\rrbracket$ since
$h^{\beta}(\bot)\in\llbracket\kappa\rrbracket$. If $\alpha$ is a limit
cardinal, we appeal to Lemma 5.8; note that $(f^{\beta}(\bot))_{\beta<\alpha}$
is an increasing chain.

Note that in the above lemma, $\mathit{LFP}(h)\in\llbracket\kappa\rrbracket$
would not hold if we drop the condition $U=\emptyset$; recall Remark 5.2. That
justifies the corresponding conditions in rule T-Mu and T-Nu.

The following theorem is soundness of the type system. Let
$\llbracket\mathcal{K}\rrbracket$ be the subset of
$\llbracket\textit{tr}(\mathcal{K})\rrbracket$ consisting of interpretations
$\rho$ such that $\rho(X)\in\llbracket\mathcal{K}(X)\rrbracket$ for every
$X\in\mathit{dom}(\mathcal{K})$. For
$\Delta=(Y_{1}:\mathit{Prop}^{T_{1},U_{1}},\dots,Y_{m}:\mathit{Prop}^{T_{m},U_{m}})$,
we write $\lambda\Delta.\varphi$ for $\lambda Y_{1}.\dots\lambda
Y_{m}.\varphi$ and $\Delta\to\kappa$ for
$\mathit{Prop}^{T_{1},U_{1}}\to\dots\to\mathit{Prop}^{T_{m},U_{m}}\to\kappa$.

######  Theorem 5.11.

Let $\phi$ be a PHFL formula such that
$\mathcal{K};\Delta\vdash_{M}\phi:\kappa$. Then, for every
$\rho\in\llbracket\mathcal{K}\rrbracket$, we have
$\llbracket\textit{tr}(\mathcal{K})\vdash\lambda\Delta.\phi:\textit{tr}(\Delta\to\kappa)\rrbracket(\rho)\in\llbracket\Delta\to\kappa\rrbracket$.

######  Proof 5.12.

By induction on the structure of derivation
$\mathcal{K};\Delta\vdash_{M}\phi:\kappa$, with case analysis on the last rule
used. We use Lemma 5.10 for the cases of T-Mu and T-Nu. For the cases of
T-Conj and T-Disj, the condition $T_{1}\cup U_{1}\cup T_{2}\cup U_{2}=S_{M}$
plays the key role. Note that if $s$ belongs to $T_{i}\cup U_{i}$, then the
semantics of $\lambda\Delta.\phi_{0}\land\phi_{1}$ at $s$ coincides with
either that of $\lambda\Delta.\phi_{1-i}$ or a constant function
$\lambda\tilde{v}.0$. Other cases are easy.

Let us discuss another important property of the type system. For
$\kappa=\mathit{Prop}^{T_{1},U_{1}}\to\dots\to\mathit{Prop}^{T_{k},U_{k}}\to\mathit{Prop}^{T,U}$
and $f,g\in\llbracket\textit{tr}(\kappa)\rrbracket$, we write
$f\precsim_{\kappa}g$ if
$f\,v_{1}\,\dots\,v_{k}\sqsubseteq_{\mathit{Prop}}g\,v_{1}\,\dots\,v_{k}$ for
every
$(v_{1},\dots,v_{k})\in\llbracket\mathit{Prop}^{T_{1},U_{1}}\rrbracket\times\dots\times\llbracket\mathit{Prop}^{T_{k},U_{k}}\rrbracket$.
For interpretations $\rho_{0},\rho_{1}\in\llbracket\mathcal{K}\rrbracket$, we
write $\rho_{0}\precsim_{\mathcal{K}}\rho_{1}$ if
$\rho_{0}(X)\precsim_{\mathcal{K}(X)}\rho_{1}(X)$ for every
$X\in\mathit{dom}(\mathcal{K})$. We write $f\sim_{\kappa}g$ for
$f\preceq_{\kappa}g\land g\preceq_{\kappa}f$, and analogously for
interpretations. The results in the rest of this subsection allows us to
compute the semantics of a formula of type $\kappa$ up to $\sim_{\kappa}$.

######  Lemma 5.13.

Let
$\kappa=\mathit{Prop}^{T_{1},U_{1}}\to\dots\to\mathit{Prop}^{T_{k},U_{k}}\to\mathit{Prop}^{T,U}$
be a refined type and $h_{0}$ and $h_{1}$ be monotone functions on
$\textit{tr}(\kappa)$ such that $x\in\llbracket\kappa\rrbracket$ implies
$h_{0}\,x,h_{1}\,x\in\llbracket\kappa\rrbracket$ and that
$x_{0}\precsim_{\kappa}x_{1}$ implies
$h_{0}\,x_{0}\precsim_{\kappa}h_{1}\,x_{1}$.

  * •

If $U=\emptyset$, then
$\mathit{LFP}(h_{0})\precsim_{\kappa}\mathit{LFP}(h_{1})$.

  * •

If $T=\emptyset$, then
$\mathit{GFP}(h_{0})\precsim_{\kappa}\mathit{GFP}(h_{1})$.

Here $\mathit{LFP}$ and $\mathit{GFP}$ are taken in
$\llbracket\textit{tr}(\kappa)\rrbracket$.

######  Proof 5.14.

We prove the former; the proof of the latter is analogous. As discussed in the
proof of Lemma 5.10, $\mathit{LFP}(h_{0})=h_{0}^{\alpha}(\bot)$ and
$\mathit{LFP}(h_{1})=h_{1}^{\alpha}(\bot)$ for some sufficiently large ordinal
$\alpha$. We prove $h_{0}^{\alpha}(\bot)\precsim_{\kappa}h_{1}^{\alpha}(\bot)$
by induction on $\alpha$. Trivially
$h_{0}^{\alpha}(\bot)=\bot\precsim_{\kappa}\bot=h_{1}^{\alpha}(\bot)$. For
$\alpha=\beta+1$, since
$h_{0}^{\beta}(\bot)\precsim_{\kappa}h_{1}^{\beta}(\bot)$ by the induction
hypothesis,
$h_{0}(h_{0}^{\beta}(\bot))\precsim_{\kappa}h_{1}(h_{1}^{\beta}(\bot))$
follows from the assumption. If $\alpha$ is a limit cardinal, then
$h_{i}^{\alpha}=\bigsqcup_{\beta<\alpha}h_{i}^{\beta}(\bot)$. For every
$(v_{1},\dots,v_{k})\in\llbracket\mathit{Prop}^{T_{1},U_{1}}\rrbracket\times\dots\times\llbracket\mathit{Prop}^{T_{k},U_{k}}\rrbracket$,
we have
$h_{i}^{\alpha}(\bot)(v_{1})\dots(v_{k})=\bigsqcup_{\beta<\alpha}(h_{i}^{\beta}(\bot)(v_{1})\dots(v_{k}))$
by definition. Since
$h_{0}^{\beta}(\bot)(v_{1})\dots(v_{k})\precsim_{\kappa}h_{1}^{\beta}(\bot)(v_{1})\dots(v_{k})$
holds for every $\beta<\alpha$ by the induction hypothesis, we have
$h_{0}^{\alpha}(\bot)(v_{1})\dots(v_{k})\precsim_{\kappa}h_{1}^{\alpha}(\bot)(v_{1})\dots(v_{k})$.

######  Lemma 5.15.

Let $\phi$ be a PHFL formula such that
$\mathcal{K};\Delta\vdash_{M}\phi:\kappa$. Then, for every
$\rho,\rho^{\prime}\in\llbracket\mathcal{K}\rrbracket$ such that
$\rho\precsim_{\mathcal{K}}\rho^{\prime}$, we have
$\llbracket\lambda\Delta.\phi\rrbracket(\rho)\precsim_{\Delta\to\kappa}\llbracket\lambda\Delta.\phi\rrbracket(\rho^{\prime})$.

######  Proof 5.16.

By induction on the structure of derivation
$\mathcal{K};\Delta\vdash_{M}\phi:\kappa$. The most cases are easy. For
fixpoints, we appeal to Lemma 5.13. The details are given in Appendix A.

The above lemma shows that the semantic domain for $\kappa$ can be regarded as
$\llbracket\kappa\rrbracket$ modulo $\sim_{\kappa}$. Furthermore the least and
greatest fixpoints can be characterized in terms of the preorder
$\precsim_{\kappa}$.

######  Lemma 5.17.

Let $\kappa$ be a refined type and $h$ be a monotone function on
$\textit{tr}(\kappa)$ such that $x\in\llbracket\kappa\rrbracket$ implies
$h\,x\in\llbracket\kappa\rrbracket$ and that $x\precsim_{\kappa}x^{\prime}$
implies $h\,x\precsim_{\kappa}h\,x^{\prime}$. If
$\mathit{LFP}(h)\in\llbracket\kappa\rrbracket$, then $\mathit{LFP}(h)$ is a
least element in $\\{x\in\llbracket\kappa\rrbracket\mid
h\,x\precsim_{\kappa}x\\}$ with respect to $\precsim_{\kappa}$. Similarly, if
$\mathit{GFP}(h)\in\llbracket\kappa\rrbracket$, then $\mathit{GFP}(h)$ is a
greatest postfixpoint of $h$ w.r.t $\precsim_{\kappa}$.

######  Proof 5.18.

Assume
$\kappa=\mathit{Prop}^{T_{1},U_{1}}\to\dots\to\mathit{Prop}^{T_{k},U_{k}}\to\mathit{Prop}^{T,U}$.
Let $\bot_{\kappa}$ be the least element of $\llbracket\kappa\rrbracket$,
which is defined by: for every $s\in S_{M}$,

$\begin{array}[]{l}\bot_{\mathit{Prop}^{T,U}}(s)=\begin{cases}1&\mbox{if $s\in
U$}\\\ 0&\mbox{otherwise.}\end{cases}\\\
\bot_{\kappa}\,v_{1}\,\dots\,v_{k}=\begin{cases}\bot_{\mathit{Prop}^{T,U}}&\mbox{if
$v_{i}\sqsupseteq\bot_{\mathit{Prop}^{T_{i},U_{i}}}$ for every $i$}\\\ \lambda
s.0&\mbox{otherwise.}\end{cases}\end{array}$

For an ordinal number $\alpha$, we define $x_{\alpha}$ by
$x_{0}=\bot_{\kappa}$, $x_{\beta+1}=h(x_{\beta})$ and
$x_{\alpha}=\bigsqcup_{\beta<\alpha}x_{\beta}$ if $\alpha$ is a limit ordinal.
By the monotonicity of $h$ and Lemma 5.8, the sequence
$\\{x_{\alpha}\\}_{\alpha}$ is well-defined and forms an increasing chain.
Thus, there exists an ordinal $\alpha$ such that $x_{\alpha}$ is a fixpoint of
$h$, and in particular, an element of $\\{x\in\llbracket\kappa\rrbracket\mid
h\,x\precsim_{\kappa}x\\}$. It follows by straightforward induction on
$\alpha$ that $x_{\alpha}$ is also a least element of
$\\{x\in\llbracket\kappa\rrbracket\mid h\,x\precsim_{\kappa}x\\}$. Now, by the
assumption that $\mathit{LFP}(h)\in\llbracket\kappa\rrbracket$,
$\mathit{LFP}(h)$ is also an element of $\\{x\in\llbracket\kappa\rrbracket\mid
h\,x\precsim_{\kappa}x\\}$, and since
$\mathit{LFP}(h)\sqsubseteq{}x_{\alpha}$, $\mathit{LFP}(h)$ is also a least
element of $\\{x\in\llbracket\kappa\rrbracket\mid h\,x\precsim_{\kappa}x\\}$.
The proof for $\mathit{GFP}(h)$ is analogous.

If $\mathcal{K};\emptyset\vdash_{M}\mu X.\phi:\kappa$ and
$\rho\in\llbracket\mathcal{K}\rrbracket$, then $h=\llbracket\lambda
X.\phi\rrbracket(\rho)$ satisfies the condition of the lemma above (recall
Lemma 5.15). Hence $\llbracket\mu X.\phi\rrbracket(\rho)$ is
$\sim_{\kappa}$-equivalent to every least fixpoint of $\llbracket\lambda
X.\phi\rrbracket(\rho)$ with respect to $\precsim_{\kappa}$; in other words,
to compute $\llbracket\mu X.\phi\rrbracket(\rho)$ up to $\sim_{\kappa}$, it
suffices to compute a least fixpoint of $\llbracket\lambda
X.\phi\rrbracket(\rho)$ in the quotient set
$\llbracket\kappa\rrbracket/\sim_{\kappa}$. A similar statement holds for $\nu
X.\phi$.

###  5.2. Decidability

This subsection gives a description of the interpretation of a PHFL formula
using the first-order theory of reals, and obtains the decidability of the
restricted fragment of PHFL model checking. To this end, we need to represent
an element in $\llbracket\kappa\rrbracket$ as a tuple of reals. Each element
of $\llbracket\mathit{Prop}^{T,U}\rrbracket$ can be naturally written as an
$n$-tuple of $[0,1]$ where $n$ is the number of states in $M$. What remains is
a representation of functions
$\llbracket\mathit{Prop}^{T_{1},U_{1}}\to\dots\to\mathit{Prop}^{T_{m},U_{m}}\to\mathit{Prop}^{T,U}\rrbracket$.

The key result is Lemma 5.15, which allows us to identify
$x,y\in\llbracket\kappa\rrbracket$ if $x\sim_{\kappa}y$. Let
$\kappa=\mathit{Prop}^{T_{1},U_{1}}\to\dots\to\mathit{Prop}^{T_{m},U_{m}}\to\mathit{Prop}^{T,U}$.)
Since $x\in\llbracket\kappa\rrbracket$ is affine on
$\llbracket\mathit{Prop}^{T_{1},U_{1}}\rrbracket\times\dots\times\llbracket\mathit{Prop}^{T_{m},U_{m}}\rrbracket$,
the $\sim_{\kappa}$-equivalence class of $x$ contains an affine function on
$[0,1]^{m}$, i.e., $x\sim_{\kappa}f$ holds for some

$f\,v_{1}\,\dots\,v_{k}\,s=c_{s}+\sum_{i=1}^{m}\sum_{s^{\prime}\in
S}c_{s,i,s^{\prime}}v_{i}(s^{\prime}).$

We can use the tuple of coefficients $(c_{s},(c_{s,i,s^{\prime}})_{i\leq
k,s^{\prime}\in S})_{s\in S}$ as a representation of $x$.

Henceforth, we assume the set $S_{M}$ of states of $M$ is $\\{1,\ldots,n\\}$.
We define the _affine semantics_
$\mathop{(\\!|}\mathit{Prop}^{m}\to\mathit{Prop}\mathop{|\\!)}$ of type
$\mathit{Prop}^{m}\to\mathit{Prop}$ by

$\displaystyle\mathop{(\\!|}\mathit{Prop}^{m}\to\mathit{Prop}\mathop{|\\!)}$
$\displaystyle=\\{(c_{i,j,k})_{i\in\\{1,\ldots,n\\},j\in\\{0,\ldots,m\\},k\in\\{0,\ldots,n\\}}\in[0,1]^{n(m+1)(n+1)}\mid$
$\displaystyle\qquad\qquad\sum_{j=0}^{m}\sum_{k=0}^{n}c_{i,j,k}\leq 1\mbox{
for every $i=1,\dots,n$.}\\}$

The tuple $(c_{i,j,k})_{i,j,k}\in\mathop{(\\!|}\kappa\mathop{|\\!)}$
represents the function
$f\in\llbracket\mathit{Prop}^{m}\to\mathit{Prop}\rrbracket$ such that, for
each $i\in S_{M}=\\{1,\ldots,n\\}$,

$f\,g_{1}\,\cdots\,g_{m}\,i=c_{i,0,0}+\Sigma_{j\in\\{1,\ldots,m\\},k\in\\{1,\ldots,n\\}}c_{i,j,k}\cdot
g_{j}(k).$

We write $(c_{i,j,k})_{i,j,k}^{\dagger}$ for the function $f$ above. The
_affine semantics_ $\mathop{(\\!|}\kappa\mathop{|\\!)}$ of refined type
$\kappa$ is defined by

$\mathop{(\\!|}\kappa\mathop{|\\!)}=\\{(c_{i,j,k})_{i,j,k}\in\mathop{(\\!|}\textit{tr}(\kappa)\mathop{|\\!)}\mid(c_{i,j,k})_{i,j,k}^{\dagger}\in\llbracket\kappa\rrbracket\\}.$

######  Lemma 5.19.

For every $x\in\llbracket\kappa\rrbracket$, there exists
$\mathbf{c}=(c_{i,j,k})_{i,j,k}\in\mathop{(\\!|}\kappa\mathop{|\\!)}$ such
that $x\sim_{\kappa}\mathbf{c}^{\dagger}$.

######  Proof 5.20.

Let
$\kappa=\mathit{Prop}^{T_{1},U_{1}}\to\dots\to\mathit{Prop}^{T_{m},U_{m}}\to\mathit{Prop}^{T,U}$.
Since $x\in\llbracket\kappa\rrbracket$, it is affine on
$\llbracket\mathit{Prop}^{T_{1},U_{1}}\rrbracket\times\dots\times\llbracket\mathit{Prop}^{T_{m},U_{m}}\rrbracket$,
i.e. for every
$(v_{1},\dots,v_{m})\in\llbracket\mathit{Prop}^{T_{1},U_{1}}\rrbracket\times\dots\times\llbracket\mathit{Prop}^{T_{m},U_{m}}\rrbracket$
and $i\in S_{M}$,

$x\,v_{1}\,\dots\,v_{m}\,i=c_{i,0,0}+\sum_{j=1}^{m}\sum_{k=1}^{n}c_{i,j,k}v_{j}(k).$

We can assume without loss of generality that $c_{i,j,k}=0$ if $k\in T_{j}$
since $v_{j}(k)=0$ in this case. Let $c_{i,0,k}=c_{i,j,0}=0$ for $j,k\geq 0$.
Then
$(c_{i,j,k})_{i,j,k}\in\mathop{(\\!|}\mathit{Prop}^{m}\to\mathit{Prop}\mathop{|\\!)}$
and $(c_{i,j,k})_{i,j,k}^{\dagger}\sim_{\kappa}x$. Therefore
$(c_{i,j,k})_{i,j,k}\in\mathop{(\\!|}\kappa\mathop{|\\!)}$ since the latter
implies $(c_{i,j,k})_{i,j,k}^{\dagger}\in\llbracket\kappa\rrbracket$.

######  Remark 5.21.

For $x\in\llbracket\kappa\rrbracket$,
$\mathbf{c}\in\mathop{(\\!|}\kappa\mathop{|\\!)}$ such that
$x\sim_{\kappa}\mathbf{c}^{\dagger}$ is not necessarily unique. The
representation becomes unique if one imposes the following conditions. Assume
that
$\kappa=\mathit{Prop}^{T_{1},U_{1}}\to\dots\to\mathit{Prop}^{T_{m},U_{m}}\to\mathit{Prop}^{T,U}$.

  * •

$c_{i,j,0}=c_{i,0,k}=0$ for $j,k>0$. Note that these coefficients are not used
in $(c_{i,j,k})_{i,j,k}^{\dagger}$.

  * •

$c_{i,j,k}=0$ if $k\in T_{j}$. If $k\in T_{j}$, then $v_{j}(k)=0$ and thus
$c_{i,j,k}$ does not affect the value of $(c_{i,j,k})_{i,j,k}^{\dagger}$. So
we can assume without loss of generality that $c_{i,j,k}=0$.

  * •

$c_{i,j,k}=0$ if $k\in U_{j}$. If $k\in U_{j}$, then $v_{j}(k)=1$. So, by
adding $c_{i,j,k}$ to the constant part $c_{i,0,0}$ if necessarily, we obtain
another representation that belongs to the same $\sim_{\kappa}$-equivalence
class and that $c_{i,j,k}=0$.

A representation $\mathbf{c}\in\mathop{(\\!|}\kappa\mathop{|\\!)}$ is
_canonical_ if it satisfies the above conditions. It is not difficult to see
that each $\sim_{\kappa}$-equivalence class has exactly one canonical
representation.

The second and third conditions are convenient for computing the affine
semantics of $\phi_{1}\lor\phi_{2}$ and $\phi_{1}\land\phi_{2}$. Suppose
$\emptyset;\Delta\vdash_{M}\phi_{i}:\mathit{Prop}^{T_{i},U_{i}}$ for
$i\in\\{1,2\\}$ and $T_{1}\cup U_{1}\cup T_{2}\cup U_{2}=S_{M}$. If
$(c_{i,j,k})_{i,j,k}$ and $(c^{\prime}_{i,j,k})_{i,j,k}$ are canonical
representations for the (affine) semantics of $\lambda\Delta.\phi_{1}$ and
$\lambda\Delta.\phi_{2}$ respectively, then the semantics
$(c^{\prime\prime}_{i,j,k})_{i,j,k})$ of $\lambda\Delta.\phi_{1}\land\phi_{2}$
is also obtained pointwise by:

$c^{\prime\prime}_{i,j,k}=\left\\{\begin{array}[]{ll}\min(c_{i,0,0},c^{\prime}_{i,0,0})&\mbox{if
$j=k=0$}\\\ c^{\prime}_{i,j,k}&\mbox{if $i\in U_{1}$}\\\ c_{i,j,k}&\mbox{if
$i\in U_{2}\setminus U_{1}$}\\\ 0&\mbox{otherwise}\end{array}\right.$

As stated before, we will describe the affine semantics of a well-typed PHFL
formula using the first-order theory of reals. Before doing so, however, we
show an example of directly computing the affine semantics.

######  Example 5.22.

Let $M$ be the Markov chain $(\\{1,2\\},P,\rho_{\mathit{AP}},1)$ where
$\rho_{\mathit{AP}}(p_{i})=\\{i\\}$ for $i\in\\{1,2\\}$, and
$P(1,1)=P(1,2)=0.5$ and $P(2,2)=1$, as depicted below.

Let $\phi$ be $\mu X.\lambda Y.(p_{2}\land Y)\lor\mathbin{\bigcirc}(p_{1}\land
X(Y))$. For $\rho\in\mathop{(\\!|}\mathcal{K}\mathop{|\\!)}$, we write
$\mathop{(\\!|}\mathcal{K};\Delta\vdash_{M}\phi:\kappa\mathop{|\\!)}(\rho)$
for the (canonical) matrix representation of
$\llbracket\textit{tr}(\mathcal{K})\vdash\lambda\textit{tr}(\Delta).\phi\rrbracket(\rho^{\dagger})$.
Let us compute
$\mathop{(\\!|}\emptyset;\emptyset\vdash_{M}\phi:\kappa\mathop{|\\!)}$ where
$\kappa=\mathit{Prop}^{\emptyset,\emptyset}\to\mathit{Prop}^{\emptyset,\emptyset}$.

Let $\rho$ be
$\\{X\mapsto(v_{i,j,k})_{i\in\\{1,2\\},j\in\\{0,1\\},k\in\\{0,1,2\\}}\\}$. We
write below an element $(c_{i,j,k})_{i,j,k}$ of
$\mathop{(\\!|}\kappa\mathop{|\\!)}$ as a matrix $(M_{1}\;M_{2})$, where
$M_{i}$ denotes $(c_{i,j,k})_{j,k}$. We can compute the affine semantics of
subexpressions as follows.

$\displaystyle\mathop{(\\!|}X\mathbin{:}\kappa;Y\mathbin{:}\mathit{Prop}^{\emptyset,\emptyset}\vdash_{M}Y:\mathit{Prop}^{\emptyset,\emptyset}\mathop{|\\!)}(\rho)$
$\displaystyle=\left(\begin{array}[]{lllclll}0&0&0&&0&0&0\\\ 0&1&0&&0&0&1\\\
\end{array}\right)$
$\displaystyle\mathop{(\\!|}X\mathbin{:}\kappa;Y\mathbin{:}\mathit{Prop}^{\emptyset,\emptyset}\vdash_{M}p_{2}:\mathit{Prop}^{\\{1\\},\\{2\\}}\mathop{|\\!)}(\rho)$
$\displaystyle=\left(\begin{array}[]{lllclll}0&0&0&&1&0&0\\\ 0&0&0&&0&0&0\\\
\end{array}\right)$
$\displaystyle\mathop{(\\!|}X\mathbin{:}\kappa;Y\mathbin{:}\mathit{Prop}^{\emptyset,\emptyset}\vdash_{M}p_{2}\land
Y:\mathit{Prop}^{\\{1\\},\emptyset}\mathop{|\\!)}(\rho)$
$\displaystyle=\left(\begin{array}[]{lllclll}0&0&0&&0&0&0\\\ 0&0&0&&0&0&1\\\
\end{array}\right)$ (Recall the discussion in the latter half of Remark 5.21.)
$\displaystyle\mathop{(\\!|}X\mathbin{:}\kappa;Y\mathbin{:}\mathit{Prop}^{\emptyset,\emptyset}\vdash_{M}X(Y):\mathit{Prop}^{\emptyset,\emptyset}\mathop{|\\!)}(\rho)$
$\displaystyle=\left(\begin{array}[]{lllclll}v_{1,0,0}&0&0&&v_{2,0,0}&0&0\\\
0&v_{1,1,1}&v_{1,1,2}&&0&v_{2,1,1}&v_{2,1,2}\\\ \end{array}\right)$
$\displaystyle\mathop{(\\!|}X\mathbin{:}\kappa;Y\mathbin{:}\mathit{Prop}^{\emptyset,\emptyset}\vdash_{M}\mathbin{\bigcirc}X(Y):\mathit{Prop}^{\emptyset,\emptyset}\mathop{|\\!)}(\rho)$
$\displaystyle\qquad=\left(\begin{array}[]{lllclll}\frac{1}{2}(v_{1,0,0}+v_{2,0,0})&0&0&&v_{2,0,0}&0&0\\\
0&\frac{1}{2}(v_{1,1,1}+v_{2,1,1})&\frac{1}{2}(v_{1,1,2}+v_{2,1,2})&&0&v_{2,1,1}&v_{2,1,2}\\\
\end{array}\right)\hfill$ ($\mathbin{\bigcirc}$ can be computed pointwise)
$\displaystyle\mathop{(\\!|}X\mathbin{:}\kappa;Y\mathbin{:}\mathit{Prop}^{\emptyset,\emptyset}\vdash_{M}p_{1}:\mathit{Prop}^{\\{2\\},\\{1\\}}\mathop{|\\!)}(\rho)=\left(\begin{array}[]{lllclll}1&0&0&&0&0&0\\\
0&0&0&&0&0&0\\\ \end{array}\right)$
$\displaystyle\mathop{(\\!|}X\mathbin{:}\kappa;Y\mathbin{:}\mathit{Prop}^{\emptyset,\emptyset}\vdash_{M}p_{1}\land\mathbin{\bigcirc}X(Y):\mathit{Prop}^{\\{2\\},\emptyset}\mathop{|\\!)}(\rho)$
$\displaystyle\qquad=\left(\begin{array}[]{lllclll}\frac{1}{2}(v_{1,0,0}+v_{2,0,0})&0&0&&0&0&0\\\
0&\frac{1}{2}(v_{1,1,1}+v_{2,1,1})&\frac{1}{2}(v_{1,1,2}+v_{2,1,2})&&0&0&0\end{array}\right)$
$\displaystyle\mathop{(\\!|}X\mathbin{:}\kappa;Y\mathbin{:}\mathit{Prop}^{\emptyset,\emptyset}\vdash_{M}(p_{2}\land
Y)\lor(p_{1}\land\mathbin{\bigcirc}X(Y)):\mathit{Prop}^{\emptyset,\emptyset}\mathop{|\\!)}(\rho)$
$\displaystyle\qquad=\left(\begin{array}[]{lllclll}\frac{1}{2}(v_{1,0,0}+v_{2,0,0})&0&0&&0&0&0\\\
0&\frac{1}{2}(v_{1,1,1}+v_{2,1,1})&\frac{1}{2}(v_{1,1,2}+v_{2,1,2})&&0&0&1\end{array}\right)$
$\displaystyle\mathop{(\\!|}X\mathbin{:}\kappa;\emptyset\vdash_{M}\lambda
Y.(p_{2}\land
Y)\lor(p_{1}\land\mathbin{\bigcirc}X(Y)):\kappa\mathop{|\\!)}(\rho)$
$\displaystyle\qquad=\left(\begin{array}[]{lllclll}\frac{1}{2}(v_{1,0,0}+v_{2,0,0})&0&0&&0&0&0\\\
0&\frac{1}{2}(v_{1,1,1}+v_{2,1,1})&\frac{1}{2}(v_{1,1,2}+v_{2,1,2})&&0&0&1\end{array}\right)$

Thus, we have:

$\small\begin{array}[]{l}\mathop{(\\!|}\emptyset;\emptyset\vdash_{M}\phi:\kappa\mathop{|\\!)}(\emptyset)\\\
=\mathit{LFP}(\lambda\left(\begin{array}[]{lllclll}v_{1,0,0}&\\_&\\_&&v_{2,0,0}&\\_&\\_\\\
\\_&v_{1,1,1}&v_{1,1,2}&&\\_&v_{2,1,1}&v_{2,1,2}\end{array}\right).\\\
\qquad\qquad\left(\begin{array}[]{lllclll}\frac{1}{2}(v_{1,0,0}+v_{2,0,0})&0&0&&0&0&0\\\
0&\frac{1}{2}(v_{1,1,1}+v_{2,1,1})&\frac{1}{2}(v_{1,1,2}+v_{2,1,2})&&0&0&1\end{array}\right)\\\
=\left(\begin{array}[]{lllclll}0&0&0&&0&0&0\\\ 0&0&1&&0&0&1\\\
\end{array}\right).\\\ \end{array}\\\ $

Using the result above, we obtain:

$\mathop{(\\!|}\emptyset;\emptyset\vdash_{M}\phi(p):\kappa\mathop{|\\!)}(\emptyset)=\left(\begin{array}[]{lllclll}1&0&0&&1&0&0\\\
\end{array}\right).$

Thus, $\phi(p_{2})$ holds at state $1$ with probability $1$. ∎

In the example above, we have directly computed the affine semantics. In
general, however, we describe the affine semantics $(c_{i,j,k})_{i,j,k}$ by
using logical formulas, to deal with arbitrary alternations of fixpoint
operators. All the operations and properties on $\llbracket\kappa\rrbracket$
required for computing the affine semantics are definable by using the first-
order theory of reals. Assume
$\kappa=\mathit{Prop}^{T_{1},U_{1}}\to\dots\to\mathit{Prop}^{T_{m},U_{m}}\to\mathit{Prop}^{T,U}$
and let $\mathbf{c}=(c_{i,j,k})_{i,j,k}\in\mathop{(\\!|}\kappa\mathop{|\\!)}$.
For example, the value $\mathbf{c}^{\dagger}\,v_{1}\,\dots\,v_{m}\,i$ can be
represented as a term

$c_{i,0,0}+\sum_{j=1}^{m}\sum_{k=1}^{n}c_{i,j,k}v_{j}(k).$

Then, for $\mathbf{c},\mathbf{d}\in\mathop{(\\!|}\kappa\mathop{|\\!)}$, the
relation $\mathbf{c}\precsim_{\kappa}\mathbf{d}$ is written as

$\displaystyle\forall v_{1},\dots,v_{m}\in[0,1]^{n}.$
$\displaystyle\Big{(}\bigwedge_{j=1,\dots,m}v_{j}\in\mathop{(\\!|}\mathit{Prop}^{T_{j},U_{j}}\mathop{|\\!)}\Big{)}\Rightarrow\bigwedge_{i=1,\dots,n}\Big{[}\big{(}\mathbf{c}^{\dagger}\,v_{1}\,\dots\,v_{k}\,i\big{)}\leq\big{(}\mathbf{d}^{\dagger}\,v_{1}\,\dots\,v_{k}\,i\big{)}\Big{]}$

and $\mathbf{c}^{\dagger}\sim_{\kappa}\mathbf{d}^{\dagger}$ as

$\mathbf{c}^{\dagger}\precsim_{\kappa}\mathbf{d}^{\dagger}~{}~{}\wedge~{}~{}\mathbf{d}^{\dagger}\precsim_{\kappa}\mathbf{c}^{\dagger}.$

The meets and joins are also describable: for example,
$\mathbf{c}_{1}^{\dagger}\sqcap\mathbf{c}_{2}^{\dagger}\sim_{\kappa}\mathbf{d}^{\dagger}$
is equivalent to

$\displaystyle\forall
v_{1},\dots,v_{m}\in[0,1]^{n}.\Big{(}\bigwedge_{j=1,\dots,m}v_{j}\in\mathop{(\\!|}\mathit{Prop}^{T_{j},U_{j}}\mathop{|\\!)}\Big{)}$
$\displaystyle\qquad\Rightarrow\bigwedge_{i=1,\dots,n}\Big{[}\big{(}\mathbf{d}^{\dagger}\,v_{1}\,\dots\,v_{k}\,i\big{)}=\max\Big{(}(\mathbf{c}_{1}^{\dagger}\,v_{1}\,\dots\,v_{k}\,i),~{}(\mathbf{c}_{2}^{\dagger}\,v_{1}\,\dots\,v_{k}\,i)\Big{)}\Big{]};$

note that $\max$ as well as $\min$ is an operation definable in the first-
order theory of reals.

######  Lemma 5.23.

Suppose $\mathcal{K};\Delta\vdash_{M}\phi:\kappa$ and
$\mathcal{K}=\\{X_{1}:\kappa_{1},\dots,X_{N}:\kappa_{N}\\}$. Then one can
effectively construct a formula $\Phi$ of the first-order real arithmetic such
that, for every
$\mathbf{c}_{\ell}\in\mathop{(\\!|}\kappa_{\ell}\mathop{|\\!)}$
($\ell=1,\dots,N$) and
$\mathbf{d}\in\mathop{(\\!|}\Delta\to\kappa\mathop{|\\!)}$,

$\Phi(\mathbf{c}_{1},\dots,\mathbf{c}_{N},\mathbf{d})~{}~{}\Leftrightarrow~{}~{}\llbracket\lambda\Delta.\phi\rrbracket(\\{X_{\ell}\mapsto\mathbf{c}_{\ell}^{\dagger}\mid
1\leq\ell\leq N\\})\sim_{\Delta\to\kappa}\mathbf{d}^{\dagger}.$

######  Proof 5.24.

By induction on the structure of derivation
$\mathcal{K};\Delta\vdash_{M}\phi:\kappa$. The most cases are easy. For
example, consider the case that the last rule is (T-Conj). Then
$\phi=\phi_{1}\wedge\phi_{2}$ and
$\mathcal{K};\Delta\vdash_{M}\phi_{i}:\mathit{Prop}^{T_{i},U_{i}}$ for
$i=1,2$. By the induction hypothesis, we have predicates $\Phi_{1}$ and
$\Phi_{2}$ representing $\llbracket\lambda\Delta.\phi_{1}\rrbracket$ and
$\llbracket\lambda\Delta.\phi_{2}\rrbracket$. Then
$\Phi(\mathbf{c}_{1},\dots,\mathbf{c}_{N},\mathbf{d})$ is defined as

$\displaystyle\exists\mathbf{d}_{1}\in\mathop{(\\!|}\Delta\to\mathit{Prop}^{T_{1},U_{1}}\mathop{|\\!)}.~{}\exists\mathbf{d}_{2}\in\mathop{(\\!|}\Delta\to\mathit{Prop}^{T_{2},U_{2}}\mathop{|\\!)}.$
$\displaystyle\quad\Phi_{1}(\mathbf{c}_{1},\dots,\mathbf{c}_{N},\mathbf{d}_{1})~{}~{}\wedge~{}~{}\Phi_{2}(\mathbf{c}_{1},\dots,\mathbf{c}_{N},\mathbf{d}_{2})~{}~{}\wedge~{}~{}\mathbf{d}^{\dagger}\sim_{\kappa}\mathbf{d}_{1}^{\dagger}\sqcap\mathbf{d}_{2}^{\dagger}.$

Since
$\llbracket\lambda\Delta.\phi_{i}\rrbracket(\\{X_{\ell}\mapsto\mathbf{c}_{\ell}^{\dagger}\mid
1\leq\ell\leq
N\\})\in\llbracket\Delta\to\mathit{Prop}^{T_{i},U_{i}}\rrbracket$ by Theorem
7, there exists a
$\mathbf{d}_{i}\in\mathop{(\\!|}\Delta\to\mathit{Prop}^{T_{i},U_{i}}\mathop{|\\!)}$
such that $\Phi_{i}(\mathbf{c}_{1},\dots,\mathbf{c}_{N},\mathbf{d}_{i})$.

The only non-trivial cases are fixpoints. Consider the case that the last rule
is (T-Mu). Then $\phi=\nu X.\phi_{0}$ and
$\mathcal{K},X:\kappa;\Delta\vdash_{M}\phi_{0}:\kappa$. By the induction
hypothesis, we have $\Phi_{0}$ representing the semantics of $\phi_{0}$. Then
$\Phi(\mathbf{c}_{1},\dots,\mathbf{c}_{N},\mathbf{d})$ is defined as

$\Phi_{0}(\mathbf{c}_{1},\dots,\mathbf{c}_{N},\mathbf{d},\mathbf{d})~{}~{}\wedge~{}~{}\forall\mathbf{d}^{\prime}\in\mathop{(\\!|}\kappa\mathop{|\\!)}.\Phi_{0}(\mathbf{c}_{1},\dots,\mathbf{c}_{N},\mathbf{d}^{\prime},\mathbf{d}^{\prime})\Rightarrow\mathbf{d}^{\dagger}\precsim_{\kappa}\mathbf{d}^{\prime\dagger}.$

The first condition says that $\mathbf{d}^{\dagger}$ is a fixpoint of
$\llbracket\lambda X.\phi_{0}\rrbracket$ modulo $\sim_{\kappa}$. The second
condition says that $\mathbf{d}^{\dagger}$ is a least element in the set of
fixpoints $\mathbf{d}^{\prime\dagger}$ of $\llbracket\lambda
X.\phi_{0}\rrbracket$ modulo $\sim_{\kappa}$. Correctness of the above formula
follows from Corollary 5.17.

######  Theorem 5.24.

Given a closed formula $\phi$ and a Markov chain $M$ such that
$\emptyset;\emptyset\vdash_{M}\phi:\mathit{Prop}^{T,U}$, it is decidable
whether $M\models\phi$.

######  Proof 5.25.

Assume that $s_{\text{in},M}=1$. By Lemma 5.23, one can effectively construct
a formula $\Phi$ of the first-order real arithmetic such that
$\Phi(r_{1},\dots,r_{n})$ is valid if and only if
$\llbracket\phi\rrbracket_{M}(\emptyset)(i)=r_{i}$ for every $i=1,\dots,n$.
Hence $M\models\phi$ if and only if $\exists
r_{2},\dots,r_{n}.\Phi(1,r_{2},\dots,r_{n})$. The validity of this formula is
decidable [Tar51].

######  Remark 5.26.

The formula obtained in the proof above contains both universal and
existential quantifiers in general; hence the complexity is doubly exponential
time in general [DH88]. However, if $\phi$ is of the form
$[\phi^{\prime}]_{\geq r}$ where $\phi^{\prime}$ contains no occurrences of
$\nu$ and $[\cdot]_{J}$, then we can express $\Phi$ using only existential
quantifiers, and appeal to a decision algorithm for the existential theory of
the reals, whose complexity is PSPACE [Can88]. In fact, to deal with
$\mu$-formulas in the restricted fragment, it suffices to consider only
inequalities of the form $\mathit{LFP}(h)\preceq_{\kappa}x$, which can be
represented by an existential formula $\exists
x^{\prime}.(x^{\prime}\precsim_{\kappa}x\land
h\,x^{\prime}\precsim_{\kappa}x^{\prime})$. Note that $\precsim$ is definable
by a quantifier-free formula, as stated in the lemma below. Note also that the
semantics of conjunctions and disjunctions can be expressed without using
quantifiers, as discussed in Remark 5.21.

######  Lemma 5.27.

Let
$\kappa=\mathit{Prop}^{T_{1},U_{1}}\to\dots\to\mathit{Prop}^{T_{m},U_{m}}\to\mathit{Prop}^{T,U}$.
For $J\subseteq\\{1,\dots,m\\}\times\\{1,\dots,n\\}$, we write
$J\in\mathcal{J}(\kappa)$ if the characteristic function belongs to
$\prod_{i=1}^{m}\llbracket\mathit{Prop}^{T_{i},U_{i}}\rrbracket$, i.e.,

  * •

if $k\in T_{j}$, then $(k,j)\notin J$, and

  * •

if $k\in U_{j}$, then $(k,j)\in J$.

Let
$(c_{i,j,k})_{i,j,k},(c^{\prime}_{i,j,k})_{i,j,k}\in\mathop{(\\!|}\kappa\mathop{|\\!)}$.
Then,
$(c_{i,j,k})_{i,j,k}^{\dagger}\preceq_{\kappa}(c^{\prime}_{i,j,k})_{i,j,k}^{\dagger}$
if and only if:

$\bigwedge_{i\in\\{1,\ldots,n\\}}\bigwedge_{J\in\mathcal{J}(\kappa)}\left(c_{i,0,0}+\sum_{(j,k)\in
J}c_{i,j,k}\leq c^{\prime}_{i,0,0}+\sum_{(j,k)\in
J}c^{\prime}_{i,j,k}\right).$

######  Proof 5.28.

  * If: Suppose $g_{1}\in\llbracket\mathit{Prop}^{T_{1},U_{1}}\rrbracket,\ldots,g_{m}\in\llbracket\mathit{Prop}^{T_{m},U_{m}}\rrbracket$. We regard $(g_{1},\dots,g_{m})=(g_{j}(k))_{j\in\\{1,\dots,m\\},k\in\\{1,\dots,n\\}}$ as an $mn$-dimensional vector. We also identify $J\in\mathcal{J}(\kappa)$ with $(h_{j}(k))_{j,k}$ where $h_{j}(k)=1$ if $(j,k)\in J$ and $h_{j}(k)=0$ if $(j,k)\notin J$.

Let $0=s_{0}<s_{1}<s_{2}<\dots<s_{N}=1$ be the sequence obtained by sorting
$\\{g_{j}(k)\mid 1\leq j\leq m,1\leq k\leq n\\}\cup\\{0,1\\}$. For each
$\ell>0$, we define $J_{\ell}$ and $r_{\ell}$ by

$J_{\ell}=\\{(j,k)\mid s_{\ell}\leq h_{j}(k)\\}\qquad\mbox{and}\qquad
r_{\ell}=s_{\ell}-s_{\ell-1}.$

Then

$(g_{1},\dots,g_{m})=\sum_{\ell}r_{\ell}J_{\ell}.$

Hence

$\displaystyle(c_{i,j,k})_{i,j,k}^{\dagger}\,g_{1}\,\dots\,g_{m}\,i$
$\displaystyle=\sum_{\ell}r_{\ell}(c_{i,0,0}+\sum_{(j,k)\in
J_{\ell}}c_{i,j,k})$
$\displaystyle\leq\sum_{\ell}r_{\ell}(c^{\prime}_{i,0,0}+\sum_{(j,k)\in
J_{\ell}}c^{\prime}_{i,j,k})$
$\displaystyle=(c_{i,j,k})_{i,j,k}^{\dagger}\,g_{1}\,\dots\,g_{m}\,i.$

  * Only if: For each $J\in\mathcal{J}(\kappa)$, let $g_{j}$ be the element of $\llbracket\mathit{Prop}\rrbracket$ such that $g_{j}(k)=1$ if $(j,k)\in J$ and $g_{j}(k)=0$ if $(j,k)\not\in J$. Then $g_{j}\in\llbracket\mathit{Prop}^{T_{j},U_{j}}\rrbracket$ for every $j=1,\dots,m$. We have

$c_{i,0,0}+\sum_{(j,k)\in
J}c_{i,j,k}=(c_{i,j,k})_{i,j,k}^{\dagger}\,g_{1}\,\cdots\,g_{m}\,i\leq(c^{\prime}_{i,j,k})_{i,j,k}^{\dagger}\,g_{1}\,\cdots\,g_{m}\,i=c^{\prime}_{i,0,0}+\sum_{(j,k)\in
J}c^{\prime}_{i,j,k},$

as required.

###  5.3. Expressivity

We have already seen in Example 5.3 and Lemma 5.6 that the decidable fragment
of the order-1 PHFL model checking problem strictly subsumes
$\mu^{p}{}$-calculus model checking. To provide a further evidence of the
expressivity of the decidable fragment, in this subsection, we show that the
termination problem for recursive Markov chains (or, probabilistic pushdown
systems) [EY09, BEKK13] can be encoded into the decidable fragment of order-1
PHFL model checking. Since recursive Markov chains are known to be equivalent
to order-1 probabilistic higher-order recursion schemes (PHORS) [KLG20], we
encode below the termination problem for the latter into the PHFL model
checking problem.

We first recall the definition of PHORS, specialized for order 1.

######  Definition 5.29.

An order-1 PHORS $\mathcal{G}$ is a triple $(\mathcal{X},\mathcal{R},t)$,
where:

  * •

$\mathcal{X}$ is a finite map from (order-1) variables to their arities;

  * •

$\mathcal{R}$ is a finite set of rules of the form:

$X\,y_{1}\,\cdots,y_{\mathcal{X}(X)}\to t_{L}\oplus_{p}t_{R},$

where $t_{L},t_{R}$ range over the set of
$(\mathcal{X},\\{y_{1},\ldots,y_{\mathcal{X}(X)}\\})$-terms. Here, the set of
$(\mathcal{X},V)$-terms, ranged over by $t$, is defined by the grammar:

$t::=\mathtt{e}\mid y\mid X\,t_{1}\,\cdots,t_{\mathcal{X}(X)},$

where $y$ and $X$ range over $V$ and $\mathit{dom}(\mathcal{X})$ respectively,
and $\mathtt{e}$ is a special symbol denoting termination.

  * •

$t$ is a $(\mathcal{X},\emptyset)$-term.

For
$\mathcal{G}=(\mathcal{X}_{\mathcal{G}},\mathcal{R}_{\mathcal{G}},t_{\mathcal{G}})$,
the reduction relation
$t\stackrel{{\scriptstyle\pi,p}}{{\longrightarrow}}_{\mathcal{G}}t^{\prime}$
on terms (where $\pi\in\\{L,R\\}^{*}$ and $p\in[0,1]$) is defined by:

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\end{array}}{\begin{array}[]{@{}c@{}}t\stackrel{{\scriptstyle\epsilon,1}}{{\longrightarrow}}_{\mathcal{G}}t\end{array}}$

$\displaystyle\frac{\begin{array}[]{@{}c@{}}t\stackrel{{\scriptstyle\pi,q}}{{\longrightarrow}}_{\mathcal{G}}X\,t_{1}\,\cdots\,t_{k}\quad\quad
X\,y_{1}\,\cdots\,y_{k}\to
t_{L}\oplus_{p}t_{R}\in\mathcal{R}_{\mathcal{G}}\end{array}}{\begin{array}[]{@{}c@{}}t\stackrel{{\scriptstyle\pi
L,q\cdot
p}}{{\longrightarrow}}_{\mathcal{G}}[t_{1}/y_{1},\ldots,t_{k}/y_{k}]t_{L}\end{array}}$

$\displaystyle\frac{\begin{array}[]{@{}c@{}}t\stackrel{{\scriptstyle\pi,q}}{{\longrightarrow}}_{\mathcal{G}}X\,t_{1}\,\cdots\,t_{k}\quad\quad
X\,y_{1}\,\cdots\,y_{k}\to
t_{L}\oplus_{p}t_{R}\in\mathcal{R}_{\mathcal{G}}\end{array}}{\begin{array}[]{@{}c@{}}t\stackrel{{\scriptstyle\pi
R,q\cdot(1-p)}}{{\longrightarrow}}_{\mathcal{G}}[t_{1}/y_{1},\ldots,t_{k}/y_{k}]t_{R}\end{array}}$

Note that the reduction is deterministic: for $\pi\in\\{L,R\\}^{*}$, there
exists at most one $(p,t^{\prime})$ such that
$t\stackrel{{\scriptstyle\pi,p}}{{\longrightarrow}}_{\mathcal{G}}t^{\prime}$.
The _termination probability_ of
$\mathcal{G}=(\mathcal{X}_{\mathcal{G}},\mathcal{R}_{\mathcal{G}},t_{\mathcal{G}})$,
written $\mathit{ProbT}(\mathcal{G})$, is defined by:

$\begin{array}[]{l}\mathit{ProbT}(\mathcal{G},t,\pi)=\left\\{\begin{array}[]{ll}p&\mbox{if
$t\stackrel{{\scriptstyle\pi,p}}{{\longrightarrow}}_{\mathcal{G}}\mathtt{e}$}\\\
0&\mbox{otherwise}\end{array}\right.\\\
\mathit{ProbT}(\mathcal{G})=\sum_{\pi\in\\{L,R\\}^{*}}\mathit{ProbT}(\mathcal{G},t_{\mathcal{G}},\pi).\end{array}$

The following example has been taken from [KLG20].

######  Example 5.30.

Let $\mathcal{G}$ be the order-1 PHORS $(\mathcal{X},\mathcal{R},X_{0})$,
where:

$\begin{array}[]{l}\mathcal{X}=\\{X_{0}\mapsto 0,F\mapsto 1\\}\\\
\mathcal{R}=\\{X_{0}\ =\ X_{1}\,\mathtt{e}\oplus_{1}X_{0},\quad X_{1}\,y\ =\
y\oplus_{p}X_{1}(X_{1}\,y)\\}.\end{array}$

Then, we have $X_{0}\stackrel{{\scriptstyle
L,1}}{{\longrightarrow}}_{\mathcal{G}}X_{1}\,\mathtt{e}\stackrel{{\scriptstyle
L,p}}{{\longrightarrow}}_{\mathcal{G}}\mathtt{e}$ and
$X_{0}\stackrel{{\scriptstyle
L,1}}{{\longrightarrow}}_{\mathcal{G}}X_{1}\,\mathtt{e}\stackrel{{\scriptstyle
R,1-p}}{{\longrightarrow}}_{\mathcal{G}}X_{1}(X_{1}\,\mathtt{e})\stackrel{{\scriptstyle
L,p}}{{\longrightarrow}}_{\mathcal{G}}X_{1}\,\mathtt{e}\stackrel{{\scriptstyle
L,p}}{{\longrightarrow}}_{\mathcal{G}}\mathtt{e}$. The termination probability
$\mathit{ProbT}(\mathcal{G})$ is $1$ if $p\geq\frac{1}{2}$ and $\frac{p}{1-p}$
if $p<\frac{1}{2}$. ∎

We now encode an order-1 PHORS $\mathcal{G}$ into a Markov chain
$M_{\mathcal{G}}$ and a closed order-1 PHFL formula $\phi_{\mathcal{G}}$ such
that
$\emptyset;\emptyset\vdash_{M}\phi_{\mathcal{G}}:\mathit{Prop}^{\emptyset,\emptyset}$
and $\mathit{ProbT}(\mathcal{G})$ coincides with the probability that
$\phi_{\mathcal{G}}$ holds at the initial state of $M_{\mathcal{G}}$ (i.e.,
$\mathit{ProbT}(\mathcal{G}=\llbracket\phi_{\mathcal{G}}\rrbracket(\emptyset)(s_{\text{in}})$).
We first give a construction of $M$. Let $\\{p_{1},\ldots,p_{m}\\}$ be the set
$\\{p,1-p\mid\oplus_{p}\mbox{ occurs in }\mathcal{G}\\}$. We assume
$p_{1}<p_{2}<\cdots<p_{m}$. We define the Markov chain
$M_{\mathcal{G}}=(S,P,\rho_{\mathit{AP}},s_{\text{in}})$ as follows.

  * •

$S=\\{s_{0},s_{1},\dots,s_{m+1}\\}$,

  * •

$P$ satisfies $P(s_{0},s_{1})=p_{1}$, $P(s_{0},s_{i})=p_{i}-p_{i-1}$ for
$2\leq i\leq m$, $P(s_{0},s_{m+1})=1-p_{m}$, $P(s_{i},s_{0})=1$ for $1\leq
i\leq m+1$ and $P(s_{i},s_{j})=0$ otherwise,

  * •

$\rho_{\mathit{AP}}(P_{i})=\\{s_{i}\\}$ for each $0\leq i\leq m+1$, and

  * •

$s_{\text{in}}=s_{0}$.

Note that $\llbracket\mathbin{\bigcirc}(P_{1}\lor\cdots\lor
P_{i})\rrbracket(\emptyset)(s_{0})=p_{i}$ and
$\llbracket\mathbin{\bigcirc}(P_{i+1}\lor\cdots\lor
P_{m+1})\rrbracket(\emptyset)(s_{0})=1-p_{i}$. Now for each term of $t$ of
PHORS $\mathcal{G}$, we construct a formula $\left<t\right>$, so that the
termination probability of $t$ coincides with the probability that $\phi_{t}$
holds at $s_{0}$. The translation is given by:

$\begin{array}[]{l}\left<\mathtt{e}\right>=\text{true}\qquad\left<y\right>=y\qquad\left<X_{i}\,t_{1}\,\cdots\,t_{k}\right>=X_{i}\,\left<t_{1}\right>\,\cdots\,\left<t_{k}\right>.\end{array}$

For each rule
$X_{i}\,y_{i}\,\cdots\,y_{\mathcal{X}(X_{i})}=t_{L}\oplus_{p_{i}}t_{R}$ of
$\mathcal{R}$, we construct the following equality on PHFL formulas:

$X_{i}=\lambda
y_{1},\ldots,y_{\mathcal{X}(X_{i})}.\mathbin{\bigcirc}(((P_{1}\lor\cdots\lor
P_{i})\land\mathbin{\bigcirc}\left<t_{L}\right>)\lor((P_{i+1}\lor\cdots\lor
P_{m+1})\land\mathbin{\bigcirc}\left<t_{R}\right>)).$

We thus obtain a system of mutually recursive equations
$\\{X_{1}=\phi_{1},\cdots,X_{k}=\phi_{k}\\}$, whose least solution $\theta$
(which maps each $X_{i}$ to a formula $\psi_{i}$ that satisfies
$\psi_{i}=\theta\phi_{i}$) can be represented by using the least fixpoint
operators in an obvious manner. We then let $\phi_{\mathcal{G}}$ be
$\theta\left<t_{\mathcal{G}}\right>$.

######  Example 5.31.

Recall $\mathcal{G}$ in Example 5.30. Assuming $p<\frac{1}{2}$,
$M_{\mathcal{G}}$ is:

  * •

$S=\\{s_{0},s_{1},s_{2},s_{3},s_{4}\\}$.

  * •

$P(s_{0},s_{1})=p$, $P(s_{0},s_{2})=1-2p$, $P(s_{0},s_{3})=p$,
$P(s_{0},s_{4})=0$, $P(s_{i},s_{0})=1$ for $i\in\\{1,2,3,4\\}$ and
$P(s_{i},s_{j})=0$ for $i,j>0$.

  * •

$\rho_{\mathit{AP}}(P_{i})=\\{s_{i}\\}$ for each $i\in\\{0,\dots,4\\}$, and

  * •

$s_{\text{in}}=s_{0}$.

The rules of $\mathcal{G}$ are translated to the following equations:

$\begin{array}[]{l}X_{0}=\mathbin{\bigcirc}(((P_{1}\lor P_{2}\lor
P_{3})\land\mathbin{\bigcirc}(X_{1}\,\mathtt{e}))\lor(P_{4}\land\mathbin{\bigcirc}X_{0}))\\\
X_{1}=\lambda
y.\mathbin{\bigcirc}((P_{1}\land\mathbin{\bigcirc}y)\lor((P_{2}\lor P_{3}\lor
P_{4})\land\mathbin{\bigcirc}(X_{1}(X_{1}\,y))))\end{array}$

Thus, $\phi_{\mathcal{G}}$ is given as:

$\mu X_{0}.\mathbin{\bigcirc}(((P_{1}\lor P_{2}\lor
P_{3})\land\mathbin{\bigcirc}(\psi_{1}\,\mathtt{e}))\lor(P_{4}\land\mathbin{\bigcirc}X_{0})),$

where $\psi_{1}$ is:

$\mu X_{1}.\lambda
y.\mathbin{\bigcirc}((P_{1}\land\mathbin{\bigcirc}y)\lor((P_{2}\lor P_{3}\lor
P_{4})\land\mathbin{\bigcirc}(X_{1}(X_{1}\,y)))).$

Actually, $\phi_{\mathcal{G}}$ can be simplified to $\psi_{1}\,\mathtt{e}$ in
this case. ∎

To see the correctness of the above encoding, recall that
$\llbracket\mathbin{\bigcirc}(P_{1}\lor\cdots\lor
P_{i})\rrbracket(\emptyset)(s_{0})=p_{i}$ and
$\llbracket\mathbin{\bigcirc}(P_{i+1}\lor\cdots\lor
P_{m+1})\rrbracket(\emptyset)(s_{0})=1-p_{i}$. Thus, by the equality on
$X_{i}$ above, the probability that
$\theta(X_{i}\,\left<t_{1}\right>\,\cdots,\left<t_{\mathcal{X}(X_{i})}\right>)$
holds at $s_{0}$ is equivalent to $p_{i}\cdot q_{L}+(1-p_{i})\cdot q_{R}$,
where $q_{L}$ and $q_{R}$ are respectively the probabilities that
$\theta(\left<[t_{1}/y_{1},\ldots,t_{\mathcal{X}(X_{i})}/y_{\mathcal{X}(X_{i})}]t_{L}\right>)$
and
$\theta(\left<[t_{1}/y_{1},\ldots,t_{\mathcal{X}(X_{i})}/y_{\mathcal{X}(X_{i})}]t_{R}\right>)$
hold at $s_{0}$. Thus, the formula
$\theta(X_{i}\,\left<t_{1}\right>\,\cdots,\left<t_{\mathcal{X}(X_{i})}\right>)$
mimics the termination probability of
$X_{i}\,\left<t_{1}\right>\,\cdots,\left<t_{\mathcal{X}(X_{i})}\right>$, which
is equivalent to $p_{i}\cdot q^{\prime}_{L}+(1-p_{i})\cdot q^{\prime}_{R}$,
where $q^{\prime}_{L}$ and $q^{\prime}_{R}$ are respectively the termination
probabilities of
$[t_{1}/y_{1},\ldots,t_{\mathcal{X}(X_{i})}/y_{\mathcal{X}(X_{i})}]t_{L}$ and
$[t_{1}/y_{1},\ldots,t_{\mathcal{X}(X_{i})}/y_{\mathcal{X}(X_{i})}]t_{R}$. We
omit a formal proof of correctness of the encoding.

We now check that $\phi_{\mathcal{G}}$ belongs to the restricted fragment. To
this end, it suffices to check that, for each rule $X\,y_{1}\,\cdots\,y_{k}\to
t_{L}\oplus_{p}t_{R}\in\mathcal{R}$, the type judgment:

$\mathcal{K}_{\mathcal{X}};\Delta\vdash_{M_{\mathcal{G}}}\mathbin{\bigcirc}(((P_{1}\lor\cdots\lor
P_{i})\land\mathbin{\bigcirc}\left<t_{L}\right>)\lor((P_{i+1}\lor\cdots\lor
P_{m+1})\land\mathbin{\bigcirc}\left<t_{R}\right>)):\mathit{Prop}^{\emptyset,\emptyset}$

holds for
$\mathcal{K}_{\mathcal{X}}=\\{X\mathbin{:}(\mathit{Prop}^{\emptyset,\emptyset})^{\mathcal{X}(X)}\to\mathit{Prop}^{\emptyset,\emptyset}\mid
X\in\mathit{dom}(\mathcal{X})\\}$ and
$\Delta=y_{1}\mathbin{:}\mathit{Prop}^{\emptyset,\emptyset},\ldots,y_{k}\mathbin{:}\mathit{Prop}^{\emptyset,\emptyset}$.

By a straightforward induction on the structure of $t_{L}$, we have:
$\mathcal{K}_{\mathcal{X}};\Delta\vdash_{M_{\mathcal{G}}}\left<t_{L}\right>:\mathit{Prop}^{\emptyset,\emptyset}$,
which implies
$\mathcal{K}_{\mathcal{X}};\Delta\vdash_{M_{\mathcal{G}}}\mathbin{\bigcirc}\left<t_{L}\right>:\mathit{Prop}^{\emptyset,\emptyset}$.
We also have:

$\mathcal{K}_{\mathcal{X}};\Delta\vdash_{M_{\mathcal{G}}}P_{1}\lor\cdots\lor
P_{i}:\mathit{Prop}^{\\{P_{0},P_{i+1},\ldots,P_{m+1}\\},\\{P_{1},\ldots,P_{i}\\}}.$

Thus, by using T-And, we have:

$\mathcal{K}_{\mathcal{X}};\Delta\vdash_{M_{\mathcal{G}}}(P_{1}\lor\cdots\lor
P_{i})\land\mathbin{\bigcirc}\left<t_{L}\right>:\mathit{Prop}^{\\{P_{0},P_{i+1},\ldots,P_{m+1}\\},\emptyset}.$

Similarly, we have:

$\mathcal{K}_{\mathcal{X}};\Delta\vdash_{M_{\mathcal{G}}}(P_{i+1}\lor\cdots\lor
P_{m+1})\land\mathbin{\bigcirc}\left<t_{R}\right>:\mathit{Prop}^{\\{P_{0},P_{1},\ldots,P_{i}\\},\emptyset}.$

Thus, by using T-Or and T-Avg, we obtain

$\mathcal{K}_{\mathcal{X}};\Delta\vdash_{M_{\mathcal{G}}}\mathbin{\bigcirc}(((P_{1}\lor\cdots\lor
P_{i})\land\mathbin{\bigcirc}\left<t_{L}\right>)\lor((P_{i+1}\lor\cdots\lor
P_{m+1})\land\mathbin{\bigcirc}\left<t_{R}\right>)):\mathit{Prop}^{\emptyset,\emptyset}$

as required.

##  6\. Related Work

As mentioned in Section 1, PHFL can be regarded as a probabilistic extension
of the higher-order fixpoint logic, and as a higher-order extension of the
$\mu^{p}$-calculus. We thus compare our work with previous studies on (non-
probabilistic) higher-order fixpoint logic and those on (non-higher-order)
probabilistic logics. As already mentioned, for (non-probabilistic) HFL, model
checking of finite-state systems is known to be decidable [VV04], and
$k$-EXPTIME complete [ALS07]. This is in a sharp contrast with our result that
PHFL model checking is highly undecidable (both $\Pi^{1}_{1}$-hard and
$\Sigma^{1}_{1}$-hard) even at order 1.

As for studies on probabilistic logics, besides the $\mu^{p}$-calculus, there
are other probabilistic extensions of the modal $\mu$-calculus [MM97, HK97,
MS13]. Łukasiewicz $\mu$-calculus introduced by Mio and Simpson [MS13] is
among the most expressive ones, which has, in addition to $\land$ and $\lor$,
another kind of conjunction ($\odot$) and disjunction ($\oplus$), called
Łukasiewicz operations. To our knowledge, ours is the first _higher-order_ and
probabilistic extension of the modal $\mu$-calculus. The decidable fragment of
PHFL studied in Section 5 is strictly more expressive than the
$\mu^{p}$-calculus. We conjecture that the expressive power of PHFL is
incomparable to that of Łukasiewicz $\mu$-calculus. On the one hand, the
property defined by the PHFL formula in the proof of Theorem 1 cannot be
expressed in Łukasiewicz $\mu$-calculus, hence PHFL is not subsumed by
Łukasiewicz $\mu$-calculus. On the other hand, Łukasiewicz operations do not
seem expressible in PHFL. It would be interesting to study a higher-order
extension of Łukasiewicz $\mu$-calculus (in other words, an extension of PHFL
with Łukasiewicz operations).

Recently, Kobayashi et al. [KLG19] introduced PHORS, a probabilistic extension
of higher-order recursion schemes (HORS), which can also be viewed as a
higher-order extension of recursive Markov chains (or probabilistic pushdown
systems), and proved that the almost sure termination problem is undecidable.
Although the problem setting is quite different (in our work, the _logic_ is
higher-order whereas the _system_ to be verified is higher-order in their
work), our encoding of the $\mu$-arithmetic in Section 4 has been partially
inspired by their undecidability proof; they also represented a natural number
$n$ as the probability $\frac{1}{2^{n}}$.

In Section 3, we have used the undecidability of the value-1 problem for
probabilistic automata to prove the undecidability of PHFL model checking.
Fijalkow et al. [FGKO15] studied a decidable subclass of probabilistic
automata called leaktight automata. The idea of their restriction appears to
be quite different from our type-based restriction of the PHFL model checking
problem.

##  7\. Conclusion

We have introduced PHFL, a probabilistic logic which can be regarded as both a
probabilistic extension of HFL and a higher-order extension of the
probabilistic logic $\mu^{p}$-calculus. We have shown that the model-checking
problem for PHFL for a finite Markov chain is undecidable for the $\mu$-only
and order-$1$ fragment. We have also shown that the model-checking problem for
the full order-$1$ fragment of PHFL is $\Pi^{1}_{1}$-hard and
$\Sigma^{1}_{1}$-hard. As positive results, we have introduced a decidable
subclass of the PHFL model-checking problem, and showed that the termination
problem of Recursive Markov Chains can be encoded in the subclass.

Finding an upper bound of the hardness of the PHFL model-checking problem is
left for future work. It is also left for future work to find a larger
decidable class of PHFL model-checking problems.

### Acknowledgements

We would like to thank anonymous referees for useful comments. This work was
supported by JSPS KAKENHI Grant Number JP15H05706 and JP20H00577, and
JP20H05703.

## References

  * [ALS07] Roland Axelsson, Martin Lange, and Rafal Somla.  The complexity of model checking higher-order fixpoint logic.  Logical Methods in Computer Science, 3(2), 2007.
  * [BEKK13] Tomás Brázdil, Javier Esparza, Stefan Kiefer, and Antonín Kucera.  Analyzing probabilistic pushdown automata.  Formal Methods in System Design, 43(2):124–163, 2013.
  * [Can88] John F. Canny.  Some algebraic and geometric computations in PSPACE.  In Janos Simon, editor, Proceedings of the 20th Annual ACM Symposium on Theory of Computing, May 2-4, 1988, Chicago, Illinois, USA, pages 460–467. ACM, 1988.
  * [CKP15] Pablo F. Castro, Cecilia Kilmurray, and Nir Piterman.  Tractable probabilistic mu-calculus that expresses probabilistic temporal logics.  In Ernst W. Mayr and Nicolas Ollinger, editors, 32nd International Symposium on Theoretical Aspects of Computer Science, STACS 2015, March 4-7, 2015, Garching, Germany, volume 30 of LIPIcs, pages 211–223. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2015.
  * [DH88] James H. Davenport and Joos Heintz.  Real quantifier elimination is doubly exponential.  J. Symb. Comput., 5(1/2):29–35, 1988.
  * [EY09] Kousha Etessami and Mihalis Yannakakis.  Recursive markov chains, stochastic grammars, and monotone systems of nonlinear equations.  J. ACM, 56(1):1:1–1:66, 2009.