11institutetext: Univ Paris Est Creteil, LACL, F-94010 Creteil, France
11email: <given<EMAIL_ADDRESS>
# Fairness and promptness in Muller formulas

Léo Tible  Youssouf Oualhadj  Daniele Varacca

###### Abstract

In this paper we consider two different views of the model checking problem
for the Linear Temporal Logic (LTL). On the one hand, we consider the
_universal_ model checking problem for LTL, where one asks that for a given
system and a given formula all the runs of the system satisfy the formula. On
the other hand, the _fair_ model checking problem for LTL asks that for a
given system and a given formula almost all the runs of the system satisfy the
formula.

It was shown that these two problems have the same theoretical complexity i.e.
PSPACE-complete. The question arises whether one can find a fragment of LTL
for which the complexity of these two problems differs. One such fragment was
identified in a previous work, namely the _Muller fragment_.

We address a similar comparison for the _prompt_ fragment of LTL (pLTL). pLTL
extends LTL with an additional operator, i.e. the _prompt-eventually_. This
operator ensures the existence of a bound such that liveness properties are
satisfied within this bound.

We show that the corresponding Muller fragment for pLTL does not enjoy the
same algorithmic properties with respect to the comparison considered. We also
identify a new expressive fragment for which the fair model checking is faster
than the universal one.

###### Keywords:

Model Checking Temporal logics Fairness.

##  1 Introduction

Linear Temporal Logic (LTL) allows system designers to easily describe
behavioral properties of a system [17]. Its expressive power and convenience
of use proved useful in many areas such as system design and verification [7,
20], agent planning [4, 11], knowledge representation [10], and control and
synthesis [18, 19]. At the heart of these applications a fundamental formal
approach is always to be found, namely, the _model-checking problem_ [22].

Universal and fair model-checking When trying to verify a system against a
specification, one usually models the system through a formalism called
_Labeled Transition System_ (LTS), which can be seen as a form of graph. A run
of the system is an infinite path in the LTS. The original approach to model-
checking consists in verifying that all possible runs of the LTS comply with
the specification. Some systems may not satisfy the specification only because
of few _unlikely_ runs. To avoid discarding these systems, the _fair_ model
checking approach gives a formal definition of _small set_ of executions, and
then satisfies that the set of executions that do not satisfy the
specification is indeed small. Two main notions of smallness appear in the
literature. If the system is endowed with a probability distribution, then a
set is small if it has probability 0. One can also define a topology on the
set of executions, and then a set is small if it is of the first Baire
category, or _comeager_ [16]. It turns out that, for LTL specifications over
_finite_ LTS, these two definitions of smallness actually coincide [23]. The
following example presents an intuitive difference between the _universal_ and
the fair _setting_.

$a$Idle$b$Query$c$Grant Figure 1: A simple system.

###### Example 1

Consider the example of Fig. 1, this figure models a “toy protocol” that could
either be in an idle state, a querying state or granting state. Assume now
that the modeler wants to check that _the protocol is not always idle_.
Without any fairness assumption, this system will be rejected since it could
always repeat the selfloop of state $a$. However, as we will see later, the
formalisation of the fairness assumption is able to express that the set of
runs consisting of this selfloop itself is _small_. Therefore, it can be
ignored and we can say that the system fairly satisfies the specification.

LTL model-checking The complexity of verifying that all the runs of a system
satisfy an LTL formula is known to be a PSPACE-complete problem [22]. The
complexity is measured with respect to the size of the specification, an LTL
formula in our case. This high complexity is due to the fact that one has to
transform the specification, into one described by a _non-deterministic Büchi
automaton_. Such an automaton is usually exponential in the size of the
specification, hence the complexity blowup [1].

In order to circumvent this blow-up, a natural idea is to identify fragments
of LTL with easier model checking problem. In the seminal work of Sistla and
Clark [22], they identified fragments whose model checking is
$\mathsf{coNP}$-complete. In particular they showed this complexity for the
class of formulas that only uses the temporal operator $\mathsf{F}$. We also
cite the fragment identified by Muscholl et al. [15]. This fragment is
obtained by prohibiting the use of until operator and requiring to use only
next operators indexed by a letter. They showed that the model checking
problem is $\mathsf{NP}$-complete. Finally we highlight the work of Emerson et
al. [9] where they studied the fragment of _Muller formulas_ , i.e., the
fragment built upon $\mathsf{F}^{\infty}$, and showed that it is also
$\mathsf{coNP}$-complete. We will see later that this fragment enjoys a nice
property.

The same complexity bound holds for the _fair_ model checking problem as well
[8]. Indeed, verifying that the set of executions that do not satisfy a
formula is small is also a PSPACE-complete task. Again, this follows from the
translation into the automata-theoretic world. However, for at least one
expressive fragment of LTL, these complexities differ. Indeed for the fragment
of Muller Formulas, while the universal model checking problem is
$\mathsf{coNP}$-complete, the fair model checking problem can be solved by a
linear time algorithm presented in [21]. This follows from the fact that
Muller formulas can be checked without prior processing thus avoiding the
exponential blowup.

$a$A$b$B Figure 2: LTL vs. pLTL.

###### Example 2

Consider again the example of Fig. 1. A Muller formula that one could check is
of the form _infinitely often a query is made and infinitely often a grant is
granted._ The intuition is that such a specification can be checked by only
studying the strongly connected components (SCCs) of the system. Here, we see
that neither the SCC $\\{a\\}$, nor $\\{b,c\\}$ satisfy the specification. It
is also worth mentioning that, as we will see later, in the presence of
_fairness assumption_ , one only has to check the so-called bottom SCCs
(BSCCs), in our case $\\{b,c\\}$.

Refining LTL Consider the standard specification: All along the execution, if
a message is sent, an acknowledgment will be received, that can be expressed
in LTL. A system may satisfy this specification universally or fairly, even
when the waiting time for the acknowledgment grows indefinitely during the
execution. _Prompt LTL_ (pLTL), introduced by Kupferman et al. [14], can
express the above specification in the following and more precise form: There
exists a time bound $t$ such that, along any execution, if a message is sent,
an acknowledgment will be received within $t$ seconds. Of course a natural
question is whether pLTL and LTL are equivalent. In Example 3, we show a
simple model that separates LTL from pLTL.

###### Example 3

Consider the LTS of Fig. 2, and consider the specification that asks that
either A or B is seen infinitely often. Clearly enough, any infinite path in
the system of Fig. 2 satisfies this LTL specification. The corresponding pLTL
specification asks for the existence of a bound $k$ such that either A or B is
seen infinitely often within a window of $k$ steps. Now, for any bound $k\geq
0$, the run $a^{k+1}b^{k+1}a^{k+1}b^{k+1}\cdots$ does not satisfy this
specification.

Despite the fact that it can express more precise properties, the model
checking problem for pLTL is still known to be PSPACE-complete [14]. This is
achieved through an _efficient translation_ into LTL. The fair model checking
problem has the same complexity also: although an explicit proof is not
published, a careful inspection of the proof of [14] shows that the
translation into LTL formulas holds for the fair setting, and thus it is
sufficient to invoke the algorithm from [8] without further blowup. Prompt
Muller Formulas In this paper we consider the model checking problem in both
the fair and universal framework in the context of pLTL, in particular of the
_Muller fragment_ of pLTL. As we mentioned, Muller formulas were introduced as
a fragment of LTL. In this context, this fragment has a
$\mathsf{coNP}$-complete universal model checking problem [21]. This is
already a nice property since being in this complexity class allows one to
scale better in real life application by applying symbolic approaches using
SAT-solvers. We also mentioned that, for this fragment, the fair model
checking problem is linear in the size of the formula.

From a practical point of view, this fragment is very handy when one wants to
express _asymptotic behaviors_. For instance, a classical specification to
seek in a reactive system is _responsiveness_. This specification requires
from the system that queries are eventually granted, moreover, it requires
that the most urgent ones are considered first. But how can one measure the
urgency of a query? In LTL, one can think of two ways. The first is to
consider that a query is urgent if it occurs _infinitely often_. The drawback
with this modelization is that it is not precise enough. Indeed, a query could
be asked infinitely often but with a vanishing frequency. A system could very
well satisfy such property but in practice this would yield no guarantees. On
the other hand, one could model the urgence as _from some point on, the query
is always raised until it is granted_ , but this is too strong now. Thanks to
our fragment _prompt Muller formula_ , one can model queries with positive
frequencies. Indeed, the existence of a bound, implies that the query appears
within a bounded frame of time ensuring a more robust behavior.

Prefix independent prompt Muller Formulas Finally we introduce a more
_permissive_ fragment. Along its execution, a system may violate a property
during an _initial_ phase, but once it enters a _steady regime_ it satisfy
this very property. We therefore introduce the _initialized Muller_ fragment
for pLTL. This fragment expresses the fact that a system should satisfy a
specification in the long run, i.e., we ignore the finite initialization
phase. This vision is inspired from _prefix independent_ specifications. Such
specifications are only interested in the asymptotic behavior of a system. For
instance, _parity, Rabin, Street, Büchi_ are all $\omega$-regular
specifications whose satisfaction is independent of any finite prefix [1]. Not
only do these specifications seem to be more suited to real life applications,
they also in general enjoy nice properties, especially in the probabilistic
setting, c.f. [5, 12, 13]. We also mention results [3, 6] where prefix
independence has been considered in a setting rather close to ours, and there
again they exhibited well behaved properties [2] especially when compared to
the _prefix dependent_ framework. Our fragment generalizes the concept of
prefix independence for prompt Muller formulas.

Contributions and organisation Our original contributions are as follows.

We first show that universal model checking for the Muller fragment of pLTL is
$\mathsf{coNP}$-complete. In order to show the membership, we had to depart
from the already existing reduction in the classical LTL and develop new
technical tools. Our approach is based on the concept of _avoiding sequences_.
Intuitively, these are sequences of simple cycles, each of which _avoids_ a
state formula, c.f. Definition 6. We show that for any disjunctive prompt
Muller formula, the existence of a counter example in a system is equivalent
to the existence of specific avoiding sequence. We also show that these
sequences are small and canonical representations for counter examples. This
is established in Lemma 2 and Lemma 3.

Our second contribution is to show that the complexities for universal and
fair model checking for this fragment are the same. In order to obtain this,
we show that universal and fair model checking for this fragment cannot be
separated, c.f. Theorem 4.1. This latter observation can be intuitively
explained by the fact that if a system is a fair model for some pLTL Muller
formula, then any run, including those with measure 0, have to satisfy the
formula, c.f. Lemma 6.

Our third contribution is to show that the complexity of universal and fair
model checking for the prefix independent Muller Formula fragment differ. The
universal model checking is again $\mathsf{coNP}$-complete, but we give a
_quadratic_ time algorithm solving the fair model checking problem for this
fragment.

##  2 Preliminaries

Throughout the document we will use the following notations and conventions:
$\mathsf{AP}$ is a set of atomic propositions. For an arbitrary set $E$,
$E^{*}$ is the set of all the finite sequences over $E$, $E^{+}$ is the set of
all the non empty finite sequences over $E$, $E^{\omega}$ is the set of all
the infinite sequences of over $E$. When $E$ is a finite set, $|E|$ will
denote the number of its elements.

Labelled Transition System _LTS_ for short is a tuple
$\mathcal{L}=\langle\mathsf{S},s_{\mathsf{init}},\mathsf{T},\mathsf{lbl}\colon\mathsf{S}\to
2^{\mathsf{AP}}\rangle$ such that $\mathsf{S}$ is a set of states,
$s_{\mathsf{init}}\in\mathsf{S}$ is an initial state,
$\mathsf{T}\subseteq\mathsf{S}\times\mathsf{S}$ is a set of transitions, and
$\mathsf{lbl}\ :\mathsf{S}\to 2^{\mathsf{AP}}$ is a labeling function. For a
state $s\in\mathsf{S}$, the set of successors of $s$ is
$\mathsf{Succ}(s)=\\{t\in\mathsf{S}|(s,t)\in\mathsf{T}\\}$. A _path_ in
$\mathcal{L}$ is a finite sequence of states $\pi=s_{0}s_{1}\cdots s_{k}$ of
length $k+1$ such that $\forall 0\leq i\leq
k-1,s_{i+1}\in\mathsf{Succ}(s_{i})$. We denote by $|\pi|$ the length of $\pi$,
i.e. $|\pi|=k+1$. A _run_ in $\mathcal{L}$ is an infinite sequence of states
$\rho=s_{0}s_{1}\cdots$ such that $\forall i\geq 0$,
$s_{i+1}\in\mathsf{Succ}(s_{i})$. Let $\rho$ be a run and let $i\geq 0$, then
$\rho[i]=s_{i}$, $\rho[i..]=s_{i}s_{i+1}\cdots$, that is the infinite suffix
starting in the $(i+1)$th letter, and $\rho[..i]$ is the prefix up to
$(i+1)$th position, that is $\rho[..i]=s_{0}\cdots s_{i}$. For $i<j$,
$\rho[i..j]$ is the path $s_{i}\cdots s_{j}$. We use the same notation for a
path $\pi$, in this case $\pi[i..]$ will be a finite suffix.

We will also use the following notations: The set of states visited infinitely
often by $\rho$ is $\mathsf{Inf}(\rho)=\\{s\in\mathsf{S}\mid\forall i\geq
0,\exists j>i,\rho[j]=s\\}$. The set of all the paths (resp. runs) over
$\mathcal{L}$ is $\mathsf{Paths}(\mathcal{L})$ (resp.
$\mathsf{Runs}(\mathcal{L})$). The set of all initialized runs over
$\mathcal{L}$ is $\mathsf{Runs_{init}}(\mathcal{L})$, that is
$\\{\rho\in\mathsf{Runs}(\mathcal{L})\mid\rho[0]=s_{\mathsf{init}}\\}$.

Linear Temporal Logic _LTL_ for short is the set of formulas $\phi$ defined
using the following grammar:

$\displaystyle\phi::=\alpha\mid\lnot\phi\mid\phi\lor\phi\mid\mathsf{X}\leavevmode\nobreak\
\phi\mid\phi\leavevmode\nobreak\ \mathsf{U}\leavevmode\nobreak\ \phi\ .$

where $\alpha$ is in $\mathsf{AP}$.

We also recall that LTL formulas are evaluated over runs of $\mathcal{L}$ as
follows:

$\displaystyle\rho$ $\displaystyle\models\alpha\text{ iff
}\alpha\in\mathsf{lbl}(\rho[0])\ ,\ \rho\models\lnot\phi\text{ iff
}\rho\not\models\phi\ ,\ \rho\models\mathsf{X}\leavevmode\nobreak\ \phi\text{
iff }\rho[1..]\models\phi\ ,$ $\displaystyle\rho$
$\displaystyle\models\phi\lor\psi\text{ iff }\rho\models\phi\text{ or
}\rho\models\psi\ ,\ \rho\models\phi\leavevmode\nobreak\
\mathsf{U}\leavevmode\nobreak\ \psi\text{ iff }\exists i\geq
0,\leavevmode\nobreak\ \rho[i..]\models\psi\text{ and }\forall
j<i,\leavevmode\nobreak\ \rho[j..]\models\phi\ ,$

where
$\rho\in\mathsf{Runs}(\mathcal{L}),\alpha\in\mathsf{AP},\phi\in\text{LTL}\text{,
and }\psi\in\text{LTL}$.

Given a formula $\phi\in\mathsf{LTL}$, the size $|\phi|$ is the number of
operators that appear in $\phi$. In the sequel, we will use the following
macros:

$\displaystyle\mathsf{F}\phi=\mathsf{true}\leavevmode\nobreak\
\mathsf{U}\leavevmode\nobreak\ \phi\ ,\leavevmode\nobreak\
\mathsf{G}\phi=\lnot\mathsf{F}\lnot\phi\ ,\leavevmode\nobreak\
\mathsf{F}^{\infty}\phi=\mathsf{G}\mathsf{F}\phi\enspace.$

The first formula is true for any run where $\phi$ is true in the _future_ ,
the second formula is true for any run where $\phi$ always holds, and the
third formula is true for any run where there exists infinitely many positions
where $\phi$ holds.

######  Problem 1 (Model checking)

Given an LTS $\mathcal{L}$ and an LTL formula $\phi$, the _model checking
problem_ consists in checking whether
$\forall\rho\in\mathsf{Runs_{init}}(\mathcal{L}),\leavevmode\nobreak\
\rho\models\phi$. In this case, we will write $\mathcal{L}\models\phi$.

######  Theorem 2.1 ([22])

The model checking problem is $\mathsf{PSPACE}$-complete.

Fairness in model checking As seen in the example of Fig. 1, the LTS is not
considered a model for the formula $\mathsf{F}\mathsf{G}\lnot(\sf{Idle})$ due
to a single run. In fact, one can say that such run is likely to occur only if
the system is controlled by a demonic entity. In a less pessimistic scenario,
one can imagine that the transition $(a,b)$ in Fig. 1 should at least happen
once. Under this assumption, one clearly sees that as soon as it happens, the
formula $\mathsf{F}\mathsf{G}(\lnot\sf{Idle})$ is satisfied. This alternative
vision on the behavior of the system was introduced in [21] and is called
model checking under fairness assumption.

In order to impose fairness, one can use different formalisms [23]. In our
case we use a _fair coin_. At each state, a fair coin is flipped and the
succesor state is chosen accordingly. This coin flipping induces a natural
probability measure over $\mathsf{Runs_{init}}(\mathcal{L})$. In the fair
model checking problem, one asks whether _almost all_ the runs of an LTS
satisfy a given formula $\phi$. In order to build the probability measure over
$\mathsf{Runs_{init}}(\mathcal{L})$, we use the notion of _cylinders_. Let
$\pi\in\mathsf{Paths}(\mathcal{L})$, the cylinder induced by $\pi$, denoted
$\mathsf{Cyl}(\pi)$, is the set
$\\{\rho\in\mathsf{Runs}(\mathcal{L})\mid\pi\text{ is a prefix of }\rho\\}$.
$\mathbb{P}_{\mathcal{L}}(\mathsf{Cyl}(\pi))$ is defined by induction over the
set of all the cylinders as follows:

$\displaystyle\forall s\in\mathsf{S},\leavevmode\nobreak\
\mathbb{P}_{\mathcal{L}}(\mathsf{Cyl}(s))=\begin{cases}1\text{ if
}s=s_{\mathsf{init}}\\\ 0\text{ otherwise}\end{cases}$

Let $\pi\in\mathsf{Paths}(\mathcal{L})$ such that $|\pi|=n$ and
$s\in\mathsf{S}$, then

$\displaystyle\mathbb{P}_{\mathcal{L}}(\mathsf{Cyl}(\pi
s))=\begin{cases}\frac{\mathbb{P}_{\mathcal{L}}(\mathsf{Cyl}(\pi))}{|\mathsf{Succ}(\pi[n])|}\text{
if }s\in\mathsf{Succ}(\pi[n])\\\ 0\text{ otherwise}\end{cases}$

This measure is uniquely extended over the set $\mathsf{Runs_{init}}$ thanks
to Caratheodory’s theorem.

######  Problem 2 (Fair model checking)

Given an LTS $\mathcal{L}$ and an LTL formula $\phi$, the fair model checking
problem consists in checking whether
$\mathbb{P}_{\mathcal{L}}(\\{\rho\in\mathsf{Runs_{init}}(\mathcal{L})\mid\rho\models\phi\\})=1$.
In this case, we will write $\mathcal{L}\models_{\text{\tiny{\sf AS}}}\phi$.

An appealing question is then whether the latter version is any easier than
the former version of the problem. It turns out that both versions are equally
difficult.

######  Theorem 2.2 ([8])

The fair model checking problem is $\mathsf{PSPACE}$-complete.

The _Muller_ fragment of LTL In order to reduce the complexity of the model
checking problem, one can consider subclasses of LTL formula. In order to
define subclasses we use the notion of _fragment_. A fragment is the set of
all the formulas obtained by restricting to particular temporal operators. For
example, if $op_{1},\ldots,op_{k}$ are $k$ temporal operators, we will denote
by $\mathsf{L}(op_{1}\ldots,op_{k})$ the set of all the formulas where the
only temporal operators allowed are $op_{1},\ldots,op_{k}$. For instance,
$\mathsf{L}(\mathsf{X}\leavevmode\nobreak\ ,\leavevmode\nobreak\
\mathsf{U}\leavevmode\nobreak\ )$ coincides with LTL. Another example is
$\mathsf{L}(\mathsf{F})$ which is the fragment where only $\mathsf{F}$ is
allowed. This fragment is known as RLTL and it is interesting since its model
checking problem is $\mathsf{coNP}$ complete [22]. In this paper our starting
point will be $\mathsf{L}(\mathsf{F}^{\infty})$ whose universal model checking
is $\mathsf{coNP}$-complete [9], but fair model checking is linear [21].

A _state formula_ is an LTL formula where no temporal operator appears. We
also introduce the notion of _positive fragment_ denoted
$\mathsf{L}^{+}(op_{1},\ldots,op_{k})$, i.e., the set of all the formulas in
$\mathsf{L}(op_{1},\ldots,op_{k})$ such that each atomic proposition is in the
scope of some temporal operator $op_{1},\ldots,op_{k}$. The positive fragment
$\mathsf{L^{+}(\mathsf{F}^{\infty})}$ is called the _Muller_ fragment, and is
formally defined as the smallest non empty set such that :

  * •

If $\phi\in\mathsf{L(\mathsf{F}^{\infty})}$, then
$\mathsf{F}^{\infty}\phi\in\mathsf{L^{+}(\mathsf{F}^{\infty})}$.

  * •

If $\phi_{1},\phi_{2}\in\mathsf{L^{+}(\mathsf{F}^{\infty})}$, then
$\phi_{1}\lor\phi_{2}$,
$\phi_{1}\land\phi_{2}\in\mathsf{L^{+}(\mathsf{F}^{\infty})}$.

As explained earlier, the Muller fragment enjoys nice algorithmic properties.

######  Theorem 2.3 ([21])

The universal model checking problem for Muller formulas is
$\mathsf{coNP}$-complete, and the fair model checking problem can be solved in
linear time.

Promptness in LTL A prompt LTL formula $\phi$ is defined according to the
following grammar:

$\displaystyle\phi::=\alpha\mid\lnot\alpha\mid\phi\lor\phi\mid\phi\land\phi\mid\mathsf{X}\leavevmode\nobreak\
\phi\mid\phi\leavevmode\nobreak\ \mathsf{U}\leavevmode\nobreak\
\phi\mid\phi\leavevmode\nobreak\ \mathsf{R}\leavevmode\nobreak\
\phi\mid\mathsf{F}_{\mathsf{P}}\phi$

The main difference lies in the addition of $\mathsf{F}_{\mathsf{P}}$. This
operator states that $\phi$ has to be satisfied in a “prompt” fashion. The
semantics of this operator is defined with respect to a bound $k\geq 0$. For a
given $k$, we will write $(\rho,k)\models\mathsf{F}_{\mathsf{P}}\phi$ if and
only if $\exists i\leq k,\leavevmode\nobreak\ (\rho[i..],k)\models\phi$. For
the other operators, the bound $k$ is irrelevant, thus they are evaluated
using the semantics of LTL. In this case we will not specify $k$. Another
difference is that we do not allow the negation of $\mathsf{F}_{\mathsf{P}}$.
This was already the case in [14]. Indeed, this makes more sense since the
negation of the newly added operator $\mathsf{F}_{\mathsf{P}}$ seems
unnatural, as the quantification over the bound is outside the formula.
Therefore, we must explicitly add the conjunction $\land$, as well as the
_release_ operator $\leavevmode\nobreak\ \mathsf{R}\leavevmode\nobreak\ $ the
dual of the _until_ operator $\leavevmode\nobreak\
\mathsf{U}\leavevmode\nobreak\ $. Given an LTS $\mathcal{L}$, and a pLTL
formula $\phi$, we say that $\mathcal{L}$ is a model for $\phi$, and write
$\mathcal{L}\models\phi$ if and only if there exists a bound $k$ such that for
all $\rho\in\mathsf{Runs_{init}}(\mathcal{L})$ , $(\rho,k)\models\phi$. We
write $\mathcal{L}\models_{\text{\tiny{\sf AS}}}\phi$ if and only if there
exists a bound $k$ such
$\mathbb{P}_{\mathcal{L}}(\\{\rho)\in\mathsf{Runs_{init}}(\mathcal{L})\mid(\rho,k)\models\phi\\})=1$.

######  Problem 3 (Universal prompt model checking)

Given an LTS $\mathcal{L}$ and a pLTL formula $\phi$, is it the case that
$\mathcal{L}\models\phi$ ?

######  Problem 4 (Fair prompt model checking)

Given an LTS $\mathcal{L}$ and a pLTL formula $\phi$, is it the case that
$\mathcal{L}\models_{\text{\tiny{\sf AS}}}\phi$ ?

From now on and when clear from the context we will refer to these two last
problems as _universal model checking_ and _fair model checking_.

The prompt Muller fragment The prompt Muller fragment denoted by
$\mathsf{L}(\mathsf{F}^{\infty}_{\mathsf{P}})$ in the context of pLTL is
obtained by the following abstract grammar:

$\phi::=\alpha\mid\lnot\alpha\mid\phi\lor\phi\mid\phi\land\phi\mid\mathsf{F}_{\mathsf{P}}^{\infty}\phi$

where, for a bound $k\geq 0$,
$(\rho,k)\models\mathsf{F}_{\mathsf{P}}^{\infty}\phi$ if and only if $\forall
i\exists j\leq k,(\rho[(i+j)..],k)\models\phi$.

Our hope as stated earlier is to show that fair model checking of this
fragment is easier that its universal counterpart complexity-wise. In the
sequel it will be useful to consider the so-called _positive fragment_
$\mathsf{L}^{+}(\mathsf{F}_{\mathsf{P}}^{\infty})$, i.e.:

  * •

If $\phi\in\mathsf{L(\mathsf{F}_{\mathsf{P}}^{\infty})}$, then
$\mathsf{F}^{\infty}\phi\in\mathsf{L}^{+}(\mathsf{F}_{\mathsf{P}}^{\infty})$.

  * •

If $\phi_{1},\phi_{2}\in\mathsf{L}^{+}(\mathsf{F}_{\mathsf{P}}^{\infty})$,
then $\phi_{1}\lor\phi_{2}$,
$\phi_{1}\land\phi_{2}\in\mathsf{L}^{+}(\mathsf{F}_{\mathsf{P}}^{\infty})$ and
$\mathsf{F}_{\mathsf{P}}^{\infty}\phi_{1}\in\mathsf{L}^{+}(\mathsf{F}_{\mathsf{P}}^{\infty})$.

##  3 Universal model checking for prompt Muller fragment

A remarkable property of the Muller fragment of LTL is that the satisfaction
of a formula only depends of the asymptotic behavior of the system. Therefore,
as it is shown in [21] (a corollary of a result from [9]), a system satisfies
a Muller formula if and only if every strongly connected set satisfies the
formula. These sets are not maximal as opposed to strongly connected
components. Thus, there could exist exponentially many such sets. Roughly
speaking, the algorithm guesses a strongly connected set where the formula is
not satisfied in order to show that a system is not a model. The main result
of this section is that the $\mathsf{coNP}$ complexity carries over to our
setting.

###### Theorem 3.1

The universal model checking problem for
$\mathsf{L}(\mathsf{F}_{\mathsf{P}}^{\infty})$ is $\mathsf{coNP}$-complete.

The proof of this theorem turns out to be more technical than what was
presented in the setting of [21]. There are two main reasons why the proofs
for pLTL must be different.

First, using the translation presented in [14] from pLTL to LTL builds
formulas in a fragment whose model checking is already
$\mathsf{PSPACE}$-complete. Second, checking only the strongly connected set
is not enough in this case. In fact, it is possible for a system to satisfy a
formula in all its strongly connected sets yet not be a valid model.

The rest of this section is dedicated to the proof of Theorem 3.1. We first
present the technical tools that we will need in our algorithm. Second we
establish a crucial property for the $\mathsf{coNP}$ membership, namely the
existence of a small witness. Finally we establish the $\mathsf{coNP}$
membership.

###  3.1 Technical definitions

The goal of this section is to introduce the tools needed to prove that one
can polynomially define a faulty run, and then polynomially prove that it is
faulty. The first step is to limit our attention to formulas without
conjunctions.

Throughout this section, we will fix a LTS
$\mathcal{L}=\langle\mathsf{S},s_{\mathsf{init}},\mathsf{T},\mathsf{lbl}\colon\mathsf{S}\to
2^{\mathsf{AP}}\rangle$.

######  Definition 1 (Filtering)

Let $\phi$ be a prompt Muller formula, $k\geq 0$, and $\rho$ be some run in
$\mathcal{L}$, assume that $(\rho,k)\not\models\phi$, then we define the
filtering of $\phi$ denoted $\mathsf{flt}_{\rho,k}(\phi)$ as the formula
obtained from $\phi$ as follows:

$\displaystyle\mathsf{flt}_{\rho,k}(\alpha)=\alpha\ ,\
\mathsf{flt}_{\rho,k}(\phi_{1}\lor\phi_{2})=\mathsf{flt}_{\rho,k}(\phi_{1})\lor\mathsf{flt}_{\rho,k}(\phi_{2})\
,\
\mathsf{flt}_{\rho,k}(\mathsf{F}_{\mathsf{P}}^{\infty}\phi)=\mathsf{F}_{\mathsf{P}}^{\infty}\mathsf{flt}_{\rho,k}(\phi)$
$\displaystyle\mathsf{flt}_{\rho,k}(\phi_{1}\land\phi_{2})=\begin{cases}\mathsf{flt}_{\rho,k}(\phi_{1})\text{
if }(\rho,k)\not\models\phi_{1}\\\ \mathsf{flt}_{\rho,k}(\phi_{2})\text{
otherwise }\end{cases}$

###### Lemma 1

Let $\phi$ be a prompt Muller formula, $k\geq 0$, and $\rho$ some run in
$\mathcal{L}$, then $(\rho,k)\not\models\phi$ if and only if
$(\rho,k)\not\models\mathsf{flt}_{\rho,k}(\phi)$.

The filtration of the formula is a choice over each conjunction. A formula is
filtered if it is a filtration w.r.t. some run $\rho$ and some bound $k$. For
the sake of readability, the explicit run and bound will be omitted.

######  Definition 2 (Canonical form for filtered formula)

Let $\psi$ be a filtered formula. We say that $\psi$ is in _canonical form_
when it is written in the following form:

$\bigvee_{i=0}^{l}a_{i}\lor\bigvee_{i=0}^{k}\mathsf{F}_{\mathsf{P}}^{\infty}\psi_{i}$

where $a_{i}$ are atomic formulas and the $\psi_{i}$ are filtered formulas in
canonical form.

###### Remark 1

Notice that if a filtered formula $\psi$ does not start with a state formula
it is always possible to write it in canonical form by adding
$\mathsf{false}$, i.e.
$\psi\equiv\mathsf{false}\lor\bigvee_{i=0}^{k}\mathsf{F}_{\mathsf{P}}^{\infty}\psi_{i}$.

###### Example 4

As an ongoing example, consider the set $\\{a,b,c,d\\}$ of atomic variables,
and let

$\phi=\mathsf{F}_{\mathsf{P}}^{\infty}\left(a\lor\mathsf{F}_{\mathsf{P}}^{\infty}\left(\left(b\land
c\right)\lor\mathsf{F}_{\mathsf{P}}^{\infty}d\right)\lor\left(\mathsf{F}_{\mathsf{P}}^{\infty}c\land\mathsf{F}_{\mathsf{P}}^{\infty}d\right)\right)$

Then, consider

$\displaystyle\psi\equiv\mathsf{F}_{\mathsf{P}}^{\infty}\left(a\lor\mathsf{F}_{\mathsf{P}}^{\infty}\left(b\lor\mathsf{F}_{\mathsf{P}}^{\infty}d\right)\lor\mathsf{F}_{\mathsf{P}}^{\infty}c\right)\enspace,\enspace\psi^{*}\equiv\mathsf{false}\lor\underbrace{\mathsf{F}_{\mathsf{P}}^{\infty}\left(a\lor\underbrace{\mathsf{F}_{\mathsf{P}}^{\infty}\left(b\lor\mathsf{F}_{\mathsf{P}}^{\infty}d\right)}_{\psi_{1}}\lor\underbrace{\mathsf{F}_{\mathsf{P}}^{\infty}c}_{\psi_{2}}\right)}_{\psi}$

On the left hand side, we have a filtration of $\phi$ and on the right hand
side we have the same formula in canonical form. Note that $\psi$ is indeed a
filtration of $\phi$ for some LTS $\mathcal{L}$, some run $\rho$ of
$\mathcal{L}$, and some bound $k$.

In the rest of this section, we use the following notation. For any finite
sequence $u$ in $\mathsf{S}^{*}$ we denote by $\mathsf{occ}(u)$ the set of
states visited along $u$. A _loop_ is a path $\pi\in\mathsf{S}^{*}$ in
$\mathcal{L}$ such that the first and last states of $\pi$ are the same, that
is $\pi[0]=\pi[|\pi|-1]$. A _cycle_ is the set of states of some loop, that
is, it is a set of states $C\subseteq\mathsf{S}$ such that there is a loop
$\pi_{C}$ that satisfies $\mathsf{occ}(\pi_{C})=C$.

######  Definition 3 (Avoiding cycles)

Let $C$ be a cycle, and let $\theta$ be a state formula. We say that $C$ is
$\theta$-avoiding if no state in $C$ satisfies $\theta$.

We now define a representation of a filtered formula as a syntax tree. This
representation is useful to better visualize the formula, and the order in
which sub-formulas must be falsified.

###### Definition 4

Let
$\psi\equiv\bigvee_{i=0}^{l}a_{i}\lor\bigvee_{i=0}^{k}\mathsf{F}_{\mathsf{P}}^{\infty}\psi_{i}$
be a filtered formula in canonical form, we associate with $\psi$ a tree
$\mathsf{Tree}(\psi)$ as follows:

  * •

the root $t_{0}$ of $\mathsf{Tree}(\psi)$ is labeled by
$\bigvee_{i=0}^{l}a_{i}$,

  * •

the children $t_{1},\ldots,t_{k}$ of $t_{0}$ are respectively obtained by
$\mathsf{Tree}(\psi_{i})$.

###### Example 5

In the continuation of Example 4, consider the LTS $\mathcal{L}_{\psi}$
depicted in Fig. 3(a). We label the state with the propositions that are not
valid. For instance, in state $s_{1}$ propositions $b,c,d$ are true. The tree
associated with $\psi^{*}$ is depicted in Fig. 3(b).

$s_{1}$$\lnot a$$v_{1}$$\lnot c$$v_{2}$$\lnot b$$s_{2}$$\lnot c$$s_{3}$$\lnot
b$$s_{4}$$\lnot d$ (a) The LTS $\mathcal{L}_{\psi}$. For the sake of clarity,
we label the state with the atomic propositions that are falsified in each
state.

$\mathsf{false}$$a$$b$$c$$d$ (b) The tree associated with the formula
$\psi^{*}$. According to $\mathsf{Tree}(\psi^{*})$, a $b$-avoiding cycle
should be visited before a $d$-avoiding cycle, but $b$-avoiding and
$c$-avoiding cycles could be visited in any given order.

Figure 3: The LTS $\mathcal{L}_{\psi}$ and the tree associated with the
formula $\psi^{*}$.

For the following definition, we denote by $\prec_{\mathcal{T}}$ the natural
partial order over the nodes of a tree, i.e., for two nodes $n$ and $m$,
$n\prec_{\mathcal{T}}m$ if and only if $n$ is an ancestor of $m$. Given a node
$n\in\mathsf{Tree}(\psi)$, let $\theta_{n}$ be the state formula labelling
$n$. We say that a cycle is $n$-avoiding, if it is $\theta_{n}$-avoiding.

######  Definition 5 (Avoiding Sequence)

Let $\psi$ be a filtered formula in canonical form. A $\psi$-avoiding sequence
is given by:

  * •

a total ordering $n_{0},\ldots,n_{l}$ of the nodes of $\mathsf{Tree}(\psi)$,
such that if $n_{i}\prec_{\mathcal{T}}n_{j}$, then $i<j$.

  * •

a function $w$ that associates to each node $n_{i}$ a path
$w(n_{i})\in\mathsf{S}^{+}$ such that for each $0\leq i\leq l$,
$\mathsf{occ}(w(n_{i}))$ is a $n_{i}$-avoiding cycle.

###### Remark 2

If $i<j$, and therefore $w(n_{i})$ appears before $w(n_{j})$ in the sequence,
we will sometimes write $w(n_{i})\prec_{\psi}w(n_{j})$, even if $\prec_{\psi}$
is not technically an order over words. Indeed, some words can appear multiple
times, if for $i\neq j$, $w(n_{i})=w(n_{j})$. It is important to keep every
occurrence as they correspond to different $\mathsf{F}_{\mathsf{P}}^{\infty}$
that need to be falsified. In the following we will also say that a sequence
$u_{0},\ldots,u_{l}$ of words $\mathsf{S}^{+}$ is a $\psi$-avoiding sequence,
without explicit mention of the ordering on the nodes and the function $w$.

Not all avoiding sequences represent a run of the system. We say that an
avoiding sequence is realisable, if it is compliant with the ordering induced
by the avoiding sequence.

######  Definition 6 (Realisable avoiding sequence)

Let $U=u_{0},\ldots,u_{l}$ be an avoiding sequence. We say that $U$ is
realisable in $\mathcal{L}$, if there exists a finite sequence
$v_{0},v_{1},\ldots,v_{l+1}$ of elements in $\mathsf{Paths}(\mathcal{L})$,
such that all of the following hold:

  * •

$v_{0}[0]=s_{\mathsf{init}}$,

  * •

$\forall 1\leq i\leq l+1$, $v_{i}[0]\in\mathsf{occ}(u_{i-1})$,

  * •

$\forall 0\leq i\leq l$, $v_{i}[|v_{i}|-1]\in\mathsf{occ}(u_{i})$,

  * •

$v_{l+1}\in S^{\omega}$.

We call the sequence $v_{0},v_{1},\ldots,v_{l+1}$ a realisation witness for
the pair $(U,\mathcal{L})$.

We can now construct the run that will falsify the formula. Given any bound
$k$, we need to iterate each avoiding cycle such that the resulting path is of
length at least $k$. As each cycle has at least one element, it is enough to
iterate each loop $k$ times to guarantee this. The construction of the
resulting run is formalized in the following definition.

######  Definition 7 ($k$-pumping)

Let $U=u_{0},\ldots,u_{l}$ be an avoiding sequence, and $\mathcal{L}$ be an
LTS, and $v_{0},v_{1},\ldots,v_{l+1}$ be a realisation witness for
$(U,\mathcal{L})$. A $k$-pumping of $(U,v_{0},v_{1},\ldots,v_{l+1})$ is any
run of the form $v_{0}(u_{0})^{k}v_{1}(u_{1})^{k}\ldots
v_{l}(u_{l})^{k}v_{l+1}$ where $k\geq 1$.

######  Definition 8 (Realisation of an avoiding sequence)

Let $U=u_{0},\ldots,u_{l}$ be an avoiding sequence, and $\rho$ be a run of
some LTS $\mathcal{L}$. We say that $\rho$ realizes $U$ in $\mathcal{L}$ if
there exists a sequence of non negative integers $j_{0}\leq
j_{1}\leq\ldots\leq j_{l}$ such that for any $0\leq i\leq
l,\rho[j_{i}]\in\mathsf{occ}(u_{i})$.

###### Remark 3

One can easily prove that any avoiding sequence $U$ is realized in a LTS
$\mathcal{L}$ if and only if there exists a run $\rho$ in $\mathcal{L}$
realizing $U$.

###### Example 6

In the continuation of Example 5, we build a $\psi$-avoiding sequence. We
consider the following mapping,

$\displaystyle a\mapsto s_{1},\ $ $\displaystyle b\mapsto v_{2}s_{3},\ $
$\displaystyle c\mapsto v_{1}s_{2},\ $ $\displaystyle d\mapsto s_{4}.$

With the following ordering $s_{1}\prec\ v_{2}s_{3}\prec v_{1}s_{2}\prec
s_{4}$. One can easily check that this ordering agrees with
$\mathsf{Tree}(\psi)$. Moreover, notice that each element of this sequence is
an avoiding sequence for the node it is mapped to. Finally, notice that this
sequence is realizable in $\mathcal{L}_{\psi}$. For example any run in
$s_{1}^{+}(v_{2}s_{3})^{+}s_{2}(v_{1}s_{2})^{+}(s_{4})^{\omega}$ is a
realization in $\mathcal{L}_{\psi}$.

Now we argue that for any $k>0$ there exists a run in
$s_{1}^{+}(v_{2}s_{3})^{+}s_{2}(v_{1}s_{2})^{+}(s_{4})^{\omega}$ which is a
counter example for $\psi$. Indeed, choose some $k>0$ and consider the
infinite word
$\rho_{k}=s_{1}^{k}(v_{2}s_{3})^{k}s_{2}(v_{1}s_{2})^{k}s_{4}^{k}s_{4}^{\omega}$,
then repeating $s_{1}$ $k$ times falsifies $a$ for $k$ consecutive steps. Now
notice that each of the $k$ first steps also falsify the sub-formula
$\psi_{1}$. This is because from each of these positions, the cycles
$\\{v_{2},s_{3}\\}$, $\\{v_{1},s_{2}\\}$, and $\\{s_{4}\\}$ are reached and
repeated $k$ consecutive times which falsifies in order $b$, $c$, and $d$.
Thus the $k$ first steps of $\rho_{k}$ witness the fact that $\rho_{k}$
falsifies $\psi$.

###  3.2 Small witness properties

We are now ready to state our main ingredient towards the
$\mathsf{coNP}$-membership, that is, the _small witness property_. This
property states that for a given LTS $\mathcal{L}$, a filtered formula in
canonical form $\psi$ and some bound $k\geq|S|+1$, _there exists a run $\rho$
such that $(\rho,k)\not\models\mathsf{F}_{\mathsf{P}}^{\infty}\psi$ if and
only if there exists a realisable $\psi$-avoiding sequence._ The proof of this
property relies on two lemmas. Lemma 2 establishes the left to right direction
and Lemma 3 established the converse direction.

$\rho=$$\cdots$$\cdots$$i+k$$i$$u^{\theta}$$u^{\psi_{1}}_{1}$$u^{\psi_{2}}_{1}$$u^{\psi_{1}}_{2}$
Figure 4:  Building a realisation of an avoiding sequence from a counter
example.

######  Lemma 2 ()

Let $\mathcal{L}$ be an LTS, $\psi$ be a filtered formula in canonical form,
and assume that there exists $\rho$ and $k\geq|\mathsf{S}|+1$ such that
$(\rho,k)\not\models\mathsf{F}_{\mathsf{P}}^{\infty}\psi$, then there exists a
$\psi$-avoiding sequence $U$ which is realized by $\rho$.

In order to prove this lemma, we need to build an avoiding sequence from a
counter example. To do this, we rely on the intuition depicted in Fig. 4. In
this figure, a run $\rho$ is a counter example to a formula
$\psi\equiv\mathsf{F}_{\mathsf{P}}^{\infty}(\theta\lor\mathsf{F}_{\mathsf{P}}^{\infty}\psi_{1}\lor\mathsf{F}_{\mathsf{P}}^{\infty}\psi_{2})$.
Now because $\rho$ is a counter example for some fixed bound $k$, clearly
there exists a postion $i$ such that for the next $k$ consecutive positions,
$\theta$ does not hold. From these positions one can extract a
$\theta$-avoiding cycle ($u^{\theta}$ in the figure). We repeat this
inductively, while maintaining the order of appearance of each cycle. For
instance in the figure above, $\psi_{1}$ is falsified using two cycles
$u_{1}^{\psi_{1}}$ and $u_{2}^{\psi_{1}}$, but also see that $\psi_{2}$ is
falsified using a cycle overlapping $u_{1}^{\psi_{1}}$ and $u_{2}^{\psi_{1}}$
but since it starts after $u_{1}^{\psi_{1}}$ the order obtained is
$u^{\psi_{1}}_{1}\prec u^{\psi_{2}}_{1}\prec u^{\psi_{1}}_{2}$. The proof
formalizes this intuition by extracting cycles and the induced order
inductively. The full proof is in Appendix 0.A.1.

######  Lemma 3 ()

Let $\mathcal{L}$ be an LTS, $\psi$ be a filtered formula in canonical form,
and let $U$ be a realisable $\psi$-avoiding sequence in $\mathcal{L}$. For any
$k$-pumping $\rho_{k}$ of some realisation witness
$(U,v_{0},v_{1},\ldots,v_{l+1})$ for $(U,\mathcal{L})$, we have
$(\rho_{k},k)\not\models\mathsf{F}_{\mathsf{P}}^{\infty}\psi$.

The proof of this lemma is less technical, it is based on the intuition that
one can build counter examples by successively pumping the avoiding cycles
associated with $U$. The proof is available in Appendix 0.A.2.

###  3.3 Proof of Theorem 3.1

We are now ready to prove the main result of this section that is Theorem 3.1.
To establish the membership in $\mathsf{coNP}$ we present a non deterministic
procedure, c.f. Algorithm 1. The hardness follows easily from the results of
[9]. Indeed a close inspection of the proof establishing the $\mathsf{coNP}$
hardness of the plain Muller fragment of LTL shows that the same encoding of
_3-SAT_ applies in our case.

Data: An LTS
$\mathcal{L}=\langle\mathsf{S},s_{\mathsf{init}},\mathsf{T},\mathsf{lbl}\colon\mathsf{S}\to
2^{\mathsf{AP}}\rangle$ and a formula
$\phi\in\mathsf{L(\mathsf{F}_{\mathsf{P}}^{\infty})}$

Result: Whether $\mathcal{L}\not\models\phi$

Guess a filtered formula $\psi\equiv\theta\lor\psi^{\prime}$ of $\phi$, where
$\theta=\bigvee_{i=0}^{l}a_{i}$ and
$\psi^{\prime}=\bigvee_{i=0}^{m}\mathsf{F}_{\mathsf{P}}^{\infty}\psi_{i}$;

Guess a sequence $U=u_{0},\ldots,u_{m}$ of size $(|S|+1)|\psi^{\prime}|$;

Compute the tree $\mathsf{Tree}(\psi^{\prime})$;

Guess a mapping $w$ between the nodes of the tree and the sequence;

Check that the initial state does not satisfy $\theta$;

Check that $U$ is associated with $\mathsf{Tree}(\psi^{\prime})$;

Check that $U$ is $\psi^{\prime}$-avoiding;

Check that $U$ is realisable in $\mathcal{L}$;

Accepts the input if all checks succeeded;

Algorithm 1 Non deterministic algorithm for the universal model checking of
$\mathsf{L(\mathsf{F}_{\mathsf{P}}^{\infty})}$

Thanks to Lemma 2 and Lemma 3, we establish the correctness of Algorithm 1.

######  Lemma 4 ()

Given an LTS $\mathcal{L}$ and a formula
$\phi\in\mathsf{L(\mathsf{F}_{\mathsf{P}}^{\infty})}$, Algorithm 1 accepts if
and only if, for all $k$, there is a run $\rho_{k}$ in $\mathsf{Runs_{init}}$
such that $(\rho_{k},k)\not\models\phi$.

Finally Theorem 3.1 follows from the next lemma.

######  Lemma 5 ()

The universal model checking problem for
$\mathsf{L}(\mathsf{F}_{\mathsf{P}}^{\infty})$ is in $\mathsf{coNP}$.

##  4 Fair model checking for prompt Muller fragment

Now that we established that the universal model checking problem is
$\mathsf{coNP}$-complete for the prompt Muller fragment, we will address the
fair version of the problem. We will actually show that assuming fairness for
the behavior of the system does not simplify the problem. Formally we show
that:

###### Theorem 4.1

For all LTS $\mathcal{L}$ and formula
$\phi\in\mathsf{L}(\mathsf{F}^{\infty}_{\mathsf{P}})$,
$\mathcal{L}\models\phi$ if and only if $\mathcal{L}\models_{\text{\tiny{\sf
AS}}}\phi$.

Actually, by its own construction, any witness against the satisfaction of a
formula in $\mathsf{L}(\mathsf{F}^{\infty}_{\mathsf{P}})$ can be described by
a _finite path_. One can say that the set of the counter examples of a given
formula is open in the Cantor topology. Therefore, this witness has a positive
probability using our measure $\mathbb{P}_{\mathcal{L}}$. This yields the fact
that such a witness is also a witness for the fair model checking. We
formalize this intuition bellow using the following lemma.

$\rho=$$\cdots$$\cdots$$i$$i+k$$\not\models\phi$$\not\models\psi$$\not\models\psi$$\not\models\psi$$\not\models\psi$$\not\models\psi$$w_{i}$$w_{i+1}$$w_{i+2}$$w_{i+3}$$w_{i+k}$$w$$\rho^{\prime}$
Figure 5:  Visual representation of the proof for the case
$\phi=\mathsf{F}_{\mathsf{P}}^{\infty}\psi$

######  Lemma 6 ()

Let $\phi$ be a formula, $\mathcal{L}$ be an LTS and assume that there exists
a run $\rho$ such that for some $k>0$ we have $(\rho,k)\not\models\phi$, then
there exists a prefix $w$ of $\rho$ such that for any run
$\rho^{\prime}\in\mathsf{Cyl}(w)$ we have $(\rho^{\prime},k)\not\models\phi$.

The proof consists in extracting a prefix $w$ from a counter example $\rho$.
We will proceed by induction over the structure of the formula. Arguably, the
most technical case is the one where the formula
$\phi\equiv\mathsf{F}_{\mathsf{P}}^{\infty}\psi$. To catch this intuition,
consider Fig. 5 where we depict a run $\rho$ which is a counter example to
$\phi$ for some bound $k$. Using the shape of the formula, the main trick for
the proof is to locate $k$ consecutive positions where $\psi$ does not hold.
These are the positions located in Fig. 5 along $\rho$. From each of these
positions we will extract prefixes $w_{i},\ldots,w_{i+k}$ such that they all
verify the lemma, i.e., the cylinder obtained from each of them does not
satisfy $\phi$. To conclude the proof we extract from $\rho$ a prefix $w$ that
contains all the prefixes $w_{i},\ldots,w_{i+k}$ and argue that this prefix
$w$ satisfies the lemma. The full proof is in Appendix 0.B.1.

######  Proof (Proof of Theorem 4.1)

The implication
$\mathcal{L}\models\phi\implies\mathcal{L}\models_{\text{\tiny{\sf AS}}}\phi$
is trivial.

The converse implication follows from Lemma 6. In order to see this, assume by
contrapositive that there exists an LTS $\mathcal{L}$ and a simple formula
$\phi$ such that $\mathcal{L}\not\models\phi$. This means that for each $k\geq
0$, there exists a run $\rho_{k}\in\mathsf{Runs_{init}}$ such that
$(\rho_{k},k)\not\models\phi$. By Lemma 6, there exists a prefix $w$ of
$\rho_{k}$ such that for any run $\rho^{\prime}\in\mathsf{Cyl}(w)$,
$(\rho^{\prime},k)\not\models\phi$. To conclude, it is sufficient to notice
that $w$ is finite thus $\mathsf{Cyl}(w)$ has positive probability, and since
this holds for any $k\geq 0$, it follows that
$\mathcal{L}\not\models_{\text{\tiny{\sf AS}}}\phi$.

##  5 Initialized formulas

In this section we identify a fragment for which the fair model checking
problem has a lower complexity.

###### Definition 9

The fragment
$\mathsf{\mathsf{F}\big{(}\mathsf{L}^{+}(\mathsf{F}_{\mathsf{P}}^{\infty})\big{)}}$
is defined as follows: a formula
$\phi\in\mathsf{\mathsf{F}\big{(}\mathsf{L}^{+}(\mathsf{F}_{\mathsf{P}}^{\infty})\big{)}}$
if and only if there is a formula
$\psi\in\mathsf{L}^{+}(\mathsf{F}_{\mathsf{P}}^{\infty})$ such that
$\phi=\mathsf{F}\psi$.

Intuitively, a formula
$\mathsf{F}\psi\in\mathsf{\mathsf{F}\big{(}\mathsf{L}^{+}(\mathsf{F}_{\mathsf{P}}^{\infty})\big{)}}$
means that at some point, after some initialization, the model satisfies a
formula $\psi\in\mathsf{L}^{+}(\mathsf{F}_{\mathsf{P}}^{\infty})$. This
fragment enjoys the property of prefix independence i.e., if $\rho$ is a run
and $\phi$ is a formula in
$\mathsf{\mathsf{F}\big{(}\mathsf{L}^{+}(\mathsf{F}_{\mathsf{P}}^{\infty})\big{)}}$,
then the following holds for any $k\geq 0$ and $i\geq 0$,
$(\rho,k)\models\phi$ if and only if $(\rho[i..],k)\models\phi$.

###  5.1 Universal model checking for
$\mathsf{\mathsf{F}\big{(}\mathsf{L}^{+}(\mathsf{F}_{\mathsf{P}}^{\infty})\big{)}}$
is $\mathsf{coNP}$ complete

In this section we show the following Theorem:

###### Theorem 5.1

The universal model checking problem for
$\mathsf{\mathsf{F}\big{(}\mathsf{L}^{+}(\mathsf{F}_{\mathsf{P}}^{\infty})\big{)}}$
is $\mathsf{coNP}$-complete.

$a$A$b$B Figure 6:
$\mathsf{\mathsf{F}\big{(}\mathsf{L}^{+}(\mathsf{F}_{\mathsf{P}}^{\infty})\big{)}}$
vs. $\mathsf{L(\mathsf{F}_{\mathsf{P}}^{\infty})}$.

This complexity result follows almost immediately from the following
observation: Let $\mathcal{L}$ be an LTS which is not a model for some formula
in
$\mathsf{\mathsf{F}\big{(}\mathsf{L}^{+}(\mathsf{F}_{\mathsf{P}}^{\infty})\big{)}}$.
This means that $\mathcal{L}$ contains a faulty execution. We argue that this
execution necessarily happens inside the same SCC, i.e., there exists an SCC
that contains a counter example. We shall call this property, _the
concentration property_. To get some intuition on why it is the case, consider
for example the system depicted in Fig. 6, and consider the formula
$\mathsf{F}(\mathsf{F}_{\mathsf{P}}^{\infty}\sf{A}\lor\mathsf{F}_{\mathsf{P}}^{\infty}\sf{B})$.
Notice that this system consists of two trivial SCCs $\\{a\\}$, and $\\{b\\}$.
Notice also that this system contains essentially two kinds of infinite runs;
those which stay in $\\{a\\}$ and those which ultimately reach $\\{b\\}$. In
the former case the formula is satisfied since $\sf{A}$ is always visited, and
in the latter case the formula is satisfied because as soon as $\\{b\\}$ is
reached, $\sf{B}$ is always visited. However if we consider the same formula
for the system depicted in Fig. 2, then the formula is not satisfied anymore.
The main difference between these two models is that in the first case the
necessary avoiding cycles are found in different SCCs while they are in the
same SCC in the second case. This observation is the core idea towards the
$\mathsf{coNP}$ membership of the universal model checking problem for this
fragment. We formalize this in Lemma 7 and prove it in Appendix 0.C.1.

######  Lemma 7 ()

Let $\mathcal{L}$ be an LTS,
$\psi\in\mathsf{L}^{+}(\mathsf{F}_{\mathsf{P}}^{\infty})$ be a filtered
formula in canonical form, and $k\geq|\mathsf{S}|+1$, there exists a run
$\rho$ such that $(\rho,k)\not\models\mathsf{F}\psi$ if and only if there
exists a strongly connected component $C$ and a $\psi$-avoiding sequence
realized in $C$.

To obtain the membership, we use a variation of Algorithm 1 that consists in
accepting an input if and only if the guessed avoiding sequence can be
realized inside the same strongly connected component. The correctness of this
variation follows from Lemma 7. Notice also that this verification is not
detrimental to the membership in $\mathsf{coNP}$ since one can decompose the
system into strongly connected components in linear time. The hardness is
again obtained from [9] by noticing that the same encoding once more applies
to the fragment considered here. This mainly follows from the fact that the
encoding of 3-SAT builds a strongly connected LTS. This yields Theorem 5.1.
For the sake of completness the modification of Algorithm 1 is in Appendix
0.C.1

###  5.2 A PTIME algorithm for the fair model checking of
$\mathsf{\mathsf{F}\big{(}\mathsf{L}^{+}(\mathsf{F}_{\mathsf{P}}^{\infty})\big{)}}$

The main focus of this part will be the proof of the following theorem:

###### Theorem 5.2

The fair model checking problem for
$\mathsf{\mathsf{F}\big{(}\mathsf{L}^{+}(\mathsf{F}_{\mathsf{P}}^{\infty})\big{)}}$
can be solved in polynomial time.

We will need the following notions:

######  Definition 10 (Strict predecessor)

Given an LTS $\mathcal{L}$ and a subset $U\subseteq\mathsf{S}$ of states, the
strict predecessor set of $U$ is the set
$\mathsf{SPred}(U)=\\{s\in\mathsf{S}\mid\mathsf{Succ}(s)\subseteq U\\}$.

In other words, $\mathsf{SPred}(U)$ describes the set of states $s$ from where
it is unavoidable to hit $U$ in one step. Consider now the operator $\mu\colon
U\mapsto U\cup\mathsf{SPred}(U)$.

######  Definition 11 (Sure attractor)

Given an LTS $\mathcal{L}$ and a subset $U\subseteq\mathsf{S}$ of states. We
call the smallest fixed point of $\mu$ denoted by $\mathsf{SPred}^{*}(U)$ the
set of _sure attractor_.

Data: An LTS
$\mathcal{L}=\langle\mathsf{S},s_{\mathsf{init}},\mathsf{T},\mathsf{lbl}\colon\mathsf{S}\to
2^{\mathsf{AP}}\rangle$ and a formula
$\mathsf{F}\phi\in\mathsf{\mathsf{F}\big{(}\mathsf{L}^{+}(\mathsf{F}_{\mathsf{P}}^{\infty})\big{)}}$

Result: Whether $\mathcal{L}\models_{\text{\tiny{\sf AS}}}\mathsf{F}\phi$

_CheckSystem(_$\mathcal{L},\mathsf{F}\phi$_)_

$\textnormal{{Components}}\leftarrow$ The set of all the BSCCs of
$\mathcal{L}$;

forall  _$\textnormal{{C}}\in\textnormal{{Components}}$_ do

tmp $\leftarrow$ CheckBSCC(_$\textnormal{{C}},\mathcal{L},\phi$_);

if  _$\textnormal{{tmp}}\neq\textnormal{{C}}$_ then

return _no_ ;

return _yes_ ;

_CheckBSCC(_$\textnormal{{C}},\mathcal{L},\phi$_)_

if  _$\phi\in\mathsf{AP}$_ then

return the set $\\{s\in\textnormal{{C}}\mid\phi\in\mathsf{lbl}(s)\\}$;

else if  _$\phi=\psi\land\theta$_ then

return CheckBSCC(_$\textnormal{{C}},\mathcal{L},\psi$_) $\cap$
CheckBSCC(_$\textnormal{{C}},\mathcal{L},\theta$_);

else if  _$\phi=\psi\lor\theta$_ then

return CheckBSCC(_$\textnormal{{C}},\mathcal{L},\psi$_) $\cup$
CheckBSCC(_$\textnormal{{C}},\mathcal{L},\theta$_);

else if  _$\phi=\mathsf{F}_{\mathsf{P}}^{\infty}\psi$_ then

tmp $\leftarrow$ CheckBSCC(_$\textnormal{{C}},\mathcal{L},\psi$_);

if
_$\mathsf{SPred}^{*}(\textnormal{{C}},\textnormal{{tmp}})=\textnormal{{C}}$_
then

return C;

else

return $\emptyset$;

Algorithm 2 Polynomial time algorithm for the fair model checking of
$\mathsf{\mathsf{F}\big{(}\mathsf{L}^{+}(\mathsf{F}_{\mathsf{P}}^{\infty})\big{)}}$

Since formulas in
$\mathsf{F}\phi\in\mathsf{F}(\mathsf{L}^{+}(\mathsf{F}_{\mathsf{P}}^{\infty}))$
define _prefix independent_ sets, we can ignore any finite prefix of a run,
and only check that $\phi$ is almost surely satisfied in each BSCC. The
decomposition into BSCCs can be done using standard graph techniques. The crux
resides in checking whether a BSCC $B$ is “good”, i.e., whether the formula is
almost surely satisfied in $B$. This is done by a _tableaux like_ approach. We
recursively compute the set of states from where _sub-formulas_ are satisfied.
The key observation lies in the fact thet $B$ is “good” if and only if the
formula can be satisfied from anywhere in $B$. This intuition is described in
Algorithm 2. Thanks to Lemma 8 and Lemma 9, Theorem 5.2 follows by noticing
that the set of all the BSCCs can be computed in linear time.

######  Lemma 8 ()

Given an LTS $\mathcal{L}$ and a formula
$\mathsf{F}\phi\in\mathsf{F}(\mathsf{L}^{+}(\mathsf{F}_{\mathsf{P}}^{\infty}))$,
then $\mathcal{L}\models_{\text{\tiny{\sf AS}}}\mathsf{F}\phi$ if and only if
CheckSystem returns yes.

######  Lemma 9 ()

Given an LTS $\mathcal{L}$, a BSCC B of $\mathcal{L}$ and a formula
$\mathsf{F}\phi\in\mathsf{F}(\mathsf{L}^{+}(\mathsf{F}_{\mathsf{P}}^{\infty}))$,
the procedure ${\sf CheckBSCC(B,\mathcal{L},\phi)}$ runs in time
$O(|\phi||B|^{2})$.

##  6 Discussion and conclusion

In this section we discuss our results, some immediate corollaries and future
work. The first point we address might seem technical at a first glance, but
we believe that it is worth mentioning. It concerns the maner in which the
quantification on the bound is used in the evaluation of pLTL:

#### Strong against weak semantics

Recall that pLTL formulas are evaluated with respect to a uniform bound $k$,
i.e., for a system to be a model to some formula, all its runs are evaluated
using the same bound $k$. Let us refer to this semantics as _strong_. One
could want to relax this semantics and ask that a system $\mathcal{L}$
satisfies a formula $\phi$ if for every run $\rho$ there exists a bound $k$
such that $(\rho,k)\models\phi$. Let us call this semantics _weak_. This
raises the following questions: _are both semantics equivalent?_ Obviously,
the strong semantics always implies the weak one. However, the converse does
not hold. To separate these two semantics, consider the system depicted in
Fig. 6, and the formula
$\phi=\mathsf{F}_{\mathsf{P}}^{\infty}\sf{A}\lor\mathsf{F}_{\mathsf{P}}^{\infty}\sf{B}$.
This system is a model to the formula $\psi$ with respect to the weak
semantics but not the strong one. This raises in turn another natural
question: _Are these two semantics equivalent in some fragment?_ We answer
positively to this question by noticing that they collapse for formulas in
$\mathsf{F}(\mathsf{L}^{+}(\mathsf{F}_{\mathsf{P}}^{\infty}))$. This actually
follows from noticing that _The weak and strong semantics are equivalent for
formulas in $\phi\in\mathsf{L(\mathsf{F}_{\mathsf{P}}^{\infty})}$ if they are
evaluated over a strongly connected LTS_. This is formally proved in Appendix
0.D.

#### Probabilistic model checking

The last point we want to discuss is the complexity of quantitative
verification for the fragment
$\mathsf{F}(\mathsf{L}^{+}(\mathsf{F}_{\mathsf{P}}^{\infty}))$. Once again,
our fragment behaves well, in that one can compute the _satisfaction
probability_ of a system with respect to a formula in
$\mathsf{F}(\mathsf{L}^{+}(\mathsf{F}_{\mathsf{P}}^{\infty}))$ in polynomial
time. This is formally proved in Appendix 0.D.

#### Future work

First, we plan on studying the complexity of the weak semantics for formulas
in $\mathsf{F}(\mathsf{L}^{+}(\mathsf{F}_{\mathsf{P}}^{\infty}))$. Second, we
plan on studying the synthesis problem induced by these fragments.

## References

  * [1] Christel Baier and Joost-Pieter Katoen.  Principles of model checking.  MIT Press, 2008.
  * [2] Thomas Brihaye, Florent Delgrange, Youssouf Oualhadj, and Mickael Randour.  Life is random, time is not: Markov decision processes with window objectives.  Log. Methods Comput. Sci., 16(4), 2020.
  * [3] Véronique Bruyère, Quentin Hautem, and Mickael Randour.  Window parity games: an alternative approach toward parity games with time bounds.  In Domenico Cantone and Giorgio Delzanno, editors, Proceedings of the Seventh International Symposium on Games, Automata, Logics and Formal Verification, GandALF 2016, Catania, Italy, 14-16 September 2016, volume 226 of EPTCS, pages 135–148, 2016.
  * [4] Diego Calvanese, Giuseppe De Giacomo, and Moshe Y. Vardi.  Reasoning about actions and planning in LTL action theories.  In Dieter Fensel, Fausto Giunchiglia, Deborah L. McGuinness, and Mary-Anne Williams, editors, Proceedings of the Eights International Conference on Principles and Knowledge Representation and Reasoning (KR-02), Toulouse, France, April 22-25, 2002, pages 593–602. Morgan Kaufmann, 2002.
  * [5] Krishnendu Chatterjee.  Concurrent games with tail objectives.  Theor. Comput. Sci., 388(1-3):181–198, 2007.
  * [6] Krishnendu Chatterjee, Laurent Doyen, Mickael Randour, and Jean-François Raskin.  Looking at mean-payoff and total-payoff through windows.  Inf. Comput., 242:25–52, 2015.
  * [7] Edmund M. Clarke, E. Allen Emerson, and A. Prasad Sistla.  Automatic verification of finite-state concurrent systems using temporal logic specifications.  ACM Trans. Program. Lang. Syst., 8(2):244–263, 1986.
  * [8] Costas Courcoubetis and Mihalis Yannakakis.  The complexity of probabilistic verification.  J. ACM, 42(4):857–907, 1995.
  * [9] E. Allen Emerson and Chin-Laung Lei.  Modalities for model checking: Branching time logic strikes back.  Sci. Comput. Program., 8(3):275–306, 1987.
  * [10] Ronald Fagin, Joseph Y. Halpern, Yoram Moses, and Moshe Y. Vardi.  Reasoning About Knowledge.  MIT Press, Cambridge, MA, USA, 2003.
  * [11] Giuseppe De Giacomo and Moshe Y. Vardi.  Automata-theoretic approach to planning for temporally extended goals.  In Susanne Biundo and Maria Fox, editors, Recent Advances in AI Planning, 5th European Conference on Planning, ECP’99, Durham, UK, September 8-10, 1999, Proceedings, volume 1809 of Lecture Notes in Computer Science, pages 226–238. Springer, 1999.
  * [12] Hugo Gimbert and Florian Horn.  Solving simple stochastic tail games.  In Moses Charikar, editor, Proceedings of the Twenty-First Annual ACM-SIAM Symposium on Discrete Algorithms, SODA 2010, Austin, Texas, USA, January 17-19, 2010, pages 847–862. SIAM, 2010.
  * [13] Hugo Gimbert and Edon Kelmendi.  Two-player perfect-information shift-invariant submixing stochastic games are half-positional.  CoRR, abs/1401.6575, 2014.
  * [14] Orna Kupferman, Nir Piterman, and Moshe Vardi.  From liveness to promptness.  Formal Methods in System Design, 34, 04 2009.
  * [15] Anca Muscholl and Igor Walukiewicz.  An np-complete fragment of LTL.  Int. J. Found. Comput. Sci., 16(4):743–753, 2005.
  * [16] J.C. Oxtoby.  Measure and Category: A Survey of the Analogies Between Topological and Measure Spaces.  Graduate Texts in Mathematics. Springer New York, 1971.
  * [17] Amir Pnueli.  The temporal logic of programs.  In 18th Annual Symposium on Foundations of Computer Science (sfcs 1977), pages 46–57, 1977.
  * [18] Amir Pnueli and Roni Rosner.  On the synthesis of a reactive module.  In Conference Record of the Sixteenth Annual ACM Symposium on Principles of Programming Languages, Austin, Texas, USA, January 11-13, 1989, pages 179–190. ACM Press, 1989.
  * [19] Amir Pnueli and Roni Rosner.  On the synthesis of an asynchronous reactive module.  In Giorgio Ausiello, Mariangiola Dezani-Ciancaglini, and Simona Ronchi Della Rocca, editors, Automata, Languages and Programming, 16th International Colloquium, ICALP89, Stresa, Italy, July 11-15, 1989, Proceedings, volume 372 of Lecture Notes in Computer Science, pages 652–671. Springer, 1989.
  * [20] Jean-Pierre Queille and Joseph Sifakis.  Specification and verification of concurrent systems in CESAR.  In Mariangiola Dezani-Ciancaglini and Ugo Montanari, editors, International Symposium on Programming, 5th Colloquium, Torino, Italy, April 6-8, 1982, Proceedings, volume 137 of Lecture Notes in Computer Science, pages 337–351. Springer, 1982.
  * [21] Matthias Schmalz, Hagen Völzer, and Daniele Varacca.  Model checking almost all paths can be less expensive than checking all paths.  In Vikraman Arvind and Sanjiva Prasad, editors, FSTTCS 2007: Foundations of Software Technology and Theoretical Computer Science, 27th International Conference, New Delhi, India, December 12-14, 2007, Proceedings, volume 4855 of Lecture Notes in Computer Science, pages 532–543. Springer, 2007.
  * [22] A. Sistla and Edmund Clarke.  The complexity of propositional linear temporal logics.  J. ACM, 32:733–749, 07 1985.
  * [23] Hagen Völzer and Daniele Varacca.  Defining fairness in reactive and concurrent systems.  J. ACM, 59(3):13:1–13:37, 2012.

## Appendix

##  Appendix 0.A Proofs from Section 3

In the proof of Lemma 2 and Lemma 3, we use the notion of the _rank_ of a
formula:

######  Definition 12 (Rank of a filtered formula)

Let $\psi$ be a filtered formula in canonical form, the rank of $\psi$ denoted
$\mathsf{Rk}(\psi)$ computes the nesting depth of temporalities in $\psi$.
Formally it is obtained as follows:

$\displaystyle\mathsf{Rk}(\psi)=\begin{cases}0\text{ if }\psi\text{ is a state
formula}\\\
1+\max\\{\mathsf{Rk}(\psi_{1}),\ldots,\mathsf{Rk}(\psi_{m})\\}\text{ if
}\psi=\theta\lor\bigvee_{i=0}^{m}\mathsf{F}_{\mathsf{P}}^{\infty}\psi_{i}\end{cases}$

###  0.A.1 Proof of Lemma 2

See 2

###### Proof

Let us prove this result by induction over the rank of the formula.

If $\mathsf{Rk}(\psi)=0$, let us write $\psi=\theta$. As
$(\rho,k)\not\models\mathsf{F}_{\mathsf{P}}^{\infty}\theta$, by definition,
there exists a position $j_{0}\geq 0$ such that for all $j_{0}\leq j\leq
j_{0}+k$, $\theta\not\in\mathsf{lbl}(\rho[j]$). Since $k\geq|\mathsf{S}|+1$,
$\rho[j_{0}..(j_{0}+k)]$ contains a cycle, let say
$u^{\theta}=\rho[j_{1}..j_{2}]$, for some $j_{0}\leq j_{1}<j_{2}\leq j_{0}+k$.
By construction, $\mathsf{occ}(u^{\theta})$ is $\theta$-avoiding. Since
$\rho[j_{1}]\in\mathsf{occ}(u^{\theta})$, $u^{\theta}$ is realized by $\rho$.
Since $\mathsf{Tree}(\theta)$ consists of a single node labeled by $\theta$,
$u^{\theta}$ is a $\psi$-avoiding sequence realized by $\rho$.

If $\mathsf{Rk}(\psi)\geq 1$, $\psi$ being filtered, let us write
$\psi=\theta\lor\bigvee_{i=0}^{m}\mathsf{F}_{\mathsf{P}}^{\infty}\psi_{i}$. We
build a $\psi$-avoiding sequence $U^{\psi}$ associated with
$\mathsf{Tree}(\psi)$. We build a mapping $w^{\psi}$ from the nodes of
$\mathsf{Tree}(\psi)$ to $\mathsf{S}^{+}$, and an order $\prec_{\psi}$ over
the image of $w^{\psi}$.

As $(\rho,k)\not\models\mathsf{F}_{\mathsf{P}}^{\infty}\psi$, by definition,
exists a position $j_{0}\geq 0$ such that for all $j_{0}\leq j\leq j_{0}+k$,
$(\rho[j..],k)\not\models\theta\lor\bigvee_{i=0}^{m}\mathsf{F}_{\mathsf{P}}^{\infty}\psi_{i}$.
In a similar way as before, exists a $\theta$-avoiding cycle $u^{\theta}$
realized by $\rho$. The word $u^{\theta}$ will be the image of the root of
$\mathsf{Tree}(\psi)$ and the minimum for the order $\prec_{\psi}$.

Let us write $\rho^{\prime}=\rho[j_{0}+k..]$. Then,
$(\rho^{\prime},k)\not\models\bigvee_{i=0}^{m}\mathsf{F}_{\mathsf{P}}^{\infty}\psi_{i}$.
Therefore, for each $0\leq i\leq m$,
$(\rho^{\prime},k)\not\models\mathsf{F}_{\mathsf{P}}^{\infty}\psi_{i}$.
Moreover, for each $0\leq i\leq m$, $\mathsf{Rk}(\psi_{i})<\mathsf{Rk}(\psi)$.
By induction hypothesis, exists for each $0\leq i\leq m$ a $\psi_{i}$-avoiding
sequence $u^{\psi_{i}}$ realized by $\rho^{\prime}$. Let us write
$u^{\psi_{i}}=u^{\psi_{i}}_{0},\ldots,u^{\psi_{i}}_{l_{i}}$ for some
$l_{i}\geq 0$. For each node $n$ in $\mathsf{Tree}(\psi)$, let us define
$w^{\psi}(n)=u^{\theta}$ if $n$ is the root of the tree, and
$w^{\psi}(n)=w^{\psi_{i}}(n)$ if $n$ is in $\mathsf{Tree}_{\psi_{i}}$, where
$w^{\psi_{i}}$ is the mapping over $\mathsf{Tree}(\psi_{i})$ induced by
$U^{\psi_{i}}$. Note that each $w^{\psi}(n)$ is either $u^{\theta}$ or a
$u^{\psi_{i}}_{l}$ for some $i$ and $l$, and therefore, we use one or the
other without distinction. By Definition 8, as each $u^{\psi_{i}}$ for $0\leq
i\leq m$ is realized by $\rho^{\prime}$, there exists a non-decreasing
sequence of positions $p^{\psi_{i}}_{0},\ldots,p^{\psi_{i}}_{l_{i}}$ such that
for all $0\leq l\leq l_{i}$,
$\rho^{\prime}[p^{\psi_{i}}_{l}]\in\mathsf{occ}(u^{\psi_{i}}_{l})$. Let us
construct the order $\prec_{\rho^{\prime}}$ over the words $u^{\psi_{i}}_{l}$,
for all $0\leq i\leq m$ and $0\leq l\leq l_{i}$ as follows:

  * •

If $p^{\psi_{i}}_{l}<p^{\psi_{i^{\prime}}}_{l^{\prime}}$ then
$u^{\psi_{i}}_{l}\prec_{\rho^{\prime}}u^{\psi_{i^{\prime}}}_{l^{\prime}}$.

  * •

If $p^{\psi_{i}}_{l}=p^{\psi_{i^{\prime}}}_{l^{\prime}}$ then
$\begin{cases}\text{if $i=i^{\prime}$,
$u^{\psi_{i}}_{l}\prec_{\rho^{\prime}}u^{\psi_{i}}_{l^{\prime}}$ if and only
if $l<l^{\prime}$}\\\ \text{otherwise the order is arbitrary}\end{cases}$

We extend $\prec_{\rho^{\prime}}$ to $\prec_{\psi}$ by adding $u^{\theta}$ as
a minimum.

We claim that $\prec_{\psi}$ agrees with $\mathsf{Tree}(\psi)$, that is, if
$n$ and $n^{\prime}$ are two nodes in $\mathsf{Tree}(\psi)$ such that
$n\prec_{\mathcal{T}}n^{\prime}$, then
$w^{\psi}(n)\prec_{\psi}w^{\psi}(n^{\prime})$. Let
$n\prec_{\mathcal{T}}n^{\prime}$ be two nodes of $\mathsf{Tree}(\psi)$. Two
cases can occur.

  * •

If $n$ is the root of $\mathsf{Tree}(\psi)$, then $w^{\psi}(n)=u^{\theta}$ is
the minimum of $\prec_{\psi}$.

  * •

If $n$ is not the root of $\mathsf{Tree}(\psi)$, then $n$ is a node of some
$\mathsf{Tree}(\psi_{i})$, for some $0\leq i\leq m$. Therefore, $n^{\prime}$
is also a node of $\mathsf{Tree}(\psi_{i})$, and since $u^{\psi_{i}}$ is a
$\psi_{i}$-avoiding sequence associated with $\mathsf{Tree}(\psi_{i})$,
$w^{\psi}(n)=u^{\psi_{i}}_{l}$ and
$w^{\psi}(n^{\prime})=u^{\psi_{i}}_{l^{\prime}}$ for some $l<l^{\prime}$.
Since $U^{\psi_{i}}$ is realized by $\rho^{\prime}$, by construction of
$\prec_{\rho^{\prime}}$,

    * –

either $p^{\psi_{i}}_{l}<p^{\psi_{i}}_{l^{\prime}}$, hence
$u^{\psi_{i}}_{l}\prec_{\psi}u^{\psi_{i}}_{l^{\prime}}$,

    * –

or $p^{\psi_{i}}_{l}=p^{\psi_{i}}_{l^{\prime}}$, and since $l<l^{\prime}$,
$u^{\psi_{i}}_{l}\prec_{\psi}u^{\psi_{i}}_{l^{\prime}}$.

Therefore, $(w^{\psi},\prec_{\psi})$ is a sequence associated with
$\mathsf{Tree}(\psi)$. Let us call it
$U^{\psi}=u^{\psi}_{0},u^{\psi}_{1},u^{\psi}_{2},\ldots,u^{\psi}_{l_{\psi}}$.

Now, let us prove that $U^{\psi}$ is $\psi$-avoiding. By construction of
$U^{\psi}$, $u^{\psi}_{0}=u^{\theta}$ is $n_{0}$-avoiding, since $n_{0}$ is
the root of $\mathsf{Tree}(\psi)$ and labeled by $\theta$, and
$\mathsf{occ}(u^{\theta})$ is $\theta$-avoiding. For another node $n$, $n$ is
in $\mathsf{Tree}(\psi_{i})$ for some $0\leq i\leq m$. By induction
hypothesis, $U^{\psi_{i}}$ is $\psi_{i}$-avoiding, and therefore
$occ(w^{\psi_{i}}(n))$ is $n$-avoiding. Since $w^{\psi}(n)=w^{\psi_{i}}(n)$
for each $n$, $U^{\psi}$ is $\psi$-avoiding.

To conclude, let us prove that $\rho$ realizes $U^{\psi}$. For each $1\leq
l\leq l_{\psi}$, there exists a $0\leq i\leq m$ and a $0\leq l^{\prime}\leq
l_{i}$ such that $u^{\psi}_{l}=u^{\psi_{i}}_{l^{\prime}}$. By definition of
$p^{\psi_{i}}$,
$\rho^{\prime}[p^{\psi_{i}}_{l^{\prime}}]\in\mathsf{occ}(u^{\psi_{i}}_{l^{\prime}})$
and therefore
$\rho^{\prime}[p^{\psi_{i}}_{l^{\prime}}]\in\mathsf{occ}(u^{\psi}_{l})$. Let
$p^{\psi}_{l}=(j_{0}+k)+p^{\psi_{i}}_{l^{\prime}}$, and $p^{\psi}_{0}=j_{1}$.
Therefore, $\rho[p^{\psi}_{0}]=\rho[j_{1}]\in\mathsf{occ}[\theta]$, and for
$1\leq l\leq l_{\psi}$,
$\rho[p^{\psi}_{l}]=\rho^{\prime}[p^{\psi_{i}}_{l^{\prime}}]\in\mathsf{occ}(u^{\psi}_{l})$.
By construction, the sequence $p^{\psi}_{0},\ldots,p^{\psi}_{l_{\psi}}$ is
non-decreasing, and therefore $\rho$ realizes $U^{\psi}$.

###  0.A.2 Proof of Lemma 3

See 3

###### Proof

Let $U$ be a realisable $\psi$-avoiding sequence, let us write
$U=u_{0}\ldots,u_{l}$, and let us show by induction over the rank
$\mathsf{Rk}(\psi)$ that each $k$-pumping $\rho_{k}$ of some realisation
witness $(U,v_{0},v_{1},\ldots,v_{l+1})$ satisfies
$(\rho_{k},k)\not\models\mathsf{F}_{\mathsf{P}}^{\infty}\psi$.

If $\mathsf{Rk}(\psi)=0$, then $\psi=\theta$ is a state formula, $U$ has a
unique word $u_{0}$, and $\mathsf{occ}(u_{0})$ is $\theta$-avoiding. Consider
the $k$-pumping $\rho_{k}=v_{0}u_{0}^{k}v_{1}$. Then, for each $0\leq j\leq
k$, $\rho_{k}[|v_{0}|+j]\in u_{0}$, therefore
$\theta\not\in\mathsf{lbl}(\rho_{k}[|v_{0}|+j])$. This means that
$(\rho_{k},k)\not\models\mathsf{F}_{\mathsf{P}}^{\infty}\psi$.

If $\mathsf{Rk}(\psi)\geq 1$, since $\psi$ is filtered and in canonical form,
write
$\psi\equiv\theta\lor\bigvee_{i=1}^{l^{\prime}}(\mathsf{F}_{\mathsf{P}}^{\infty}\psi_{i})$
where $\theta$ is a state formula, and let $j_{0}=|v_{0}|$, and $\rho_{k}$ be
a $k$-pumping. Then, by definition, for each $0\leq j\leq k$,
$\rho_{k}[j_{0}+j]\in u_{0}$, thus,
$\theta\not\in\mathsf{lbl}(\rho_{k}[j_{0}+j])$. Choose a position $0\leq i\leq
m$, we build $U^{\psi_{i}}$ the $\psi_{i}$-avoiding sequence induced by $U$ by
considering the restriction of $U$ over the subtree $\mathsf{Tree}(\psi_{i})$
of $\mathsf{Tree}(\psi)$. Write
$U^{\psi_{i}}=u^{\psi_{i}}_{0},\ldots,u^{\psi_{i}}_{l}$ and let us define
$p_{0}<\ldots<p_{l}$ such that
$u^{\psi_{i}}_{0}=u_{p_{0}},\ldots,u^{\psi_{i}}_{l}=u_{p_{l}}$. Then

$(U^{\psi_{i}},v_{1}(u_{1})^{k}v_{2}\cdots
v_{p_{0}},v_{p_{0}+1}(u_{p_{0}+1})^{k}\cdots
v_{p_{1}},\ldots,v_{p_{m}+1}(u_{p_{m}+1})^{k}\cdots v_{l+1})$

is a realisation witness of $(u^{\psi_{i}},\mathcal{L})$. Moreover,
$\rho^{\prime}_{k}=\rho_{k}[(j_{0}+k|u_{0}|)..]$ is a $k$-pumping of this
realisation witness.

Now by induction hypothesis,
$(\rho^{\prime}_{k},k)\not\models\mathsf{F}_{\mathsf{P}}^{\infty}\psi_{i}$.
Furthermore, for all positions $0\leq j\leq k$, $\rho^{\prime}_{k}$ is a
suffixe of $\rho_{k}[(j_{0}+j)..]$, thus
$(\rho_{k}[(j_{0}+j)..],k)\not\models\mathsf{F}_{\mathsf{P}}^{\infty}\psi_{i}$.
Finally, since this holds true for each $0\leq i\leq m$, it follows that for
all positions $0\leq j\leq k$, we have

$(\rho_{k}[(j_{0}+j)..],k)\not\models\theta\lor\bigvee_{i=1}^{l^{\prime}}(\mathsf{F}_{\mathsf{P}}^{\infty}\psi_{i})$

hence, $(\rho_{k},k)\not\models\mathsf{F}_{\mathsf{P}}^{\infty}\psi$ which
concludes the proof.

###  0.A.3 Proof of Lemma 4

We first prove the following lemma:

###### Lemma 10

Given an LTS $\mathcal{L}$ and a filtered formula
$\phi\in\mathsf{L}^{+}(\mathsf{F}_{\mathsf{P}}^{\infty})$, then

$\forall k\geq 0,\leavevmode\nobreak\
(\rho_{k},k)\not\models\mathsf{F}_{\mathsf{P}}^{\infty}\psi\iff\forall k\geq
0,\leavevmode\nobreak\ (\rho_{k},k)\not\models\psi$

###### Proof

First notice that if $\psi$ is filtered and in
$\mathsf{L}^{+}(\mathsf{F}_{\mathsf{P}}^{\infty})$, then necessarily
$\psi\equiv\bigvee_{i=0}^{m}\mathsf{F}_{\mathsf{P}}^{\infty}\psi_{i}$ for some
$m>0$.

$\displaystyle(\rho_{k},k)\not\models\mathsf{F}_{\mathsf{P}}^{\infty}\psi$
$\displaystyle\implies\exists j_{0}\geq 0,\leavevmode\nobreak\ \forall 0\leq
j\leq k,\leavevmode\nobreak\ (\rho_{k}[(j_{0}+j)..],k)\not\models\psi$
$\displaystyle\implies\forall 0\leq i\leq m,\leavevmode\nobreak\
(\rho_{k}[(j_{0}+j)..],k)\not\models\mathsf{F}_{\mathsf{P}}^{\infty}\psi_{i}$
$\displaystyle\implies\forall 0\leq i\leq m,\leavevmode\nobreak\
(\rho_{k},k)\not\models\mathsf{F}_{\mathsf{P}}^{\infty}\psi_{i}$
$\displaystyle\implies(\rho_{k},k)\not\models\bigvee_{i=0}^{m}\mathsf{F}_{\mathsf{P}}^{\infty}\psi_{i}\equiv\psi$

where the first and second implications are by definition of the evaluation,
and the third is by property of $\mathsf{F}_{\mathsf{P}}^{\infty}$.

To show the other direction, we show the contrapositive

$\displaystyle\exists k\geq 0,\leavevmode\nobreak\
(\rho_{k},k)\models\mathsf{F}_{\mathsf{P}}^{\infty}\psi$
$\displaystyle\implies\forall j_{0}\geq 0,\leavevmode\nobreak\ \exists 0\leq
j\leq k\leavevmode\nobreak\ (\rho_{k}[(j_{0}+j)..],k)\models\psi^{\prime}$
$\displaystyle\implies\forall 0\leq i\leq m,\leavevmode\nobreak\ \exists 0\leq
j_{i}\leq k,\leavevmode\nobreak\
(\rho_{k}[j_{i}..],k)\models\mathsf{F}_{\mathsf{P}}^{\infty}\psi_{i}$
$\displaystyle\implies(\rho_{k},2k)\models\mathsf{F}_{\mathsf{P}}^{\infty}\psi_{i}\implies(\rho_{k},2k)\models\bigvee_{i=0}^{m}\mathsf{F}_{\mathsf{P}}^{\infty}\psi_{i}\equiv\psi$

where the first implication is by definition of the evaluation, the second is
by setting $j_{0}=0$ and distributing over all the formulas $\psi_{i}$, and
the third one holds because we add the missing prefix $\rho_{k}[..j_{i}]$.

See 4

###### Proof

We start with left to right direction. If Algorithm 1 accepts, then there
exists:

  * •

$i.$ a filtration $\psi$ of $\phi$ of the form
$\psi\equiv\theta\lor\psi^{\prime}$, where $\theta=\bigvee_{i=0}^{l}a_{i}$ and
$\psi^{\prime}=\bigvee_{i=0}^{m}\mathsf{F}_{\mathsf{P}}^{\infty}\psi_{i}$.

  * •

$ii.$ a $\psi^{\prime}$-avoiding sequence $U$ realisable in $\mathcal{L}$.

Let us show that for each $k$, there exists a run $\rho_{k}$ such that
$(\rho_{k},k)\not\models\phi$. Let $k\geq|S|+1$, first, since the initial
state does not satisfy $\bigvee_{i=0}^{l}a_{i}$, any run
$\rho\in\mathsf{Runs_{init}}$ is such that $(\rho,k)\not\models\theta$.
Second, by Lemma 3, there exists a run $\rho_{k}\in\mathsf{Runs_{init}}$ such
that $(\rho_{k},k)\not\models\mathsf{F}_{\mathsf{P}}^{\infty}\psi^{\prime}$.
By Lemma 10 $\rho_{k}$ is also a counter example for bound $k$ to the formula
$\psi^{\prime}$. By Lemma 1, this implies that $(\rho_{k},k)\not\models\phi$.
To conclude this direction one has to notice that counter examples for the
bound $|S|+1$ are also counter examples for smaller bounds.

Now we show the right to left direction. Assume that for each $k$, there
exists a run $\rho_{k}\in\mathsf{Runs_{init}}$ such that
$(\rho_{k},k)\not\models\phi$. By Lemma 1
$(\rho_{k},k)\not\models\mathsf{flt}_{\rho_{k}}(\phi)$. In order to apply
Lemma 2, let $\mathsf{flt}_{\rho_{k}}(\phi)\equiv\theta\lor\psi^{\prime}$
where $\theta=\bigvee_{i=0}^{l}a_{i}$ and
$\psi^{\prime}=\bigvee_{i=0}^{m}\mathsf{F}_{\mathsf{P}}^{\infty}\psi_{i}$.
By Lemma 10 we have that for each $k\geq 0$,
$(\rho_{k},k)\not\models\mathsf{F}_{\mathsf{P}}^{\infty}\psi^{\prime}$. By
Lemma 2, we build a $\psi^{\prime}$-avoiding sequence realized by $\rho_{k}$,
thus realizable in $\mathcal{L}$, hence Algorithm 1 will guess it and the
checks will be satisfied. To conclude that Algorithm 1 accepts, it remains to
notice that $(\rho_{k},k)\not\models\theta\lor\psi^{\prime}$ implies in
particular that $\rho[0]=s_{\mathsf{init}}$ does not satisfies $\theta$.

###  0.A.4 Proof of Lemma 5

See 5

###### Proof

Let $\mathcal{L}$ be an LTS, and a formula
$\psi\in\mathsf{L(\mathsf{F}_{\mathsf{P}}^{\infty})}$, first notice that each
guess is of polynomial size. Let us show that the verification phase can be
done in polynomial time.

  * •

To check that the initial state does not satisfy $\bigvee_{i=0}^{l}a_{i}$, one
has to check whether each $a_{i}\in\mathsf{lbl}(s_{\mathsf{init}})$. This is
clearly done in linear time.

  * •

To check that $U$ is associated with $\mathsf{Tree}(\psi)$, first, we check
that for each $0\leq j\leq m$, $w(n_{j})=u_{j}$. This can be done in
$O(|\mathsf{S}||\psi|)$. Then, we check for each $n\prec n^{\prime}$ in
$\mathsf{Tree}(\psi)$ that $w(n)\prec w(n^{\prime})$, i.e., if $w(n)=u_{j}$
and $w(n^{\prime})=u_{j^{\prime}}$, we check that $j<j^{\prime}$. This can be
done in $O(|\psi|^{2})$.

  * •

To check that $U$ is $\psi$-avoiding, we check that for each
$n\in\mathsf{Tree}(\psi)$, $\mathsf{occ}(w(n))$ is a $n$-avoiding cycle. As
$n$ is labeled by state formulas $\theta_{n}$, we check that for each $s\in
w(n)$, $\theta_{n}\not\in\mathsf{lbl}(s)$. This can be done in
$O(|\mathsf{S}||\psi|)$.

  * •

To check that $U$ is realisable in $\mathcal{L}$, we check that $u_{0}[0]$ is
reachable from $s_{\mathsf{init}}$, and that for each $0\leq j\leq l-1$, the
first state of $u_{j+1}$ is reachable from the last state of $u_{j}$, that is
$u_{j+1}[0]$ is reachable from $u_{j}[|u_{j}^{\psi_{i}}|-1]$. Thus we perform
$m$ reachability test, thus it takes at most $O(|S|^{2}|\psi|)$.

The lemma follows.

##  Appendix 0.B Proofs from Section 4

###  0.B.1 Proof of Lemma 6

See 6

###### Proof

We proceed by induction over the structure of the formula. Let $\phi$ be a
formula and let $\rho$ be a run and assume that for some $k>0$ we have
$(\rho,k)\not\models\phi$.

  * •

If $\phi=\theta$ is a state formula, then
$\theta\not\in\mathsf{lbl}(s_{\mathsf{init}})$. Hence any run
$\rho\in\mathsf{Runs_{init}}$ is such that $(\rho,k)\not\models\theta$ since
$\mathsf{Runs_{init}}=\mathsf{Cyl}(s_{\mathsf{init}})$.

  * •

If $\phi=\psi_{1}\land\psi_{2}$, then
$(\rho,k)\not\models\psi_{1}\land\psi_{2}$ if and only if
$(\rho,k)\not\models\psi_{1}$ or $(\rho,k)\not\models\psi_{2}$. W.l.o.g.,
suppose that $(\rho,k)\not\models\psi_{1}$, then by induction, there exists a
prefix $w$ of $\rho$ such that

$\forall\rho^{\prime}\in\mathsf{Cyl}(w),(\rho^{\prime},k)\not\models\psi_{1}\implies\forall\rho^{\prime}\in\mathsf{Cyl}(w),(\rho^{\prime},k)\not\models(\psi_{1}\land\psi_{2})\equiv\phi$

  * •

If $\phi=\psi_{1}\lor\psi_{2}$, then

$((\rho,k)\not\models\psi_{1}\lor\psi_{2})\iff(\rho,k)\not\models\psi_{1}\text{
and }(\rho,k)\not\models\psi_{2}$

By induction, there exist two prefixes $w_{1}$ and $w_{2}$ of $\rho$ such that

$\forall\rho^{\prime}\in\mathsf{Cyl}(w_{1}),(\rho^{\prime},k)\not\models\psi_{1}\text{
and
}\forall\rho^{\prime}\in\mathsf{Cyl}(w_{2}),(\rho^{\prime},k)\not\models\psi_{2}$

Now, since $w_{1}$ and $w_{2}$ are prefixes of the same word, one of them is a
prefix of the other, w.o.l.g., assume that $w_{2}$ is a prefix of $w_{1}$.
Then we have:

$\displaystyle\mathsf{Cyl}(w_{1})\subseteq\mathsf{Cyl}(w_{2})$
$\displaystyle\implies\forall\rho^{\prime}\in\mathsf{Cyl}(w_{1}),(\rho^{\prime},k)\not\models\psi_{2}$
$\displaystyle\implies\forall\rho^{\prime}\in\mathsf{Cyl}(w_{1}),(\rho^{\prime},k)\not\models\psi_{1}\lor\psi_{2}\equiv\phi$

  * •

If $\phi=\mathsf{F}_{\mathsf{P}}^{\infty}\psi$, then
$(\rho,k)\not\models\mathsf{F}_{\mathsf{P}}^{\infty}\psi$. By definition, this
means that there exists a position $i\geq 0$, such that for all positions
$0\leq j\leq k$, we have

$\forall j,\text{ s.t. }0\leq j\leq k,\leavevmode\nobreak\
(\rho[(i+j)..],k)\not\models\psi$

Applying the induction hypothesis from each postion $j$ we can extract a
prefix $w_{j}$ of $\rho[(i+j)..]$ such that:

$\forall\rho^{\prime}_{j}\in\mathsf{Cyl}(w_{j})\leavevmode\nobreak\
,(\rho^{\prime}_{j},k)\not\models\psi$

Now we will extract the prefix $w$, to do this, let $w$ be the smallest prefix
of $\rho$ containing all the prefixes $w_{j}$. Formally, let
$i_{0}=i+\max\\{0+|w_{0}|,\ldots,k+|w_{k}|\\}$, and chose $w=\rho[..i_{0}]$.
Let us show that $w$ satisfies the claim of the lemma. Let $\rho^{\prime}$ be
a run in $\mathsf{Cyl}(w)$, then

$\displaystyle\forall 0\leq j\leq k,\leavevmode\nobreak\
\rho^{\prime}[(i+j)..]\in\mathsf{Cyl}(w_{j})$ $\displaystyle\implies\forall
0\leq j\leq k,\leavevmode\nobreak\ (\rho^{\prime}[(i+j)..],k)\not\models\psi$
$\displaystyle\implies(\rho^{\prime},k)\not\models\mathsf{F}_{\mathsf{P}}^{\infty}\psi$

where the first implication is by construction of $w_{j}$ and the second one
by definition of $\mathsf{F}_{\mathsf{P}}^{\infty}$. This concludes the proof.

##  Appendix 0.C Proofs from Section 5

###  0.C.1 Proof of Lemma 7

Lemma 7 is useful to establish the correctness of the following procedure.

Data: An LTS
$\mathcal{L}=\langle\mathsf{S},s_{\mathsf{init}},\mathsf{T},\mathsf{lbl}\colon\mathsf{S}\to
2^{\mathsf{AP}}\rangle$ and a formula
$\phi\in\mathsf{L(\mathsf{F}_{\mathsf{P}}^{\infty})}$

Result: whether $\mathcal{L}\not\models\phi$

Guess the filtered formula $\psi$ of
$\phi\in\mathsf{L}^{+}(\mathsf{F}_{\mathsf{P}}^{\infty})$;

Guess a sequence $U=u_{0},\ldots,u_{l}$ of size $(|S|+1)|\psi|$;

Compute the tree $\mathsf{Tree}(\psi)$;

Guess a mapping between the nodes of the tree and the sequence;

Check that $U$ is associated with $\mathsf{Tree}(\psi)$;

Check that $U$ is $\psi$-avoiding;

Check that there exists an SCC $C$ s.t. $U$ is realisable inside $C$;

Algorithm 3 Non deterministic algorithm for the universal model checking of
$\mathsf{\mathsf{F}\big{(}\mathsf{L}^{+}(\mathsf{F}_{\mathsf{P}}^{\infty})\big{)}}$

See 7

###### Proof

Assume that there exists a run $\rho$ such that
$(\rho,k)\not\models\mathsf{F}\psi$. The set $C=\\{s\in\mathsf{S}\mid\forall
i,\exists j\geq i,\rho[j]=s\\}$ of infinitely often visited states in $\rho$
belongs to some SCC $C$. By definition, there exists a position $i_{0}$ such
that for all positions $j\geq i_{0}$, $\rho[j]\in C$. Since
$(\rho,k)\not\models\mathsf{F}\psi$, by definition of $\mathsf{F}$, for all
$j\geq 0$, $(\rho[(i_{0}+j)..],k)\not\models\psi$. Now since $\psi$ is
filtered and in $\mathsf{L}^{+}(\mathsf{F}_{\mathsf{P}}^{\infty})$ we can
apply Lemma 10. Therefore,
$(\rho[i_{0}..],k)\not\models\mathsf{F}_{\mathsf{P}}^{\infty}\psi$. By Lemma 2
over the LTS induced by $C$, there exists a $\psi$-avoiding sequence realized
in $C$.

Now, assume that there exists a strongly connected component $C$ and a
$\psi$-avoiding sequence $U$ realized in $C$. By Lemma 3, exists a run $\rho$
over $C$ such that $(\rho,k)\not\models\mathsf{F}_{\mathsf{P}}^{\infty}\psi$.
Since $\psi\in\mathsf{L}^{+}(\mathsf{F}_{\mathsf{P}}^{\infty})$ and is
filtered, Lemma 10 gives that $(\rho,k)\not\models\psi$. By Lemma 6, there
exists a prefix $w$ of $\rho$ such that for each run
$\rho^{\prime}\in\mathsf{Cyl}(w)$ over $C$ we have
$(\rho^{\prime},k)\not\models\psi$. Since $C$ is strongly connected, there
exists a path from $w[|w|-1]$ the last position of $w$ to $w[0]$. Let us call
this path $w^{\prime}$. Then, considere the run
$\rho^{\prime}=(ww^{\prime})^{\omega}$. By construction, for each $i\geq 0$,
there exists a position $j\geq i$ such that
$\rho^{\prime}[j..]\in\mathsf{Cyl}(w)$, therefore,
$(\rho^{\prime}[j..],k)\not\models\psi$. Since
$\psi\in\mathsf{L}(\mathsf{F}_{\mathsf{P}}^{\infty})$, this implies that for
each $j^{\prime}\leq j$, $(\rho^{\prime}[j^{\prime}..],k)\not\models\psi$.
Since this holds for infinitely many $j$, this means that
$(\rho^{\prime},k)\not\models\mathsf{F}\psi$.

###  0.C.2 Proof of Lemma 8

In order to state the proof of Lemma 8, we first need to introduce some
technical properties of Algorithm 2

First we relate the set $\mathsf{SPred}^{*}(U)$ with the avoiding cycles. Let
$B$ be a BSCC, we denote by $S^{\theta}_{B}=\\{s\in
B\mid\theta\in\mathsf{lbl}(s)\\}$.

###### Lemma 11

Let $\theta$ be a state formula, $B$ be a BSCC, then
$\mathsf{SPred}^{*}(S^{\theta}_{B})=B$ if and only if $B$ does not contain a
$\theta$-avoiding cycle.

###### Proof

First, by contrapositive, assume that $B$ contains a $\theta$-avoiding cycle
$C=\\{s_{0},\ldots,s_{n}\\}$ and let us prove that
$\mathsf{SPred}^{*}(S^{\theta}_{B})\neq B$. By definition, for all $0\leq
i\leq n$, $\theta\not\in\mathsf{lbl}(s_{i})$, and therefore $s_{i}\not\in
S^{\theta}_{B}$. By definition of the sure attractor, it is the smallest fixed
point of $\mu$. For each $0\leq i\leq n$, $s_{i}$ has a successor in $C$, and
that successor is not in $S^{\theta}_{B}$. Therefore,
$s_{i}\not\in\mu(S^{\theta}_{B})$. Since each $s_{i}$ has a succesor in $C$
that is not in $\mu(S^{\theta}_{B})$, $s_{i}\not\in\mu^{2}(S^{\theta}_{B})$.
By the same reasoning, for each $l\geq 0$ and $0\leq i\leq n$,
$s_{i}\not\in\mu^{l}(S^{\theta}_{B})$. Therefore,
$s_{i}\not\in\mathsf{SPred}^{*}(S^{\theta}_{B})$, and
$\mathsf{SPred}^{*}(S^{\theta}_{B})\neq B$.

Now, by contrapositive, assume that $\mathsf{SPred}^{*}(s^{\theta}_{B})\neq B$
and let us show that exists a $\theta$-avoiding cycle. Let
$s_{0}\not\in\mathsf{SPred}^{*}(S^{\theta}_{B})\neq B$. By definition of
$\mathsf{SPred}^{*}$, this implies that $s_{0}\not\in S^{\theta}_{B}$ and,
since $B$ is a BSCC, there must exist a successor $s_{1}$ such that
$s_{1}\not\in\mathsf{SPred}^{*}(S^{\theta}_{B})$. Repeating this argument from
$s_{1}$, there must exist $s_{2}\in\mathsf{Succ}(s_{1})$ such that
$s_{2}\not\in\mathsf{SPred}^{*}(S^{\theta}_{B})$. Since $B$ is finite, at some
point, we will find two state that $s_{i_{0}}=s_{i_{1}}$ such that
$C=\\{s_{i_{0}},\ldots,s_{i_{1}-1}\\}$ is a cycle. Moreover for all $i_{0}\leq
j\leq i_{1}-1,\leavevmode\nobreak\ s_{j}\not\in S^{\theta}_{B}$. Therefore,
$C$ is a $\theta$-avoiding cycle.

###### Lemma 12

Given an LTS $\mathcal{L}$, a BSCC $B$ of $\mathcal{L}$ and a formula
$\phi\in\mathsf{L}^{+}(\mathsf{F}_{\mathsf{P}}^{\infty})$, then exactly one of
the followings holds:

  * •

${\sf CheckBSCC(B,\mathcal{L},\phi)}=B$.

  * •

${\sf CheckBSCC(B,\mathcal{L},\phi)}=\emptyset$.

###### Proof

Let $B$ be a BSCC of $\mathcal{L}$, and
$\phi\in\mathsf{L}^{+}(\mathsf{F}_{\mathsf{P}}^{\infty})$. Let us prove the
result by structural induction over $\phi$. By definition of
$\mathsf{L}^{+}(\mathsf{F}_{\mathsf{P}}^{\infty})$, three cases can occur.

  * •

$\phi=\mathsf{F}_{\mathsf{P}}^{\infty}\psi$,
$\psi\in\mathsf{L(\mathsf{F}_{\mathsf{P}}^{\infty})}$: Then, ${\sf
CheckBSCC(B,\mathcal{L},\phi)}$ returns either $B$ or $\emptyset$, and the
result holds.

  * •

$\phi=\psi\lor\psi^{\prime}$,
$\psi,\theta\in\mathsf{L}^{+}(\mathsf{F}_{\mathsf{P}}^{\infty})$: By induction
hypothesis, ${\sf CheckBSCC(B,\mathcal{L},\psi)}$ is either equal to $B$ or to
$\emptyset$, and the same holds for ${\sf
CheckBSCC(B,\mathcal{L},\psi^{\prime})}$. Given that ${\sf
CheckBSCC(B,\mathcal{L},\phi)}={\sf CheckBSCC(B,\mathcal{L},\psi)}\cup{\sf
CheckBSCC(B,\mathcal{L},\psi^{\prime})}$, ${\sf
CheckBSCC(B,\mathcal{L},\phi)}$ is either empty (if both ${\sf
CheckBSCC(B,\mathcal{L},\psi)}$ and ${\sf
CheckBSCC(B,\mathcal{L},\psi^{\prime})}$ are empty) or equal to $B$ otherwise.

  * •

$\phi=\psi\land\psi^{\prime}$,
$\psi,\theta\in\mathsf{L}^{+}(\mathsf{F}_{\mathsf{P}}^{\infty})$: By induction
hypothesis, ${\sf CheckBSCC(B,\mathcal{L},\psi)}$ is either equal to $B$ or to
$\emptyset$, and the same holds for ${\sf
CheckBSCC(B,\mathcal{L},\psi^{\prime})}$. Given that ${\sf
CheckBSCC(B,\mathcal{L},\phi)}={\sf CheckBSCC(B,\mathcal{L},\psi)}\cap{\sf
CheckBSCC(B,\mathcal{L},\psi^{\prime})}$, ${\sf
CheckBSCC(B,\mathcal{L},\phi)}$ is either equal to $B$ (if both ${\sf
CheckBSCC(B,\mathcal{L},\psi)}$ and ${\sf
CheckBSCC(B,\mathcal{L},\psi^{\prime})}$ are equal to $B$) or empty otherwise.

###### Lemma 13

Given an LTS $\mathcal{L}$, a BSCC $B$ of $\mathcal{L}$, a formula
$\phi\in\mathsf{L(\mathsf{F}_{\mathsf{P}}^{\infty})}$, $b$ a state in $B$, and
$N=|\mathsf{S}|+1$, then the following assertions are equivalent:

  * •

$b\in{\sf CheckBSCC(B,\mathcal{L},\phi)}$.

  * •

Any run $\rho$ in $bB^{\omega}$ satisfies $(\rho,N)\models\phi$.

###### Proof

Let us show the equivalence by structural induction over $\phi$.

  * •

$\phi=\theta\in\mathsf{AP}$: Then, $b\in{\sf CheckBSCC(B,\mathcal{L},\theta)}$
if, and only if, $\theta\in\mathsf{lbl}(b)$. As $\theta\in\mathsf{lbl}(b)$ if
and only if any run $\rho$ in $bB^{\omega}$ satisfies $(\rho,N)\models\phi$,
the equivalence holds.

  * •

$\phi=\psi\land\psi^{\prime}$: First, assume that $b\in{\sf
CheckBSCC(B,\mathcal{L},\phi)}$. By construction, this implies that $b\in{\sf
CheckBSCC(B,\mathcal{L},\psi)}$ and $b\in{\sf
CheckBSCC(B,\mathcal{L},\psi^{\prime})}$. By induction hypothesis, any run
$\rho$ in $bB^{\omega}$ satisfies $(\rho,N)\models\psi$ and
$(\rho,N)\models\psi^{\prime}$, and therefore $\rho,N\models\phi$.

Now, assume that any run $\rho$ in $bB^{\omega}$ satisfies
$(\rho,N)\models\phi$. By definition, this means that $(\rho,N)\models\psi$
and $(\rho,N)\models\psi^{\prime}$. By induction hypothesis, this implies that
$b\in{\sf CheckBSCC(B,\mathcal{L},\psi)}$ and $b\in{\sf
CheckBSCC(B,\mathcal{L},\psi^{\prime})}$. By construction, this implies that
$b\in{\sf CheckBSCC(B,\mathcal{L},\phi)}$.

  * •

$\phi=\psi\lor\psi^{\prime}$: First, assume that $b\in{\sf
CheckBSCC(B,\mathcal{L},\phi)}$. By construction, this implies that $b\in{\sf
CheckBSCC(B,\mathcal{L},\psi)}$ or $b\in{\sf
CheckBSCC(B,\mathcal{L},\psi^{\prime})}$. W.l.o.g., assume $b\in{\sf
CheckBSCC(B,\mathcal{L},\psi)}$. By induction hypothesis, any run $\rho$ in
$bB^{\omega}$ satisfies $(\rho,N)\models\psi$ and therefore
$(\rho,N)\models\phi$.

Now, assume that any run $\rho$ in $bB^{\omega}$ satisfies
$(\rho,N)\models\phi$. By definition, this means that $(\rho,N)\models\psi$ or
$(\rho,N)\models\psi^{\prime}$. W.l.o.g., assume that $(\rho,N)\models\psi$.
By induction hypothesis, this implies that $b\in{\sf
CheckBSCC(B,\mathcal{L},\psi)}$. By construction, this implies that $b\in{\sf
CheckBSCC(B,\mathcal{L},\phi)}$.

  * •

$\phi=\mathsf{F}_{\mathsf{P}}^{\infty}\psi$: First, note that $\exists
b\in{\sf CheckBSCC(B,\mathcal{L},\phi)}$ is equivalent to ${\sf
CheckBSCC(B,\mathcal{L},\phi)}=B$, and therefore to $\mathsf{SPred}^{*}(C,{\sf
CheckBSCC(B,\mathcal{L},\psi)})=B$. Thus, it is enough to prove that
$\mathsf{SPred}^{*}(C,{\sf CheckBSCC(B,\mathcal{L},\psi)})=B$ if and only if
any run $\rho$ in $B^{\omega}$ satisfies $(\rho,N)\models\phi$. Let us
introduce a new label $A^{\psi}$. Let us label each set in ${\sf
CheckBSCC(B,\mathcal{L},\psi)}$ with $A^{\psi}$, and exactly those states. By
induction hypothesis, for each $b\in B$, $b\in{\sf
CheckBSCC(B,\mathcal{L},\phi)}$ if and only if any run $\rho$ in $bB^{\omega}$
satisfies $(\rho,N)\models\psi$. By construction of $A^{\psi}$, this is
equivalent to $(\rho,N)\models\theta$, where $\theta=A^{\psi}$ is a state
formula. Since ${\sf CheckBSCC(B,\mathcal{L},\psi)}$ is the maximum set
labeled by $A^{\psi}$, by Lemma 11, $\mathsf{SPred}^{*}(C,{\sf
CheckBSCC(B,\mathcal{L},\psi)})=B$ if and only if there exists no
$\theta$-avoiding cycle. By construction of $A^{\psi}$, there exists no
$\theta$-avoiding cycle is equivalent to there exists no $\psi$-avoiding
cycle. Using Lemma 2 and Lemma 3, there exists no $\psi$-avoiding cycle if and
only if for all run $\rho$ in $B^{\omega}$,
$(\rho,N)\models\mathsf{F}_{\mathsf{P}}^{\infty}\psi$.

See 8

######  Proof (Proof of Lemma 8)

First, assume that $\mathcal{L}$ fairly satisfies the formula, that is, exists
a $k$ such that
$\mathbb{P}_{\mathcal{L}}(\\{\rho\in\mathsf{Runs_{init}}(\mathcal{L})\mid(\rho,k)\models\mathsf{F}\phi\\})=1$.
Consider a BSCC $B$ of $\mathcal{L}$. Then, since $B$ is reachable,
$\mathbb{P}_{\mathcal{L}}(\\{\rho\in\mathsf{Runs_{init}}(\mathcal{L})\mid\text{$\rho$
ends in $B$}\\})\geq 0$. This implies that $\mathbb{P}_{B}(\\{\rho\in
B^{\omega}\mid(\rho,k)\models\mathsf{F}\phi\\})=1$, and since $B$ is a BSCC,
$\mathbb{P}_{B}(\\{\rho\in B^{\omega}\mid(\rho,k)\models\phi\\})=1$. By lemma
6, this implies that for all $\rho\in B^{\omega}$, $(\rho,k)\models\phi$.
Since this holds for any $\rho$ starting in any state of $B$, by lemma 13,
this implies that ${\sf CheckBSCC(B,\mathcal{L},\phi)}=B$. Since this holds
for any BSCC $B$ of $\mathcal{L}$, by definition of CheckSystem, it returns
yes.

Now, assume that $\mathcal{L}$ does not fairly satisfy the formula, that is,
for all $k$,
$\mathbb{P}_{\mathcal{L}}(\\{\rho\in\mathsf{Runs_{init}}(\mathcal{L})\mid(\rho,k)\models\mathsf{F}\phi\\})<1$.
Let us fixe a $k$. Note that
$\mathbb{P}_{\mathcal{L}}(\\{\rho\in\mathsf{Runs_{init}}(\mathcal{L})\mid\text{$\rho$
does not end in some BSCC $B$}\\})=0$. Therefore exists a BSCC $B_{k}$ of
$\mathcal{L}$ such that $\mathbb{P}_{B_{k}}(\\{\rho\in
B_{k}^{\omega}\mid(\rho,k)\models\mathsf{F}\phi\\})<1$, there exists at least
one $\rho_{k}\in B_{k}^{\omega}$ such that
$(\rho_{k},k)\not\models\mathsf{F}\phi$, and therefore, in particular,
$(\rho_{k},k)\not\models\phi$. By lemma 13, this means that
$\rho[0]\not\in{\sf CheckBSCC(B,\mathcal{L},\phi)}$ and therefore, by lemma
12, since $\phi\in\mathsf{L}^{+}(\mathsf{F}_{\mathsf{P}}^{\infty})$, ${\sf
CheckBSCC(B,\mathcal{L},\phi)}=\emptyset$. By definition of CheckSystem, it
returns no.

###  0.C.3 Proof of Lemma 9

See 9

###### Proof

We show by structural induction over $\phi$ that ${\sf
CheckBSCC(B,\mathcal{L},\phi)}$ can be computed in time $|\phi||B|^{2}$.

  * •

$\phi\in\mathsf{AP}$ is a state formula. Then, ${\sf
CheckBSCC(B,\mathcal{L},\phi)}$ is the set of states $s$ such that
$\phi\in\mathsf{lbl}(s)$. This can be computed in time $|B|\leq|B|^{2}$.

  * •

$\phi=\psi_{1}\land\psi_{2}$. Then, ${\sf CheckBSCC(B,\mathcal{L},\phi)}={\sf
CheckBSCC(B,\mathcal{L},\psi_{1})}\cap{\sf
CheckBSCC(B,\mathcal{L},\psi_{2})}$. By induction hypothesis, ${\sf
CheckBSCC(B,\mathcal{L},\psi_{1})}$ can be computed in time
$|\psi_{1}||B|^{2}$, and ${\sf CheckBSCC(B,\mathcal{L},\psi_{2})}$ can be
computed in time $|\psi_{2}||B|^{2}$. Since ${\sf
CheckBSCC(B,\mathcal{L},\psi_{1})}\subseteq B$ and ${\sf
CheckBSCC(B,\mathcal{L},\psi_{2})}\subseteq B$, the intersection can be
computed in time $|B|$. Therefore, ${\sf CheckBSCC(B,\mathcal{L},\phi)}$ can
be computed in time
$|\psi_{1}||B|^{2}+|\psi_{2}||B|^{2}+|B|\leq(|\psi_{1}|+|\psi_{2}|+1)|B|^{2}\leq|\phi||B|^{2}$.

  * •

$\phi=\psi_{1}\lor\psi_{2}$. Then, ${\sf CheckBSCC(B,\mathcal{L},\phi)}={\sf
CheckBSCC(B,\mathcal{L},\psi_{1})}\cup{\sf
CheckBSCC(B,\mathcal{L},\psi_{2})}$. By induction hypothesis, ${\sf
CheckBSCC(B,\mathcal{L},\psi_{1})}$ can be computed in time
$|\psi_{1}||B|^{2}$, and ${\sf CheckBSCC(B,\mathcal{L},\psi_{2})}$ can be
computed in time $|\psi_{2}||B|^{2}$. Since ${\sf
CheckBSCC(B,\mathcal{L},\psi_{1})}\subseteq B$ and ${\sf
CheckBSCC(B,\mathcal{L},\psi_{2})}\subseteq B$, the union can be computed in
time $|B|$. Therefore, ${\sf CheckBSCC(B,\mathcal{L},\phi)}$ can be computed
in time
$|\psi_{1}||B|^{2}+|\psi_{2}||B|^{2}+|B|\leq(|\psi_{1}|+|\psi_{2}|+1)|B|^{2}\leq|\phi||B|^{2}$.

  * •

$\phi=\mathsf{F}_{\mathsf{P}}^{\infty}\psi$. Then, to compute ${\sf
CheckBSCC(B,\mathcal{L},\phi)}$, first, ${\sf CheckBSCC(B,\mathcal{L},\psi)}$
is computed. By induction hypothesis, this is done in time $|\psi||B|^{2}$.
Then, $\mathsf{SPred}^{*}$ is computed. This is done in time $|B|^{2}$.
Therefore, ${\sf CheckBSCC(B,\mathcal{L},\phi)}$ is computed in time
$(|\psi|+1)|B|^{2}=|\phi||B|^{2}$.

##  Appendix 0.D Proofs from Section 6

###### Lemma 14

Given an LTS $\mathcal{L}$ and a formula
$\phi\in\mathsf{L(\mathsf{F}_{\mathsf{P}}^{\infty})}$, if $\mathcal{L}$ is
strongly connected, then the weak and strong prompt model checking problems
are equivalent.

###### Proof

The strong model checking trivially induces the weak one. We prove the
converse by contrapositive. Assume that $\forall k,\leavevmode\nobreak\
\exists\rho_{k},(\rho_{k},k)\not\models\phi$, and show that
$\exists\rho,\leavevmode\nobreak\ \forall k,(\rho,k)\not\models\phi$. In the
following we consider $k\geq|\mathsf{S}|+1$ since the other case follows from
the case $k=|\mathsf{S}|+1$.

Let $\psi_{k}=\mathsf{flt}_{\rho_{k}}(\phi)\equiv\theta\lor\psi_{k}^{\prime}$,
where $\theta=\bigvee_{i=0}^{l}a_{i}$ and
$\psi_{k}^{\prime}=\bigvee_{i=0}^{m}\mathsf{F}_{\mathsf{P}}^{\infty}\psi_{i}$.
By Lemma 1, $(\rho_{k},k)\not\models\psi_{k}$. Therefore,
$\theta\not\in\mathsf{lbl}(s_{\mathsf{init}})$ any run
$\rho\in\mathsf{Runs_{init}}\not\models\theta$. Moreover,
$(\rho_{k},k)\not\models\psi_{k}^{\prime}$, and since
$\psi^{\prime}_{k}\in\mathsf{L}^{+}(\mathsf{F}_{\mathsf{P}}^{\infty})$ and is
filtered, by Lemma 10 we have that
$(\rho_{k},k)\not\models\mathsf{F}_{\mathsf{P}}^{\infty}\psi_{k}^{\prime}$. By
Lemma 2, there exists $\psi^{\prime}_{k}$-avoiding sequence
$U^{k}=u^{k}_{0},\ldots,u^{k}_{l_{k}}$ for some $l_{k}\geq 0$, and let
$v^{k}_{0},\ldots,v^{k}_{l_{k}+1}$ a realisation witness for
$(U^{k},\mathcal{L})$. We will now build a run $\rho^{*}$ which is a counter
example for every $k$. Denote $w^{k}$ a path from the last element of
$u^{k}_{l_{k}}$ to the first element of $u^{k+1}_{0}$. Such a path must exists
since $\mathcal{L}$ is strongly connected. Now let
$\rho^{*}=v^{N}_{0}u^{N}_{0}v^{N}_{1}\cdots
v^{N}_{l_{N}}u^{N}_{l_{N}}w^{N}u^{N+1}_{0}v^{N+1}_{1}\ldots$ By construction,
$\rho^{*}$ realizes each $U^{k}$. By Lemma 3,
$(\rho^{*},k)\not\models\mathsf{F}_{\mathsf{P}}^{\infty}\psi^{\prime}_{k}$,
and since
$\psi^{\prime}_{k}\in\mathsf{L}^{+}(\mathsf{F}_{\mathsf{P}}^{\infty})$ is
filtered, by Lemma 10, $(\rho^{*},k)\not\models\psi^{\prime}_{k}$. Since
$\rho^{*}\in\mathsf{Runs_{init}}$, $(\rho^{*},k)\not\models\theta$ and
$(\rho^{*},k)\not\models\psi_{k}$ By Lemma 1, $(\rho^{*},k)\not\models\phi$.
The lemma follows.

###### Corollary 1

The strong and weak prompt model checking for
$\mathsf{F}(\mathsf{L}^{+}(\mathsf{F}_{\mathsf{P}}^{\infty}))$ are equivalent.

###### Proof

The strong model checking trivially induces the weak one. To see why the
convers holds, notice that any infinite run ends in some SCC, and since the
fragment enjoys the prefix independence, one only has to study what happens in
each SCC. A straight-forward application of Lemma 14 concludes the proof.

The proof that the probabilistic model checking can be computed in polynomial
time comes from the following _zero-one-law_ for the BSCCs of some LTS
$\mathcal{L}$:

_Let $B$ be a BSCC and $\phi$ a formula in
$\mathsf{L}^{+}(\mathsf{F}_{\mathsf{P}}^{\infty})$, then either almost all the
runs of $B$ satisfy $\phi$ or almost no run of $B$ does._

Now to conclude, one has to notice that the probability of reaching $B$ can be
computed in polynomial time and use the prefix independence of
$\mathsf{F}(\mathsf{L}^{+}(\mathsf{F}_{\mathsf{P}}^{\infty}))$.

###### Lemma 15

Given an LTS $\mathcal{L}$ and a formula
$\phi\in\mathsf{L}^{+}(\mathsf{F}_{\mathsf{P}}^{\infty})$, if $\mathcal{L}$ is
strongly connected, then either:

  * •

there exists $k\geq 0$ such that
$\mathbb{P}_{\mathcal{L}}(\\{\rho\in\mathsf{Runs_{init}}(\mathcal{L})\mid(\rho,k)\models\phi\\})=1$
or,

  * •

for all $k\geq 0,\leavevmode\nobreak\
\mathbb{P}_{\mathcal{L}}(\\{(\rho,k)\in\mathsf{Runs_{init}}(\mathcal{L})\mid(\rho,k)\models\phi\\})=0$.

###### Proof

Assume that for some $k\geq 0$,

$\displaystyle\mathbb{P}_{\mathcal{L}}(\\{\rho\in\mathsf{Runs_{init}}(\mathcal{L})\mid(\rho,k)\models\phi\\})=\lambda$
(1)

with $\lambda\in(0,1]$, and show that necessarily

$\mathbb{P}_{\mathcal{L}}(\\{\rho\in\mathsf{Runs_{init}}(\mathcal{L})\mid(\rho,k)\models\phi\\})=1$

If $\lambda=1$, then the result trivially follows, if not then

$\displaystyle\mathbb{P}_{\mathcal{L}}(\\{\rho\in\mathsf{Runs_{init}}(\mathcal{L})\mid(\rho,k)\models\phi\\})=\lambda$
$\displaystyle\implies\mathbb{P}_{\mathcal{L}}(\\{\rho\in\mathsf{Runs_{init}}(\mathcal{L})\mid(\rho,k)\not\models\phi\\})=1-\lambda>0$
$\displaystyle\implies\exists\rho\in\mathsf{Runs_{init}}(\mathcal{L}),\leavevmode\nobreak\
(\rho,k)\not\models\phi$ $\displaystyle\implies\exists w\text{ a prefix of
}\rho,\leavevmode\nobreak\ \forall\leavevmode\nobreak\
\rho^{\prime}\in\mathsf{Cyl}(w),\leavevmode\nobreak\
(\rho^{\prime},k)\not\models\phi$
$\displaystyle\implies\mathbb{P}_{\mathcal{L}}(\\{\rho\in\mathsf{Runs_{init}}(\mathcal{L})\mid(\rho,k)\not\models\phi\\})=1$

The third implication is by Lemma 6, and the last implication is a consequence
of the Borel Cantelli Lemma which yields that $\mathsf{Cyl}(w)$ is almost
sure, but this contradicts Equation (1).

###### Corollary 2

Given an LTS $\mathcal{L}$ and a formula
$\phi\in\mathsf{L}^{+}(\mathsf{F}_{\mathsf{P}}^{\infty})$,
$\mathbb{P}_{\mathcal{L}}(\\{\rho\in\mathsf{Runs_{init}}(\mathcal{L})\mid(\rho,k)\models\phi\\})$
can be computed in polynomial time.

###### Proof

By Lemma 15 and prefix independence of the fragment, the probability of
satisfying some formula is the same as the probability of reaching the BSCCs
where this formula is satisfied. By Lemma 9 one can compute the set of BSCCs
that are good for the formula in polynomial time. To conclude, recall that
computing the probability of reaching a BSCC can be done in polynomial time
using standard procedure from finite Markov chain literature.