characterized by $\mathcal{B}$, for some monotonic $\mathcal{B}$, and let us
define the following processes, for $k>0$:
$p_{k}=\sum_{i=1}^{k}a^{i}b\mathtt{0}$.

Since $I(p_{k})=I(p_{k+1})$ and $p_{k}$ is a subtree of $p_{k+1}$, it is clear
that $p_{k+1}\lesssim_{\mathsf{C}}p_{k}$ holds, for all $k$ (see the picture
below to verify the claim for $k=1$, i.e., $p_{2}\lesssim_{\mathsf{C}}p_{1}$).

${p_{2}}$${p_{1}}$${\cdot}$${\cdot}$${\lesssim_{\mathsf{C}}}$${\cdot}$${\cdot}$${\cdot}$${\cdot}$${\cdot}$aababab

On the other hand, $p_{k}\not\lesssim_{\mathsf{C}}p_{k+1}$, because the branch
$a^{k+1}b\mathtt{0}$ cannot be matched by any branch in $p_{k}$, where the
longest sequence of consecutive $a$’s is $a^{k}$. Thus, we have a non-well-
founded sequence of strictly decreasing processes
$\ldots\lnsim_{\mathsf{C}}p_{k+1}\lnsim_{\mathsf{C}}p_{k}\ldots\lnsim_{\mathsf{C}}p_{1}$.

For all $k$, $p_{k+1}\lnsim_{\mathsf{C}}p_{k}$ implies
$\mathcal{L}_{\mathsf{C}}(p_{k+1})\subset\mathcal{L}_{\mathsf{C}}(p_{k})$,
which, by monotonicity of $\mathcal{B}$ (Definition 5), in turn implies
$\mathcal{B}(p_{k+1})\subset\mathcal{B}(p_{k})$. Thus, there exist infinitely
many formulae $\psi_{1},\psi_{2},\ldots,\psi_{k},\ldots$ such that
$\psi_{k}\in\mathcal{B}(p_{k})\setminus\mathcal{B}(p_{k+1})$ for all $k$. We
show that the formulae $\\{\psi_{k}\\}_{k\geq 1}$ are pairwise different, that
is, $\psi_{k}\neq\psi_{j}$ for each $k\neq j$. To this end, let us suppose,
towards a contradiction, that there exist $j,k$ such that $j<k$ and
$\psi_{k}=\psi_{j}$. By construction, we have that
$\psi_{j}\in\mathcal{B}(p_{j})\setminus\mathcal{B}(p_{j+1})$ and
$\psi_{k}=\psi_{j}\in\mathcal{B}(p_{k})\setminus\mathcal{B}(p_{k+1})$. Since
$j+1\leq k$, we have that $\mathcal{B}(p_{k})\subseteq\mathcal{B}(p_{j+1})$,
which means that $\psi_{k}=\psi_{j}\in\mathcal{B}(p_{j+1})$, leading to a
contradiction.

Therefore the sequence $\\{\psi_{k}\\}_{k\geq 1}$ includes infinitely many
different formulae. Since $\mathcal{B}(p_{1})$ contains them all, the
hypothesis of finiteness of $\mathcal{B}(p_{1})$ is contradicted, and the
thesis follows. ∎

#### Acknowledgements

We thank the anonymous referees for their comments, which led to improvements
in the paper.

## References

## References

  * [1] L. Aceto, D. Della Monica, I. Fábregas, A. Ingólfsdóttir, When are prime formulae characteristic?, in: G. F. Italiano, G. Pighizzini, D. Sannella (Eds.), Proc. of the 40th International Symposium on Mathematical Foundations of Computer Science (MFCS)—Part I, Vol. 9234 of LNCS, Springer-Verlag Berlin Heidelberg, 2015, pp. 76–88.  doi:10.1007/978-3-662-48057-1_6.
  * [2] L. Aceto, A. Ingólfsdóttir, K. G. Larsen, J. Srba, Reactive Systems: Modelling, Specification and Verification, Cambridge University Press, 2007.
  * [3] C. Baier, J. Katoen, Principles of model checking, MIT Press, 2008.
  * [4] E. M. Clarke, O. Grumberg, D. A. Peled, Model Checking, MIT Press, 1999.
  * [5] R. M. Keller, Formal verification of parallel programs, Commun. ACM 19 (7) (1976) 371–384.
  * [6] D. de Frutos-Escrig, C. Gregorio-Rodríguez, M. Palomino, D. Romero-Hernández, Unifying the linear time-branching time spectrum of process semantics, Logical Methods in Computer Science 9 (2) (2013) 1–74.
  * [7] R. J. van Glabbeek, The linear time-branching time spectrum I: The semantics of concrete, sequential processes, in: Handbook of Process Algebra, Elsevier, 2001, pp. 3–99.
  * [8] M. Hennessy, R. Milner, Algebraic laws for nondeterminism and concurrency, J. ACM 32 (1) (1985) 137–161.
  * [9] R. Milner, Communication and Concurrency, Prentice Hall, 1989.
  * [10] D. Park, Concurrency and automata on infinite sequences, in: P. Deussen (Ed.), Theoretical Computer Science, 5th GI-Conference, Karlsruhe, Germany, March 23-25, 1981, Proceedings, Vol. 104 of Lecture Notes in Computer Science, Springer, 1981, pp. 167–183.  doi:10.1007/BFb0017309.
  * [11] L. Aceto, M. Hennessy, Termination, deadlock, and divergence, Journal of the ACM 39 (1) (1992) 147–187.
  * [12] B. Bloom, W. Fokkink, R. J. van Glabbeek, Precongruence formats for decorated trace semantics, ACM Transactions on Computational Logic 5 (1) (2004) 26–78.
  * [13] S. Graf, J. Sifakis, A modal characterization of observational congruence on finite terms of CCS, Information and Control 68 (1-3) (1986) 125–145.
  * [14] B. Steffen, A. Ingólfsdóttir, Characteristic formulae for processes with divergence, Information and Computation 110 (1) (1994) 149–163.
  * [15] L. Aceto, A. Achilleos, A. Francalanza, A. Ingólfsdóttir, The complexity of identifying characteristic formulas for $\mu$HML, in: Proc. of the 11th Panhellenic Logic Symposium (PLS), 2017, pp. 216–222.
  * [16] A. Achilleos, The completeness problem for modal logic, in: S. Artemov, A. Nerode (Eds.), Logical Foundations of Computer Science, Springer International Publishing, 2018, pp. 1–21.
  * [17] R. Cleaveland, B. Steffen, Computing behavioural relations, logically, in: J. L. Albert, B. Monien, M. Rodríguez-Artalejo (Eds.), Proceedings of the 18th International Colloquium on Automata, Languages and Programming (ICALP), Vol. 510 of Lecture Notes in Computer Science, Springer, 1991, pp. 127–138.  doi:10.1007/3-540-54233-7_129.
URL https://doi.org/10.1007/3-540-54233-7

  * [18] G. Boudol, K. G. Larsen, Graphical versus logical specifications, Theoretical Computer Science 106 (1) (1992) 3–20.  doi:10.1016/0304-3975(92)90276-L.
  * [19] L. Aceto, I. Fábregas, D. de Frutos Escrig, A. Ingólfsdóttir, M. Palomino, Graphical representation of covariant-contravariant modal formulas, in: Proc. of the 18th EXPRESS, Vol. 64 of EPTCS, 2011, pp. 1–15.
  * [20] I. Fábregas, D. de Frutos-Escrig, M. Palomino, Logics for contravariant simulations, in: Proc. of FMOODS-FORTE, Vol. 6117 of LNCS, 2010, pp. 224–231.

##  Appendix A Proofs for semantics in van Glabbeek’s branching time spectrum

###  A.1 Finite characterization

We prove here that logics in van Glabbeek’s branching-time spectrum are
finitely characterized by some monotonic $\mathcal{B}$ (condition (i) in
Corollary 4).

######  Lemma 1.

Let $X\in\mathsf{Btime\text{-}spectrum}$. $\mathcal{L}_{X}$ is finitely
characterized by $\mathcal{B}_{X}$, for some monotonic $\mathcal{B}_{X}$ (see
Table 1).

###### Proof.

We consider each semantics $X\in\mathsf{Btime\text{-}spectrum}$ and we show
that $\mathcal{B}_{X}$ (as defined in Table 1) is such that for each $p\in P$:

  1. (_i_)

$\emptyset\subset\mathcal{B}_{X}(p)\subseteq\mathcal{L}_{X}(p)$,

  2. (_ii_)

for each $\phi\in\mathcal{L}_{X}(p)$, it holds
$\bigcap_{\psi\in\mathcal{B}_{X}(p)}\llbracket\psi\rrbracket\subseteq\llbracket\phi\rrbracket$,

  3. (_iii_)

$\mathcal{B}_{X}(p)$ is finite, and

  4. (_iv_)

for each $q\in P$, if $\mathcal{L}_{X}(p)\subseteq\mathcal{L}_{X}(q)$ then
$\mathcal{B}_{X}(p)\subseteq\mathcal{B}_{X}(q)$.

Before considering each semantics separately, we notice that, for every
$X\in\mathsf{Btime\text{-}spectrum}$, we have that
$\mathbf{tt}\in\mathcal{B}_{X}(p)$, and thus
$\emptyset\subset\mathcal{B}_{X}(p)$. Consequently, we can focus on showing
that $\mathcal{B}_{X}(p)\subseteq\mathcal{L}_{X}(p)$ holds when proving
property (_i_).

In addition, we find it convenient to partially factorize the proofs of
properties (_i_) and (_iii_). To this end, we show that, for every
$X\in\mathsf{Btime\text{-}spectrum}$,

if $\mathcal{B}_{X}^{-}(p)\subseteq\mathcal{L}_{X}(p)$ for all $p\in P$, then
$\mathcal{B}_{X}(p)\subseteq\mathcal{L}_{X}(p)$ for all $p\in P$, and (_i_ ′)
if $\mathcal{B}_{X}^{-}(p)$ is finite for all $p\in P$, then
$\mathcal{B}_{X}(p)$ is finite for all $p\in P$. (_iii_ ′)

Let $X\in\mathsf{Btime\text{-}spectrum}$.

First, let us assume that $\mathcal{B}_{X}^{-}(p)\subseteq\mathcal{L}_{X}(p)$
holds for all $p\in P$; we show that
$\mathcal{B}_{X}(p)\subseteq\mathcal{L}_{X}(p)$ holds for all $p\in P$ as
well, by induction on the depth of $p$. When $I(p)=\emptyset$ (base case), we
have $\mathcal{B}_{X}^{+}(p)=\\{\mathbf{tt}\\}\subseteq\mathcal{L}_{X}(p)$,
and therefore $\mathcal{B}_{X}(p)\subseteq\mathcal{L}_{X}(p)$ holds as well.
To deal with the inductive step ($I(p)\neq\emptyset$), let
$\phi\in\mathcal{B}_{X}^{+}(p)$. If $\phi=\mathbf{tt}$, then
$\phi\in\mathcal{L}_{X}(p)$, and we are done. Assume $\phi=\langle
a\rangle\bigwedge_{\psi\in\Psi}\psi$, where $a\in Act$ and
$\Psi\subseteq\mathcal{B}_{X}(p^{\prime})$ for some $p^{\prime}$ such that
$p\stackrel{{\scriptstyle a}}{{\rightarrow}}p^{\prime}$. By the inductive
hypothesis, we have that
$\mathcal{B}_{X}(p^{\prime})\subseteq\mathcal{L}_{X}(p^{\prime})$, meaning
that $p^{\prime}\in\llbracket\psi\rrbracket$ for all $\psi\in\Psi$. Since
$p\stackrel{{\scriptstyle a}}{{\rightarrow}}p^{\prime}$, we have that
$p\in\llbracket\langle a\rangle\bigwedge_{\psi\in\Psi}\psi\rrbracket$, which
amounts to $\phi\in\mathcal{L}_{X}(p)$.

Now, let us assume $\mathcal{B}_{X}^{-}(p)$ to be finite for every $p\in P$;
we show that also $\mathcal{B}_{X}(p)$ is finite for every $p\in P$, by
induction on the depth of $p$. When $I(p)=\emptyset$ (base case),
$\mathcal{B}_{X}(p)=\\{\mathbf{tt}\\}\cup\mathcal{B}_{X}^{-}(p)$, which is
clearly finite. Let us deal now with the inductive step ($I(p)\neq\emptyset$).
By the construction of $\mathcal{B}_{X}^{+}(p)$, a formula belongs to
$\mathcal{B}_{X}^{+}(p)$ if, and only if, it is either $\mathbf{tt}$ or
$\langle a\rangle\varphi$, where $a\in Act$ and
$\varphi=\bigwedge_{\psi\in\Psi}\psi$, for some
$\Psi\subseteq\mathcal{B}_{X}(p^{\prime})$ and some $p^{\prime}$ such that
$p\stackrel{{\scriptstyle a}}{{\rightarrow}}p^{\prime}$. By the inductive
hypothesis, $\mathcal{B}_{X}(p^{\prime})$ is finite. Since $Act$ is also
finite and processes are finitely branching, there are only finitely many such
formulae $\langle a\rangle\varphi$, meaning that $\mathcal{B}_{X}^{+}(p)$ is
finite. Therefore
$\mathcal{B}_{X}(p)=\mathcal{B}_{X}^{+}(p)\cup\mathcal{B}_{X}^{-}$ is finite
as well.

As a consequence of (_i_ ′), showing that
$\mathcal{B}_{X}^{-}(p)\subseteq\mathcal{L}_{X}(p)$ holds for all $p\in P$ is
enough to prove property (_i_); similarly, thanks to (_iii_ ′), showing
finiteness of $\mathcal{B}^{-}(p)$ for all $p\in P$ is enough to prove
property (_iii_). We will use (_i_ ′) and (_iii_ ′) to prove, respectively,
properties (_i_) and (_iii_) for all semantics.

To keep the notation light, we often omit the subscripts identifying the
semantics as it is clear from the context, e.g., when working out the case of
simulation semantics, we write $\mathcal{L}$, $\mathcal{B}$, and $p\lesssim q$
instead of $\mathcal{L}_{\mathsf{S}}$, $\mathcal{B}_{\mathsf{S}}$, and
$p\lesssim_{\mathsf{S}}q$, respectively, and similarly for the other
semantics.

Case simulation ($\mathsf{S}$). For the sake of clarity we recall from Table 1
that $\mathcal{B}$ is defined as

$\mathcal{B}(p)=\\{\mathbf{tt}\\}\cup\\{\langle a\rangle\varphi\mid a\in
Act,\varphi=\bigwedge_{\psi\in\Psi}\psi,\Psi\subseteq\mathcal{B}(p^{\prime}),p\stackrel{{\scriptstyle
a}}{{\rightarrow}}p^{\prime}\\}$.

Since $\mathcal{B}^{-}(p)=\emptyset$ for all $p\in P$, properties (_i_) and
(_iii_) immediately follow from (_i_ ′) and (_iii_ ′), respectively. Notice
also that property (_iii_) implies that $\mathcal{B}$ is well defined.

In order to prove property (_ii_), we let $\phi\in\mathcal{L}(p)$, for a
generic $p\in P$, and we proceed by induction on the structure of $\phi$
(notice that we can ignore the case $\phi=\mathbf{ff}$, as
$\phi\in\mathcal{L}(p)$ implies $\phi\neq\mathbf{ff}$).

  * •

$\phi=\mathbf{tt}$: the claim follows trivially.

  * •

$\phi=\varphi_{1}\vee\varphi_{2}$: it holds that
$\varphi_{i}\in\mathcal{L}(p)$ for some $i\in\\{1,2\\}$. By the inductive
hypothesis, we have that
$\bigcap_{\psi\in\mathcal{B}(p)}\llbracket\psi\rrbracket\subseteq\llbracket\varphi_{i}\rrbracket$
and, since $\llbracket\varphi_{i}\rrbracket\subseteq\llbracket\phi\rrbracket$,
we obtain the claim.

  * •

$\phi=\varphi_{1}\wedge\varphi_{2}$: it holds that
$\varphi_{i}\in\mathcal{L}(p)$ for all $i\in\\{1,2\\}$. By the inductive
hypothesis, we have that
$\bigcap_{\psi\in\mathcal{B}(p)}\llbracket\psi\rrbracket\subseteq\llbracket\varphi_{i}\rrbracket$
for all $i\in\\{1,2\\}$. This implies that
$\bigcap_{\psi\in\mathcal{B}(p)}\llbracket\psi\rrbracket\subseteq\llbracket\varphi_{1}\rrbracket\cap\llbracket\varphi_{2}\rrbracket=\llbracket\phi\rrbracket$.

  * •

$\phi=\langle a\rangle\varphi$: by definition we have that
$\varphi\in\mathcal{L}(p^{\prime})$ for some $p\stackrel{{\scriptstyle
a}}{{\rightarrow}}p^{\prime}$. By the inductive hypothesis, we have that
$\bigcap_{\psi\in\mathcal{B}(p^{\prime})}\llbracket\psi\rrbracket\subseteq\llbracket\varphi\rrbracket$.
We define $\zeta=\langle
a\rangle\bigwedge_{\psi\in\mathcal{B}(p^{\prime})}\psi$. Clearly, $\zeta$
belongs to $\mathcal{B}^{+}(p)$ (by construction—notice that $\zeta$ is well
defined due to the finiteness of $\mathcal{B}(p^{\prime})$) and
$\llbracket\zeta\rrbracket\subseteq\llbracket\phi\rrbracket$ (because
$\bigcap_{\psi\in\mathcal{B}(p^{\prime})}\llbracket\psi\rrbracket\subseteq\llbracket\varphi\rrbracket$).
Hence,
$\bigcap_{\psi\in\mathcal{B}(p)}\llbracket\psi\rrbracket\subseteq\llbracket\zeta\rrbracket\subseteq\llbracket\phi\rrbracket$
holds.

Finally, we show that $\mathcal{B}$ is monotonic (property (_iv_)). Consider
$p,q\in P$, with $\mathcal{L}(p)\subseteq\mathcal{L}(q)$. We want to show that
$\phi\in\mathcal{B}(p)$ implies $\phi\in\mathcal{B}(q)$, for each $\phi$.
Firstly, we observe that, by $\mathcal{L}(p)\subseteq\mathcal{L}(q)$ and
Theorem 4, $p\lesssim q$ holds. Thus, for each $a\in Act$ and $p^{\prime}\in
P$ with $p\stackrel{{\scriptstyle a}}{{\rightarrow}}p^{\prime}$, there exists
some $q^{\prime}\in P$ such that $q\stackrel{{\scriptstyle
a}}{{\rightarrow}}q^{\prime}$ and $p^{\prime}\lesssim q^{\prime}$. We also
observe that $\mathcal{B}^{-}(p)=\mathcal{B}^{-}(q)=\emptyset$. In order to
show that $\mathcal{B}(p)\subseteq\mathcal{B}(q)$, we proceed by induction on
the depth of $p$. If $I(p)=\emptyset$, then
$\mathcal{B}^{+}(p)=\\{\mathbf{tt}\\}\subseteq\mathcal{B}^{+}(q)$, and the
thesis follows. Otherwise ($I(p)\neq\emptyset$), let us consider a formula
$\phi\in\mathcal{B}(p)$. If $\phi\in\mathcal{B}^{-}(p)$, then the claim
follows from $\mathcal{B}^{-}(p)=\mathcal{B}^{-}(q)\subseteq\mathcal{B}(q)$.
If $\phi=\mathbf{tt}$, then, by definition of $\mathcal{B}^{+}$, we have
$\phi\in\mathcal{B}^{+}(q)\subseteq\mathcal{B}(q)$. Finally, if $\phi=\langle
a\rangle\varphi\in\mathcal{B}^{+}(p)$, then, by definition of
$\mathcal{B}^{+}$, there exist $p^{\prime}\in P$, with
$p\stackrel{{\scriptstyle a}}{{\rightarrow}}p^{\prime}$, such that
$\varphi=\bigwedge_{\psi\in\Psi}\psi$ for some
$\Psi\subseteq\mathcal{B}(p^{\prime})$. This implies the existence of some
$q^{\prime}\in P$ such that $q\stackrel{{\scriptstyle
a}}{{\rightarrow}}q^{\prime}$ and $p^{\prime}\lesssim q^{\prime}$ (and
therefore $\mathcal{L}(p^{\prime})\subseteq\mathcal{L}(q^{\prime})$ by Theorem
4). By the inductive hypothesis,
$\mathcal{B}(p^{\prime})\subseteq\mathcal{B}(q^{\prime})$ holds as well, which
means that $\Psi\subseteq\mathcal{B}(q^{\prime})$. Hence, we have that
$\langle a\rangle\varphi\in\mathcal{B}^{+}(q)\subseteq\mathcal{B}(q)$.

Case complete simulation ($\mathsf{CS}$). For the sake of clarity we recall
from Table 1 that $\mathcal{B}$ is defined as
$\mathcal{B}(p)=\mathcal{B}^{+}(p)\cup\mathcal{B}^{-}(p)$, where

  * •

$\mathcal{B}^{+}(p)=\\{\mathbf{tt}\\}\cup\\{\langle a\rangle\varphi\mid a\in
Act,\varphi=\bigwedge_{\psi\in\Psi}\psi,\Psi\subseteq\mathcal{B}(p^{\prime}),p\stackrel{{\scriptstyle
a}}{{\rightarrow}}p^{\prime}\\}$, and

  * •

$\mathcal{B}^{-}(p)=\\{\mathbf{0}\mid p\stackrel{{\scriptstyle
a}}{{\not\rightarrow}},\forall a\in Act\\}$.

For all $p\in P$, if $I(p)=\emptyset$, then
$\mathcal{B}^{-}(p)=\\{\mathbf{0}\\}$ and $\mathbf{0}\in\mathcal{L}(p)$,
otherwise $\mathcal{B}^{-}(p)=\emptyset$; thus, $\mathcal{B}^{-}(p)$ is finite
and $\mathcal{B}^{-}(p)\subseteq\mathcal{L}(p)$. Hence, properties (_i_) and
(_iii_) immediately follow from (_i_ ′) and (_iii_ ′), respectively. Notice
also that property (_iii_) implies that $\mathcal{B}$ is well defined.

In order to prove property (_ii_), we let $\phi\in\mathcal{L}(p)$, for a
generic $p\in P$, and we proceed by induction on the structure of $\phi$.
Apart from a new base case ($\phi=\mathbf{0}$, which we deal with below), the
proof is the same as in the case of simulation semantics above.

  * •

$\phi=\mathbf{0}$: it is enough to observe that $\phi\in\mathcal{B}(p)$, which
implies
$\bigcap_{\psi\in\mathcal{B}(p)}\llbracket\psi\rrbracket\subseteq\llbracket\phi\rrbracket$.

Finally, we show that $\mathcal{B}$ is monotonic (property (_iv_)). Consider
$p,q\in P$, with $\mathcal{L}(p)\subseteq\mathcal{L}(q)$. We want to show that
$\phi\in\mathcal{B}(p)$ implies $\phi\in\mathcal{B}(q)$, for each $\phi$.
Firstly, we observe that, by $\mathcal{L}(p)\subseteq\mathcal{L}(q)$ and
Theorem 4, $p\lesssim q$ holds. Thus, $I(p)=\emptyset$ if and only if
$I(q)=\emptyset$, which implies $\mathcal{B}^{-}(p)=\mathcal{B}^{-}(q)$;
moreover, we have that for each $a\in Act$ and $p^{\prime}\in P$ with
$p\stackrel{{\scriptstyle a}}{{\rightarrow}}p^{\prime}$, there exists some
$q^{\prime}\in P$ such that $q\stackrel{{\scriptstyle
a}}{{\rightarrow}}q^{\prime}$ and $p^{\prime}\lesssim q^{\prime}$. In order to
show that $\mathcal{B}(p)\subseteq\mathcal{B}(q)$, we proceed by induction on
the depth of $p$. If $I(p)=\emptyset$, then $I(q)=\emptyset$ as well. Thus, we
have that $\mathcal{B}^{+}(p)=\mathcal{B}^{+}(q)=\\{\mathbf{tt}\\}$, and the
thesis follows. Otherwise ($I(p)\neq\emptyset$), let us consider a formula
$\phi\in\mathcal{B}(p)$. If $\phi\in\mathcal{B}^{-}(p)$, then the claim
follows from $\mathcal{B}^{-}(p)=\mathcal{B}^{-}(q)\subseteq\mathcal{B}(q)$.
If $\phi=\mathbf{tt}$, then, by definition of $\mathcal{B}^{+}$, we have
$\phi\in\mathcal{B}^{+}(q)\subseteq\mathcal{B}(q)$. Finally, if $\phi=\langle
a\rangle\varphi\in\mathcal{B}^{+}(p)$, then, by definition of
$\mathcal{B}^{+}$, there exist $p^{\prime}\in P$, with
$p\stackrel{{\scriptstyle a}}{{\rightarrow}}p^{\prime}$, such that
$\varphi=\bigwedge_{\psi\in\Psi}\psi$ for some
$\Psi\subseteq\mathcal{B}(p^{\prime})$. This implies the existence of some
$q^{\prime}\in P$ such that $q\stackrel{{\scriptstyle
a}}{{\rightarrow}}q^{\prime}$ and $p^{\prime}\lesssim q^{\prime}$ (and
therefore $\mathcal{L}(p^{\prime})\subseteq\mathcal{L}(q^{\prime})$ by Theorem
4). By the inductive hypothesis,
$\mathcal{B}(p^{\prime})\subseteq\mathcal{B}(q^{\prime})$ holds as well, which
means that $\Psi\subseteq\mathcal{B}(q^{\prime})$. Hence, we have that
$\langle a\rangle\varphi\in\mathcal{B}^{+}(q)\subseteq\mathcal{B}(q)$.

Case ready simulation ($\mathsf{RS}$). See the proof of Lemma 1 at page 1.

Case trace simulation ($\mathsf{TS}$). For the sake of clarity we recall from
Table 1 that $\mathcal{B}$ is defined as
$\mathcal{B}(p)=\mathcal{B}^{+}(p)\cup\mathcal{B}^{-}(p)$, where

  * •

$\mathcal{B}^{+}(p)=\\{\mathbf{tt}\\}\cup\\{\langle a\rangle\varphi\mid a\in
Act,\varphi=\bigwedge_{\psi\in\Psi}\psi,\Psi\subseteq\mathcal{B}(p^{\prime}),p\stackrel{{\scriptstyle
a}}{{\rightarrow}}p^{\prime}\\}$, and

  * •

$\mathcal{B}^{-}(p)=\\{[\tau a]\mathbf{ff}\mid\tau\in\mathit{traces}(p),a\in
Act,\tau a\notin\mathit{traces}(p)\\}$.

It is easy to see that, for all $p$,  $(a)$ $\mathcal{B}^{-}(p)$is finite,
because $Act$ is finite and so is $\mathit{traces}(p)$, and  $(b)$
$\mathcal{B}^{-}(p)\subseteq\mathcal{L}(p)$trivially holds, by definition of
$\mathcal{B}^{-}(p)$.  Hence, properties (_i_) and (_iii_) immediately follow
from (_i_ ′) and (_iii_ ′), respectively. Notice also that property (_iii_)
implies that $\mathcal{B}$ is well defined.

In order to prove property (_ii_), we let $\phi\in\mathcal{L}(p)$, for a
generic $p\in P$, and we proceed by induction on the structure of $\phi$.
Inductive steps work as in previous cases; the following additional base case,
with respect to previous cases, must be considered.

  * •

$\phi=[\tau a]\mathbf{ff}$: if $\phi\in\mathcal{B}^{-}(p)$, the property holds
trivially. Otherwise, $\phi\notin\mathcal{B}^{-}(p)$ implies
$\tau\notin\mathit{traces}(p)$ (notice that $\tau a\notin\mathit{traces}(p)$:
indeed, if $\tau a\in\mathit{traces}(p)$ then $\phi\notin\mathcal{L}(p)$, thus
raising a contradiction). There must be two prefixes
$\tau^{\prime}=a_{1}\ldots a_{k}$ and $\tau^{\prime\prime}=a_{1}\ldots
a_{k}a_{k+1}$ of $\tau$ (i.e., $\tau^{\prime}$ is the largest proper prefix of
$\tau^{\prime\prime}$—possibly $\tau^{\prime}=\varepsilon$ and/or
$\tau^{\prime\prime}=\tau$) such that
$p\stackrel{{\scriptstyle\tau^{\prime}}}{{\longrightarrow}}$ and
$p\stackrel{{\scriptstyle\tau^{\prime\prime}}}{{\not\rightarrow}}$. The
formula $\psi=[\tau^{\prime\prime}]\mathbf{ff}$ is such that
$\psi\in\mathcal{B}^{-}(p)$ and
$\llbracket\psi\rrbracket\subseteq\llbracket\phi\rrbracket$. The thesis
follows immediately.

Finally, we show that $\mathcal{B}$ is monotonic (property (_iv_)). Consider
$p,q\in P$, with $\mathcal{L}(p)\subseteq\mathcal{L}(q)$. We want to show that
$\phi\in\mathcal{B}(p)$ implies $\phi\in\mathcal{B}(q)$, for each $\phi$.
Firstly, we observe that, by $\mathcal{L}(p)\subseteq\mathcal{L}(q)$ and
Theorem 4, $p\lesssim q$ holds. Thus, we have that
$\mathit{traces}(p)=\mathit{traces}(q)$, which implies
$\mathcal{B}^{-}(p)=\mathcal{B}^{-}(q)$; moreover, we have that for each $a\in
Act$ and $p^{\prime}\in P$ with $p\stackrel{{\scriptstyle
a}}{{\rightarrow}}p^{\prime}$, there exists some $q^{\prime}\in P$ such that
$q\stackrel{{\scriptstyle a}}{{\rightarrow}}q^{\prime}$ and
$p^{\prime}\lesssim q^{\prime}$. In order to show that
$\mathcal{B}(p)\subseteq\mathcal{B}(q)$, we proceed by induction on the depth
of $p$. If $I(p)=\emptyset$, then $I(q)=\emptyset$ as well. Thus, we have that
$\mathcal{B}^{+}(p)=\mathcal{B}^{+}(q)=\\{\mathbf{tt}\\}$, and the thesis
follows. Otherwise ($I(p)\neq\emptyset$), let us consider a formula
$\phi\in\mathcal{B}(p)$. If $\phi\in\mathcal{B}^{-}(p)$, then the claim
follows from $\mathcal{B}^{-}(p)=\mathcal{B}^{-}(q)\subseteq\mathcal{B}(q)$.
If $\phi=\mathbf{tt}$, then, by definition of $\mathcal{B}^{+}$, we have
$\phi\in\mathcal{B}^{+}(q)\subseteq\mathcal{B}(q)$. Finally, if $\phi=\langle
a\rangle\varphi\in\mathcal{B}^{+}(p)$, then, by definition of
$\mathcal{B}^{+}$, there exist $p^{\prime}\in P$, with
$p\stackrel{{\scriptstyle a}}{{\rightarrow}}p^{\prime}$, such that
$\varphi=\bigwedge_{\psi\in\Psi}\psi$ for some
$\Psi\subseteq\mathcal{B}(p^{\prime})$. This implies the existence of some
$q^{\prime}\in P$ such that $q\stackrel{{\scriptstyle
a}}{{\rightarrow}}q^{\prime}$ and $p^{\prime}\lesssim q^{\prime}$ (and
therefore $\mathcal{L}(p^{\prime})\subseteq\mathcal{L}(q^{\prime})$ by Theorem
4). By the inductive hypothesis,
$\mathcal{B}(p^{\prime})\subseteq\mathcal{B}(q^{\prime})$ holds as well, which
means that $\Psi\subseteq\mathcal{B}(q^{\prime})$. Hence, we have that
$\langle a\rangle\varphi\in\mathcal{B}^{+}(q)\subseteq\mathcal{B}(q)$.

Case 2-nested simulation ($\mathsf{2S}$). For the sake of clarity we recall
from Table 1 that $\mathcal{B}$ is defined as
$\mathcal{B}(p)=\mathcal{B}^{+}(p)\cup\mathcal{B}^{-}(p)$, where

  * •

$\mathcal{B}^{+}(p)=\\{\mathbf{tt}\\}\cup\\{\langle a\rangle\varphi\mid a\in
Act,\varphi=\bigwedge_{\psi\in\Psi}\psi,\Psi\subseteq\mathcal{B}(p^{\prime}),p\stackrel{{\scriptstyle
a}}{{\rightarrow}}p^{\prime}\\}$, and

  * •

$\mathcal{B}^{-}(p)=\\{[a]\varphi\in\mathcal{L}(p)\mid a\in
Act,\varphi=\bigvee_{p^{\prime}\in\textit{max-
succ}(p,a)}\bigwedge_{\psi\in\mathcal{B}^{-}(p^{\prime})}\psi\\}$,

where $\textit{max-succ}(p,a)=\\{p^{\prime}\in P\mid p\stackrel{{\scriptstyle
a}}{{\rightarrow}}p^{\prime}\text{ and }\nexists
p^{\prime\prime}.p\stackrel{{\scriptstyle
a}}{{\rightarrow}}p^{\prime\prime}\text{ and
}p^{\prime}<_{\mathsf{S}}p^{\prime\prime}\\}$.

By definition, $\mathcal{B}^{-}(p)\subseteq\mathcal{L}(p)$ for every $p\in P$;
moreover, it is easy to verify that $\mathcal{B}^{-}(p)$ is finite, by
induction on the depth on $p$ and by recalling that $Act$ is finite and
processes are finitely branching. Hence, properties (_i_) and (_iii_)
immediately follow from (_i_ ′) and (_iii_ ′), respectively. Notice also that
property (_iii_) implies that $\mathcal{B}$ is well defined.

In order to prove property (_ii_), we let $\phi\in\mathcal{L}(p)$, for a
generic $p\in P$, and we proceed, as usual, by induction on the structure of
$\phi$. With respect to the previous semantics, we have to consider new
formulae of the form $\neg\varphi$. They are treated as an additional base
case, which, in turn, is handled by means of (inner) induction on the
structure of $\varphi$.

  * •

$\phi=\mathbf{tt}$ (base case): the claim follows trivially.

  * •

$\phi=\neg\varphi$ (base case): according to the definition of the syntax of
$\mathcal{L}_{\mathsf{2S}}$, $\varphi$ must belong to
$\mathcal{L}_{\mathsf{S}}$. We show that
$\bigcap_{\psi\in\mathcal{B}_{\mathsf{2S}}(p)}\llbracket\psi\rrbracket\subseteq\llbracket\neg\varphi\rrbracket$
holds for all $\varphi\in\mathcal{L}_{\mathsf{S}}$. We proceed by (inner)
induction on the structure of $\varphi$ (notice that we can ignore the case
$\varphi=\mathbf{tt}$, as $\phi\in\mathcal{L}(p)$ implies
$\varphi\neq\mathbf{tt}$).

    * –

$\varphi=\mathbf{ff}$: the claim follows trivially.

    * –

$\varphi=\varphi_{1}\wedge\varphi_{2}$: then, $\neg\varphi$ is logically
equivalent to $\neg\varphi_{1}\vee\neg\varphi_{2}$. Thus,
$\phi\in\mathcal{L}(p)$ implies $\neg\varphi_{i}\in\mathcal{L}(p)$ for some
$i\in\\{1,2\\}$. By inductive hypothesis,
$\bigcap_{\psi\in\mathcal{B}(p)}\llbracket\psi\rrbracket\subseteq\llbracket\neg\varphi_{i}\rrbracket$
and, since
$\llbracket\neg\varphi_{i}\rrbracket\subseteq\llbracket\neg\varphi\rrbracket$,
the thesis follows.

    * –

$\varphi=\varphi_{1}\vee\varphi_{2}$: then, $\neg\varphi$ is logically
equivalent to $\neg\varphi_{1}\wedge\neg\varphi_{2}$. Thus,
$\phi\in\mathcal{L}(p)$ implies $\neg\varphi_{i}\in\mathcal{L}(p)$ for every
$i\in\\{1,2\\}$. By inductive hypothesis,
$\bigcap_{\psi\in\mathcal{B}(p)}\llbracket\psi\rrbracket\subseteq\llbracket\neg\varphi_{i}\rrbracket$
for every $i\in\\{1,2\\}$, which means that
$\bigcap_{\psi\in\mathcal{B}(p)}\llbracket\psi\rrbracket\subseteq\llbracket\neg\varphi_{1}\rrbracket\cap\llbracket\neg\varphi_{2}\rrbracket=\llbracket\neg\varphi\rrbracket$,
hence the thesis.

    * –

$\varphi=\langle a\rangle\varphi_{1}$: then, $\neg\varphi$ is logically
equivalent to $[a]\neg\varphi_{1}$. Thus, $\phi\in\mathcal{L}(p)$ implies
$\neg\varphi_{1}\in\mathcal{L}(p^{\prime})$ for every $p^{\prime}\in P$ such
that $p\stackrel{{\scriptstyle a}}{{\rightarrow}}p^{\prime}$. By the inductive
hypothesis,
$\bigcap_{\psi\in\mathcal{B}(p^{\prime})}\llbracket\psi\rrbracket\subseteq\llbracket\neg\varphi_{1}\rrbracket$
for every $p^{\prime}\in P$ such that $p\stackrel{{\scriptstyle
a}}{{\rightarrow}}p^{\prime}$, from which it follows
$\bigcup_{p^{\prime}\in\textit{max-
succ}(p,a)}\bigcap_{\psi\in\mathcal{B}(p^{\prime})}\llbracket\psi\rrbracket\subseteq\llbracket\neg\varphi_{1}\rrbracket$.
We define $\zeta=[a]\bigvee_{p^{\prime}\in\textit{max-
succ}(p,a)}\bigwedge_{\psi\in\mathcal{B}^{-}(p^{\prime})}\psi$ (notice that
$\zeta=[a]\mathbf{ff}$ if $p\stackrel{{\scriptstyle a}}{{\not\rightarrow}}$).
If is not difficult to show, by induction on the depth of $p$, that, for all
$p,q\in P$, if $p\lesssim_{\mathsf{S}}q$ then $p\in\llbracket\psi\rrbracket$
for all $\psi\in\mathcal{B}^{-}(q)$. Moreover, we observe that for every
$p^{\prime}$ such that $p\stackrel{{\scriptstyle
a}}{{\rightarrow}}p^{\prime}$, there is $q\in\textit{max-succ}(p,a)$ with
$p^{\prime}\lesssim_{\mathsf{S}}q$. Therefore, $\zeta\in\mathcal{L}(p)$,
because for all $p^{\prime}$ with $p\stackrel{{\scriptstyle
a}}{{\rightarrow}}p^{\prime}$ we have that
$p^{\prime}\in\llbracket\bigwedge_{\psi\in\mathcal{B}^{-}(q)}\psi\rrbracket$,
where $q$ is such that $q\in\textit{max-succ}(p,a)$ and
$p^{\prime}\lesssim_{\mathsf{S}}q$. Moreover, we have that
$\zeta\in\mathcal{B}^{-}(p)$ (by definition of $\mathcal{B}^{-}(p)$) and
therefore
$\bigcap_{\psi\in\mathcal{B}(p)}\llbracket\psi\rrbracket\subseteq\llbracket\zeta\rrbracket$.
By $\bigcup_{p^{\prime}\in\textit{max-
succ}(p,a)}\bigcap_{\psi\in\mathcal{B}(p^{\prime})}\llbracket\psi\rrbracket\subseteq\llbracket\neg\varphi_{1}\rrbracket$,
we have
$\llbracket\zeta\rrbracket\subseteq\llbracket[a]\neg\varphi_{1}\rrbracket=\llbracket\neg\varphi\rrbracket$,
and the thesis immediately follows.

  * •

$\phi\in\\{\varphi_{1}\vee\varphi_{2},\varphi_{1}\wedge\varphi_{2},\langle
a\rangle\varphi\\}$ (inductive step): the proof is exactly the same as in the
previous cases.

Before showing that $\mathcal{B}$ is monotonic (property (_iv_)), we prove, as
a preliminary result, that if $p\equiv_{\mathsf{S}}q$ then
$\mathcal{B}^{-}(p)=\mathcal{B}^{-}(q)$. To this end, we first prove that if
$p\equiv_{\mathsf{S}}q$, then for every $a\in Act$ and
$p^{\prime}\in\textit{max-succ}(p,a)$ there is $q^{\prime}\in\textit{max-
succ}(q,a)$ such that $p^{\prime}\equiv_{\mathsf{S}}q^{\prime}$. (Notice that,
since $\equiv_{\mathsf{S}}$ is symmetric, this also implies that for every
$a\in Act$ and $q^{\prime}\in\textit{max-succ}(q,a)$ there is
$p^{\prime}\in\textit{max-succ}(p,a)$ such that
$p^{\prime}\equiv_{\mathsf{S}}q^{\prime}$.) Let $p,q\in P$ be such that
$p\equiv_{\mathsf{S}}q$, and let $a\in Act$ and $p^{\prime}\in\textit{max-
succ}(p,a)$. By $p\lesssim_{\mathsf{S}}q$, there is $q^{\prime}$ such that
$q\stackrel{{\scriptstyle a}}{{\rightarrow}}q^{\prime}$ and
$p^{\prime}\lesssim_{\mathsf{S}}q^{\prime}$. We show that
$q^{\prime}\in\textit{max-succ}(q,a)$ and
$p^{\prime}\equiv_{\mathsf{S}}q^{\prime}$. In order to show the former,
assume, towards a contradiction, that $q^{\prime}\notin\textit{max-
succ}(q,a)$; thus, there is $q^{\prime\prime}$ such that
$q\stackrel{{\scriptstyle a}}{{\rightarrow}}q^{\prime\prime}$ and
$q^{\prime}<_{\mathsf{S}}q^{\prime\prime}$. By $q\lesssim_{\mathsf{S}}p$, we
have that there is $p^{\prime\prime}$ such that $p\stackrel{{\scriptstyle
a}}{{\rightarrow}}p^{\prime\prime}$ and
$q^{\prime\prime}\lesssim_{\mathsf{S}}p^{\prime\prime}$. Thus,
$p^{\prime\prime}$ is such that $p\stackrel{{\scriptstyle
a}}{{\rightarrow}}p^{\prime\prime}$ and
$p^{\prime}<_{\mathsf{S}}p^{\prime\prime}$, thus getting a contradiction with
the hypothesis that $p^{\prime}\in\textit{max-succ}(p,a)$. Therefore,
$q^{\prime}\in\textit{max-succ}(q,a)$. Now, in order to show that
$p^{\prime}\equiv_{\mathsf{S}}q^{\prime}$, it is enough to prove that
$q^{\prime}\lesssim_{\mathsf{S}}p^{\prime}$ (as we already know that
$p^{\prime}\lesssim_{\mathsf{S}}q^{\prime}$). Assume, towards a contradiction,
that $q^{\prime}\not\lesssim_{\mathsf{S}}p^{\prime}$ (i.e.,
$p^{\prime}<_{\mathsf{S}}q^{\prime}$). By $q\lesssim_{\mathsf{S}}p$, there is
$p^{\prime\prime}$ such that $p\stackrel{{\scriptstyle
a}}{{\rightarrow}}p^{\prime\prime}$ and
$q^{\prime}\lesssim_{\mathsf{S}}p^{\prime\prime}$. Therefore,
$p^{\prime}<_{\mathsf{S}}p^{\prime\prime}$, thus getting a contradiction with
the hypothesis that $p^{\prime}\in\textit{max-succ}(p,a)$. Therefore,
$q^{\prime}\lesssim_{\mathsf{S}}p^{\prime}$, which means
$q^{\prime}\equiv_{\mathsf{S}}p^{\prime}$. We turn to proving that if
$p\equiv_{\mathsf{S}}q$ then $\mathcal{B}^{-}(p)=\mathcal{B}^{-}(q)$. By the
symmetry of $\equiv_{\mathsf{S}}$, it is enough to prove that
$\mathcal{B}^{-}(p)\subseteq\mathcal{B}^{-}(q)$. We proceed by induction on
the depth of $p$. If $I(p)=\emptyset$ (base case), then $I(q)=\emptyset$ as
well, and $\mathcal{B}^{-}(p)=\mathcal{B}^{-}(q)=\\{[a]\mathbf{ff}\mid a\in
Act\\}$. If $I(p)\neq\emptyset$ (inductive step), then let
$[a]\varphi\in\mathcal{B}^{-}(p)$. We distinguish two cases.

  * •

If $a\not\in I(p)$, then $\varphi=\mathbf{ff}$ and, by
$q\lesssim_{\mathsf{S}}p$, $a\not\in I(q)$, which implies
$[a]\varphi\in\mathcal{B}^{-}(q)$.

  * •

If $a\in I(p)$, then $\varphi=\bigvee_{p^{\prime}\in\textit{max-
succ}(p,a)}\bigwedge_{\psi\in\mathcal{B}^{-}(p^{\prime})}\psi$. By
$p\equiv_{\mathsf{S}}q$, we have that for every $p^{\prime}\in\textit{max-
succ}(p,a)$ there is $q^{\prime}\in\textit{max-succ}(q,a)$ with
$p^{\prime}\equiv_{\mathsf{S}}q^{\prime}$, which, by inductive hypothesis,
implies $\mathcal{B}^{-}(p^{\prime})=\mathcal{B}^{-}(q^{\prime})$. The
converse direction holds as well, that is, for every
$q^{\prime}\in\textit{max-succ}(q,a)$ there is $p^{\prime}\in\textit{max-
succ}(p,a)$ with $p^{\prime}\equiv_{\mathsf{S}}q^{\prime}$, which, by
inductive hypothesis, implies
$\mathcal{B}^{-}(p^{\prime})=\mathcal{B}^{-}(q^{\prime})$. Consequently,
$[a]\varphi\in\mathcal{B}^{-}(q)$, and we are done.

We are now ready to show that $\mathcal{B}$ is monotonic (property (_iv_)).
Consider $p,q\in P$, with $\mathcal{L}(p)\subseteq\mathcal{L}(q)$. We want to
show that $\phi\in\mathcal{B}(p)$ implies $\phi\in\mathcal{B}(q)$, for each
$\phi$. Firstly, we observe that, by $\mathcal{L}(p)\subseteq\mathcal{L}(q)$
and Theorem 4, $p\lesssim_{\mathsf{2S}}q$ holds. Thus, we have that
$p\equiv_{\mathsf{S}}q$, which implies $\mathcal{B}^{-}(p)=\mathcal{B}^{-}(q)$
(thanks to the previous result); moreover, we have that for each $a\in Act$
and $p^{\prime}\in P$ with $p\stackrel{{\scriptstyle
a}}{{\rightarrow}}p^{\prime}$, there exists some $q^{\prime}\in P$ such that
$q\stackrel{{\scriptstyle a}}{{\rightarrow}}q^{\prime}$ and
$p^{\prime}\lesssim_{\mathsf{2S}}q^{\prime}$. In order to show that
$\mathcal{B}(p)\subseteq\mathcal{B}(q)$, we proceed by induction on the depth
of $p$. If $I(p)=\emptyset$, then $I(q)=\emptyset$ as well. Thus, we have that
$\mathcal{B}^{+}(p)=\mathcal{B}^{+}(q)=\\{\mathbf{tt}\\}$, and the thesis
follows. Otherwise ($I(p)\neq\emptyset$), let us consider a formula
$\phi\in\mathcal{B}(p)$. If $\phi\in\mathcal{B}^{-}(p)$, then the claim
follows from $\mathcal{B}^{-}(p)=\mathcal{B}^{-}(q)\subseteq\mathcal{B}(q)$.
If $\phi=\mathbf{tt}$, then, by definition of $\mathcal{B}^{+}$, we have
$\phi\in\mathcal{B}^{+}(q)\subseteq\mathcal{B}(q)$. Finally, if $\phi=\langle
a\rangle\varphi\in\mathcal{B}^{+}(p)$, then, by definition of
$\mathcal{B}^{+}$, there exist $p^{\prime}\in P$, with
$p\stackrel{{\scriptstyle a}}{{\rightarrow}}p^{\prime}$, such that
$\varphi=\bigwedge_{\psi\in\Psi}\psi$ for some
$\Psi\subseteq\mathcal{B}(p^{\prime})$. This implies the existence of some
$q^{\prime}\in P$ such that $q\stackrel{{\scriptstyle
a}}{{\rightarrow}}q^{\prime}$ and $p^{\prime}\lesssim_{\mathsf{2S}}q^{\prime}$
(and therefore $\mathcal{L}(p^{\prime})\subseteq\mathcal{L}(q^{\prime})$ by
Theorem 4). By the inductive hypothesis,
$\mathcal{B}(p^{\prime})\subseteq\mathcal{B}(q^{\prime})$ holds as well, which
means that $\Psi\subseteq\mathcal{B}(q^{\prime})$. Hence, we have that
$\langle a\rangle\varphi\in\mathcal{B}^{+}(q)\subseteq\mathcal{B}(q)$.

Case bisimulation ($\mathsf{BS}$). For the sake of clarity we recall from
Table 1 that $\mathcal{B}$ is defined as
$\mathcal{B}^{+}(p)\cup\mathcal{B}^{-}(p)$, where

  * •

$\mathcal{B}^{+}(p)=\\{\mathbf{tt}\\}\cup\\{\langle a\rangle\varphi\mid a\in
Act,\varphi=\bigwedge_{\psi\in\Psi}\psi,\Psi\subseteq\mathcal{B}(p^{\prime}),p\stackrel{{\scriptstyle
a}}{{\rightarrow}}p^{\prime}\\}$, and

  * •

$\mathcal{B}^{-}(p)=\\{[a]\varphi\in\mathcal{L}(p)\mid a\in
Act,\varphi=\bigvee_{p\stackrel{{\scriptstyle
a}}{{\rightarrow}}p^{\prime}}\bigwedge_{\psi\in\mathcal{B}(p^{\prime})}\psi\\}$.

By definition, $\mathcal{B}^{-}(p)\subseteq\mathcal{L}(p)$ for every $p\in P$;
moreover, it is easy to verify that $\mathcal{B}^{-}(p)$ is finite, by
induction on the depth on $p$ and by recalling that $Act$ is finite and
processes are finitely branching. Hence, properties (_i_) and (_iii_)
immediately follow from (_i_ ′) and (_iii_ ′), respectively. Notice also that
property (_iii_) implies that $\mathcal{B}$ is well defined.

In order to prove property (_ii_), we let $\phi\in\mathcal{L}(p)$, for a
generic $p\in P$, and we proceed, as usual, by induction on the structure of
$\phi$. With respect to the previous semantics, bisimulation one is
characterized by the use of free negation (formula of the form $\neg\varphi$,
for every $\varphi\in\mathcal{L}$). By using the fact that $\neg\langle
a\rangle\varphi$ is equivalent to $[a]\neg\varphi$, it suffices to show how to
deal with formulae in the form $[a]\varphi$, for every
$\varphi\in\mathcal{L}$; the other cases are dealt with as in the previous
cases.

  * •

$\phi=[a]\varphi$: by $\phi\in\mathcal{L}(p)$, we have that
$\varphi\in\mathcal{L}(p^{\prime})$ for all $p^{\prime}$ such that
$p\stackrel{{\scriptstyle a}}{{\rightarrow}}p^{\prime}$. By the inductive
hypothesis,
$\bigcap_{\psi\in\mathcal{B}(p^{\prime})}\llbracket\psi\rrbracket\subseteq\llbracket\varphi\rrbracket$,
for each $p^{\prime}$ such that $p\stackrel{{\scriptstyle
a}}{{\rightarrow}}p^{\prime}$, from which it follows
$\bigcup_{p\stackrel{{\scriptstyle
a}}{{\rightarrow}}p^{\prime}}\bigcap_{\psi\in\mathcal{B}(p^{\prime})}\llbracket\psi\rrbracket\subseteq\llbracket\varphi\rrbracket$.
We define $\zeta=[a]\bigvee_{p\stackrel{{\scriptstyle
a}}{{\rightarrow}}p^{\prime}}\bigwedge_{\psi\in\mathcal{B}(p^{\prime})}\psi$
(notice that $\zeta=[a]\mathbf{ff}$ if $p\stackrel{{\scriptstyle
a}}{{\not\rightarrow}}$). Clearly, for all $p^{\prime}$ such that
$p\stackrel{{\scriptstyle a}}{{\not\rightarrow}}p^{\prime}$, it holds
$p^{\prime}\in\llbracket\psi\rrbracket$ for all
$\psi\in\mathcal{B}(p^{\prime})$. Therefore, $p\in\llbracket\zeta\rrbracket$,
which means $\zeta\in\mathcal{L}(p)$. Moreover, we have that
$\zeta\in\mathcal{B}^{-}(p)$ (by definition of $\mathcal{B}^{-}(p)$) and
therefore
$\bigcap_{\psi\in\mathcal{B}(p)}\llbracket\psi\rrbracket\subseteq\llbracket\zeta\rrbracket$.
By $\bigcup_{p\stackrel{{\scriptstyle
a}}{{\rightarrow}}p^{\prime}}\bigcap_{\psi\in\mathcal{B}(p^{\prime})}\llbracket\psi\rrbracket\subseteq\llbracket\varphi\rrbracket$,
we have
$\llbracket\zeta\rrbracket\subseteq\llbracket[a]\varphi\rrbracket=\llbracket\phi\rrbracket$,
and the thesis immediately follows.

Finally, we show that $\mathcal{B}$ is monotonic (property (_iv_)). Consider
$p,q\in P$, with $\mathcal{L}(p)\subseteq\mathcal{L}(q)$. We want to show that
$\mathcal{B}(p)\subseteq\mathcal{B}(q)$. Firstly, we observe that, by
$\mathcal{L}(p)\subseteq\mathcal{L}(q)$ and Theorem 4, $p\lesssim q$ holds.
Moreover, by the definition of bisimulation semantics, $p\lesssim q$ implies
$q\lesssim p$, and thus $p\equiv q$. It is straightforward to show, by
induction on the depth of $p$, that if $p\equiv q$, then
$\mathcal{B}(p)=\mathcal{B}(q)$, hence the thesis. ∎

###  A.2 Existence of $\bar{\chi}(\cdot)$

In what follows, we show that it is possible to build, for each $\chi(p)$, a
formula $\bar{\chi}(p)$, with the properties described in Corollary 4(ii).

######  Lemma 2.

Let $X\in\mathsf{Btime\text{-}spectrum}$. For each $p\in P$ and
$\chi_{{}_{X}}(p)$ characteristic within $\mathcal{L}_{X}$ for $p$, there
exists a formula in $\mathcal{L}_{X}$, denoted by $\bar{\chi}_{{}_{X}}(p)$,
such that either

  * •

$\llbracket\bar{\chi}(p)\rrbracket=P\setminus\llbracket\chi(p)\rrbracket$, or

  * •

$p\not\in\llbracket\bar{\chi}_{{}_{X}}(p)\rrbracket$ and $\\{p^{\prime}\in
P\mid
p^{\prime}\not\lesssim_{X}p\\}\subseteq\llbracket\bar{\chi}_{{}_{X}}(p)\rrbracket$.

###### Proof.

We consider each semantics $X\in\mathsf{Btime\text{-}spectrum}$ in turn. As in
the previous section, for the sake of a lighter notation, we often omit the
subscripts identifying the semantics as it is clear from the context, e.g., we
write $\mathcal{L}$, $\bar{\chi}$, and $p\not\lesssim q$ instead of
$\mathcal{L}_{\mathsf{S}}$, $\bar{\chi}_{\mathsf{S}}$, and
$p\not\lesssim_{\mathsf{S}}q$, respectively.

Case simulation ($\mathsf{S}$). For the sake of clarity we recall here the
definition of $\bar{\chi}$ from Table 1:

$\bar{\chi}(p)=\bigvee_{a\in Act}\langle
a\rangle\bigwedge_{p\stackrel{{\scriptstyle
a}}{{\rightarrow}}p^{\prime}}\bar{\chi}(p^{\prime})$.

Let us first show that for every $p\in P$ we have
$p\not\in\llbracket\bar{\chi}(p)\rrbracket$. We proceed by induction on the
depth of $p$.

  * •

$I(p)=\emptyset$: we have $\bar{\chi}(p)=\bigvee_{a\in Act}\langle
a\rangle\mathbf{tt}$, and thus $p\notin\llbracket\bar{\chi}(p)\rrbracket$.

  * •

$I(p)\neq\emptyset$: obviously, $p\notin\llbracket\langle
a\rangle\mathbf{tt}\rrbracket$ holds for every $a\notin I(p)$. Now, for every
$p\stackrel{{\scriptstyle a}}{{\rightarrow}}p^{\prime}$, by induction
hypothesis, $p^{\prime}\notin\llbracket\bar{\chi}(p^{\prime})\rrbracket$.
Thus, $p^{\prime}\notin\llbracket\bigwedge_{p\stackrel{{\scriptstyle
a}}{{\rightarrow}}p^{\prime}}\bar{\chi}(p^{\prime})\rrbracket$ and therefore
$p\notin\llbracket\langle a\rangle\bigwedge_{p\stackrel{{\scriptstyle
a}}{{\rightarrow}}p^{\prime}}\bar{\chi}(p^{\prime})\rrbracket$. Hence, we
obtain that $p\not\in\llbracket\bar{\chi}(p)\rrbracket$.

Now, let us show that $\\{p^{\prime}\in P\mid p^{\prime}\not\lesssim
p\\}\subseteq\llbracket\bar{\chi}(p)\rrbracket$. The proof is by induction on
the depth of $p$.

  * •

$I(p)=\emptyset$: we have that $\\{p^{\prime}\in P\mid p^{\prime}\not\lesssim
p\\}=P\setminus\\{p^{\prime}\in P\mid I(p^{\prime})=\emptyset\\}$. It is easy
to see that $P\setminus\\{p^{\prime}\in P\mid
I(p^{\prime})=\emptyset\\}=\llbracket\bigvee_{a\in Act}\langle
a\rangle\mathbf{tt}\rrbracket=\llbracket\bar{\chi}(p)\rrbracket$.

  * •

$I(p)\neq\emptyset$: let $q\not\lesssim p$. Thus there exists some
$q^{\prime}$, with $q\stackrel{{\scriptstyle a}}{{\rightarrow}}q^{\prime}$,
such that, for every $p^{\prime}$, $p\stackrel{{\scriptstyle
a}}{{\rightarrow}}p^{\prime}$ implies $q^{\prime}\not\lesssim p^{\prime}$.
Then, by inductive hypothesis,
$q^{\prime}\in\llbracket\bar{\chi}(p^{\prime})\rrbracket$ for every
$p^{\prime}$ such that $p\stackrel{{\scriptstyle
a}}{{\rightarrow}}p^{\prime}$. Thus,
$q^{\prime}\in\llbracket\bigwedge_{p\stackrel{{\scriptstyle
a}}{{\rightarrow}}p^{\prime}}\bar{\chi}(p^{\prime})\rrbracket$ and therefore
$q\in\llbracket\langle a\rangle\bigwedge_{p\stackrel{{\scriptstyle
a}}{{\rightarrow}}p^{\prime}}\bar{\chi}(p^{\prime})\rrbracket$. Hence, we
conclude $q\in\llbracket\bar{\chi}(p)\rrbracket$.

Case complete simulation ($\mathsf{CS}$). For the sake of clarity we recall
here the definition of $\bar{\chi}$ from Table 1:

$\begin{array}[]{lll@{\hspace{20mm}}l}\bar{\chi}(p)&=&\big{(}\bigvee_{a\in
Act}\langle a\rangle\bigwedge_{p\stackrel{{\scriptstyle
a}}{{\rightarrow}}p^{\prime}}\bar{\chi}(p^{\prime})\big{)}\vee\mathbf{0}\hfil\hskip
56.9055pt&\text{if $I(p)\neq\emptyset$}\\\ \bar{\chi}(p)&=&\bigvee_{a\in
Act}\langle a\rangle\bigwedge_{p\stackrel{{\scriptstyle
a}}{{\rightarrow}}p^{\prime}}\bar{\chi}(p^{\prime})\hfil\hskip
56.9055pt&\text{if $I(p)=\emptyset$}\end{array}$

Let us first show that for every $p\in P$ we have
$p\not\in\llbracket\bar{\chi}(p)\rrbracket$. We proceed by induction on the
depth of $p$.

  * •

$I(p)=\emptyset$: we have $\bar{\chi}(p)=\bigvee_{a\in Act}\langle
a\rangle\mathbf{tt}$, and obviously
$p\notin\llbracket\bar{\chi}(p)\rrbracket$.

  * •

$I(p)\neq\emptyset$: obviously, $p\notin\llbracket\mathbf{0}\rrbracket$ and
$p\notin\llbracket\langle a\rangle\mathbf{tt}\rrbracket$ for every $a\notin
I(p)$. Now, for every $p\stackrel{{\scriptstyle a}}{{\rightarrow}}p_{1}$, by
the inductive hypothesis, $p_{1}\notin\llbracket\bar{\chi}(p_{1})\rrbracket$.
Thus, $p_{1}\notin\llbracket\bigwedge_{p\stackrel{{\scriptstyle
a}}{{\rightarrow}}p^{\prime}}\bar{\chi}(p^{\prime})\rrbracket$ and therefore
$p\notin\llbracket\langle a\rangle\bigwedge_{p\stackrel{{\scriptstyle
a}}{{\rightarrow}}p^{\prime}}\bar{\chi}(p^{\prime})\rrbracket$. Hence, we
obtain that $p\not\in\llbracket\bar{\chi}(p)\rrbracket$.

Now, let us show that $\\{p^{\prime}\in P\mid p^{\prime}\not\lesssim
p\\}\subseteq\llbracket\bar{\chi}(p)\rrbracket$. The proof is by induction on
the depth of $p$.

  * •

$I(p)=\emptyset$: we have that $\\{p^{\prime}\in P\mid p^{\prime}\not\lesssim
p\\}=P\setminus\\{p^{\prime}\in P\mid I(p^{\prime})=\emptyset\\}$ because,
when $I(p)=\emptyset$, $q\not\lesssim p$ holds exactly for processes $q$ with
$I(q)\neq\emptyset$. It is easy to see that $P\setminus\\{p^{\prime}\in P\mid
I(p^{\prime})=\emptyset\\}=\llbracket\bigvee_{a\in Act}\langle
a\rangle\mathbf{tt}\rrbracket=\llbracket\bar{\chi}(p)\rrbracket$.

  * •

$I(p)\neq\emptyset$: let $q\not\lesssim p$. Thus, either $I(q)=\emptyset$ and
$I(p)\neq\emptyset$ (or analogously $I(p)=\emptyset$ and $I(q)\neq\emptyset$),
or there exists some $q^{\prime}$, with $q\stackrel{{\scriptstyle
a}}{{\rightarrow}}q^{\prime}$, such that, for every $p^{\prime}$,
$p\stackrel{{\scriptstyle a}}{{\rightarrow}}p^{\prime}$ implies
$q^{\prime}\not\lesssim p^{\prime}$. If it is the case that $I(q)=\emptyset$
and $I(p)\neq\emptyset$ (respectively, $I(p)=\emptyset$ and
$I(q)\neq\emptyset$), then $q\in\llbracket\mathbf{0}\rrbracket$ (respectively,
$q\in\llbracket\langle a\rangle\mathbf{tt}\rrbracket$ holds for some $a\notin
I(p)$). In any case, $q\in\llbracket\bar{\chi}(p)\rrbracket$ holds.

Otherwise, if there exist $a\in Act$ and $q^{\prime}\in P$, with
$q\stackrel{{\scriptstyle a}}{{\rightarrow}}q^{\prime}$, such that
$q^{\prime}\not\lesssim p^{\prime}$ for every $p\stackrel{{\scriptstyle
a}}{{\rightarrow}}p^{\prime}$, then, by the inductive hypothesis,
$q^{\prime}\in\llbracket\bar{\chi}(p^{\prime})\rrbracket$ for every
$p^{\prime}$. Thus,
$q^{\prime}\in\llbracket\bigwedge_{p\stackrel{{\scriptstyle
a}}{{\rightarrow}}p^{\prime}}\bar{\chi}(p^{\prime})\rrbracket$ and therefore
$q\in\llbracket\langle a\rangle\bigwedge_{p\stackrel{{\scriptstyle
a}}{{\rightarrow}}p^{\prime}}\bar{\chi}(p^{\prime})\rrbracket$. Hence, we
conclude $q\in\llbracket\bar{\chi}(p)\rrbracket$.

Case ready simulation: ($\mathsf{RS}$). See the proof of Lemma 2 at page 2.

Case trace simulation ($\mathsf{TS}$). For the sake of clarity we recall here
the definition of $\bar{\chi}$ from Table 1:

$\bar{\chi}(p)=\big{(}\bigvee_{a\in act}\langle
a\rangle\bigwedge_{p\stackrel{{\scriptstyle
a}}{{\rightarrow}}p^{\prime}}\bar{\chi}(p^{\prime})\big{)}\vee\bigvee_{\tau\in\mathit{traces}(p),\tau
a\notin\mathit{traces}(p)}\langle\tau
a\rangle\mathbf{tt}\vee\bigvee_{p\stackrel{{\scriptstyle\tau
a}}{{\rightarrow}}p^{\prime}}[\tau a]\mathbf{ff}$.

Let us first show that for every $p\in P$ we have
$p\not\in\llbracket\bar{\chi}(p)\rrbracket$. We proceed by induction on the
depth of $p$.

  * •

$I(p)=\emptyset$: we have $\bar{\chi}(p)=\bigvee_{a\in Act}\langle
a\rangle\mathbf{tt}$, and thus $p\notin\llbracket\bar{\chi}(p)\rrbracket$.

  * •

$I(p)\neq\emptyset$: obviously, $p\notin\llbracket\langle\tau
a\rangle\mathbf{tt}\rrbracket$ holds for every $\tau\in\mathit{traces}(p)$ and
$a\in Act$ such that $\tau a\notin\mathit{traces}(p)$. Moreover,
$p\notin\llbracket[\tau a]\mathbf{ff}\rrbracket$ holds for every $\tau
a\in\mathit{traces}(p)$. Now, for every $p\stackrel{{\scriptstyle
a}}{{\rightarrow}}p_{1}$, by the inductive hypothesis,
$p_{1}\notin\llbracket\bar{\chi}(p_{1})\rrbracket$. Thus,
$p_{1}\notin\llbracket\bigwedge_{p\stackrel{{\scriptstyle
a}}{{\rightarrow}}p^{\prime}}\bar{\chi}(p^{\prime})\rrbracket$ and therefore
$p\notin\llbracket\langle a\rangle\bigwedge_{p\stackrel{{\scriptstyle
a}}{{\rightarrow}}p^{\prime}}\bar{\chi}(p^{\prime})\rrbracket$. Hence, we
obtain that $p\not\in\llbracket\bar{\chi}(p)\rrbracket$.

Now, let us show that $\\{p^{\prime}\in P\mid p^{\prime}\not\lesssim
p\\}\subseteq\llbracket\bar{\chi}(p)\rrbracket$, that is,
$\llbracket\bar{\chi}(p)\rrbracket$ contains at least the elements that are
either strictly above $p$ or incomparable with it. The proof is by induction
on the depth of $p$.

  * •

$I(p)=\emptyset$: we have that $\\{p^{\prime}\in P\mid p^{\prime}\not\lesssim
p\\}=P\setminus\\{p^{\prime}\in P\mid I(p^{\prime})=\emptyset\\}$ because,
when $I(p)=\emptyset$, $q\not\lesssim p$ holds exactly for processes $q$ with
$I(q)\neq\emptyset$. It is easy to see that $P\setminus\\{p^{\prime}\in P\mid
I(p^{\prime})=\emptyset\\}=\llbracket\bigvee_{a\in Act}\langle
a\rangle\mathbf{tt}\rrbracket=\llbracket\bar{\chi}(p)\rrbracket$.

  * •

$I(p)\neq\emptyset$: let $q\not\lesssim p$. Thus, either
$\mathit{traces}(q)\neq\mathit{traces}(p)$ or there exists some $q^{\prime}$,
with $q\stackrel{{\scriptstyle a}}{{\rightarrow}}q^{\prime}$, such that, for
every $p^{\prime}$, $p\stackrel{{\scriptstyle a}}{{\rightarrow}}p^{\prime}$
implies $q^{\prime}\not\lesssim p^{\prime}$. If it is the case that
$\mathit{traces}(q)\neq\mathit{traces}(p)$, then either
$q\in\llbracket\langle\tau a\rangle\mathbf{tt}\rrbracket$ for some $\tau a$
such that $\tau\in\mathit{traces}(p)$ and $\tau a\notin\mathit{traces}(p)$, or
$q\in\llbracket[\tau a]\mathbf{ff}\rrbracket$ for some $\tau
a\in\mathit{traces}(p)$. In either case,
$q\in\llbracket\bar{\chi}(p)\rrbracket$ holds.

If, on the other hand, $\mathit{traces}(p)=\mathit{traces}(q)$, then there
exist $a\in Act$ and $q^{\prime}\in P$, with $q\stackrel{{\scriptstyle
a}}{{\rightarrow}}q^{\prime}$, such that $q^{\prime}\not\lesssim p^{\prime}$
for every $p\stackrel{{\scriptstyle a}}{{\rightarrow}}p^{\prime}$, then, by
the inductive hypothesis,
$q^{\prime}\in\llbracket\bar{\chi}(p^{\prime})\rrbracket$ for every
$p^{\prime}$. Thus,
$q^{\prime}\in\llbracket\bigwedge_{p\stackrel{{\scriptstyle
a}}{{\rightarrow}}p^{\prime}}\bar{\chi}(p^{\prime})\rrbracket$ and therefore
$q\in\llbracket\langle a\rangle\bigwedge_{p\stackrel{{\scriptstyle
a}}{{\rightarrow}}p^{\prime}}\bar{\chi}(p^{\prime})\rrbracket$ (notice that
$a\in I(p)$, due to $a\in I(q)$ and $\mathit{traces}(p)=\mathit{traces}(q)$).
Hence, we conclude $q\in\llbracket\bar{\chi}(p)\rrbracket$.

Case 2-Nested simulation ($\mathsf{2S}$). For the sake of clarity we recall
here the definition of $\bar{\chi}$ from Table 1:

$\begin{array}[]{lll}\bar{\chi}(p)&=&\big{(}\bigvee_{a\in Act}\langle
a\rangle\bigwedge_{p\stackrel{{\scriptstyle
a}}{{\rightarrow}}p^{\prime}}\bar{\chi}(p^{\prime})\big{)}\vee\bar{\Phi}(p)\\\
\bar{\Phi}(p)&=&\bigvee_{a\in I(p)}[a]\mathbf{ff}\vee\bigvee_{a\in
I(p)}\bigvee_{p\stackrel{{\scriptstyle
a}}{{\rightarrow}}p^{\prime}}[a]\bar{\Phi}(p^{\prime})\end{array}$

Let us first show that for every $p\in P$ we have
$p\not\in\llbracket\bar{\chi}(p)\rrbracket$. We proceed by induction on the
depth of $p$.

  * •

$I(p)=\emptyset$: we have $\bar{\chi}(p)=\bigvee_{a\in Act}\langle
a\rangle\mathbf{tt}$, and thus $p\notin\llbracket\bar{\chi}(p)\rrbracket$.

  * •

$I(p)\neq\emptyset$: obviously, $p\notin\llbracket\langle
a\rangle\mathbf{tt}\rrbracket$ holds for every $a\notin I(p)$. Next, for every
$p\stackrel{{\scriptstyle a}}{{\rightarrow}}p^{\prime}$, by the inductive
hypothesis, $p^{\prime}\notin\llbracket\bar{\chi}(p^{\prime})\rrbracket$.
Thus, $p\notin\llbracket\langle a\rangle\bar{\chi}(p^{\prime})\rrbracket$, for
each $p^{\prime}$ such that $p\stackrel{{\scriptstyle
a}}{{\rightarrow}}p^{\prime}$. Therefore $p\notin\llbracket\langle
a\rangle\bigwedge_{p\stackrel{{\scriptstyle
a}}{{\rightarrow}}p^{\prime}}\bar{\chi}(p^{\prime})\rrbracket$. We are left
with showing that $p\notin\llbracket\bar{\Phi}(p)\rrbracket$. To this end,
observe that $p\notin\llbracket[a]\mathbf{ff}\rrbracket$ for all $a\in I(p)$;
moreover, for all $p\stackrel{{\scriptstyle a}}{{\rightarrow}}p^{\prime}$,
since $p^{\prime}\notin\llbracket\bar{\chi}(p^{\prime})\rrbracket$ holds by
the inductive hypothesis, in particular we have
$p^{\prime}\notin\llbracket\bar{\Phi}(p^{\prime})\rrbracket$. Thus,
$p\notin\llbracket[a]\bar{\Phi}(p^{\prime})\rrbracket$ for each $p^{\prime}$
such that $p\stackrel{{\scriptstyle a}}{{\rightarrow}}p^{\prime}$ and
$p\notin\llbracket\bigvee_{p\stackrel{{\scriptstyle
a}}{{\rightarrow}}p^{\prime}}[a]\bar{\Phi}(p^{\prime})\rrbracket$. Hence, we
obtain that $p\not\in\llbracket\bar{\chi}(p)\rrbracket$.

Now, let us show that $\\{p^{\prime}\in P\mid p^{\prime}\not\lesssim
p\\}\subseteq\llbracket\bar{\chi}(p)\rrbracket$. The proof is by induction on
the depth of $p$.

  * •

$I(p)=\emptyset$: we have that $\\{p^{\prime}\in P\mid p^{\prime}\not\lesssim
p\\}=P\setminus\\{p^{\prime}\in P\mid I(p^{\prime})=\emptyset\\}$. It is easy
to see that $P\setminus\\{p^{\prime}\in P\mid
I(p^{\prime})=\emptyset\\}=\llbracket\bigvee_{a\in
Act}\langle\mathbf{tt}\rangle\rrbracket=\llbracket\bar{\chi}(p)\rrbracket$.

  * •

$I(p)\neq\emptyset$: let $q\not\lesssim_{\mathsf{2S}}p$. Thus, by definition,
either there exists $a\in Act$ and $q^{\prime}$, with
$q\stackrel{{\scriptstyle a}}{{\rightarrow}}q^{\prime}$, such that, for every
$p^{\prime}$, $p\stackrel{{\scriptstyle a}}{{\rightarrow}}p^{\prime}$ implies
$q^{\prime}\not\lesssim_{\mathsf{2S}}p^{\prime}$, or
$p\not\lesssim_{\mathsf{S}}q$.

First, if there exist $a\in Act$ and $q^{\prime}\in P$, with
$q\stackrel{{\scriptstyle a}}{{\rightarrow}}q^{\prime}$, such that
$q^{\prime}\not\lesssim_{\mathsf{2S}}p^{\prime}$ for every
$p\stackrel{{\scriptstyle a}}{{\rightarrow}}p^{\prime}$, by the inductive
hypothesis, $q^{\prime}\in\llbracket\bar{\chi}(p^{\prime})\rrbracket$ for
every $p^{\prime}$ such that $p\stackrel{{\scriptstyle
a}}{{\rightarrow}}p^{\prime}$. Thus,
$q^{\prime}\in\llbracket\bigwedge_{p\stackrel{{\scriptstyle
a}}{{\rightarrow}}p^{\prime}}\bar{\chi}(p^{\prime})\rrbracket$ and therefore
$q\in\llbracket\langle a\rangle\bigwedge_{p\stackrel{{\scriptstyle
a}}{{\rightarrow}}p^{\prime}}\bar{\chi}(p^{\prime})\rrbracket$.

Otherwise, if $p\not\lesssim_{\mathsf{S}}q$, then there exist $a\in Act$ and
$p^{\prime}$ with $p\stackrel{{\scriptstyle a}}{{\rightarrow}}p^{\prime}$,
such that $p^{\prime}\not\lesssim_{\mathsf{S}}q^{\prime}$ for every
$q\stackrel{{\scriptstyle a}}{{\rightarrow}}q^{\prime}$. We show by induction
on the depth of $q$ that if $p\not\lesssim_{\mathsf{S}}q$ then
$q\in\bar{\Phi}(p)$. If $I(q)=\emptyset$, then
$q\in\llbracket[a]\mathbf{ff}\rrbracket$ for some $a\in I(p)$ (notice that
$I(p)\neq\emptyset$ by assumption) and thus $q\in\bar{\Phi}(p)$. Now, when
$I(q)\neq\emptyset$, by the inductive hypothesis,
$q^{\prime}\in\llbracket\bar{\Phi}(p^{\prime})\rrbracket$ for every
$q\stackrel{{\scriptstyle a}}{{\rightarrow}}q^{\prime}$. Thus
$q\in\llbracket[a]\bar{\Phi}(p^{\prime})\rrbracket$, which implies that
$q\in\llbracket\bar{\Phi}(p)\rrbracket$. Since $p\not\lesssim_{\mathsf{S}}q$
by assumption, we have that $q\in\llbracket\bar{\Phi}(p)\rrbracket$. Therefore
$q\in\llbracket\bar{\chi}(p)\rrbracket$ holds by definition of
$\bar{\chi}(p)$, and we are done.

Case bisimulation ($\mathsf{BS}$). We simply define
$\bar{\chi}(p)=\neg\chi(p)$ ($\chi(p)$ exists thanks to Proposition 10) and
$\llbracket\bar{\chi}(p)\rrbracket=P\setminus\llbracket\chi(p)\rrbracket$
holds trivially. ∎

##  Appendix B Proofs for semantics in van Glabbeek’s linear time spectrum

######  Lemma 5.

For all $p,q\in P$ such that $p\lesssim_{\mathsf{T}}q$, we have $0pt(p)\leq
0pt(q)$.

###### Proof.

The claim immediately follows from the definition of $0pt(p)$ (i.e., $0pt(p)$
is the length of a longest trace in $\mathsf{T}(p)$) and the fact that
$p\lesssim_{\mathsf{T}}q$ if and only if
$\mathsf{T}(p)\subseteq\mathsf{T}(q)$. ∎

######  Corollary 5.

Let $X\in\mathsf{Ltime\text{-}spectrum}$. For all $p,q\in P$ such that
$p\lesssim_{X}q$, we have $0pt(p)\leq 0pt(q)$.

######  Lemma 6.

$\mathcal{B}_{X}(p)\subseteq\mathcal{L}_{X}(p)$ holds for every
$X\in\mathsf{Ltime\text{-}spectrum}$ and $p\in P$.

###### Proof.

Let $X\in\mathsf{Ltime\text{-}spectrum}$, $p\in P$, and
$\phi\in\mathcal{B}_{X}(p)$. If $\phi=\mathbf{tt}$, then the thesis follows
trivially. If $\phi=\mathit{formula}_{X}(x)$ for some $x\in
X^{\mathit{fin}}(p)$, then we distinguish the following cases.

  * •

If $X=\mathsf{T}$, then $\phi=\langle\tau\rangle\mathbf{tt}$ for
$\tau\in\mathsf{T}^{\mathit{fin}}(p)\subseteq\mathsf{T}(p)$. Since
$\tau\in\mathsf{T}(p)$, it clearly holds $p\in\llbracket\phi\rrbracket$, which
means $\phi\in\mathcal{L}_{\mathsf{T}}(p)$.

  * •

If $X=\mathsf{CT}$, then $\phi=\langle\tau\rangle\mathbf{0}$ for
$\tau\in\mathsf{CT}^{\mathit{fin}}(p)\subseteq\mathsf{CT}(p)$. Since
$\tau\in\mathsf{CT}(p)$, it clearly holds $p\in\llbracket\phi\rrbracket$,
which means $\phi\in\mathcal{L}_{\mathsf{CT}}(p)$.

  * •

If $X=\mathsf{F}$, then $\phi=\langle\tau\rangle\bigwedge_{a\in
Y}[a]\mathbf{ff}$ for
$\langle\tau,Y\rangle\in\mathsf{F}^{\mathit{fin}}(p)\subseteq\mathsf{F}(p)$.
From the definition of $\mathsf{F}(p)$, it immediately follows
$p\in\llbracket\phi\rrbracket$, and we are done.

  * •

If $X=\mathsf{R}$, then $\phi=\langle\tau\rangle{\langle\\![}Y{]\\!\rangle}$
for
$\langle\tau,Y\rangle\in\mathsf{R}^{\mathit{fin}}(p)\subseteq\mathsf{R}(p)$.
From the definition of $\mathsf{R}(p)$, it immediately follows
$p\in\llbracket\phi\rrbracket$, and we are done.

  * •

If $X=\mathsf{FT}$, then let $\phi=\mathit{formula}_{\mathsf{FT}}(\sigma)$ for
$\sigma\in\mathsf{FT}^{\mathit{fin}}(p)$; we proceed by induction on $\sigma$.

    * –

If $\sigma=\varepsilon$, then $\phi=\mathbf{tt}$, and the thesis follows
trivially;

    * –

If $\sigma=a\sigma^{\prime}$, with $a\in Act$ and
$\sigma^{\prime}\in\mathsf{FT}^{\mathit{fin}}(p^{\prime})$ for some
$p^{\prime}$ such that $p\stackrel{{\scriptstyle
a}}{{\rightarrow}}p^{\prime}$, then $\phi=\langle
a\rangle\mathit{formula}_{\mathsf{FT}}(\sigma^{\prime})$ and
$\mathit{formula}_{\mathsf{FT}}(\sigma^{\prime})\in\mathcal{B}_{\mathsf{FT}}(p^{\prime})$444Notice
that, while it is clear that $\sigma^{\prime}\in\mathsf{FT}(p^{\prime})$, we
are not guaranteed in general that $|\sigma^{\prime}|\leq 2\cdot
0pt(p^{\prime})$ holds (which is needed for $\sigma^{\prime}$ to belong to
$\mathsf{FT}^{\mathit{fin}}(p^{\prime})$). However, it can be shown that we
can always reduce to the case where this holds (see item (f) at page (f) for a
detailed explanation).. By the inductive hypothesis, we have that
$\mathit{formula}_{\mathsf{FT}}(\sigma^{\prime})\in\mathcal{L}_{\mathsf{FT}}(p^{\prime})$,
that is,
$p^{\prime}\in\llbracket\mathit{formula}_{\mathsf{FT}}(\sigma^{\prime})\rrbracket$.
It follows that $p\in\llbracket\phi\rrbracket$, which equals to
$\phi\in\mathcal{L}_{\mathsf{FT}}(p)$.

    * –

If $\sigma=Y\sigma^{\prime}$, with $Y\in\mathcal{P}(Act)$ and
$\sigma^{\prime}\in\mathsf{FT}^{\mathit{fin}}(p)$, then $\phi=\bigwedge_{a\in
Y}{[a]\mathbf{ff}}\wedge\mathit{formula}_{\mathsf{FT}}(\sigma^{\prime})$. By
$Y\sigma^{\prime}\in\mathsf{FT}(p^{\prime})$, we have that
$p\in\llbracket\bigwedge_{a\in Y}{[a]\mathbf{ff}}\rrbracket$. By
$\sigma^{\prime}\in\mathsf{FT}^{\mathit{fin}}(p)$, it holds
$\mathit{formula}_{\mathsf{FT}}(\sigma^{\prime})\in\mathcal{B}_{\mathsf{FT}}(p)$
and thus, by the inductive hypothesis,
$\mathit{formula}_{\mathsf{FT}}(\sigma^{\prime})\in\mathcal{L}_{\mathsf{FT}}(p)$,
that is,
$p\in\llbracket\mathit{formula}_{\mathsf{FT}}(\sigma^{\prime})\rrbracket$. It
follows that $p\in\llbracket\phi\rrbracket$, which equals to
$\phi\in\mathcal{L}_{\mathsf{FT}}(p)$.

  * •

If
$X\in\\{\mathsf{RT},\mathsf{IFT},\mathsf{PFT},\mathsf{I2T},\mathsf{P2T}\\}$,
then the proof uses the same inductive argument as in the previous case, and
thus we omit the details.

  * •

If $X=\mathsf{IF}$, then
$\phi=\langle\tau\rangle\bigwedge_{\tau^{\prime}\in\Gamma}[\tau^{\prime}]\mathbf{ff}$
for
$\langle\tau,\Gamma\rangle\in\mathsf{IF}^{\mathit{fin}}(p)\subseteq\mathsf{IF}(p)$.
From the definition of $\mathsf{IF}(p)$, it immediately follows that
$p\in\llbracket\phi\rrbracket$, and we are done.

  * •

If $X=\mathsf{PF}$, then
$\phi=\langle\tau\rangle{\langle\\![}\Gamma{]\\!\rangle}$ for
$\langle\tau,\Gamma\rangle\in\mathsf{PF}^{\mathit{fin}}(p)\subseteq\mathsf{PF}(p)$.
From the definition of $\mathsf{PF}(p)$, it immediately follows that
$p\in\llbracket\phi\rrbracket$, and we are done.

  * •

If $X=\mathsf{I2}$, then
$\phi=\langle\tau\rangle\bigwedge_{[p^{\prime}]_{\scalebox{0.5}{$\mathsf{BS}$}}\in\mathbb{P}}\neg\chi_{{}_{\mathsf{S}}}(p^{\prime})$
for
$\langle\tau,\mathbb{P}\rangle\in\mathsf{I2}^{\mathit{fin}}(p)\subseteq\mathsf{I2}(p)$.
By the definition of $\mathsf{I2}(p)$,
$\langle\tau,\mathbb{P}\rangle\in\mathsf{I2}(p)$ implies that there is some
$q$ such that $p\stackrel{{\scriptstyle\tau}}{{\rightarrow}}q$ and
$q_{\downarrow_{\mathsf{S}}}\cap\mathbb{P}=\emptyset$. From
$q_{\downarrow_{\mathsf{S}}}\cap\mathbb{P}=\emptyset$, it follows that
$p^{\prime}\not\lesssim_{\mathsf{S}}q$ for all
$[p^{\prime}]_{\scalebox{0.5}{$\mathsf{BS}$}}\in\mathbb{P}$, which means that
$q\notin\llbracket\chi_{{}_{\mathsf{S}}}(p^{\prime})\rrbracket$ for all
$[p^{\prime}]_{\scalebox{0.5}{$\mathsf{BS}$}}\in\mathbb{P}$. Therefore,
$p\in\llbracket\phi\rrbracket$, and we are done.

  * •

If $X=\mathsf{P2}$, then $\phi=\langle\tau\rangle\alpha(\mathbb{P})$, with

$\alpha(\mathbb{P})=\bigwedge_{[p^{\prime}]_{\scalebox{0.5}{$\mathsf{BS}$}}\in\mathbb{P}}\chi_{{}_{\mathsf{S}}}(p^{\prime})\wedge\bigvee_{[p^{\prime}]_{\scalebox{0.5}{$\mathsf{BS}$}}\in\mathbb{P}}simulated\text{-}by(p^{\prime})$

and

$simulated\text{-}by(p^{\prime})=\bigwedge_{a\in
Act}[a]\bigvee_{p^{\prime}\stackrel{{\scriptstyle
a}}{{\rightarrow}}p^{\prime\prime}}simulated\text{-}by(p^{\prime\prime})$.

By the definition of $\mathsf{P2}(p)$,
$\langle\tau,\mathbb{P}\rangle\in\mathsf{P2}(p)$ implies that there is some
$q$ such that $p\stackrel{{\scriptstyle\tau}}{{\rightarrow}}q$ and
$q_{\downarrow_{\mathsf{S}}}=\mathbb{P}$. It follows that
$p^{\prime}\lesssim_{\mathsf{S}}q$ for all
$[p^{\prime}]_{\scalebox{0.5}{$\mathsf{BS}$}}\in\mathbb{P}$, which means that
$q\in\llbracket\chi_{{}_{\mathsf{S}}}(p^{\prime})\rrbracket$ for all
$[p^{\prime}]_{\scalebox{0.5}{$\mathsf{BS}$}}\in\mathbb{P}$. Moreover, by
$q_{\downarrow_{\mathsf{S}}}=\mathbb{P}$, we have that
$[q]_{\scalebox{0.5}{$\mathsf{BS}$}}\in\mathbb{P}$. Since $q\in
simulated\text{-}by(q)$ clearly holds, we conclude
$p\in\llbracket\phi\rrbracket$, and we are done. ∎

######  Lemma 7.

Formula $\bigwedge_{\psi\in\mathcal{B}_{X}(p)}\psi$ is characteristic for $p$
within $\mathcal{L}_{X}$, for all $X\in\mathsf{Ltime\text{-}spectrum}$ and
$p\in P$.

###### Proof.

According to Proposition 1(i), Theorem 6, and Definition 9, it suffices to
show, for all $X\in\mathsf{Ltime\text{-}spectrum}$ and $p\in P$, that
$\llbracket\bigwedge_{\psi\in\mathcal{B}_{X}(p)}\psi\rrbracket=\\{p^{\prime}\in
P\mid X(p)\subseteq X(p^{\prime})\\}$.

In order to show the inclusion $\\{p^{\prime}\in P\mid X(p)\subseteq
X(p^{\prime})\\}\subseteq\llbracket\bigwedge_{\psi\in\mathcal{B}_{X}(p)}\psi\rrbracket$,
let $p^{\prime}\in P$ be such that $X(p)\subseteq X(p^{\prime})$. By
Proposition 16 ((a) $\Rightarrow$ (b)), we have $X^{\mathit{fin}}(p)\subseteq
X^{\mathit{fin}}(p^{\prime})$. We show that
$p^{\prime}\in\llbracket\psi\rrbracket$ for all $\psi\in\mathcal{B}_{X}(p)$.
To this end, consider a generic element $\psi$ of $\mathcal{B}_{X}(p)$, which
means that $\psi=\mathit{formula}_{X}(x)$ for some $x\in
X^{\mathit{fin}}(p)\subseteq X(p)\subseteq X(p^{\prime})$. By Proposition 17
(left-to-right direction), we have
$p^{\prime}\in\llbracket\mathit{formula}_{X}(x)\rrbracket=\llbracket\psi\rrbracket$.
Since $\psi$ is a generic element of $\mathcal{B}_{X}(p)$, the claim follows.

Let us turn now to the converse inclusion. Let $p^{\prime}\in P$ be such that
$p^{\prime}\in\llbracket\psi\rrbracket$ for all $\psi\in\mathcal{B}_{X}(p)$,
which means $p^{\prime}\in\llbracket\mathit{formula}_{X}(x)\rrbracket$ for all
$x\in X^{\mathit{fin}}(p)$. By Proposition 17 (right-to-left direction), it
holds that $x\in X(p^{\prime})$ for all $x\in X^{\mathit{fin}}(p)$, that is,
$X^{\mathit{fin}}(p)\subseteq X(p^{\prime})$. By Proposition 16 ((c)
$\Rightarrow$ (a)), we have $X(p)\subseteq X(p^{\prime})$, and we are done. ∎