# First-Order Modal $\xi$-Calculus: Application and Bisimulation

Xinyu Wang

This paper proposes first-order modal $\xi$-calculus as well as genealogical
Kripke models. Inspired by modal $\mu$-calculus, first-order modal
$\xi$-calculus takes a quite similar form and extends its inductive
expressivity onto a different dimension. We elaborate on several vivid
examples that demonstrate this logic’s profound utility, especially for
depicting genealogy of concurrent computer processes. Bisimulation notion for
the logic has also been thoroughly examined.

Keywords first-order modal logic, modal $\mu$-calculus, Kripke model,
bisimulation, concurrency.

##  1 Introduction

Modal $\mu$-calculus, first proposed by Kozen in [17, 18], has been well known
among modal logicians. Equipped with notations similar to $\lambda$-calculus
[2], modal $\mu$-calculus serves as an extremely expressive yet still
decidable language (in fact EXPTIME-complete, cf. [7, 8]) that is able to
cover a wide range of variations of modal logic, especially for those study
fields which are tightly related to theoretical computer science, such as
temporal logic [23], propositional dynamic logic [24] as well as finite model
theory [12].

Rigidly speaking, semantics of modal $\mu$-calculus is commonly defined via
Tarski’s fixed-point theorem, cf. [4]. However intuitively, e.g., consider the
following modal $\mu$-calculus formula $\nu Z.\varphi\land[a]Z$, where $\nu$
is the dual of $\mu$. Here, what this $\nu Z.$ operator actually does is
assigning the rest part of the formula, namely $\varphi\land[a]Z$, to a
formula variable $Z$. Hence, the subformula $\varphi\land[a]Z$ is now able to
talk about itself via this formula variable $Z$. Through such self-reference,
our “core” formula $\varphi$ gets recursively “passed down” along the binary
relation $R_{a}$, so the original formula $\nu Z.\varphi\land[a]Z$ intuitively
says that $\varphi$ is true along every $R_{a}$-path. So far so good. Then
quite naturally, if we regard the binary relation $R_{a}$ as a horizontal
dimension in our Kripke model, we may also wonder whether this core formula
$\varphi$ can similarly be passed down recursively along other types of routes
in the model, e.g., on a vertical dimension? Actually our answer is yes, and
in parallel with modal $\mu$-calculus, we would like to call this novel kind
of modal logic as modal $\xi$-calculus.

So after all, where lies this another vertical dimension in modal
$\xi$-calculus? Let us turn our attention to first-order modal logic, where we
are able to discover another natural hierarchy, namely between the whole
Kripke model $\mathcal{M}$ itself and any element $a$ that belongs to the
(constant) domain of $\mathcal{M}$. We may also note that, e.g., there exists
arbitrary unary predicate $P$ so that $Pa$ forms an atomic formula of normal
first-order modal logic, but surely, it will be much better if such unary
predicates can be intrinsically constructed, rather than extrinsically
designated as extra symbol like $P$. Thus, what if $a$ is a Kripke model as
well, exactly the same type as $\mathcal{M}$ so that the hierarchy between
$\mathcal{M}$ and $a$ is truly a well-defined vertical dimension, and more
importantly, any formula can also be evaluated in the model $a$ just as in the
model $\mathcal{M}$ so that a formula itself can simply act like an unary
operator! Moreover, since now $a$ is the same type of Kripke model like
$\mathcal{M}$, then just as $\mathcal{M}$ possesses a domain which contains
$a$, of course $a$ also possesses its own domain, and once again, any element
in $a$’s domain is also the same type of Kripke model. Through such recursion,
a tree-like vertical genealogy gets established among a bunch of Kripke
models, and so we call this type of Kripke model as genealogical Kripke model.
Furthermore, since now any formula acts like an unary predicate, then just as
modal $\mu$-calculus, once a formula is equipped with the ability to talk
about itself, it can similarly get passed down recursively on the vertical
dimension, namely along a sequence like $a\in\text{\rm dom}(\mathcal{M})$,
$a^{\prime}\in\text{\rm dom}(a)$, $\cdots$. Thus more precisely, we call our
logic as first-order modal $\xi$-calculus, abbreviated as FOMC. For new
notations that we adopt, loosely speaking, if $\varphi$ is an FOMC-formula,
then adding a pair of question marks around it produces an unary predicate as
$\text{\rm?`}\varphi\text{\rm?}$, hence $\text{\rm?`}\varphi\text{\rm?}a$ is
also an FOMC-formula with a structure parallel to that of $Pa$. Also, we
introduce the $\xi X.$ operator as $\xi X.\varphi$, very similar to modal
$\mu$-calculus.

Importantly, here may we provide a few useful tips for readers to follow this
paper more smoothly. In fact, no matter how detailedly we manage to explain
our naïve intuitions behind first-order modal $\xi$-calculus and genealogical
Kripke models, instinctive inaccuracy of natural language might still present
obstacles toward full comprehension. Therefore, readers are strongly
recommended not only to carefully digest all the crucial definitions in
Section 2, but also to frequently take some preview on those vivid examples in
Section 3, which will certainly help to navigate readers’ understanding
through intuitive pictures. Generally speaking, although the formal definition
may seem a little complex at first, once having completely understood, readers
will certainly agree that first-order modal $\xi$-calculus is nothing but just
a quite natural mathematical generalization of common modal $\mu$-calculus.

Speaking of practical application, we firstly have to determine how to
interpret genealogical Kripke models with suitable realistic meaning.
Probably, computer scientists feel it tempting to interpret a model
$\mathcal{M}$ as a process on a modern computer, $\mathcal{M}$’s (possibly
empty) domain contains all of its children processes, and every child process
is again represented by a genealogical Kripke model. This is exactly how a
modern computer operating system (such as Linux) commonly handles multiple
concurrent processes: on the one hand, there exists a genealogical hierarchy
between the parent process and the child process; on the other hand, every
process is technically represented by the same data structure and thus
applicable to all the same properties, namely in logic, all the same unary
predicates. While a lot of other interpretations can also fit into our first-
order modal $\xi$-calculus pretty well, within this paper we shall mainly
focus on interpreting as computer processes to help to illustrate our logic
more vividly. Meanwhile, the other horizontal dimension, namely the binary
relation $R$ in a genealogical Kripke model, is usually interpreted as
temporal logic’s chronological future for computer processes, and thus often
assumed to be reflexive and transitive [11]. Nevertheless, it may not always
be so under every condition, and hence for the most general purpose we choose
not to presume any restriction on $R$.

The rest of this paper is organized as the following. Section 2 strictly
defines mathematical preliminaries. Section 3 provides several concrete
examples to illustrate powerful practical usage of first-order modal
$\xi$-calculus. Section 4 studies bisimulation of the logic. Section 5
concludes this paper and proposes some feasible directions for future work.

##  2 Preliminaries

This section defines the necessary preliminaries. Should readers find any part
of the content difficult to understand, referring to some examples in Section
3 as a vivid assistance is strongly suggested.

Also, paragraphs started with a $\bigstar$ mark contain important
clarifications. Honestly speaking, this paper indeed includes a handful of
concepts and definitions about which readers might be vulnerable to getting
confused, perhaps either because the formal definition seems a bit complex
(but actually quite natural and intuitive once fully understood), or because
it is somewhat different from the ordinary definition (while noticing such
subtle difference may prove to be crucial for correct understanding). Thus
those clarifications are particularly prepared with very careful elaboration,
just in case of various kinds of possible confusion, and so readers are barely
encouraged to simply neglect them but had better read those clarifications as
one organic, comprehensive part of this entire paper.

######  Definition 1 (Formula in Language FOMC).

Given a countable set of propositional letters $\mathbf{P}$, and a countable
set of constant symbols $\mathbf{C}$, well formed formula $\varphi$ in
Language FOMC is recursively defined as the following BNF:

$\displaystyle\varphi::=X\mid\top\mid
p\mid\text{\rm?`}\varphi\text{\rm?}x\mid\text{\rm?`}\varphi\text{\rm?}c\mid\neg\varphi\mid(\varphi\land\varphi)\mid\Box\varphi\mid\forall
x.\varphi\mid\xi X.\varphi$

where $p\in\mathbf{P}$, $c\in\mathbf{C}$, $x$ stands for arbitrary model
variable and $X$ stands for arbitrary formula variable. In the rest of this
paper, we will follow this routine to use lowercase letters for model
variables and uppercase letters for formula variables.

$\perp$, $\lor$, $\to$, $\Diamond$ and $\exists$ are abbreviations defined as
common.

From Definition 1 we can tell that in Language FOMC, there exist two distinct
kinds of variables: model variables like $x,y$ and formula variables like
$X,Y$. There can also exist some constant symbols like $c,d\in\mathbf{C}$,
which may be called as model constants as well. Thus intuitively, as their
names literally suggest, a model variable or a model constant stands for a
model (precisely speaking a genealogical Kripke model, introduced later in
Definition 6), while a formula variable represents an FOMC-formula. Readers
will gradually become aware of all these notations’ respective indispensable
function in our logic.

For now let us firstly pay our attention to one issue: usually in logic,
variables in a formula may be either free or bound, and so are they here, too.
Roughly speaking in an FOMC-formula, a $\forall x.$ operator binds a model
variable $x$, while a $\xi X.$ operator (plus some extra condition) binds a
formula variable $X$. The formal definition is as the following:

######  Definition 2 (Free Variable and Bound Variable).

In any given FOMC-formula $\varphi$, a model variable $x$ either is bound by
the nearest $\forall x.$ whose scope includes this $x$; otherwise it is a free
model variable, namely, not within any $\forall x.$’s scope.

In any given FOMC-formula $\varphi$, a formula variable $X$ either is bound,
iff it is firstly within the scope of the nearest ¿? pair, and then bound by
the nearest $\xi X.$ whose scope includes this ¿? pair; otherwise it is a free
formula variable.

######  Example 3.

For a model variable $x$, whether free or bound is just like ordinary first
order logic, e.g., $x$ is bound in FOMC-formula $\forall
x.\text{\rm?`}p\text{\rm?}x$ and is free in FOMC-formula
$\text{\rm?`}p\text{\rm?}x$.

For a formula variables $X$, however, it must firstly be within the scope of a
¿? pair, after which could it be bound by some $\xi X.$ whose scope includes
that ¿? pair. This “extra condition” requires very careful attention, e.g.,
$X$ is bound in FOMC-formula $\xi X.\text{\rm?`}X\text{\rm?}c$ but is free in
FOMC-formula $\xi X.X$ because it is not within the scope of any ¿? pair.

nothing

$\bigstar$ Important Clarification Note that from Definition 2, a bound
formula variable is not entirely similar to an ordinary bound model variable,
e.g., from Example 3 we know that $\xi X.X$ does not bind its $X$.
Intuitively, such stipulation is meant to ensure that circular evaluation will
not occur when we later define semantics in Definition 10.

Together with the concept of free and bound variables arises the concept of
logic sentences. The general idea as such is still quite common: a sentence,
also called as a closed formula, is usually defined as a formula without any
free variables. However here due to somewhat tangled nature of recursion in
FOMC-formulae, only after undergoing very careful analysis can we finally
settle down to the following precise conditions in the definition of FOMC-
sentences:

######  Definition 4 (Sentence in Language FOMC).

An FOMC-formula $\varphi$ is an FOMC-sentence, iff all of the following
conditions hold:

  * •

$\varphi$ contains neither free model variables nor free formula variables.

  * •

If $\xi X.\psi$ is a subformula of $\varphi$, then $\xi X.\psi$ contains
neither free model variables nor free formula variables.

  * •

If $\text{\rm?`}\psi\text{\rm?}x$ or $\text{\rm?`}\psi\text{\rm?}c$ is a
subformula of $\varphi$, then $\psi$ contains no free model variables.

######  Remark 5.

Actually, the formal logical language studied in this paper is FOMC-sentences
in Definition 4, rather than FOMC-formulae in Definition 1. Essentially,
Definition 1 defines FOMC-formulae by BNF, only as nothing more than an
auxiliary notion. Those extra restrictions in Definition 4 will later on
ensure a well-defined semantics (cf. Theorem 12), which cannot just be
naturally generalized onto all FOMC-formulae.

Next, let us turn to the semantical aspect and define genealogical Kripke
models, with respect to which semantics of FOMC-sentences will be interpreted:

######  Definition 6 (Genealogical Kripke Model).

A genealogical Kripke model $\mathcal{M}$ is recursively defined as a tuple
$(S_{\mathcal{M}},R_{\mathcal{M}},V_{\mathcal{M}},N_{\mathcal{M}},I_{\mathcal{M}},T_{\mathcal{M}})$
where:

  * •

$S_{\mathcal{M}}$ is a non-empty set of possible worlds.

  * •

$R_{\mathcal{M}}\subseteq S_{\mathcal{M}}\times S_{\mathcal{M}}$ is a binary
relation on $S_{\mathcal{M}}$.

  * •

$V_{\mathcal{M}}:\mathbf{P}\to\mathcal{P}(S_{\mathcal{M}})$ is a valuation
function.

  * •

$N_{\mathcal{M}}$ is a set of genealogical Kripke models.

  * •

$I_{\mathcal{M}}:S_{\mathcal{M}}\times\mathbf{C}\to N_{\mathcal{M}}$ is a
partial assignment function.

  * •

$T_{\mathcal{M}}:S_{\mathcal{M}}\times
N_{\mathcal{M}}\to\bigcup\limits_{\mathcal{N}\in
N_{\mathcal{M}}}S_{\mathcal{N}}$ is a function such that for any possible
world $s\in S_{\mathcal{M}}$ and any model $\mathcal{N}\in N_{\mathcal{M}}$,
$T_{\mathcal{M}}(s,\mathcal{N})\in S_{\mathcal{N}}$.

When the model $\mathcal{M}$ is clear from the context, we can omit
$\mathcal{M}$ in the subscript and hence denote the model $\mathcal{M}$ simply
as a tuple $(S,R,V,N,I,T)$.

In case of any misunderstanding about the above Definition 6, we would like to
present (a little longer) clarification as well as several technical remarks
right away, while elaboration on the intuitive interpretation of Definition 6
will soon follow after Remark 8.

nothing

$\bigstar$ Important Clarification In Definition 6, a genealogical Kripke
model $\mathcal{M}$ contains some part $N_{\mathcal{M}}$, which is again a set
of genealogical Kripke models. Hence Definition 6 is a recursive definition,
just like that a logic language is usually defined through BNF, and so by
Axiom of Regularity in set theory [16], circular inclusion is forbidden here
as well, therefore, we must have $\mathcal{M}\notin N_{\mathcal{M}}$. Note
that in fact $N$ can be $\varnothing$, which exactly forms the basic case of
this inductive definition; in other words, $N$ is automatically guaranteed to
reach the $\varnothing$ dead point after a finite depth of generations, thus
genealogical Kripke models are always well-founded and infinite downward
chains will never occur.

Just in case of any likely confusion, here may we emphasize over this issue
once again. Especially, readers familiar with modal $\mu$-calculus might
naturally think that it is also possible for a genealogical Kripke model here
to have itself as one of its own children models, namely $\mathcal{M}\in
N_{\mathcal{M}}$; or more generally, to contain an infinite downward chain
$\cdots\mathcal{M}_{3}\in N_{\mathcal{M}_{2}}$, $\mathcal{M}_{2}\in
N_{\mathcal{M}_{1}}$, $\mathcal{M}_{1}\in N_{\mathcal{M}}$. Definitely, we
agree that these situations are both conceptually conceivable and
mathematically manageable, nonetheless, they simply do not appear here because
a recursive definition in ZFC automatically rules them out. Such “restriction”
is essentially a direct result of the recursive nature of Definition 6, and so
actually, no extra restriction at all needs to be added into the definition.
Readers are suggested to draw an analogy from the recursive BNF in Definition
1, so that readers can also understand in a similar way, in Definition 6 we
have made neither fault nor negligence. Finally for better explicitness,
though a formal proof is omitted (which can be found in any standard textbook
on set theory, e.g., [19]), we would like to rigorously summarize our main
point in the above discussion as the following theorem:

######  Theorem 7.

There does not exist an infinite downward chain of genealogical Kripke models
$\mathcal{M}_{i}$, where $i\in\omega$, such that $\forall i\in\omega$,
$\mathcal{M}_{i+1}\in N_{\mathcal{M}_{i}}$.

######  Remark 8.

The following are several other minor points concerning Definition 6, to which
readers are suggested to pay attention as well:

  * •

$\mathcal{N}$ and $N$ are different: the former denotes some model, while the
latter denotes some part of a model, which is a set of (other) models.

  * •

On the one hand, $I$ is generally a partial function, i.e., it is not
guaranteed to be total. In fact, since the codomain $N$ may be empty,
sometimes $I$ is simply impossible to be total.

  * •

On the other hand, $T$ is a total function, and when its codomain is empty, it
is easy to see that its domain must also be empty, so this is not a problem.

Having ensured that mathematically, readers can grasp a correct understanding
about Definition 6, we next provide a brief intuitive explanation on what
every part of a genealogical Kripke model stands for. Assume that we interpret
the genealogical Kripke model $\mathcal{M}$ as a computer process, then
$N_{\mathcal{M}}$ represents all its children processes, and at every possible
state $s\in S_{\mathcal{M}}$ of the parent process $\mathcal{M}$, for any
constant symbol $c\in\mathbf{C}$, $I_{\mathcal{M}}(s,c)\in N_{\mathcal{M}}$
(if defined) selects a specific child process; for any child process
$\mathcal{N}\in N_{\mathcal{M}}$, $T_{\mathcal{M}}(s,\mathcal{N})\in
S_{\mathcal{N}}$ designates in which state this child process $\mathcal{N}$
currently is. Therefore fixing a constant symbol $c\in\mathbf{C}$, its
interpretation $I_{\mathcal{M}}(s,c)$ still depends on $s$ and so may vary
from possible world to possible world, thus even though we decide to call $c$
as a model “constant”, readers should keep aware that $c$ is after all a local
constant rather than a global one. (Of course if needed, we are also able to
easily introduce another notion of global model constants.)

Anyway, since as of data structure, both the parent process $\mathcal{M}$ and
the child process $\mathcal{N}$ are the same type of object, namely a process,
it makes perfect sense that both of them are represented by a genealogical
Kripke model so that they share exactly the same mathematical form. (By the
way, $\mathcal{N}$ may also have its own children processes as well, which are
therefore $\mathcal{M}$’s grandchildren processes.) Here then arises a quite
natural question, however: should there be any correlation between the parent
process’s current state $s\in S_{\mathcal{M}}$ and the child process’s current
state $T_{\mathcal{M}}(s,\mathcal{N})\in S_{\mathcal{N}}$, where
$\mathcal{N}\in N_{\mathcal{M}}$? We think the answer depends: in some cases
it is quite plausible to assume such kind of relation, while in some other
cases both the parent process and the children processes can act
independently. Therefore, for the most general purpose, here we choose not to
put any extra restrictions upon the relation between the parent process and
the children processes.

We move on to define semantics of FOMC-sentences. To start with, we define
interpretations both for any model variable $x$ and for any formula variable
$X$:

######  Definition 9 (Interpretation).

An interpretation $i$ is a (partial) function. For any $(k,v)\in i$,
intuitively, $i$ interprets the key $k$ as the value $v$. We also denote:

$\displaystyle
i[k:=v]=\left\\{\begin{array}[]{ll}i\cup\\{(k,v)\\},&\quad\text{if }i(k)\text{
is undefined}\\\
(i\setminus\\{(k,v^{\prime})\\})\cup\\{(k,v)\\},&\quad\text{if
}i(k)=v^{\prime},\text{ namely }(k,v^{\prime})\in i\end{array}\right.$

######  Definition 10 (Semantics).

Given a genealogical Kripke model $\mathcal{M}$ and an FOMC-sentence
$\varphi$, valuation of $\varphi$ over $\mathcal{M}$ (with two interpretations
$i$ and $j$, the first one for model variables while the second one for
formula variables, and initially $i=j=\varnothing$) is recursively defined as
$\llbracket\varphi\rrbracket^{\mathcal{M}}_{\varnothing,\varnothing}\subseteq
S_{\mathcal{M}}$ by the following:

$\displaystyle\llbracket X\rrbracket^{\mathcal{M}}_{i,j}=$
$\displaystyle\llbracket\psi\rrbracket^{\mathcal{M}}_{i,j},\text{ where
}j(X)=\psi$ $\displaystyle\llbracket\top\rrbracket^{\mathcal{M}}_{i,j}=$
$\displaystyle S_{\mathcal{M}}$ $\displaystyle\llbracket
p\rrbracket^{\mathcal{M}}_{i,j}=$ $\displaystyle V_{\mathcal{M}}(p)$
$\displaystyle\llbracket\text{\rm?`}\varphi\text{\rm?}x\rrbracket^{\mathcal{M}}_{i,j}=$
$\displaystyle\\{s\in S_{\mathcal{M}}\mid
T_{\mathcal{M}}(s,\mathcal{N})\in\llbracket\varphi\rrbracket^{\mathcal{N}}_{\varnothing,j}\\},\text{
where }i(x)=\mathcal{N}$
$\displaystyle\llbracket\text{\rm?`}\varphi\text{\rm?}c\rrbracket^{\mathcal{M}}_{i,j}=$
$\displaystyle\\{s\in S_{\mathcal{M}}\mid I_{\mathcal{M}}(s,c)\text{ is
defined and
}T_{\mathcal{M}}(s,I_{\mathcal{M}}(s,c))\in\llbracket\varphi\rrbracket^{I_{\mathcal{M}}(s,c)}_{\varnothing,j}\\}$
$\displaystyle\llbracket\neg\varphi\rrbracket^{\mathcal{M}}_{i,j}=$
$\displaystyle
S_{\mathcal{M}}\setminus\llbracket\varphi\rrbracket^{\mathcal{M}}_{i,j}$
$\displaystyle\llbracket\varphi\land\psi\rrbracket^{\mathcal{M}}_{i,j}=$
$\displaystyle\llbracket\varphi\rrbracket^{\mathcal{M}}_{i,j}\cap\llbracket\psi\rrbracket^{\mathcal{M}}_{i,j}$
$\displaystyle\llbracket\Box\varphi\rrbracket^{\mathcal{M}}_{i,j}=$
$\displaystyle\\{s\in S_{\mathcal{M}}\mid\text{for all }t\in
S_{\mathcal{M}}\text{ such that
}sR_{\mathcal{M}}t,t\in\llbracket\varphi\rrbracket^{\mathcal{M}}_{i,j}\\}$
$\displaystyle\llbracket\forall x.\varphi\rrbracket^{\mathcal{M}}_{i,j}=$
$\displaystyle S_{\mathcal{M}}\cap(\bigcap_{\mathcal{N}\in
N_{\mathcal{M}}}\llbracket\varphi\rrbracket^{\mathcal{M}}_{i[x:=\mathcal{N}],j})$
$\displaystyle\llbracket\xi X.\varphi\rrbracket^{\mathcal{M}}_{i,j}=$
$\displaystyle\llbracket\varphi\rrbracket^{\mathcal{M}}_{i,j[X:=\varphi]}$

For any genealogical Kripke model $\mathcal{M}$, any possible world $s\in
S_{\mathcal{M}}$ and any FOMC-sentence $\varphi$, we denote
$\mathcal{M},s\vDash\varphi$ iff
$s\in\llbracket\varphi\rrbracket^{\mathcal{M}}_{\varnothing,\varnothing}$.

Before proving soundness of Definition 10 in Theorem 12, we would like to
elaborate further on what on earth this definition of semantics intuitively
captures:

  * •

For $\llbracket X\rrbracket^{\mathcal{M}}_{i,j}$, if $j$ interprets the
formula variable $X$ as $\psi$, then valuation of $X$ just equals to valuation
of $\psi$. Later on we will show that in such a case $j(X)$ is guaranteed to
be defined.

  * •

For $\llbracket\text{\rm?`}\varphi\text{\rm?}x\rrbracket^{\mathcal{M}}_{i,j}$,
the idea is to treat $\text{\rm?`}\varphi\text{\rm?}$ as a unary predicate,
hence if $i$ interprets the model variable $x$ as some child model
$\mathcal{N}\in N_{\mathcal{M}}$, then for any parent model $\mathcal{M}$’s
state $s\in S_{\mathcal{M}}$, $\text{\rm?`}\varphi\text{\rm?}x$ is true at
$\mathcal{M},s$ iff $\varphi$ is true at the child model $\mathcal{N}$’s
current state $T_{\mathcal{M}}(s,\mathcal{N})$, namely
$T_{\mathcal{M}}(s,\mathcal{N})\in\llbracket\varphi\rrbracket^{\mathcal{N}}_{\varnothing,j}$.
Note that the interpretation $j$ for formula variables gets inherited but the
interpretation $i$ for model variables is reset to $\varnothing$, because
between two models $\mathcal{M}$ and $\mathcal{N}$, their language FOMC keeps
the same but their domains $N_{\mathcal{M}}$ and $N_{\mathcal{N}}$ are
separate. Later on we will also show that in such a case $i(x)$ is guaranteed
to be defined.

  * •

For $\llbracket\text{\rm?`}\varphi\text{\rm?}c\rrbracket^{\mathcal{M}}_{i,j}$,
we simply attempt to interpret the constant symbol $c$ as a child model
$I_{\mathcal{M}}(s,c)\in N_{\mathcal{M}}$ and then we can follow the similar
idea as above.

  * •

For $\llbracket\forall x.\varphi\rrbracket^{\mathcal{M}}_{i,j}$, all possible
interpretations for the model variable $x$ as some child model $\mathcal{N}\in
N_{\mathcal{M}}$ gets considered and added into the interpretation $i$,
respectively. Then the compound universal formula values as the interaction of
all possibilities, also together intersected with $S_{\mathcal{M}}$ just in
case that $N_{\mathcal{M}}$ may be $\varnothing$.

  * •

For $\llbracket\xi X.\varphi\rrbracket^{\mathcal{M}}_{i,j}$, just like modal
$\mu$-calculus, this $\xi X.$ operator here intuitively assigns the following
formula $\varphi$ to the formula variable $X$, thus this interpretation gets
added into $j$.

nothing

$\bigstar$ Important Clarification Readers familiar with semantics of modal
$\mu$-calculus may wonder, why we have not made use of Tarski’s fixed-point
theorem in the definition of semantics, just as modal $\mu$-calculus normally
does. The reason is that from Theorem 7, we already know that a genealogical
Kripke model can only have a finite depth of generations, hence the fixed
point can simply be found by induction through finitely many steps. We also
point out that unlike modal $\mu$-calculus, here $\varphi$ in $\xi X.\varphi$
does not have to be positive, either. Despite these minor technical
differences, after all, our first-order modal $\xi$-calculus indeed
generalizes the ordinary modal $\mu$-calculus onto the vertical dimension
through keeping the very core idea totally intact. Readers who may still
possess doubts about this point hitherto are extremely eagerly suggested, in
any case, to carefully reread Section 1 — the very beginning introductory part
— and especially the first several paragraphs, so as to amply convince
themselves with quite intuitive justification.

######  Remark 11.

Another point we would like to explain about the semantics in Definition 10
is, why we always designate that
$\mathcal{M},s\nvDash\text{\rm?`}\varphi\text{\rm?}c$ when
$I_{\mathcal{M}}(s,c)$ is not defined. This might simply seem like our
factitious choice, but actually we have some good reasons to justify it. Let
us interpret genealogical Kripke models as computer processes, then
$I_{\mathcal{M}}(s,c)$ is essentially a process pointer that either points to
one of $\mathcal{M}$’s children processes $\mathcal{N}\in N_{\mathcal{M}}$, or
is the NULL pointer, which can be regarded as pointing to certain fixed NULL
process. Therefore if $I_{\mathcal{M}}(s,c)$ is undefined, then for any fixed
FOMC-formula $\varphi$, we should anticipate either always
$s\in\llbracket\text{\rm?`}\varphi\text{\rm?}c\rrbracket^{\mathcal{M}}_{i,j}$
or always
$s\notin\llbracket\text{\rm?`}\varphi\text{\rm?}c\rrbracket^{\mathcal{M}}_{i,j}$,
i.e., depending on how this default NULL process is designed in advance but
not depending on the specific current state $s\in S_{\mathcal{M}}$. Here we
just arbitrarily designate that
$s\notin\llbracket\text{\rm?`}\varphi\text{\rm?}c\rrbracket^{\mathcal{M}}_{i,j}$
for every $\varphi$, which does not really cause an issue, because the
expected behavior of FOMC-formula $\text{\rm?`}\varphi\text{\rm?}c$ when
letting
$s\in\llbracket\text{\rm?`}\varphi\text{\rm?}c\rrbracket^{\mathcal{M}}_{i,j}$
can be exactly simulated by FOMC-formula
$\neg\text{\rm?`}\neg\varphi\text{\rm?}c$ when letting
$s\notin\llbracket\text{\rm?`}\neg\varphi\text{\rm?}c\rrbracket^{\mathcal{M}}_{i,j}$.

At last, before finishing this section of mathematical preliminaries, we have
to complete the indispensable task of proving the following Theorem 12,
showing that our semantics is surely well defined with respect to FOMC-
sentences.

######  Theorem 12.

Semantics in Definition 10 is well defined.

###### Proof.

For any FOMC-sentence $\varphi$, we recursively evaluate
$\llbracket\varphi\rrbracket^{\mathcal{M}}_{\varnothing,\varnothing}$.

On the one hand, we claim that this evaluating process always goes on well.
Namely, we have to make sure that whenever necessary, $i$ and $j$ will always
provide interpretation for any model variable $x$ and any formula variable
$X$, respectively. This feature is guaranteed by conditions in Definition 4,
intuitively as the following:

  * •

$\varphi$ contains neither free model variables nor free formula variables.
This clause is just the ordinary closed-formula condition.

  * •

    1. 1.

If $\xi X.\psi$ is a subformula of $\varphi$, then $\xi X.\psi$ contains no
free model variables, or equivalently, $\psi$ contains no free model
variables. This half clause is needed because $X$ may appear in a subformula
of $\psi$ as $\text{\rm?`}\cdots X\cdots\text{\rm?}x$ or $\text{\rm?`}\cdots
X\cdots\text{\rm?}c$, namely, to be passed down to a child model. As explained
by the intuition of semantics defined in Definition 10, only interpretation
for formula variables gets inherited by the child model while interpretation
for model variables is reset to $\varnothing$, thus, $\psi$ should not contain
any free model variables.

    2. 2.

If $\xi X.\psi$ is a subformula of $\varphi$, then $\xi X.\psi$ contains no
free formula variables, either. This half clause will become of use later on,
i.e., in the latter on-the-other-hand part.

  * •

If $\text{\rm?`}\psi\text{\rm?}x$ or $\text{\rm?`}\psi\text{\rm?}c$ is a
subformula of $\varphi$, then $\psi$ contains no free model variables, due to
the same intuitive reason as the above clause.

Based on the above intuitive intentions of all the clauses in Definition 4, it
then immediately becomes just self-evident that $i(x)$ and $j(X)$ will always
be properly defined whenever in need during the whole evaluating process.

On the other hand, we claim that this evaluating process will eventually
terminate instead of going on infinitely. In fact, the only possible
intermediate step when the current subformula may become more complicated is
rewriting $\llbracket X\rrbracket^{\mathcal{N}}_{i,j}$ to
$\llbracket\psi\rrbracket^{\mathcal{N}}_{i,j}$. This indicates $j(X)=\psi$, so
$\xi X.\psi$ is a subformula of $\varphi$, and since $\varphi$ is an FOMC-
sentence, $\xi X.\psi$ contains no free formula variables. Therefore,
appearance of any formula variable $Y$ in $\psi$ must be within the scope of a
¿? pair, and thus if we continue evaluating
$\llbracket\psi\rrbracket^{\mathcal{N}}_{i,j}$ and later on encounter another
intermediate stage $\llbracket
Y\rrbracket^{\mathcal{N}^{\prime}}_{i^{\prime},j^{\prime}}$, then
$\mathcal{N}^{\prime}$ must be a direct descendant of $\mathcal{N}$. By
Theorem 7, $\mathcal{N}^{\prime}\neq\mathcal{N}$ and the maximal depth of
generations in model $\mathcal{M}$ is finite. Not only do we need finite steps
to descend from $\mathcal{N}$ to one of its descendants
$\mathcal{N}^{\prime}$, but also we have finite depth of generations to
descend, namely, neither circle nor infinite chain will occur and thus
recursively evaluating
$\llbracket\varphi\rrbracket^{\mathcal{M}}_{\varnothing,\varnothing}$ is well
founded. ∎

##  3 Examples

We have seen that theoretically, first-order modal $\xi$-calculus is just a
very natural mathematical generalization of horizontal modal $\mu$-calculus
onto the other vertical dimension. While practically, first-order modal
$\xi$-calculus can depict the recursive structure of computer processes in a
genealogical Kripke model, which will be demonstrated by a series of typical
examples in the following that cover some of the most interesting topics in
concurrency control [5]. Starting easily, we first reveal some simple examples
without the $\xi X.$ operator.

nothing

$\bigstar$ Important Clarification As having been introduced in Section 1, now
the binary relation $R$ is interpreted as temporal logic and thus assumed to
be reflexive and transitive [13]. Therefore for neatness, when drawing the
graph for a model we may omit some $R$ relation arrows, but readers should
always be aware that the actual relation $R$ must be understood as the
reflexive and transitive closure.

######  Example 13.

As the following graph shows, the parent process $\mathcal{M}$ possesses two
children processes $\mathcal{N}_{1}$ and $\mathcal{N}_{2}$, with one
propositional letter $r$ representing that a process is currently running and
one constant symbol $c$ that points to the currently running child process. We
have $\mathcal{M},s_{0}\vDash\Box\exists
x.\text{\rm?`}r\text{\rm?}x\land\neg\exists
x.\Box\text{\rm?`}r\text{\rm?}x\land\Box\text{\rm?`}r\text{\rm?}c$, which
intuitively reads as: there always exists some running child process, but no
single child process is running forever, and it is always true that the
currently running child process is currently running. Divergence between the
first two clauses is well known in first-order modal logic as de dicto vs. de
re [15], while the last clause simply claims something trivial under our
present interpretation.

|
---|---
$\textstyle{\mathcal{M}:}$ $s_{0}$ $c:=\mathcal{N}_{1}$ $s_{1}$
$c:=\mathcal{N}_{2}$ $s_{2}$ $c:=\mathcal{N}_{1}$
$\textstyle{\mathcal{N}_{1},running\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\mathcal{N}_{2},stopped\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\mathcal{N}_{1},stopped\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\mathcal{N}_{2},running\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\mathcal{N}_{1},running\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\mathcal{N}_{2},dead\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\mathcal{N}_{1}:}$
$stopped$ $\neg r$ $running$ $r$ $dead$ $\neg r$
$\textstyle{\mathcal{N}_{2}:}$ $stopped$ $\neg r$ $running$ $r$ $dead$ $\neg
r$

######  Example 14.

As the following graph shows, $\mathcal{N}_{1}$ and $\mathcal{N}_{2}$ are two
children processes that require both resources $a$ and $b$ to run.
$\mathcal{N}_{1}$ asks for resource $a$ first while $\mathcal{N}_{2}$ does the
opposite, hence in theory we can imagine that a dead lock easily occurs when
$\mathcal{N}_{1}$ occupies resource $a$ and $\mathcal{N}_{2}$ occupies
resource $b$. Nonetheless, in this actual case, $\mathcal{N}_{1}$ and
$\mathcal{N}_{2}$’s common parent process $\mathcal{M}$ manages to forbid
certain combinations of states so as to prevent any possible dead lock.
Therefore we have $\mathcal{M},s_{0}\vDash\exists x.\exists
y.(\text{\rm?`}\Diamond(a\land\neg
b)\text{\rm?}x\land\text{\rm?`}\Diamond(\neg a\land
b)\text{\rm?}y)\land\neg\Diamond\exists x.\exists y.(\text{\rm?`}a\land\neg
b\text{\rm?}x\land\text{\rm?`}\neg a\land b\text{\rm?}y)$, namely, dead lock
has been avoided under the parent process $\mathcal{M}$’s supervision.

|
---|---
$\textstyle{\mathcal{N}_{1},stopped\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\mathcal{N}_{2},waiting\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\mathcal{N}_{1},stopped\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\mathcal{N}_{2},running\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{s_{3}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{s_{4}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\mathcal{M}:}$$\textstyle{s_{0}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{s_{1}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{s_{2}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\mathcal{N}_{1},stopped\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\mathcal{N}_{2},stopped\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\mathcal{N}_{1},waiting\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\mathcal{N}_{2},stopped\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\mathcal{N}_{1},running\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\mathcal{N}_{2},stopped\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\mathcal{N}_{1}:}$
$stopped$ $\neg a,\neg b$ $waiting$ $a,\neg b$ $running$ $a,b$
$\textstyle{\mathcal{N}_{2}:}$ $stopped$ $\neg a,\neg b$ $waiting$ $\neg a,b$
$running$ $a,b$

######  Remark 15.

From the examples above readers may have already noticed that actually,
genealogical Kripke models are constructed from an external omniscient
viewpoint, and we also implicitly assume that all the states of the child
process are completely transparent to the parent process. Therefore, the
parent process changes its state in accordance with the child process, even
when nothing has really changed in the parent process itself. Nevertheless, ¿?
pairs are still necessary for the parent process to query the states of its
children processes, and hence as a possible future research, by putting
restrictions on formulae we will then be able to limit the parent process’
knowledge about its children processes.

Next, we turn to a handful of more complicated examples, which clearly
demonstrate that in practical applications, the introduction of the $\xi X.$
operator enables the very same core formula to be passed among different
processes recursively.

######  Example 16.

As the following graph shows, process $\mathcal{M}$ is not running until
$s_{3}$ when its two children processes $\mathcal{N}_{1}$ and
$\mathcal{N}_{2}$ have both finished, and $\mathcal{N}_{1}$ again has a child
process $\mathcal{N}_{3}$ whose finish must be waited, too. Due to limit of
space here we only draw out one possible history of execution as the root
model $\mathcal{M}$. Anyway, we can see that there is always some process
running, which can be formulated as $\mathcal{M},s_{0}\vDash\Box\xi
X.(r\lor\exists x.\text{\rm?`}X\text{\rm?}x)$.

|
---|---
$\textstyle{\mathcal{N}_{1},stopped\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\mathcal{N}_{2},running\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\mathcal{N}_{1},dead\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\mathcal{N}_{2},dead\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\mathcal{M}:}$
$s_{0}$ $\neg r$ $s_{1}$ $\neg r$ $s_{2}$ $\neg r$ $s_{3}$ $r$
$\textstyle{\mathcal{N}_{1},waiting\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\mathcal{N}_{2},stopped\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\mathcal{N}_{1},running\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\mathcal{N}_{2},dead\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\mathcal{N}_{1}:}$
$pending$ $\neg r$ $waiting$ $\neg r$ $stopped$ $\neg r$ $running$ $r$ $dead$
$\neg r$
$\textstyle{\mathcal{N}_{3},stopped\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\mathcal{N}_{3},running\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\mathcal{N}_{3},dead\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\mathcal{N}_{3},dead\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\mathcal{N}_{3},dead\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\mathcal{N}_{2}:}$
$stopped$ $\neg r$ $running$ $r$ $dead$ $\neg r$
$\textstyle{\mathcal{N}_{3}:}$ $stopped$ $\neg r$ $running$ $r$ $dead$ $\neg
r$

######  Example 17.

We finally present several advanced examples of more complex formulae and
briefly explain their intuitive meanings, without providing sample graphs:

  * •

FOMC-sentence $\xi X.\forall x.\text{\rm?`}X\text{\rm?}x$ may look like
nonsense at first glance, but it is actually valid everywhere. In fact, it
simply reflects our assumption that there exists no circular nor infinite
genealogical hierarchy, namely, a formal expression of Theorem 7.

  * •

FOMC-sentence $\xi X.(\Box p\land\forall x.\text{\rm?`}\Diamond
X\text{\rm?}x)$ says that since the very beginning, the root process keeps to
have property $p$, and furthermore as time goes on, property $p$ gradually
diffuses down to the children processes layer by layer, so that eventually all
the descendant processes will get infected by property $p$. Undoubtedly, such
universal kind of spreading pattern — no matter this property $p$ is a
computer virus or anything else — simply happens everyday and everywhere in
our actual computers, network topology, and even human society.

  * •

FOMC-sentence $\xi X.(\Diamond\forall y.\text{\rm?`}\xi Y.(p\land\forall
z.\text{\rm?`}Y\text{\rm?}z)\text{\rm?}y\land\forall
x.\text{\rm?`}X\text{\rm?}x)$ says that for every process, there will be a
time when all its descendant processes possess property $p$, e.g., $p$
represents being a dead zombie process so that it can be cleaned up by its
parent process [25].

nothing

$\bigstar$ Important Clarification Until now, a variety of pragmatic examples
have been vividly exhibited, which should adequately convince readers of
first-order modal $\xi$-calculus’ robust universality. It hence does not look
likely that such a complex language with quite strong expressivity can be
interpreted by any simpler logic that is familiar to us. In order to justify
the above claim, a standard approach is to compare our first-order modal
$\xi$-calculus with some other well-known logic and to show that the former is
strictly more expressive. Such kind of work can definitely be carried out
without much difficulty, however honestly speaking, considering the rather
novel structure of genealogical Kripke models and the powerful expressivity
along with undecidability of first-order quantifiers, we simply think the
complexity of first-order modal $\xi$-calculus is so apparent that formal
mathematical comparison seems quite redundant.

Therefore after all, let us just informally reason a few more words on this
topic. Perhaps as one possible alternative to first-order modal
$\xi$-calculus, certain sort of multi-modal logic might be suggested, e.g.,
viewing the instantaneous parent-child relation between states of two
processes as a new modality while also introducing another global modality for
the $\forall x.$ quantifier. Such kind of multi-modal logic may capture a
decent fragment of first-order modal $\xi$-calculus, nonetheless as
illustrated in Example 13, the crucial de-dicto-de-re distinction is known to
be uniquely characteristic to first-order modal logic [9] and thus cannot get
expressed in any multi-modal logic without first-order quantifiers.

##  4 Bisimulation

As a quite powerful tool for studying modal logic, the concept of bisimulation
plays a particularly significant role over fields related to theoretical
computer science, such as process algebra [21]. In this section, we propose a
bisimulation notion for first-order modal $\xi$-calculus and prove the
bisimulation theorem in two directions, namely in one direction bisimulation
implies logical equivalence, and in the other direction logical equivalence
implies bisimulation under the Hennessy-Milner property [3].

######  Definition 18 (Pointed Genealogical Kripke Model).

A pointed genealogical Kripke model $\mathcal{M},s$ is a genealogical Kripke
model $\mathcal{M}$ with a fixed state $s\in S$.

The following Definition 19 provides the notion of bisimulation between two
pointed genealogical Kripke models. Before such formal mathematical definition
comes, however, we would like to depict an intuitive picture. Now that first-
order-like Kripke models are dealt with, say two models $\mathcal{M}$ and
$\mathcal{N}$ are bisimilar, then we not only have to designate which world in
$\mathcal{M}$ is bisimilar to which world in $\mathcal{N}$ through a binary
relation $Z\subseteq S_{\mathcal{M}}\times S_{\mathcal{N}}$, but also need to
prescribe the correspondence between children models in $\mathcal{M}$’s and
$\mathcal{N}$’s domains, viz. $N_{\mathcal{M}}$ and $N_{\mathcal{N}}$. Thus
suppose $(u,v)\in Z$, then for this pair of counterparts, we need to know at
present which child model in $N_{\mathcal{M}}$ corresponds to which child
model in $N_{\mathcal{N}}$ through a similar binary relation
$f((u,v))\subseteq N_{\mathcal{M}}\times N_{\mathcal{N}}$. Nevertheless, there
is no reason to prevent the valuation of $f$ from changing according to the
pair $(u,v)$, hence generally speaking, with respect to some fixed $Z$, $f$
should then be a function from $Z$ to $\mathcal{P}(N_{\mathcal{M}}\times
N_{\mathcal{N}})$. Therefore the detailed definition goes as the following:

######  Definition 19 (Bisimilar Pointed Models).

Two pointed models $\mathcal{M},s$ and $\mathcal{N},t$ (with the same fixed
Language FOMC) are bisimilar, iff there exist a binary relation $Z\subseteq
S_{\mathcal{M}}\times S_{\mathcal{N}}$ and a function
$f:Z\to\mathcal{P}(N_{\mathcal{M}}\times N_{\mathcal{N}})$ such that:

  * •

$(s,t)\in Z$.

  * •

$\forall(u,v)\in Z\forall p\in\mathbf{P}$, $u\in V_{\mathcal{M}}(p)$ iff $v\in
V_{\mathcal{N}}(p)$.

  * •

$\forall(u,v)\in Z\forall\mathcal{M}^{\prime}\in N_{\mathcal{M}}$,
$\exists\mathcal{N}^{\prime}\in N_{\mathcal{N}}$ such that
$(\mathcal{M}^{\prime},\mathcal{N}^{\prime})\in f((u,v))$.

  * •

$\forall(u,v)\in Z\forall\mathcal{N}^{\prime}\in N_{\mathcal{N}}$,
$\exists\mathcal{M}^{\prime}\in N_{\mathcal{M}}$ such that
$(\mathcal{M}^{\prime},\mathcal{N}^{\prime})\in f((u,v))$.

  * •

$\forall(u,v)\in Z\forall(\mathcal{M}^{\prime},\mathcal{N}^{\prime})\in
f((u,v))$, $\mathcal{M}^{\prime},T_{\mathcal{M}}(u,\mathcal{M}^{\prime})$ and
$\mathcal{N}^{\prime},T_{\mathcal{N}}(v,\mathcal{N}^{\prime})$ are bisimilar.

  * •

$\forall(u,v)\in Z\forall c\in\mathbf{C}$, either one of the following holds:

    1. 1.

both $I_{\mathcal{M}}(u,c)$ and $I_{\mathcal{N}}(v,c)$ are undefined;

    2. 2.

both $I_{\mathcal{M}}(u,c)$ and $I_{\mathcal{N}}(v,c)$ are defined, and
moreover, $I_{\mathcal{M}}(u,c),T_{\mathcal{M}}(u,I_{\mathcal{M}}(u,c))$ and
$I_{\mathcal{N}}(v,c),T_{\mathcal{N}}(v,I_{\mathcal{N}}(v,c))$ are bisimilar.

  * •

$\forall(u,v)\in Z\forall u^{\prime}\in S_{\mathcal{M}}$ if
$uR_{\mathcal{M}}u^{\prime}$, then $\exists v^{\prime}\in S_{\mathcal{N}}$,
$vR_{\mathcal{N}}v^{\prime}$, $(u^{\prime},v^{\prime})\in Z$,
$f((u,v))\subseteq f((u^{\prime},v^{\prime}))$.

  * •

$\forall(u,v)\in Z\forall v^{\prime}\in S_{\mathcal{N}}$ if
$vR_{\mathcal{N}}v^{\prime}$, then $\exists u^{\prime}\in S_{\mathcal{M}}$,
$uR_{\mathcal{M}}u^{\prime}$, $(u^{\prime},v^{\prime})\in Z$,
$f((u,v))\subseteq f((u^{\prime},v^{\prime}))$.

######  Remark 20.

Once again, Definition 19 is a recursive definition, for in order to check
whether $\mathcal{M},s$ and $\mathcal{N},t$ are bisimilar, we have to firstly
calculate the bisimilar situations between models in $N_{\mathcal{M}}$ and
models in $N_{\mathcal{N}}$. Nonetheless, just like Theorem 7, this issue does
not really cause any problem here either and thus Definition 19 is well
defined.

######  Theorem 21.

If $\mathcal{M},s$ and $\mathcal{N},t$ are bisimilar, then for any FOMC-
sentence $\varphi$,
$\mathcal{M},s\vDash\varphi\iff\mathcal{N},t\vDash\varphi$.

###### Proof.

Suppose $\mathcal{M},s$ and $\mathcal{N},t$ are bisimilar with certain fixed
$Z$ and $f$, so $(s,t)\in Z$. We inductively prove that, for any possible
intermediate stages $\llbracket\varphi\rrbracket^{\mathcal{M}}_{i,j}$ and
$\llbracket\varphi\rrbracket^{\mathcal{N}}_{k,j}$ when evaluating arbitrary
two FOMC-sentences with respect to arbitrary two genealogical Kripke
models,111We do not care about what the initial two FOMC-sentences are at the
beginning of evaluating; nor do we care about what the initial two models are
or whether they are just $\mathcal{M}$ or $\mathcal{N}$. if for every
$(x,\mathcal{M}^{\prime})\in i$, there exists $(x,\mathcal{N}^{\prime})\in k$
such that $(\mathcal{M}^{\prime},\mathcal{N}^{\prime})\in f((s,t))$,222This
condition is not asymmetric as it looks like, since $i$ and $k$ are partial
functions. then $s\in\llbracket\varphi\rrbracket^{\mathcal{M}}_{i,j}$ iff
$t\in\llbracket\varphi\rrbracket^{\mathcal{N}}_{k,j}$.333This claim is
stronger than the original theorem, because suppose $\varphi$ is an FOMC-
sentence, then we can simply start evaluating $\varphi$ from $\mathcal{M}$ and
$\mathcal{N}$ as the initial models, and since the initial stages are also
intermediate stages but at the initial stages $i=k=\varnothing$, the condition
trivially holds so we have
$s\in\llbracket\varphi\rrbracket^{\mathcal{M}}_{\varnothing,\varnothing}$ iff
$t\in\llbracket\varphi\rrbracket^{\mathcal{N}}_{\varnothing,\varnothing}$,
namely $\mathcal{M},s\vDash\varphi$ iff $\mathcal{N},t\vDash\varphi$.

As a matter of fact, two nested levels of induction are needed in this proof.
The outer level of induction deals with models $\mathcal{M}$’s and
$\mathcal{N}$’s maximal depths of generations, whose basic case is when
$N_{\mathcal{M}}=N_{\mathcal{N}}=\varnothing$. Then, the inner level of
induction deals with FOMC-formula $\varphi$’s structure. Firstly, at the basic
step of the outer level of induction, for the inner level of induction, we
only concentrate on those new cases beyond normal propositional modal logic:

  * •

Suppose $\varphi$ is in the form of $X$. Since the interpretation $j$ for
formula variables is the same, and also from proof of Theorem 12 we know that
infinite loop of $X$ will not occur, this case then holds by induction
hypothesis of the inner level.

  * •

Suppose $\varphi$ is in the form of $\text{\rm?`}\psi\text{\rm?}x$. This case
is impossible, because now $N_{\mathcal{M}}=N_{\mathcal{N}}=\varnothing$ and
there is no appropriate interpretation for model variable $x$, contradicting
Theorem 12.

  * •

Suppose $\varphi$ is in the form of $\text{\rm?`}\psi\text{\rm?}c$. Also
because $N_{\mathcal{M}}=N_{\mathcal{N}}=\varnothing$, now both
$I_{\mathcal{M}}(u,c)$ and $I_{\mathcal{N}}(v,c)$ must be undefined and thus
$\llbracket\text{\rm?`}\psi\text{\rm?}c\rrbracket^{\mathcal{M}}_{i,j}=\llbracket\text{\rm?`}\psi\text{\rm?}c\rrbracket^{\mathcal{N}}_{k,j}=\varnothing$.

  * •

Suppose $\varphi$ is in the form of $\forall x.\psi$. Also because
$N_{\mathcal{M}}=N_{\mathcal{N}}=\varnothing$, we trivially have
$\llbracket\forall x.\psi\rrbracket^{\mathcal{M}}_{i,j}=S_{\mathcal{M}}$ and
$\llbracket\forall x.\psi\rrbracket^{\mathcal{N}}_{k,j}=S_{\mathcal{N}}$.

  * •

Suppose $\varphi$ is in the form of $\xi X.\psi$. This case holds by induction
hypothesis of the inner level.

Next, we move on to the inductive step of the outer level of induction. For
the inner level of induction, we again only mention several technically subtle
cases that differ from routine proof:

  * •

Suppose $\varphi$ is in the form of $\text{\rm?`}\psi\text{\rm?}x$, and
$(x,\mathcal{M}^{\prime})\in i$, $(x,\mathcal{N}^{\prime})\in k$. Since
$(s,t)\in Z$ and $(\mathcal{M}^{\prime},\mathcal{N}^{\prime})\in f((s,t))$,
from the condition in Definition 19 we know that
$\mathcal{M}^{\prime},T_{\mathcal{M}}(s,\mathcal{M}^{\prime})$ and
$\mathcal{N}^{\prime},T_{\mathcal{N}}(t,\mathcal{N}^{\prime})$ are bisimilar,
then by induction hypothesis of the outer level we know that
$T_{\mathcal{M}}(s,\mathcal{M}^{\prime})\in\llbracket\psi\rrbracket^{\mathcal{M}^{\prime}}_{\varnothing,j}$
iff
$T_{\mathcal{N}}(t,\mathcal{N}^{\prime})\in\llbracket\psi\rrbracket^{\mathcal{N}^{\prime}}_{\varnothing,j}$,
therefore, $s\in\llbracket\varphi\rrbracket^{\mathcal{M}}_{i,j}$ iff
$t\in\llbracket\varphi\rrbracket^{\mathcal{N}}_{k,j}$.

  * •

Suppose $\varphi$ is in the form of $\text{\rm?`}\psi\text{\rm?}c$. Since
$(s,t)\in Z$, from the condition in Definition 19 we know that either both
$I_{\mathcal{M}}(s,c)$ and $I_{\mathcal{N}}(t,c)$ are undefined, then we have
$s\notin\llbracket\text{\rm?`}\psi\text{\rm?}c\rrbracket^{\mathcal{M}}_{i,j}$
and
$t\notin\llbracket\text{\rm?`}\psi\text{\rm?}c\rrbracket^{\mathcal{N}}_{k,j}$;
or both $I_{\mathcal{M}}(s,c)$ and $I_{\mathcal{N}}(t,c)$ are defined,
$I_{\mathcal{M}}(s,c),T_{\mathcal{M}}(s,I_{\mathcal{M}}(s,c))$ and
$I_{\mathcal{N}}(t,c),T_{\mathcal{N}}(t,I_{\mathcal{N}}(t,c))$ are bisimilar,
then by induction hypothesis of the outer level we know that
$T_{\mathcal{M}}(s,I_{\mathcal{M}}(s,c))\in\llbracket\psi\rrbracket^{I_{\mathcal{M}}(s,c)}_{\varnothing,j}$
iff
$T_{\mathcal{N}}(t,I_{\mathcal{N}}(t,c))\in\llbracket\psi\rrbracket^{I_{\mathcal{N}}(t,c)}_{\varnothing,j}$,
therefore, $s\in\llbracket\varphi\rrbracket^{\mathcal{M}}_{i,j}$ iff
$t\in\llbracket\varphi\rrbracket^{\mathcal{N}}_{k,j}$.

  * •

Suppose $\varphi$ is in the form of $\Box\psi$. Since $(s,t)\in Z$, from the
condition in Definition 19 we know that for every $u\in S_{\mathcal{M}}$ such
that $sR_{\mathcal{M}}u$, there exists $v\in S_{\mathcal{N}}$ such that
$tR_{\mathcal{N}}v$, $(u,v)\in Z$, $f((s,t))\subseteq f((u,v))$, and vice
versa. Hence, fix arbitrary such pair of $(u,v)\in Z$, we only have to show
that $u\in\llbracket\psi\rrbracket^{\mathcal{M}}_{i,j}$ iff
$v\in\llbracket\psi\rrbracket^{\mathcal{N}}_{k,j}$, and because
$f((s,t))\subseteq f((u,v))$, for every $(x,\mathcal{M}^{\prime})\in i$ there
exists $(x,\mathcal{N}^{\prime})\in k$ such that
$(\mathcal{M}^{\prime},\mathcal{N}^{\prime})\in f((u,v))$, so by induction
hypothesis of the inner level the above claim holds, therefore,
$s\in\llbracket\varphi\rrbracket^{\mathcal{M}}_{i,j}$ iff
$t\in\llbracket\varphi\rrbracket^{\mathcal{N}}_{k,j}$.

  * •

Suppose $\varphi$ is in the form of $\forall x.\psi$. Since $(s,t)\in Z$, from
the condition in Definition 19 we know that for every $\mathcal{M}^{\prime}\in
N_{\mathcal{M}}$ there exists $\mathcal{N}^{\prime}\in N_{\mathcal{N}}$ such
that $(\mathcal{M}^{\prime},\mathcal{N}^{\prime})\in f((s,t))$, and vice
versa. Hence, fix arbitrary such pair of
$(\mathcal{M}^{\prime},\mathcal{N}^{\prime})\in f((s,t))$, we only have to
show that
$s\in\llbracket\psi\rrbracket^{\mathcal{M}}_{i[x:=\mathcal{M}^{\prime}],j}$
iff
$t\in\llbracket\psi\rrbracket^{\mathcal{N}}_{k[x:=\mathcal{N}^{\prime}],j}$,
and because $(\mathcal{M}^{\prime},\mathcal{N}^{\prime})\in f((s,t))$, for
every $(x,\mathcal{M}^{\prime\prime})\in i[x:=\mathcal{M}^{\prime}]$ there
exists $(x,\mathcal{N}^{\prime\prime})\in k[x:=\mathcal{N}^{\prime}]$ such
that $(\mathcal{M}^{\prime\prime},\mathcal{N}^{\prime\prime})\in f((s,t))$, so
by induction hypothesis of the inner level the above claim holds, therefore,
$s\in\llbracket\varphi\rrbracket^{\mathcal{M}}_{i,j}$ iff
$t\in\llbracket\varphi\rrbracket^{\mathcal{N}}_{k,j}$.

∎

Similar to ordinary propositional modal logic [14], the reverse of Theorem 21
also holds, provided that both $\mathcal{M}$ and $\mathcal{N}$ are image-
finite models. To start with, however, we have to define what an image-finite
model is, which is still a recursive definition and actually requires
finiteness on two dimensions, namely both horizontally along the binary
relation $R$ and vertically along the set of children models $N$:

######  Definition 22 (Image-Finite Genealogical Kripke Model).

A genealogical Kripke model $\mathcal{M}$ is image-finite, iff all of the
following conditions hold:

  * •

For every $s\in S$, the set $\\{t\in S\mid sRt\\}$ is finite.

  * •

The set $N$ is finite.

  * •

For every $\mathcal{N}\in N$, the model $\mathcal{N}$ is image-finite.

For proof of the reverse of Theorem 21, as a preparation let us firstly focus
on the following Lemma 23, which constitutes the major difficulty throughout
the entire inductive proof. Just like the diagram method in model theory of
first order logic [20], here we will also expand the language from FOMC to
$\text{\sf FOMC}^{\prime}$ by adding a corresponding new constant symbol for
every element in the domain, i.e., every child model.

Formally, the expansion works as follows. Suppose $\mathcal{M}$ and
$\mathcal{N}$ are two image-finite genealogical Kripke models, $s\in
S_{\mathcal{M}}$, $t\in S_{\mathcal{N}}$, and for any FOMC-sentence $\varphi$,
$\mathcal{M},s\vDash\varphi\iff\mathcal{N},t\vDash\varphi$. Let two sets of
fresh constant symbols be
$\mathbf{C}_{\mathcal{M}}=\\{c_{\mathcal{M}^{\prime}}\mid\mathcal{M}^{\prime}\in
N_{\mathcal{M}}\\}$ and
$\mathbf{C}_{\mathcal{N}}=\\{c_{\mathcal{N}^{\prime}}\mid\mathcal{N}^{\prime}\in
N_{\mathcal{N}}\\}$, we expand the language to $\text{\sf FOMC}^{\prime}$ by
enlarging
$\mathbf{C}^{\prime}=\mathbf{C}\cup\mathbf{C}_{\mathcal{M}}\cup\mathbf{C}_{\mathcal{N}}$,
but meanwhile restricting that the appearance of any
$c\in\mathbf{C}_{\mathcal{M}}\cup\mathbf{C}_{\mathcal{N}}$ should not be
within the scope of any $\xi X.$ or the scope of any ¿? pair. Thus, $c$ will
never get passed down vertically.

Now suppose there arbitrarily exist two fixed functions $g:N_{\mathcal{M}}\to
N_{\mathcal{N}}$ and $h:N_{\mathcal{N}}\to N_{\mathcal{M}}$, then using these
two functions, we naturally view $\mathcal{M}$ and $\mathcal{N}$ also as
genealogical Kripke models for the expanded language $\text{\sf
FOMC}^{\prime}$ by letting
$I_{\mathcal{M}}^{\prime}(u,c_{\mathcal{M}^{\prime}})=\mathcal{M}^{\prime}$,
$I_{\mathcal{M}}^{\prime}(u,c_{\mathcal{N}^{\prime}})=h(\mathcal{N}^{\prime})$,
$I_{\mathcal{N}}^{\prime}(v,c_{\mathcal{M}^{\prime}})=g(\mathcal{M}^{\prime})$,
$I_{\mathcal{N}}^{\prime}(v,c_{\mathcal{N}^{\prime}})=\mathcal{N}^{\prime}$
for every $u\in S_{\mathcal{M}}$, $v\in S_{\mathcal{N}}$,
$c_{\mathcal{M}^{\prime}}\in\mathbf{C}_{\mathcal{M}}$,
$c_{\mathcal{N}^{\prime}}\in\mathbf{C}_{\mathcal{N}}$.

######  Lemma 23.

Suppose $\mathcal{M}$ and $\mathcal{N}$ are two image-finite genealogical
Kripke models, $s\in S_{\mathcal{M}}$, $t\in S_{\mathcal{N}}$, and for any
FOMC-sentence $\varphi$,
$\mathcal{M},s\vDash\varphi\iff\mathcal{N},t\vDash\varphi$. Do the expansion
as above. Then there exist two functions $g:N_{\mathcal{M}}\to
N_{\mathcal{N}}$ and $h:N_{\mathcal{N}}\to N_{\mathcal{M}}$ such that:

  * •

For any natural number $n\in\omega$ and any $sR^{n}_{\mathcal{M}}u$, there
exists $tR^{n}_{\mathcal{N}}v$ so that for any $\text{\sf
FOMC}^{\prime}$-sentence $\varphi$,
$\mathcal{M},u\vDash\varphi\iff\mathcal{N},v\vDash\varphi$.

  * •

For any natural number $m\in\omega$ and any $tR^{m}_{\mathcal{N}}v$, there
exists $sR^{m}_{\mathcal{M}}u$ so that for any $\text{\sf
FOMC}^{\prime}$-sentence $\psi$,
$\mathcal{M},u\vDash\psi\iff\mathcal{N},v\vDash\psi$.

###### Proof.

Consider the nontrivial situation when $N_{\mathcal{M}}\neq\varnothing$ and
$N_{\mathcal{N}}\neq\varnothing$. We prove by contradiction. Suppose not,
namely, for every possible functions $g:N_{\mathcal{M}}\to N_{\mathcal{N}}$
and $h:N_{\mathcal{N}}\to N_{\mathcal{M}}$, either one of the following two
cases holds:444In the following, $\bigwedge\limits_{v}$ denotes conjunction
over all possible $v$, and the same for $u$, $g$ and $h$, all of which only
have finitely many possibilities due to image-finiteness. $\varphi$ and $\psi$
generally depend on parameters $v$, $u$, $g$ and $h$, but we just omit too
many subscripts for neatness.

  * •

There exist some natural number $n\in\omega$ and $sR^{n}_{\mathcal{M}}u$ such
that for any $tR^{n}_{\mathcal{N}}v$, there exists some $\text{\sf
FOMC}^{\prime}$-sentence $\varphi$ so that
$\mathcal{M},u\vDash\varphi\nLeftrightarrow\mathcal{N},v\vDash\varphi$, and
without loss of generality, we may assume $\mathcal{M},u\vDash\varphi$ and
$\mathcal{N},v\nvDash\varphi$. Since the possible number of all the different
$v$ is finite, by conjunction we have
$\mathcal{M},s\vDash\Diamond^{n}\bigwedge\limits_{v}\varphi$ as
$sR^{n}_{\mathcal{M}}u$, but
$\mathcal{N},t\nvDash\Diamond^{n}\bigwedge\limits_{v}\varphi$ as
$tR^{n}_{\mathcal{N}}v$ for every $v$.

  * •

There exist some natural number $m\in\omega$ and $tR^{m}_{\mathcal{N}}v$ such
that for any $sR^{m}_{\mathcal{M}}u$, there exists some $\text{\sf
FOMC}^{\prime}$-sentence $\psi$ so that
$\mathcal{M},u\vDash\psi\nLeftrightarrow\mathcal{N},v\vDash\psi$, and without
loss of generality, we may assume $\mathcal{M},u\nvDash\psi$ and
$\mathcal{N},v\vDash\psi$. Since the possible number of all the different $u$
is finite, by conjunction we have
$\mathcal{N},t\vDash\Diamond^{m}\bigwedge\limits_{u}\psi$ as
$tR^{m}_{\mathcal{N}}v$, but
$\mathcal{M},s\nvDash\Diamond^{m}\bigwedge\limits_{u}\psi$ as
$sR^{m}_{\mathcal{M}}u$ for every $u$, namely,
$\mathcal{M},s\vDash\neg\Diamond^{m}\bigwedge\limits_{u}\psi$ but
$\mathcal{N},t\nvDash\neg\Diamond^{m}\bigwedge\limits_{u}\psi$.

To sum up, as $\mathcal{M}$ is not affected by $g$, we can actually conclude
that for every possible functions $g$ and $h$, we always have
$\mathcal{M},s\vDash\bigvee\limits_{h}(\bigwedge\limits_{g}\Diamond^{n}\bigwedge\limits_{v}\varphi\land\bigwedge\limits_{g}\neg\Diamond^{m}\bigwedge\limits_{u}\psi)$.
This is an $\text{\sf FOMC}^{\prime}$-sentence, in the front of which we can
add existential quantifiers binding every
$c_{\mathcal{M}^{\prime}}\in\mathbf{C}_{\mathcal{M}}$ as well as universal
quantifiers binding every
$c_{\mathcal{N}^{\prime}}\in\mathbf{C}_{\mathcal{N}}$ so as to convert it back
to an FOMC-sentence, namely
$\mathcal{M},s\vDash\exists\vec{c}_{\mathcal{M}^{\prime}}.\forall\vec{c}_{\mathcal{N}^{\prime}}.\bigvee\limits_{h}(\bigwedge\limits_{g}\Diamond^{n}\bigwedge\limits_{v}\varphi\land\bigwedge\limits_{g}\neg\Diamond^{m}\bigwedge\limits_{u}\psi)$,
and since $\mathcal{M},s\vDash\varphi\iff\mathcal{N},t\vDash\varphi$ for any
FOMC-sentence $\varphi$, we obtain
$\mathcal{N},t\vDash\exists\vec{c}_{\mathcal{M}^{\prime}}.\forall\vec{c}_{\mathcal{N}^{\prime}}.\bigvee\limits_{h}(\bigwedge\limits_{g}\Diamond^{n}\bigwedge\limits_{v}\varphi\land\bigwedge\limits_{g}\neg\Diamond^{m}\bigwedge\limits_{u}\psi)$,
and so back again to $\text{\sf FOMC}^{\prime}$-sentence we can conclude that
there exists some $g$ such that
$\mathcal{N},t\vDash\bigvee\limits_{h}(\bigwedge\limits_{g}\Diamond^{n}\bigwedge\limits_{v}\varphi\land\bigwedge\limits_{g}\neg\Diamond^{m}\bigwedge\limits_{u}\psi)$.
However, because $\mathcal{N}$ is not affected by $h$, for each disjunctive
branch here we always have
$\mathcal{N},t\nvDash\bigwedge\limits_{g}\Diamond^{n}\bigwedge\limits_{v}\varphi\land\bigwedge\limits_{g}\neg\Diamond^{m}\bigwedge\limits_{u}\psi$
for any $g$, thus a contradiction. ∎

At last, we can state the reverse of Theorem 21, usually called Hennessy-
Milner Theorem, as the following:

######  Theorem 24 (Hennessy-Milner).

If $\mathcal{M}$ and $\mathcal{N}$ are two image-finite genealogical Kripke
models, $s\in S_{\mathcal{M}}$, $t\in S_{\mathcal{N}}$, and for any FOMC-
sentence $\varphi$,
$\mathcal{M},s\vDash\varphi\iff\mathcal{N},t\vDash\varphi$. Then
$\mathcal{M},s$ and $\mathcal{N},t$ are bisimilar.

###### Proof.

According to Lemma 23, fix two functions $g:N_{\mathcal{M}}\to
N_{\mathcal{N}}$ and $h:N_{\mathcal{N}}\to N_{\mathcal{M}}$, let $Z$ be the
set of all “zig-and-zag” $(u,v)$ pairs described in the two clauses of
conclusion in Lemma 23, and let $f((u,v))=g\cup h^{-1}$ for every $(u,v)\in
Z$. We still make use of inductive proof with respect to models
$\mathcal{M}$’s and $\mathcal{N}$’s maximal depths of generations, and so as
induction hypothesis, we also know that this theorem already holds between any
pair of $\mathcal{M}^{\prime},I_{\mathcal{M}}(u,\mathcal{M}^{\prime})$ and
$\mathcal{N}^{\prime},I_{\mathcal{N}}(v,\mathcal{N}^{\prime})$, where
$(u,v)\in Z$, $\mathcal{M}^{\prime}\in N_{\mathcal{M}}$ and
$\mathcal{N}^{\prime}\in N_{\mathcal{N}}$. For any FOMC-sentence $\varphi$, by
Lemma 23 we have
$\mathcal{M},u\vDash\text{\rm?`}\varphi\text{\rm?}c_{\mathcal{M}^{\prime}}\iff\mathcal{N},v\vDash\text{\rm?`}\varphi\text{\rm?}c_{\mathcal{M}^{\prime}}$,
namely
$\mathcal{M}^{\prime},I_{\mathcal{M}}(u,\mathcal{M}^{\prime})\vDash\varphi\iff
g(\mathcal{M}^{\prime}),I_{\mathcal{N}}(v,g(\mathcal{M}^{\prime}))\vDash\varphi$,
hence by induction hypothesis,
$\mathcal{M}^{\prime},I_{\mathcal{M}}(u,\mathcal{M}^{\prime})$ and
$g(\mathcal{M}^{\prime}),I_{\mathcal{N}}(v,g(\mathcal{M}^{\prime}))$ are
bisimilar, and similarly
$h(\mathcal{N}^{\prime}),I_{\mathcal{M}}(u,h(\mathcal{N}^{\prime}))$ and
$\mathcal{N}^{\prime},I_{\mathcal{N}}(v,\mathcal{N}^{\prime})$ are bisimilar,
too. It is then not difficult to check that such $Z$ and $f$ are indeed a
bisimulation between $\mathcal{M},s$ and $\mathcal{N},t$. ∎

##  5 Conclusions and Future Work

This paper proposes first-order modal $\xi$-calculus, a logic for expressively
describing genealogical Kripke models. With illustration of several vivid
examples, we have witnessed how genealogical Kripke models naturally depict
hierarchic and concurrent practical phenomena — particularly like computer
processes, as well as how sentences of first-order modal $\xi$-calculus
succinctly but exactly capture lots of most interesting properties of the
Kripke structure. The intuitive picture is clear to understand, while
mathematically speaking, the logic itself is also technically challenging,
which can be perceived through our effortful management in order to precisely
characterize the logic’s expressivity through a bisimulation notion.

Nonetheless, this paper is still no more than a piece of primitive work, based
on which we would be glad to suggest some plausible future research
directions:

  * •

Despite that genealogical Kripke models form a rather novel kind of shape, we
can still attempt to capture part of its features through other formal
languages, which will then be put onto a thorough comparison in contrast to
our first-order modal $\xi$-calculus, investigating overall aspects such as
expressivity, succinctness, standard translation as well as characterization
theorem. It should also be worthwhile trying to combine first-order modal
$\xi$-calculus with modal $\mu$-calculus into an integrated framework, and
studying them all together from a united algebraic perspective.

  * •

Being called a sort of logical calculus, sound and complete proof systems need
to be further established for our first-order modal $\xi$-calculus, e.g.,
trying a tableau-kind system might be a good point to start [6]. Similar to
normal modal logic, we may also reasonably anticipate that different logics
dwell on different frame classes, or under different additional restrictions
over genealogical Kripke models, e.g., it sounds tempting to naturally
consider various heritage correlations between the parent and the children.
Moreover, different proof systems can also possess different computational
properties, including decidability, complexity, model checking and so on,
which should all prove quite essential in future study and practice as this
logic’s utility in computer science has been heavily suggested.

  * •

Last but not least, it seems a quite promising and exciting approach to extend
the definition of genealogical Kripke models as well as the corresponding
semantics, e.g., what if a model $\mathcal{M}$ is allowed to reflexively refer
to itself as one of its own children models, namely $\mathcal{M}\in
N_{\mathcal{M}}$? As shown by Theorem 7, a non-standard-non-recursive
definition is necessary, and so tight relevance to non-well-founded set theory
[1], as well as process algebra which has developed very fruitful in
theoretical computer science [22], could then be reasonably expected. Another
plausible extension of genealogical Kripke models might be to loosen the
restriction on constant domain [10], since in reality, construction of new
processes as well as destruction of dead zombie ones are just taking place
constantly.

## Acknowledgment

The author owes much thank to Satoshi Tojo and Mizuhito Ogawa for helpful
advice about choosing appropriate notations and writing more clearly. A
handful of anonymous reviewers on previous versions of the manuscript have
also provided tremendous valuable suggestions to help the author improve this
paper.

## References

  * [1] Aczel, P. Non-Well-Founded Sets, vol. 14 of CSLI Lecture Notes.  CSLI Publications, Stanford, CA, 1988.
  * [2] Arnold, A., and Niwiński, D. Rudiments of $\mu$-calculus.  North Holland, 2001.
  * [3] Blackburn, P., de Rijke, M., and Venema, Y. Modal Logic.  Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2001.
  * [4] Bradfield, J., and Stirling, C. Modal $\mu$-calculi.  In Handbook of Modal Logic (2006), P. Blackburn, J. van Benthem, and F. Wolter, Eds., Elsevier Science, pp. 721––756.
  * [5] Breshears, C. The Art of Concurrency.  O’Reilly Media, Sebastopol, CA, 2009.
  * [6] D’Agostino, M., Gabbay, D. M., Hähnle, R., and Posegga, J., Eds.  Handbook of Tableau Methods.  Kluwer Academic Publishers, Dordrecht, The Netherlands, 1999.
  * [7] Emerson, E. A., and Jutla, C. S. The complexity of tree automata and logics of programs.  In FoCS (1988), vol. 88, Citeseer, pp. 328–337.
  * [8] Emerson, E. A., and Jutla, C. S. The complexity of tree automata and logics of programs.  SIAM Journal on Computing 29, 1 (1999), 132–158.
  * [9] Fitting, M. Modal Logics Between Propositional and First‐order.  Journal of Logic and Computation 12, 6 (12 2002), 1017–1026.
  * [10] Fitting, M., and Mendelsohn, R. L. First-Order Modal Logic, vol. 277 of Synthese Library.  Springer, Netherlands, 1998.
  * [11] Gabbay, D. M., Hodkinson, I., and Reynolds, M. Temporal Logic: Mathematical Foundations and Computational Aspects, vol. 1.  Clarendon Press, 1994.
  * [12] Gädel, E., Kolaitis, P. G., Libkin, L., Marx, M., Spencer, J., Vardi, M. Y., Venema, Y., and Weinstein, S. Finite Model Theory and Its Applications.  Texts in Theoretical Computer Science. An EATCS Series. Springer, Berlin Heidelberg, 2007.
  * [13] Goldblatt, R. Logics of Time and Computation, vol. 7 of CSLI Lecture Notes.  CSLI Publications, Stanford, CA, 1992.
  * [14] Hennessy, M., and Milner, R. Algebraic Laws for Indeterminism and Concurrency.  Journal of the ACM 32 (1985), 137–162.
  * [15] Hughes, G., and Cresswell, M. A New Introduction to Modal Logic.  Routledge, 1996.
  * [16] Jech, T. Set Theory, 3rd millennium ed.  Springer Monographs in Mathematics. Springer, Berlin Heidelberg, 2003\.
  * [17] Kozen, D. Results on the propositional $\mu$-calculus.  In Automata, Languages and Programming (Berlin, Heidelberg, 1982), M. Nielsen and E. M. Schmidt, Eds., Springer Berlin Heidelberg, pp. 348–359.
  * [18] Kozen, D. Results on the propositional $\mu$-calculus.  Theoretical Computer Science 27, 3 (1983), 333–354.  Special Issue Ninth International Colloquium on Automata, Languages and Programming (ICALP) Aarhus, Summer 1982.
  * [19] Kunen, K. Set Theory, vol. 102 of Studies in logic and the foundations of mathematics.  Elsevier Science B.V., Amsterdam, The Netherlands, 1980.
  * [20] Marker, D. Model Theory : An Introduction, vol. 217 of Graduate Texts in Mathematics.  Springer, New York, 2002.
  * [21] Ponse, A., de Rijke, M., and Venema, Y., Eds.  Modal Logic and Process Algebra: a Bisimulation Perspective.  CSLI Publications, Stanford, 1995.
  * [22] Sangiorgi, D., and Rutten, J., Eds.  Advanced Topics in Bisimulation and Coinduction.  Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2011.
  * [23] Stirling, C. Modal and Temporal Properties of Processes.  Texts in Computer Science. Springer, New York, 2001.
  * [24] Streett, R. S. Propositional dynamic logic of looping and converse.  In Proceedings of the Thirteenth Annual ACM Symposium on Theory of Computing (New York, NY, USA, 1981), STOC ’81, Association for Computing Machinery, pp. 375––383.
  * [25] Tanenbaum, A. S. Modern Operating Systems, 4th ed.  Pearson, 2015.