A Presheaf Semantics
for Quantified Temporal Logics

Research partially supported by the Italian MIUR project PRIN 2017FTXR7S “IT-MaTTerS”.

Fabio Gadducci0000-0003-0690-3051 Davide Trotta0000-0003-4509-594X

University of Pisa, Department of Computer Science, Pisa, Italy

<EMAIL_ADDRESS><EMAIL_ADDRESS>
F. Gadducci and D. Trotta

Temporal logics stands for a widely adopted family of formalisms for the verification of computational devices, enriching propositional logics by operators predicating on the step-wise behaviour of a system.
Its quantified extensions allow

to reason on the properties of the individual components of the system at hand. The expressiveness of the resulting logics poses problems in correctly identifying a semantics that exploits its features without resorting to the imposition of restrictions on the acceptable behaviours.
In this paper we address this issue by means of counterpart models

and relational presheaves.

§ INTRODUCTION

The words “temporal logics” stand for a widely adopted family of formalisms for the specification and verification of computational devices, ranging from stand-alone programs to large-scale  systems, which find applications in diverse areas such as synthesis, planning and knowledge representation, see e.g. [29, 6] among many others.

Usually, these logics have a propositional fragment at the core, which is extended by operators predicating on the step-wise behaviour of a system.

The framework proved extremely effective, and after the foundational work carried out since Pnueli’s seminal paper [28],
research focused on the
development of techniques for the verification of properties specified via such logics, see e.g. [2, 26] for their emphasis on (graph) rewriting.

The standard model for temporal logics is represented by transition systems (also known as Kripke frames in logical jargon), where the states represent possible configurations of a device and the transition relation their possible evolution. Most often, the states have some (algebraic) structure and one is interested not just on the topology of each reachable state, but on the fate of its individual items as well. To this end,
the use of quantified temporal logics have been advocated. A typical example are graph logics, where the states are graphs (i.e. algebras of a graph signature) and the transition relation is given by a family of (partial) graph morphisms [7, 8, 9].

Unfortunately, such logics are in general not decidable [11, 19] and, as a consequence, many efforts have been devoted to the definition of logics (or the identification
of fragments) that sacrifice expressiveness in favour of computability and efficiency.

Besides these practical considerations, notice that also the characteristics of the semantical models for such logics are not clearly cut. Consider for instance a model with two states $s_0$, $s_1$, a transition from $s_0$ to $s_1$ and another transition going backward, and an item $i$ that appears in $s_0$ only. Is item $i$ being destroyed and (re)created again and again? Or is it just an identifier
that is being reused? The issue is denoted in the literature as the trans-world identity problem (see [18] as well as [3] for a survey of the related philosophical issues). An often adopted solution is to choose a set of universal items, which are used to form each state. It is then obvious how it is possible to refer to the
same element across states.
However, these solutions are not perfectly suited to model systems with dynamic allocation and
deallocation of components. Consider again the above example. The problem is that item $i$ belongs to the
universal domain, and hence it is exactly the same after every deallocation in state $s_1$. But intuitively, every instance of $i$ should instead be considered to be distinct (even if syntactically equivalent).

The solution advanced by Lewis [24] is based on what is called the counterpart paradigm: instead of a universal set of items, states are connected by (possibly partial) morphisms, so that state items are local and state evolution may account for their deallocation and

However, as far as we are aware, the use of counterpart semantics for quantified temporal or modal logics has been sparse, and even more so the attempts for their categorical presentation.

The paper builds on the set-theoretical description of a counterpart semantics for a modal logic with second-order quantifiers introduced in [13], with the goal of explaining how that model admits a natural generalization and presentation in a categorical setting, and how it can be adapted to
offer a counterpart semantics for (linear time) temporal logics with second-order quantifiers.

From a technical perspective, the starting point for our semantics was the hyperdoctrine presentation of first-order logics, as originally described by Lawvere in his work on categories with equational structure [22, 23]. More precisely, the direct inspiration was the presheaf model for modal logics with first-order quantifiers presented in [15]. Our work extends and generalizes the latter proposal in a few directions.
First of all, the focus on temporal logics, with an explicit operator for next step, required to tweak the original proposal by Ghilardi and Meloni by equipping our models with a chosen family of arrows, which represent the basics steps of a system. Furthermore, the choice of a counterpart semantics forced the transition relation between worlds to be given by families of partial morphisms between the algebras forming each world: this was modelled by using relational presheaves, instead of functional ones, as the main tool. Related to this, tackling second-order quantification required additional effort since relational presheaves do not form a topos in general [27].

The paper has the following structure. Section 2 recalls some basic properties of multi-sorted algebras, which describe the  structure of our worlds. Section 3 presents relational presheaves, showing how the latter capture a generalised notion of transition system, where a transition step is given by a partial homomorphism, and how they support suitable second-order operators. Section 4 introduces our logics, a monadic second-order extension of classical linear time temporal logics, and Section 6 finally shows how to provide it with a counterpart semantics, thanks to the categorical set-up of the previous sections. This paper is rounded up by a concluding section and by a running example, highlighting the features of the chosen logics.

Related works.
Functional presheaves can be seen as the categorical abstraction of Krikpke frames. This idea was introduced in [15, 16].
Developing this intuition, relational presheaves (see [27] for an analysis of the structure of the associated category) can be thought of as a categorification of counterpart Kripke frames in the sense of Lewis [24]. An in-depth presentation of classical counterpart semantics is in [18, 3].

In this work we use relational preaheaves to provide a categorical account to the notion of counterpart model defined in [13], introducing what we call counterpart $\mW$-models. We then specialize our models to deal with temporal logics, equipping them with what we call temporal structures.

As we already mentioned in the introduction, many authors considered quantified temporal logics and have addressed their decidability and complexity issues.
Since most of our examples are motivated by applications to graph rewriting, we just refer to [2, 30], among others.

Much less explored, though, is the side of categorical semantics.

More specifically, we are aware of a topos-theoretical description of a semantics for modal logics in [1] and a presentation in terms of Lawvere's doctrines in [5]. Moreover, for connections between the areas of coalgebra and modal logic we refer to [21, 20].

Notice that the approaches presented in these works generalise in the categorical setting the usual Kripke-style semantics, but not the counterpart one.

§ SOME NOTIONS ON MULTI-SORTED ALGEBRAS

We begin by recalling the definition of many-sorted algebras and their homomorphisms, which lies at the basis of the structure of our worlds.

A many-sorted signature $\Sigma$ is a pair $(S_{\Sigma},F_{\Sigma})$ given by a set of sorts $S_{\Sigma}=\{\tau_1,\dots,\tau_m\}$ and by a set $F_{\Sigma}=\{\freccia{\tau_1\times \cdots \times \tau_m}{f_{\Sigma}}{\tau}\; |\; \tau_i, \tau \in S_{\Sigma}\}$ of function symbols typed over $S_{\Sigma}^*$.

A many-sorted algebra $\MSalgebra{A}$ with signature $\Sigma$, i.e. a $\Sigma$-algebra, is a pair $(A,F_{\Sigma}^{\MSalgebra{A}})$ such that

* $A$ is a set whose elements are typed over $S_{\Sigma}$;

* $F_{\Sigma}^{\MSalgebra{A}}$ is a family of typed functions $\{\freccia{A_{\tau_1}\times \cdots \times A_{\tau_m}}{f_{\Sigma}^{\MSalgebra{A}}}{A_{\tau}}\; |\; f_{\Sigma} \in F_{\Sigma} \wedge \freccia{\tau_1\times\cdots \times \tau_m}{f_{\Sigma}}{\tau}\}$.

Notice that we denoted by $A_{\tau}$ the set $\{a\in A\;|\; a:\tau\}$ of elements of $A$ with type $\tau$.

Given two $\Sigma$-algebras $\MSalgebra{A}$ and $\MSalgebra{B}$, a (partial) homomorphism

$\rho$ is a family of (partial) functions $\rho:=\{\frecciaparziale{A_{\tau}}{\rho_{\tau}}{B_{\tau}}\;|\; \tau\in S_{\Sigma}\}$ typed over $S_{\Sigma}$ such that for every function symbol $\freccia{\tau_1\times\cdots\times \tau_m}{f_{\Sigma}}{\tau}$ and for every list of elements $(a_1,\dots,a_m)$, if $\rho_{\tau_i}$ is defined for the element $a_i$ of type $\tau_i$, then $\rho_{\tau}$ is defined for the element $f_{\Sigma}^{\MSalgebra{A}}(a_1,\dots,a_m)$ and $\rho_{\tau}(f_{\Sigma}^{\MSalgebra{A}}(a_1,\dots,a_m))=f_{\Sigma}^{\MSalgebra{B}}(\rho_{\tau_1}(a_1),\dots,\rho_{\tau_m}(a_m))$.

[Graph Algebra]
Let us consider the signature $\Sigma_{Gr}=(S_{Gr},F_{Gr})$ for directed graphs. The set $S_{Gr}$ consists of the sorts of nodes $\tau_N$ and edges $\tau_E$, while the set $F_{Gr}$ is composed by the function symbols
$\freccia{\tau_E}{s,t}{\tau_N}$, which determine, respectively, the source and the target node of an edge. In this case, a $\Sigma_{Gr}$-Algebra $\MSalgebra{G}$ is a directed graph and a homomorphism of $\Sigma_{Gr}$-algebras is exactly a (partial) morphism of directed graphs.
In Figure <ref> we find the visual representations for three graphs $\mathbf{G}_0$, $\mathbf{G}_1$ and $\mathbf{G}_2$.

[style=new style 0] (0) at (-11, 6) $n_0$;
[style=new style 0] (1) at (-5, 6) $n_1$;
[style=new style 0] (2) at (-8, 2) $n_2$;
[style=new style 1] (3) at (-11, 4) $e_2$;
[style=new style 1] (4) at (-5, 4) $e_1$;
[style=new style 1] (5) at (-8, 8) $e_0$;
[style=new style 0] (6) at (-1, 5) $n_3$;
[style=new style 0] (7) at (4.75, 5) $n_4$;
[style=new style 1] (8) at (2, 8) $e_3$;
[style=new style 1] (9) at (2, 2) $e_4$;
[style=new style 0] (10) at (11, 6.25) $n_5$;
[style=new style 1] (13) at (11, 3.5) $e_5$;

(2) to (3);
(0) to (5);
(1) to (4);
[style=freccia] (4) to (2);
[style=freccia] (3) to (0);
[style=freccia] (5) to (1);
(6) to (8);
(7) to (9);
[style=freccia] (9) to (6);
[style=freccia] (8) to (7);
[bend right=60, looseness=1.50] (10) to (13);
[style=freccia, bend right=60, looseness=1.50] (13) to (10);

Three graphs: $\mathbf{G}_0$ (left), $\mathbf{G}_1 $ (middle) and $\mathbf{G}_2$ (right)

Let $\Sigma$ be a many-sorted signature, and let us fix disjoint, countably infinite sets $X_{\tau}$ of variables for each sort symbol of $S_{\Sigma}$. We let $x:\tau$ indicate an element $x$ of the set $X_{\tau}$. In order to introduce the notion of term, we take into account signatures $\Sigma_X$ obtained by extending a many-sorted signature $\Sigma$ with a denumerable set $X$ of variables typed over $S_{\Sigma}$. This allows to introduce the notion of open terms over $\Sigma_X$ in the usual way.

Let $\Sigma$ be a many-sorted signature and $X$ a denumerable set of individual variables typed over $S_{\Sigma}$. The many-sorted set $T(\Sigma_X)$ of terms obtained from $\Sigma_X$ is the smallest such that

$X\subseteq T(\Sigma_X)$

$ \freccia{\tau_1\times \cdots \times \tau_m}{f_{\Sigma}}{\tau}\in F_{\Sigma}$
$t_i:\tau_i\in T(\Sigma_X)$ for $i=1,\dots,m$
$f_{\Sigma}(t_1,\dots,t_m):\tau \in T(\Sigma_X)$

Finally, we recall the notion of context and term-in-context over a signature $\Sigma_X$.

A context $\Gamma$ over a signature $\Sigma_X$ is a finite list $\context{x}{\tau}{n}$ of (variable, sort)-pairs, subject to the condition that $x_1,\dots,x_n$ are distinct.

A term-in-context takes the form $ \termincontext{t}{\tau}{\Gamma}$
where $t$ is a term, $\tau$ is a sort, and $\Gamma$ is a context over the given signature $\Sigma_X$. The well-formed terms-in-context are inductively generated by the two rules

$\termincontext{x}{\tau}{\Gamma',x:\tau, \Gamma}$

$\termincontext{t_1}{\tau_1}{\Gamma}\cdots  \termincontext{t_m}{\tau_m}{\Gamma}$

where $\freccia{\tau_1\times\cdots\times \tau_m}{f_{\Sigma}}{\tau}$ is a function symbol of $F_{\Sigma}$.

Given a many-sorted signature $\Sigma$, its syntactic category or category of contexts $\SynCat{\Sigma}$ is defined as follows

* its objects are $\alpha$-equivalence class of contexts;

* a morphism $\freccia{\Gamma}{\gamma}{\Gamma'}$, where $\Gamma'=\context{y}{\tau}{m}$, is specified by an equivalence class of lists of the form $\gamma=[t_1,\dots,t_m]$ of terms over $\Sigma_X$ such that $\termincontext{t_i}{\tau_i}{\Gamma}$ holds for $i=1,\dots,m$.

The composition of two morphisms is formed by making substitutions.

Recall that two contexts are $\alpha$-equivalent if they differ only in their variables; in other words, the list of sorts occurring in each context
are equal (and in particular, the contexts are of equal length).
Requiring the objects of the syntactic category to be $\alpha$-equivalence classes of contexts ensures that the category $\SynCat{\Sigma}$ has finite products, given by the concatenations of contexts. As for morphisms, the equivalence relation we consider is the one identifying two terms if they are equal up to substitution.

§ A CATEGORICAL PERSPECTIVE OF COUNTERPART MODELS

Kripke  semantics  is  widely  used  to  assign  a  meaning  to  modal  languages [4];  it  stems  from  Leibniz’s  intuition  of  defining  necessity  as  truth  in  every  possible  world. We start this section recalling the notion of Kripke frame, widely used
in the analysis of modality, and its development into counterpart semantics.

A Kripke frame is a 4-tuple $\angbr{W,R}{D,d}$ defined as

* $W$ is a non-empty set;

* $R$ is a binary relation of $W$;

* $D$ is a function assigning to every $w\in W$ a non-empty set $D(w)$ such that if $wRw'$ then $D(w)\subseteq D(w')$;

* $d$ is a function assigning to every $w\in W$ a set $d(w)\subseteq D(w)$.

The set $W$ is intuitively interpreted as the domain of possible worlds, whereas $R$ is the
accessibility relation among worlds. Each outer domain $D(w)$ contains the objects of which
it makes sense to talk about in $w$, while each inner domain
$d(w)$ contains the individuals actually existing in $w$.

Notice that Kripke frames are usually assumed to satisfy the increasing outer domain condition, i.e. for all $w,w'\in W$, if $wRw'$ then $D(w)\subseteq D(w')$, but this condition could represent a strong, and not enough  motivated, constraint both philosophically and from the point of view of applications. Over the years, this condition has been the heart of several discussions and controversies.

In particular, Lewis denied the possibility of identifying the same individual across possible worlds, and he substituted the notion of trans-world identity with a counterpart relation $C$, introducing counterpart theory [24].
In order to assign a meaning to terms necessary and possible according to Lewis’ counterpart theory, Kripke frames are enriched by a function $C$ such that for all $w,w\in W$, $C_{w,w'}$ is a relation on $D(w)\times D(w')$, intuitively interpreted as the counterpart relation.

A counterpart frame is a 5-tuple $\angbr{W,R}{D,d,C}$ defined as

* $W,R,D,d$ are defined as for Kripke frames, but $D$ need not to satisfy the increasing outer domain condition;

* $C$ is a function assigning to every 2-tuple $\angbr{w}{w'}$ a subset of $D(w)\times D(w')$.

As anticipated, Kripke-like solutions are not perfectly suited to model, for example, systems with dynamic allocation and
deallocation of components. This will be clearer later, when we present Example <ref>.

Alternative solutions based on counterpart relations are e.g. introduced in [13], where the authors introduce a novel approach to the semantics of quantified $\mu$-calculi, considering a sort of
labeled transition systems as semantic domain (called counterpart models), where states are algebras
and transitions are defined by counterpart relations (a family of partial homomorphisms) between

We conclude this section recalling the notion of counterpart model from [13].

Let $\Sigma$ be a many-sorted signature and $\Alg$ the set of algebras over $\Sigma$. A counterpart model is a triple $\model:=\angbr{W}{\rightsquigarrow,d}$ such that

* $W$ is a set of worlds;

* $\freccia{W}{d}{\Alg}$ is a function assigning to each world $\omega\in W$ a $\Sigma$-algebra;

* $\rightsquigarrow\subseteq (W\times (\Alg \rightharpoonup \Alg)\times W)$ is the accessibility relation over $W$ enriched with  (partial) homomorphisms (counterpart relations) between the algebras of the connected worlds.

The elements of $\rightsquigarrow$ are defined such that for every $(w_1 , cr, w_2 ) \in \rightsquigarrow $ we have that $cr : d(w_1 ) \rightharpoonup d(w_2 )$ is a (partial) homomorphism. In particular, each component $cr$ of $\rightsquigarrow$  explicitly defines the counterparts in (the algebras assigned to) the target world of (the algebras assigned to) the source world.

The intuition is that we are considering a transition system labeled with morphisms between
algebras, as an immediate generalization of graph transition systems. The counterpart relations allow to avoid the trans-world identity, i.e. the implicit identification of elements of (the algebras of) different worlds sharing the same name. As a consequence, the name of the elements has a meaning local to the belonging world. For this reason, as we will see, the counterpart
relations allow for the creation, deletion, renaming and merging of elements in a type-respecting way.

§.§ Presheaves models

The main goal of this section is to explain how the counterpart model introduced in [13] admits a natural generalization and presentation from a categorical setting.

To fix the notation, and in order to provide the intuition behind the models we introduce, we  briefly recall from [15] an interesting presentation of the notions of world, process and individuals arising from modal logic, in terms of presheaves.

In particular, given a category $\mW$, its objects $\sigma,\omega, \rho, \dots$ can be considered as worlds or instants of time, and the arrows $\freccia{\sigma}{f}{\omega}$ of the category represent temporal developments or ways of accessibility.

From this perspective, a presheaf $\presheaf{\mW}{D}$ assigns to every world $\omega$ the set $D_{\omega}:=D(\omega)$ of its individuals, and to a temporal development $\freccia{\sigma}{f}{\omega}$ a function $\freccia{D_{\omega}}{D_f}{D_{\sigma}}$ between the individuals living in the worlds $\omega$ and $\sigma$. Therefore, if we consider two elements $a\in D_{\omega}$ and $b\in D_{\sigma}$, the equality $b=D_f(a)$ can be read as "a is a future development with respect to $f$ of b".

In other words, the notion of presheaf represents the natural categorification of the notion of counterpart frame whose counterpart relation is functional.

Let $\Sigma$ be a many-sorted signature. A $\mW$-model is a triple $\model=(\mW,\sortmodel,\functionmodel)$ such that

* $\mW$ is a category of worlds;

* $\sortmodel=\{\presheaf{\mW}{\interp{\tau}{\model}}\}_{\tau\in S_{\Sigma}}$ is a set of preshaves on $\mW$, indexed on $S_{\Sigma}$;

* $\functionmodel=\{\freccia{\interp{\tau_1}{\model}\times \cdots \times \interp{\tau_m}{\model}}{\mI(f_{\Sigma})}{\interp{\tau}{\model}}\}_{f_{\Sigma}\in F_{\Sigma}}$ is a set of natural transformations of presheaves.

A $\mW$-model $\model$ induces a counterpart frame $\angbr{W,R}{D,d,C}$ defined as follows

* the set of worlds is given by the objects of the category $\mW$, i.e. $W=\mathsf{ob}(\mW)$;

* the accessibility relation $R$ is given by the class of arrows of the category $\mW$;

* $\freccia{W}{d}{\Alg}$ is a function assigning to each world $\omega\in W$ the $\Sigma$-algebra $d(\omega):=(A_{\omega},F^{A_{\omega}}_{\Sigma})$, where $A_{\omega}:=\bigcup_{\tau\in S_{\Sigma}}\{\interp{\tau}{\model}_{\omega}\}$ and $F^{A_{\omega}}_{\Sigma}:=\bigcup_{f_{\Sigma}\in F_{\Sigma}}\{\mI(f_{\Sigma})_{\omega}\}$;

* $D:=d$;

* $C$ is a function assigning to every arrow $\freccia{\omega}{g}{\sigma}$ of $R$ a function $\freccia{d(\sigma)}{C_f}{d(\omega)}$ defined on a given typed element $a\in \interp{\tau}{\model}_{\sigma}$ as  $C_f(a):=\interp{\tau}{\model}_f(a)$.

It is easy to check that every $C_f$ is a homomorphism of $\Sigma$-algebras (it follows from the naturality of each $\mI(f_{\Sigma})$)

Notice that in the usual notion of Kripke-frame the accessibility relation $R$ is simply required to be a binary relation on the set $W$ of worlds. In particular, this means that two worlds are connected by at most one temporal development or that there is at most one way to pass from a given world to another. This is another constraint that we would like to avoid.

The natural generalization of considering a set of worlds $W$ and a relation $R$ is considering a category $\mW$.

Let us consider the ordinary signature $\Sigma_{Gr}=(S_{Gr},F_{Gr})$ for directed graphs introduced in Example <ref>. In this case, a presheaves model $\model_{Gr}=(\mW,\mathfrak{S}_{\Sigma_{Gr}},\mathfrak{F}_{\Sigma_{Gr}})$ consists of

* a category of worlds $\mW$;

* $\mathfrak{S}_{\Sigma_{Gr}}=\{\interp{\tau_N}{\model},\interp{\tau_E}{\model}\}$, where  $\presheaf{\mW}{\interp{\tau_N}{\model}}$ and $\presheaf{\mW}{\interp{\tau_E}{\model}}$, representing, respectively, the presheaf of nodes $\interp{\tau_N}{\model}$ and
that of arcs $\interp{\tau_E}{\model}$;

* $\mathfrak{F}_{\Sigma_{Gr}}=\{\mI(s),\mI(t)\}$, where$\freccia{\interp{\tau_E}{\model}}{\mI(s)}{\interp{\tau_N}{\model}}$ and $\freccia{\interp{\tau_E}{\model}}{\mI(t)}{\interp{\tau_N}{\model}}$ are two natural transformations.

The intuition is that we are assigning a directed graph $d(\omega):=(\interp{\tau_N}{\model}_{\omega},\interp{\tau_E}{\model}_{\omega}, \mI(s)_{\omega},\mI(t)_{\omega}) $ to every world $\omega$, identified by the set of nodes $\interp{\tau_N}{\model}_{\omega}$, the set of arcs $\interp{\tau_E}{\model}_{\omega}$, and the two functions $\freccia{\interp{\tau_E}{\model}_{\omega}}{\mI(s)_{\omega},\mI(t)_{\omega}}{\interp{\tau_N}{\model}_{\omega}}$.
Notice also that, by the naturality of $\mI(s)$ and $\mI(t)$, we have that every arrow $\freccia{\omega}{f}{\sigma}$ induces a morphism of directed graphs
\[\freccia{(\interp{\tau_N}{\model}_{\sigma},\interp{\tau_E}{\model}_{\sigma}, \mI(s)_{\sigma},\mI(t)_{\sigma}) }{d(f)}{(\interp{\tau_N}{\model}_{\omega},\interp{\tau_E}{\model}_{\omega}, \mI(s)_{\omega},\mI(t)_{\omega}) }\]

given by $d(f):=(\interp{\tau_N}{\model}_f,\interp{\tau_E}{\model}_f)$.

Given a signature $\Sigma$ and a category $\mW$ of worlds, we define the category of $\mW$-models, denoted by $\ModelCat{\mW}{\Sigma}$, as the category whose objects are $\mW$-models $\model$, and whose arrows $\freccia{\model}{F}{\model'}$ are families of natural transformations $F:=\{\freccia{\interp{\tau}{\model}}{F_{\tau}}{\interp{\tau}{\model'}}\}_{\tau\in S_{\Sigma}}$ commuting with the natural transformations of $\functionmodel$ and $\functionmodel'$, i.e. $F_{\tau}\circ \mI(f_{\Sigma})= \mI'(f_{\Sigma})\circ (F_{\tau_1}\times \cdots\times F_{\tau_m})$ for every function symbol $\freccia{\tau_1\times,\cdots \tau_m}{f_{\Sigma}}{\tau}\in F_{\Sigma}$.

Notice that the notion of  $\mW$-model admits a clear interpretation also from the categorical perspective of functorial semantics. In details, observe that, by definition, a $\mW$-model $\model=(\mW,\sortmodel,\functionmodel)$ consists in assigning to every sort $\tau$ of the signature $\Sigma$ a presheaf $\presheaf{\mW}{\interp{\tau}{\model}}$ and to every function symbol $f_{\Sigma}$ a morphism of presheaves $\freccia{\interp{\tau_1}{\model}\times \cdots \times \interp{\tau_m}{\model}}{\mI(f_{\Sigma})}{\interp{\tau}{\model}}$. Therefore a $\mW$-model can be represented as a preserving finite products functor $\freccia{\SynCat{\Sigma}}{F_{\mW}}{\presheafcat{\mW}}$  from the syntactic category $\SynCat{\Sigma}$ into the category $\presheafcat{\mW}$ of $\mW$-presheaves.

Similarly, every such functor $\freccia{\SynCat{\Sigma}}{F_{\mW}}{\presheafcat{\mW}}$ induces a $\mW$-model denoted by $\model_F$. Therefore it is straightforward to check that the following results holds.

For every category $\mW$, the category $\ModelCat{\mW}{\Sigma}$ of $\mW$-models is equivalent to the category $\FPfunctors (\SynCat{\Sigma},\presheafcat{\mW})$  of finite product preserving functors and natural transformations from the syntactic category $\SynCat{\Sigma}$ to $\presheafcat{\mW}$ of presheaves over $\mW$.

We have seen that the notion of presheaf generalizes that of counterpart frame. However, we need to specify an important point: one of the main reasons why the counterpart semantics has been introduced is not only to avoid the increasing outer domain condition, but more generally to avoid the constraint that every individual of a world $w$ has to admit a counterpart in every world connected to $w$. Presheaves clearly are not subject to the increasing outer domain condition, i.e. if we consider an arrow $\freccia{\omega}{f}{\sigma}$, the $D_f$ is not an injection in general. On the other hand, being $D_f$ a function, we have that for every individual of $D_{\sigma}$ there exists a counterpart in $D_{\omega}$. So, to fully abstract the the ideal of counterpart semantic, we have to consider a more general notion of presheaves, i.e. relational presheaves.

§.§ Relational presheaves models

The main goal of this section is to explain how the counterpart model introduced in [13] admits a natural generalization and presentation from a categorical setting.

To fix the notation, and in order to provide the intuition behind the models we introduce, we  briefly recall from [15] an interesting presentation of the notions of world, process and individuals arising from modal logic, in terms of presheaves.

In particular, given a small category $\mW$, its objects $\sigma,\omega, \rho, \dots$ can be considered as worlds or instants of time, and the arrows $\freccia{\sigma}{f}{\omega}$ of the category represent temporal developments or ways of accessibility.
Notice that in the usual notion of Kripke-frame the accessibility relation $R$ is simply required to be a binary relation on the set $W$ of worlds. In particular, this means that two worlds are connected by at most one temporal development or that there is at most one way to pass from a given world to another. This is a constraint that we would like to avoid. The natural generalization of considering a set of worlds $W$ and a relation $R$ is considering a category $\mW$.

From this perspective, a presheaf $\presheaf{\mW}{D}$ assigns to every world $\omega$ the set $D_{\omega}:=D(\omega)$ of its individuals, and to a temporal development $\freccia{\sigma}{f}{\omega}$ a function $\freccia{D_{\omega}}{D_f}{D_{\sigma}}$ between the individuals living in the worlds $\omega$ and $\sigma$. Therefore, if we consider two elements $a\in D_{\omega}$ and $b\in D_{\sigma}$, the equality $b=D_f(a)$ can be read as a is a future development with respect to $f$ of b.

In other words, the notion of presheaf represents the natural categorification of the notion of counterpart frame whose counterpart relation is functional. In particular, it is direct to check that, given  presheaf $\presheaf{\mW}{D}$, one can define a counterpart frame $\angbr{W,R}{D,d,C}$ as follows

* $W$ is given by the objects of the category $\mW$;

* $\omega R\sigma $ if and only if there exists at least an arrow $\omega \to \sigma$ of $\mW$;

* $d$ and $D$ coincide and are given by the action of the presheaf $\presheaf{\mW}{D}$ on the objects of $\mW$, i.e. $D(\omega)=D(\omega)=D_{\omega}$;

* $C$ assigns to a given 2-tuple $\angbr{\omega}{\omega'}$ the subset of $D(\omega)\times D(\omega')$  whose elements are pairs $\angbr{a}{a'}$ such that $a\in D(\omega)$, $a'\in D(\omega')$ and there exists an arrow $\freccia{\omega}{f}{\omega'}$ such that $a=D_f(a')$.

Therefore, we have seen the link between counterpart frame (whose counterpart relation is functional) and presheaf. Now we introduce the new notion of $\mW$-model and we explain how this notion is a categorification of the notion of counterpart model in the sense of [13].

Let $\Sigma$ be a many-sorted signature. A $\mW$-model is a triple $\model=(\mW,\sortmodel,\functionmodel)$ such that

* $\mW$ is a category of worlds;

* $\sortmodel=\{\presheaf{\mW}{\interp{\tau}{\model}}\}_{\tau\in S_{\Sigma}}$ is a set of preshaves on $\mW$, indexed on $S_{\Sigma}$;

* $\functionmodel=\{\freccia{\interp{\tau_1}{\model}\times \cdots \times \interp{\tau_m}{\model}}{\mI(f_{\Sigma})}{\interp{\tau}{\model}}\}_{f_{\Sigma}\in F_{\Sigma}}$ is a set of natural transformations of presheaves.

Thus, we have seen that the choice of presheaves for the counterpart semantics is quite natural, but it comes with some restrictions: one of the main reasons why such semantics has been introduced is not only to avoid the increasing outer domain condition, but more generally to avoid the constraint that every individual of a world $w$ has to admit a counterpart in every world connected to $w$. Presheaves clearly are not subject to the increasing outer domain condition but if we consider a temporal development $\freccia{\omega}{f}{\sigma}$, and being $D_f$ a total function, we have that for every individual of $D_{\sigma}$ there exists a counterpart in $D_{\omega}$. This forces that an individual $t$ living of the world $\sigma$ necessarily has a counterpart in the world $\omega$ with respect to the development $\freccia{\omega}{f}{\sigma}$.  So, to fully abstract the the idea of counterpart semantics in categorical logic and the notion of counterpart frame, we have to consider  the case in which

\[\relazione{D_{\sigma}}{D_f}{D_{\tau}}\]

is an arbitrary relation. Therefore, in this context considering an element $\angbr{a}{b}\in D_f$ can be read as $a$ is the future counterpart with respect the development $f$ of $b$. Therefore, we recall the notion of relational presheaf.

A relational presheaf is a functor $\relpresheaf{\mC}{X}$, where $\Rel$ denotes the category of sets and relations.

The generality of the notion of relational presheaf allows for example to deal with partial functions, and to avoid the previously described situations.

Relational presheaves form a category with finite limits if as morphisms we consider the families of set functions $\psi:=\{\freccia{X_{\sigma}}{f_{\sigma}}{U_{\sigma}}\}_{\sigma\in \mC}$ such that for every $\freccia{\sigma}{g}{\tau}$ of the base category, we have that
\[\angbr{t}{s}\in X_{g}\Rightarrow\angbr{f_{\tau}(t)}{f_{\sigma}(s)}\in U_{g}\]

where $s\in X_{\sigma}$ and $t\in X_{\tau}$.
We call this kind of morphisms relational morphisms, and we denote the category of relational presheaves and relational morphisms as $\relpresheafcat{\mW}$.

Thus, we have seen the link between counterpart frames and relational presheaves. Now we introduce the new notion of counterpart $\mW$-model and we explain how this notion is a categorification of the notion of counterpart model in the sense of [13].

Let $\Sigma$ be a many-sorted signature. A counterpart $\mW$-model is a triple $\Relmodel=(\mW,\sortmodel,\functionmodel)$ such that

* $\mW$ is a category of worlds;

* $\sortmodel=\{\relpresheaf{\mW}{\interp{\tau}{\Relmodel}}\}_{\tau\in S_{\Sigma}}$ is a set of relational preshaves on $\mW$, indexed on $S_{\Sigma}$;

* $\functionmodel=\{\freccia{\interp{\tau_1}{\Relmodel}\times \cdots \times \interp{\tau_m}{\Relmodel}}{\mI(f_{\Sigma})}{\interp{\tau}{\Relmodel}}\}_{f_{\Sigma}\in F_{\Sigma}}$ is a set of morphisms of relational presheaves.

Let us consider a signature $\Sigma$ and a category $\mW$ of worlds. We define the category of counterpart $\mW$-models, denoted by $\ContModelCat{\mW}{\Sigma}$, as the category whose objects are counterpart $\mW$-models $\Relmodel$, and whose morphisms $\freccia{\Relmodel}{F}{\Relmodel'}$ are families of morphisms  $F:=\{\freccia{\interp{\tau}{\Relmodel}}{F_{\tau}}{\interp{\tau}{\Relmodel'}}\}_{\tau\in S_{\Sigma}}$ of relational presheaves, commuting with the relational morphisms of $\functionmodel$ and $\functionmodel'$, i.e. $F_{\tau}\circ \mI(f_{\Sigma})= \mI'(f_{\Sigma})\circ (F_{\tau_1}\times \cdots\times F_{\tau_m})$ for all function symbols  $\freccia{\tau_1\times\cdots\times \tau_m}{f_{\Sigma}}{\tau}\in F_{\Sigma}$ of the signature.

The notion of  counterpart $\mW$-model admits a clear interpretation also from the categorical perspective of functorial semantics. In details, observe that, by definition, a counterpart $\mW$-model $\Relmodel=(\mW,\sortmodel,\functionmodel)$ assigns to every sort $\tau$ of the signature $\Sigma$ a relational presheaf $\relpresheaf{\mW}{\interp{\tau}{\Relmodel}}$ and to every function symbol $f_{\Sigma}$ a morphism of relational presheaves $\freccia{\interp{\tau_1}{\Relmodel}\times \cdots \times \interp{\tau_m}{\Relmodel}}{\mI(f_{\Sigma})}{\interp{\tau}{\Relmodel}}$. Therefore a counterpart $\mW$-model can be represented as a preserving finite products functor $\freccia{\SynCat{\Sigma}}{F_{\mW}}{\relpresheafcat{\mW}}$ from the syntactic category $\SynCat{\Sigma}$ into the category $\relpresheafcat{\mW}$ of $\mW$-presheaves.

Similarly, every such functor $\freccia{\SynCat{\Sigma}}{F_{\mW}}{\relpresheafcat{\mW}}$ induces a counterpart $\mW$-model. It is thus straightforward to check that the following result holds.

For every category $\mW$, the category $\ContModelCat{\mW}{\Sigma}$ of counterpart $\mW$-models is equivalent to the category $\FPfunctors (\SynCat{\Sigma},\relpresheafcat{\mW})$  of finite product preserving functors and natural transformations from the syntactic category $\SynCat{\Sigma}$ to $\relpresheafcat{\mW}$ of relational presheaves over $\mW$.

Notice that if we want to recover in this categorical framework the original idea behind the notion of counterpart models introduced in [13], i.e. that every world is sent to a $\Sigma$-algebra, we just need to consider counterpart $\mW$-models $\Relmodel=(\mW,\sortmodel,\functionmodel)$ where every relational presheaf of $\sortmodel$ sends a morphism $\freccia{\omega}{f}{\sigma}$ of  $\mW$ to a relation $\relazione{\interp{\tau}{\Relmodel}_{\sigma}}{\interp{\tau}{\Relmodel}_f}{\interp{\tau}{\Relmodel}_{\omega}}$ whose converse $\relazione{\interp{\tau}{\Relmodel}_{\omega}}{(\interp{\tau}{\Relmodel}_f)^{\dagger}}{\interp{\tau}{\Relmodel}_{\sigma}}$ is a partial function.

In particular, in the following two results we provide the precise link between counterpart models in the sense of [13]
(see Def. <ref>)
and counterpart $\mW$-models.

Les us consider a counterpart $\mW$-model $\Relmodel=(\mW,\sortmodel,\functionmodel)$ such that  every relational presheaf of $\sortmodel$ sends a morphism $\freccia{\omega}{f}{\sigma}$ of  $\mW$ to a relation $\relazione{\interp{\tau}{\Relmodel}_{\sigma}}{\interp{\tau}{\Relmodel}_f}{\interp{\tau}{\Relmodel}_{\omega}}$ whose converse $\relazione{\interp{\tau}{\Relmodel}_{\omega}}{(\interp{\tau}{\Relmodel}_f)^{\dagger}}{\interp{\tau}{\Relmodel}_{\sigma}}$ is a partial function. Then the triple $\model_{\Relmodel}:=\angbr{W_{\Relmodel}}{\rightsquigarrow_{\Relmodel},d_{\Relmodel}}$ where

* the set of worlds is given by the objects of the category $\mW$, i.e. $W_{\Relmodel}=\mathsf{ob}(\mW)$,

* $\freccia{W_{\Relmodel}}{d_{\Relmodel}}{\Alg}$ is a function assigning to each world $\omega\in W_{\Relmodel}$ the $\Sigma$-algebra $d_{\Relmodel}(\omega):=(A_{\omega},F^{A_{\omega}}_{\Sigma})$ where $A_{\omega}:=\bigcup_{\tau\in S_{\Sigma}}\{\interp{\tau}{\Relmodel}_{\omega}\}$ and $F^{A_{\omega}}_{\Sigma}:=\bigcup_{f_{\Sigma}\in F_{\Sigma}}\{\mI(f_{\Sigma})_{\omega}\}$,

* for every arrow $\freccia{\omega}{f }{\sigma}$ of $\mW$ we define an element $(\omega,cr_f,\sigma)\in \rightsquigarrow_{\Relmodel}$ where the function $\frecciaparziale{d_{\Relmodel}(\omega)}{cr_f}{d_{\Relmodel}(\sigma)}$ is defined on a given typed element $a\in \interp{\tau}{\Relmodel}_{\sigma}$ as  $cr_f(a):=(\interp{\tau}{\Relmodel}_f)^{\dagger}(a)$

is a counterpart model.

Similarly, one can directly check the dual result.

Let $\Sigma:=(S_{\Sigma},F_{\Sigma})$ be a many-sorted signature, and let $\model:=\angbr{W}{\rightsquigarrow,d}$ be a counterpart model. Then the triple $\Relmodel_{\model}=(\mW,\sortmodel,\functionmodel)$ where

* the category $\mW$ is the category whose objects are the worlds of $W$ and whose arrows are obtained by defining

for every element $(\omega_1,cr,\omega_2) \in  \rightsquigarrow$ a generating arrow $cr:\omega_1\to\omega_2$,

* for a sort $\tau$ of $S_{\Sigma}$ we define the relational presheaf $\relpresheaf{\mW}{\interp{\tau}{\Relmodel_{\model}}}$ by the assignment $\interp{\tau}{\Relmodel_{\model}}_{\omega}:=d(\omega)_{\tau}$ and for a generating arrow $\freccia{\omega_1}{cr}{\omega_2}$ of $\mW$ we define $\interp{\tau}{\Relmodel_{\model}}_{\omega}:=(cr)^{\dagger}_{\tau}$,

* for any function symbol $\freccia{\tau_1\times \cdots \times \tau_m}{f_{\Sigma}}{\tau}$ of $\in F_{\Sigma}$ we define the natural transformation $\freccia{\interp{\tau_1}{\Relmodel_{\model}}\times \cdots \times \interp{\tau_m}{\Relmodel_{\model}}}{\mI(f_{\Sigma})}{\interp{\tau}{\Relmodel_{\model}}}$ by the assignment $\mI(f_{\Sigma})_{\omega}:=f_{\Sigma}^{d(\omega)}$

is a  counterpart $\mW$-model and every relational presheaf of $\sortmodel$ sends a morphism  $\freccia{\omega}{f}{\sigma}$ of  $\mW$ to a relation $\relazione{\interp{\tau}{\Relmodel_{\model}}_{\sigma}}{\interp{\tau}{\Relmodel_{\model}}_f}{\interp{\tau}{\Relmodel_{\model}}_{\omega}}$ whose converse $\relazione{\interp{\tau}{\Relmodel_{\model}}_{\omega}}{(\interp{\tau}{\Relmodel_{\model}}_f)^{\dagger}}{\interp{\tau}{\Relmodel_{\model}}_{\sigma}}$ is a partial function.

Let $\Sigma:=(S_{\Sigma},F_{\Sigma})$ be a many-sorted signature, and let $\model:=\angbr{W}{\rightsquigarrow,d}$ be a counterpart model. Notice that if we first construct the counterpart $\mW$-model $\Relmodel_{\model}$ employing Proposition <ref>, and then we construct the counterpart model $\model_{(\Relmodel_{\model})}$ employing Proposition <ref>, we have that the counterpart model $\model_{(\Relmodel_{\model})}$ may be different from
$\model$. As it will be shown in Theorem <ref>,
when considering temporal structures such a difference will be irrelevant, from a semantic point of view.

Let us consider the ordinary signature $\Sigma_{Gr}=(S_{Gr},F_{Gr})$ for directed graphs introduced in Example <ref>.
The notion of counterpart $\mW$-model allows us to provide a categorical presentation of the counterpart semantics  presented in [13].
In this case, a counterpart $\mW$-model $\Relmodel_{Gr}=(\mW,\mathfrak{S}_{\Sigma_{Gr}},\mathfrak{F}_{\Sigma_{Gr}})$ consists of

* a category of worlds $\mW$;

* $\mathfrak{S}_{\Sigma_{Gr}}=\{\interp{\tau_N}{\Relmodel},\interp{\tau_E}{\Relmodel}\}$, where $ \interp{\tau_N}{\Relmodel}$and $\interp{\tau_E}{\Relmodel}$ are two relational presheaves on the category $\mW$ of worlds such that $(\interp{\tau_N}{\Relmodel}_f)^{\dagger}$ and $(\interp{\tau_E}{\Relmodel}_f)^{\dagger}$ are partial functions for every arrow $\freccia{\omega}{f}{\sigma}$ of $\mW$;

* $\mathfrak{F}_{\Sigma_{Gr}}=\{\mI(s),\mI(t)\}$, where$\freccia{\interp{\tau_E}{\Relmodel}}{\mI(s)}{\interp{\tau_N}{\Relmodel}}$ and $\freccia{\interp{\tau_E}{\Relmodel}}{\mI(t)}{\interp{\tau_N}{\Relmodel}}$ are two morphisms of relational presheaves such that every component $\mI(t)_{\omega}$ and $\mI(s)_{\omega}$ is a function.

As anticipated in Proposition <ref>, to present as particular case the notion of counterpart model  in [13], where each world is sent to a directed graph, we needed to require that both $\mI(t)_{\omega}$ and $\mI(s)_{\omega}$ are functions for every world $\omega$.
Therefore, given the model $\Relmodel_{Gr}$, we have again that every world $\omega$ is mapped to a directed graph
\[d(\omega):=(\interp{\tau_N}{\Relmodel}_{\omega},\interp{\tau_E}{\Relmodel}_{\omega}, \mI(s)_{\omega},\mI(t)_{\omega}) \]
identified by the set of nodes $\interp{\tau_N}{\Relmodel}_{\omega}$, the set of arcs $\interp{\tau_E}{\Relmodel}_{\omega}$, and the two functions $\freccia{\interp{\tau_E}{\Relmodel}_{\omega}}{\mI(s)_{\omega},\mI(t)_{\omega}}{\interp{\tau_N}{\Relmodel}_{\omega}}$. Moreover, every morphism $\freccia{\omega}{f}{\sigma}$ of the category $\mW$ induces a partial homomorphism of directed graphs
\[\frecciaparziale{d(\omega) }{cr_f}{d(\sigma) }\]

given by $cr_f:=((\interp{\tau_N}{\Relmodel}_f)^{\dagger},(\interp{\tau_E}{\Relmodel}_f)^{\dagger})$.

As an instance of Example <ref>, we consider our running example, i.e. the three graphs $\mathbf{G}_0$, $\mathbf{G}_1$ and $\mathbf{G}_2$ presented in Fig. <ref> of Example <ref>. In this case we consider a category $\mW$ whose objects are three worlds $\omega_0$, $\omega_1$ and $\omega_2$ and the morphisms are generated by the compositions of

\[
\xymatrix{
\omega_0\ar[r]^{f_0} & \omega_1<EMAIL_ADDRESS><EMAIL_ADDRESS>& \omega_2\ar[r]^{f_3}& \omega_2.
\]

The relational presheaves of nodes and edges are given by the assignment

* $\interp{\tau_N}{\Relmodel}_{\omega_i}:=N_{\mathbf{G}_i}$, where $N_{\mathbf{G}_i}$ is the set of nodes of the graph $\mathbf{G}_i$;

* $\interp{\tau_N}{\Relmodel}_{f_0}:=\{(n_3,n_0),(n_4,n_1),(n_3,n_2) \}\subseteq N_{\mathbf{G}_1}\times N_{\mathbf{G}_0}$;

* $\interp{\tau_N}{\Relmodel}_{f_1}:=\{(n_5,n_3),(n_5,n_4)\}\subseteq N_{\mathbf{G}_2}\times N_{\mathbf{G}_1}$;

* $\interp{\tau_N}{\Relmodel}_{f_2}:=\{(n_5,n_3),(n_5,n_4)\}\subseteq N_{\mathbf{G}_2}\times N_{\mathbf{G}_1}$;

* $\interp{\tau_N}{\Relmodel}_{f_3}:=\{(n_5,n_5)\}\subseteq N_{\mathbf{G}_2}\times N_{\mathbf{G}_2}$;

* $\interp{\tau_E}{\Relmodel}_{\omega_i}:=E_{\mathbf{G}_i}$, where $E_{\mathbf{G}_i}$ is the set of edges of the graph $\mathbf{G}_i$.

* $\interp{\tau_E}{\Relmodel}_{f_0}:=\{(e_3,e_0),(e_4,e_1) \}\subseteq E_{\mathbf{G}_1}\times E_{\mathbf{G}_0}$;

* $\interp{\tau_E}{\Relmodel}_{f_1}:=\{(e_5,e_3)\}\subseteq E_{\mathbf{G}_2}\times E_{\mathbf{G}_1}$;

* $\interp{\tau_E}{\Relmodel}_{f_2}:=\{(e_5,e_4)\}\subseteq E_{\mathbf{G}_2}\times E_{\mathbf{G}_1}$;

* $\interp{\tau_E}{\Relmodel}_{f_3}:=\{(e_5,e_5)\}\subseteq E_{\mathbf{G}_2}\times E_{\mathbf{G}_2}$.

The natural transformations $\mI(s),\mI(t)$ are the domain and codomain maps. Notice that both $(\interp{\tau_N}{\Relmodel}_{f_i})^{\dagger}$ and $(\interp{\tau_E}{\Relmodel}_{f_i})^{\dagger}$ are partial functions for $i=0\dots 3$. Therefore we are under the hypotheses of Proposition <ref>. Thus, following the assignment of Example <ref>, we can consider the counterpart model $\angbr{W}{\rightsquigarrow,d}$ corresponding to the counterpart $\mW$-model, and we have that $d(\omega_i)=\mathbf{G}_i$, and $cr_{f_i}$ can be represented graphically as follows

[style=new style 0] (0) at (-11, 6) $n_0$;
[style=new style 0] (1) at (-5, 6) $n_1$;
[style=new style 0] (2) at (-8, 2) $n_2$;
[style=new style 1] (3) at (-11, 4) $e_2$;
[style=new style 1] (4) at (-5, 4) $e_1$;
[style=new style 1] (5) at (-8, 8) $e_0$;
[style=new style 0] (6) at (-1, 5) $n_3$;
[style=new style 0] (7) at (4.75, 5) $n_4$;
[style=new style 1] (8) at (2, 8) $e_3$;
[style=new style 1] (9) at (2, 2) $e_4$;
[style=new style 0] (10) at (11, 6.25) $n_5$;
[style=new style 1] (13) at (11, 3.5) $e_5$;

(2) to (3);
(0) to (5);
(1) to (4);
[style=freccia] (4) to (2);
[style=freccia] (3) to (0);
[style=freccia] (5) to (1);
(6) to (8);
(7) to (9);
[style=freccia] (9) to (6);
[style=freccia] (8) to (7);
[bend right=60, looseness=1.50] (10) to (13);
[style=freccia, bend right=60, looseness=1.50] (13) to (10);
[style=freccia_tratteggiata, bend left=15] (5) to (8);
[style=freccia_tratteggiata, bend left=15] (1) to (7);
[style=freccia_tratteggiata, bend right=15] (0) to (6);
[style=freccia_tratteggiata, bend right=45] (2) to (6);
[style=freccia_tratteggiata, bend right, looseness=0.75] (4) to (9);
[style=freccia_tratteggiata, in=-120, out=-30, loop] (13) to ();
[style=freccia_tratteggiata, in=135, out=45, loop] (10) to ();
[style=new edge style 0, bend right=45] (9) to (13);
[style=new edge style 0, bend right=45] (6) to (10);
[style=new edge style 0, bend right] (7) to (10);
[style=new edge style 1, bend left] (7) to (10);
[style=new edge style 1, bend left] (6) to (10);
[style=new edge style 1, in=-165, out=0, looseness=1.25] (8) to (13);

A counterpart model with three sequential worlds

This counterpart model in Figure <ref> illustrates two  executions of our running example instantiated with three processes (edges). The two evolutions try to instantiate the main features of our logic, as presented in the next sections. The counterpart relations (drawn with dotted lines and colors to distinguish $cr_{f_1}$ from $cr_{f_2}$) reflect
the fact that at each transition one process (edge) is discarded and its source and target channels (nodes)
are merged. In particular, the transition
$cr_{f_0}:=((\interp{\tau_N}{\Relmodel}_{f_0})^{\dagger},(\interp{\tau_E}{\Relmodel}_{f_0})^{\dagger})$ deletes edge $e_2$ and merges nodes $n_0$ and $n_2$ into $n_3$. Similarly for $cr_{f_1}$ and $cr_{f_2}$, while $cr_{f_3}$ is a cycle preserving both $e_5$ and $n_5$ , denoting that the system is idle, yet alive.

§.§ Relational power-set presheaf

While presheaves form a topos, and then the category of presheaves is strong enough to deal with higher-order features, relational presheaves on a given category rarely have such a structure, as observed in [27].

This is due to the fact that the category $\Set$ is a topos while the category of sets and relations $\Rel$ is not a topos, but an allegory [12].
To give an intuition of what an allegory is we recall the paradigm of [12]: allegories  are to binary relations between sets as categories are to functions between sets.

However, even if  the category of sets and relations lacks the topos structure, and in particular power-objects, one could employ relational presheaves for higher-order using the structure of power-allegory of the category of relations. For the formal definition and the proof that $\Rel$ is a power-allegory we refer the reader to <cit.>, while now we briefly discuss how one can define the power-set relational presheaf $\relpresheaf{\mC}{\powerelpresheaf{X}}$ of a given presheaf $\relpresheaf{\mC}{X}$.

So, let us consider a relational presheaf $\relpresheaf{\mC}{X}$. While the action of the functor $\relpresheaf{\mC}{\powerelpresheaf{X}}$ we are going to define is clear on the objects, i.e. $\sigma$ is sent to the power-set $\mathrm{P}(X_{\sigma} )$ of $X_{\sigma}$, the problem of lifting a relation $\relazione{X}{R}{Y}$ to a relation on the power-sets $\relazione{\mathrm{P}(A)}{R'}{\mathrm{P}(B)}$ has to be treated carefully.

In fact, one could define for every morphism $\freccia{\sigma}{f}{\omega}$  of $\mC$ the relation $\relazione{\powerelpresheaf{X}_{\omega}}{\powerelpresheaf{X}_f}{\powerelpresheaf{X}_{\sigma}}$ such that for every $A\subseteq X_{\omega}$ and $B\subseteq X_{\sigma}$ we have

\[\angbr{A}{B}\in\powerelpresheaf{X}_f \iff (\forall a\in A, \; \exists b\in B : \angbr{a}{b}\in X_f)\And (\forall b\in B, \; \exists a\in A : \angbr{a}{b}\in X_f). \]

This is a quite natural way of lifting relations to relations of power-sets, but notice that in this case $\powerelpresheaf{X}$ is just a lax-functor, and not a functor. In fact, we have that $\powerelpresheaf{X}_{gf}\subseteq \powerelpresheaf{X}_f\powerelpresheaf{X}_g$, but these two sets are not equal.

Since we are interested in considering relational presheaves in the strict sense, we have to lift relations in a different way. To this aim we employ the known equivalence between relations and Galois connections (or maps) on power-sets [14], i.e. the equivalence between $\Rel$ and $ \mathrm{Map}(\mathbf{Pow}) $.

Recall from <cit.> that given a relation $\relazione{A}{R}{B}$, we can define a function (preserving arbitrary unions) $\freccia{\mathrm{P}(B)}{P_R}{\mathrm{P}(A)}$ by assigning

$$P_R(S):=\{ a\in A \; | \exists b\in S \; : aRb\}$$

to every subset $S\subseteq B$. Moreover, given the equivalence $\Rel\equiv \mathrm{Map}(\mathbf{Pow}) $, and using the fact that $\mathbf{Pow}=(\mathbf{Pow}^{\op})^{\op}$, we can immediately conclude that the assignment $R\mapsto P_R $ preserves the compositions and the identities.

Let $\relpresheaf{\mC}{X}$ be a relational presheaf. The relational power-set presheaf $\relpresheaf{\mC}{\powerelpresheaf{X}}$ is the functor defined as

* for every object $\sigma\in \mC$, $\powerelpresheaf{X}(\sigma)$ is the power-set of $X_{\sigma}$;

* for every $\freccia{\sigma}{f}{\omega}$ we define the relation $\relazione{\powerelpresheaf{X}_{\omega}}{\powerelpresheaf{X}_f}{\powerelpresheaf{X}_{\sigma}}$ as $\powerelpresheaf{X}_f:=P_{X_f}$.

In particular, the relational presheaf $\relpresheaf{\mC}{\powerelpresheaf{X}}$ is an ordinary presheaf $\presheaf{\mC}{\powerelpresheaf{X}}$. Finally, given a relational presheaf $\relpresheaf{\mC}{X}$ we define the epsiloff relational presheaf $\relpresheaf{\mC}{\in_{X}}$.

Let $\relpresheaf{\mC}{X}$ be a relational presheaf. The epsiloff relational presheaf is the functor $\relpresheaf{\mC}{\in_{X}}$ defined as

* for every $\sigma\in \mC$, $\in_X(\sigma):=\{(a,A)\in X_{\sigma} \times \powerelpresheaf{X}_{\sigma} \; |\; a\in A\}$;

* for every $\freccia{\sigma}{f}{\omega}$, $(\in_X)_f$ is the relation given by $\angbr{(b,B)}{(a,A)}\in(\in_X)_f $ if and only if $\angbr{b}{a}\in X_f$ and $\powerelpresheaf{X}_f(B)=A$ where $B\subseteq X_{\omega}$ and $A\subseteq X_{\sigma}$.

It is direct to check that $\in_X$ is a functor, i.e. that it preserves compositions and identities, and also that, while the relational power-set presheaf is a set-valued sheaf, the epsiloff presheaf is just a relational presheaf in general.

§.§ Flow time and transition system

In this section we provide an overview of some possible specialization regarding the base category of worlds $\mW$ on our previous model, depending on which kind of systems we are going to consider. As anticipated, the idea is that the base category $\mW$ of our presheaves model represents an arbitrary system in which we have objects that may represent states, or instant of time, biological systems,  and arrows which represents a computational step from a state into another, a time development or an evolution.

A great advantage of this categorical abstraction is that one can easily specialized these models just considering as base category different classes of categories. In the following, we summarize some natural structures that one may consider if for example, we want to deal with the evolution of instants of time, or if we want to consider a labelled translation system.

Notation: in the following subsections we recall some definitions of particular kind of Kripke frame used in different contexts. To denote the free category generated by a given structure $S=(\mathrm{set},\mathrm{relation})$ we use the notation $\mC(S)$.

§.§.§ Flows of time, and temporal structures

With the rise in the 20th century of formal logical languages, it became natural to try to express temporal concepts and arguments in formal terms, and so it was that Arthur Prior from the 1950s came to develop tense logics. These were modal logics, with box-modalities
for ‘always in the past’ and ‘always in the future’, motivated by tenses in natural language. The advent of Kripke semantics in the 1960s gave the enterprise a boost, because a Kripke frame is so naturally seen as a set of time points endowed with
an ‘earlier-later’ relation.

Since Pnueli’s pioneering 1977 paper [28], several branches of computer science and related
ﬁelds — such as databases, speciﬁcation and veriﬁcation, synthesis of programs, temporal
planning, temporal knowledge representation — have had a huge inﬂuence, and the
use of temporal logic in some of these areas has developed to the point of commercial

The main idea is that models and structures for temporal logics have to be composed by three parts: a set of time points; a set whose elements are time points, and information about which time points come before or after which.

Formally, a simple way to express these concept is to consider the so-called flow of time.

A flow of time is a pair $(T,<)$ where $T$ is a non-empty set whose elements are called time points, and $<$ is an irreﬂexive and transitive binary relation on $T$.

Given two time points $s,u\in T$, the idea is that $s<u$ will mean intuitively that $s$ is earlier of $u$, or that $u$ is later than $s$. In this setting, the requirements that $<$ be irreﬂexive is motivated by the fact that no time point should be in the past or future of itself, and also $<$ is required to be transitive because $t$ is earlier
than $u$, and $u$ earlier than $v$, then we expect $t$ to be earlier than $v$.

Now we recall some classes of ﬂows of time, which will allow modelling several different situations.

A flow of time $(T,<)$ is said to be linear if given any two distinct time points in it, one is before the other, i.e. for every $s,t\in T$, we have that $s=t\vee s<t \vee t<s$.

An interesting class of linear flow time is provided by the class of discrete linear flow of time. This kind of flow of time are, intuitively, flow of time in which we can identify for every point $t$ an immediate predecessor and a immediate successor.

A linear flow of time $(T,<)$ is said discrete if for each $t\in T$

* if there exists an element $u\in T$ such that $t< u$, then there is a first such $u$, i.e. there is an element $u$ such that there is no $v\in T$ satisfying $t<v<u$.

* if there exists an element $u\in T$ such that $u<t$, then there is a last such $u$, i.e. there is an element $u$ such that there is no $v\in T$ satisfying $u<v<t$.

A linear, discrete flow of time can be simply represented as a sequence of point on the same line as follow

[shorten >=1pt,->]
vertex=[circle,draw=black,fill=black!30,minimum size=10pt,inner sep=0pt]

/in 1/1, 2/2, 3/3, 4/4, 5/5,
6/6, 7/7, 8/8, 9/9, 10/10
[vertex] (G-) at (,0) ;

/→in 1/2,2/3,3/4,4/5,5/6, 6/7, 7/8, 8/9, 9/10
(G-) – (G-→);

Linear flow of time

Notice that a strong limitation of linear, discrete flow of time is that every point of time has to evolve or change in a unique way. This can present a serious restriction, in particular for applications. To this purpose, we recall another class of flow of time which is also much used:

A flow of time $(T,<)$ is said to be a tree if for all $t\in T$ the set $\{ u\in T\; | \; u<t\}$ is linearly ordered by $<$. A branch of a tree is a maximal is a maximal linearly-ordered subset of $T$.

[shorten >=1pt,->]
vertex=[circle,draw=black,fill=black!30,minimum size=10pt,inner sep=0pt]

/in 1,...,4
[vertex] (A-) at (0,0.8*-0.3) ;

/in 1,...,6
[vertex] (B-) at (2.5,0.8*-0.5) ;

/→in 1/1,1/2,2/3,3/4,3/5,3/6
(A-) – (B-→);

/in 1,...,10
[vertex] (C-) at (5,0.6*-1.15) ;
/→in 1/1,1/2,2/3,2/4,2/5,4/6,4/7,4/8,5/9,6/10
(B-) – (C-→);

Tree flow of time

In a tree, the past of any time point is linear. However, its future may not be, so that
many branches may pass through (i.e., contain) any given time point. This because the future is often used to capture the indeterminacy of the future: openness, choices and chances. The linearity of the past instead captures the ﬁxed, (already) determined
nature of that part of time.

§.§.§ Labelled translation systems

The notion of Kripke frame as well as the notion flow of time are simple an intuitive abstraction of systems or instants that evolve or change over time. However, notice that both of them suffer of the limitation that the relation between worlds or instant of time has to be binary. This represents a serious constrain if, for example, one wants to consider a simple situation in which a system could evolve in another one through two distinct developments. Moreover, the requirement that the relation $<$ in the definition of flow of time to be transitive and irreflexive does not allow to consider reversible process or reversible developments. This is quite natural if one has to work with time developments, but if we are interested in a more general situation, we have to consider differents notions.

A labelled transition system (LTS) is a triple $(S,L,\rightarrow)$, where $S$ is a non-empty set of states, $L$ is the set of labels, and $\rightarrow\subset S\times L\times S$ is a relation, which is total in the first component, i.e. for every $s\in S$ there exists a label $l\in L$ and a state $s'$ such that $(s,l,s')\in \rightarrow$.

[->,>=stealth',shorten >=1pt,auto,node distance=2cm,

every state=[circle,draw=black,fill=black!30,minimum size=15pt,inner sep=0pt]

[state]         (A)                    $s_1$;
[state]         (B) [above right of=A] $s_2$;
[state]         (D) [below right of=A] $s_3$;
[state]         (C) [below right of=B] $s_4$;
[state]         (E) [right of=C]       $s_5$;

(A) edge              node $l_1$ (B)
edge              node $l_2$ (C)
(B) edge [loop above] node $l_3$ (B)
edge              node $l_4$ (C)
edge [bend left]  node $l_6$ (E)
(C) edge              node $l_5$ (D)
(D) edge [loop below] node $l_7$ (D)
edge              node $l_8$ (A)
(E) edge [bend left]  node $l_9$ (D);

Labelled transition system

An interesting generalization of the notion of labelled transition system is that of modal labelled transition system (MLTS). This notion is a specification formalism introduced by Larsen and  Thomsen  in <cit.>, allowing  for  stepwise  refinement  design  of  systems and their composition. A considerable attention has been recently paid to (MTS) due  to  many  applications,  e.g.  component-based  software  development <cit.>, interface theories <cit.>, or modal abstractions and program analysis <cit.>.

In particular, <cit.> the authors introduced the notion of modal labelled transition system to study the refinement of actions, considering modal automata as standard automata with modalities may or must.

[->,>=stealth',shorten >=1pt,auto,node distance=3.5cm and 2cm]

every state=[rectangle,draw=black,fill=black!30,minimum size=15pt,inner sep=2pt]

[state]         (A)                    client;
[state]         (B) [above right of=A] server;
[state]         (D) [below right of=A] server;
[state]         (C) [below right of=B] database;

(A) edge[style=dashed]         node request (B)
(B) edge[style=dashed]         node query (C)
edge[style=dashed]         node  processing (D)
(C) edge                         node answer (D)
(D) edge                         node response (A);

Modal labelled transition system

Figure <ref> depicts an (MLTS) that has arisen as a composition of three systems and specifies the following. A request from a client may arrive. Then we can process it directly or make a query to a database where we are guaranteed an answer. In both cases we send a response.

This idea is formalized by considering an arbitrary second relation of labeling $\dashrightarrow$ on a given (LTS) contained in the main one. This allows us to formally distinguish some particular processes from the other one.

A modal labelled transition system (MLTS) is defined by four elements $(S,L,\rightarrow,\dashrightarrow)$, where $(S,L,\rightarrow)$ is a labelled transition system (LTS), and $\dashrightarrow\subseteq S\times L\times S$ is a relation satisfying the so-called syntactic consistency requirement, i.e. $\dashrightarrow\subseteq  \rightarrow$.

If the syntactic consistency requirement is not imposed, we obtain a mixed transition systems as introduced in <cit.>.

Notice that given a modal labelled transition system (MLTS) the second relation $\dashrightarrow$ may be considered not only as processes that must happen, but this second class can be represent an arbitrary class of chosen processes or development that we want to distinguish from the rest of the processes. For example, the class $\dashrightarrow$ may represent a class of observable processes, or a class of atomic operations.

§ SYNTAX OF QUANTIFIED TEMPORAL LOGIC

Before presenting the syntax of our logic, we consider a set of second-order variables $\chi\in \mathcal{X}$, where a variable $\chi_{\tau}$ with sort $\tau\in S_{\Sigma}$ ranges over sets of elements of sort $\tau$.

Let $\Sigma$ be a many-sorted signature, $X$ a set of first-order variables and $\mathcal{X}$ a set of second-order variables, both typed over $S_{\Sigma}$. The set $\mF_{\Sigma}$ of formulae of our temporal logic is generated by the rules

\[\phi:= \mathsf{tt} \; | \; \varepsilon\in_{\tau} \chi  \;|\; \neg \phi\; |\; \phi \vee \phi \;| \; \exists_{\tau}x. \phi \;| \; \exists_{\tau}\chi. \phi \; |\; \nextoperator \phi \; |\; \phi_1 \untiloperator \phi_2.  \]

Whenever clear from the context, subscripts and types may be omitted.

The next operator $\nextoperator$ provides a way of asserting that something has to be true at the next step, i.e. $\nextoperator \phi$ means that $\phi$ has to hold at the next state.

The until operator $\untiloperator$ can be explained as follows: $ \phi_1 \untiloperator \phi_2$ means that $\phi_1$ has to hold at least until $\phi_2$ becomes true, which must hold at the current or a future position.
The sometimes modality $\dm$ is obtained as $\dm \phi:=\mathsf{tt} \untiloperator \phi$ and the always modality $\sq$ as $\sq \phi:= \neg \dm \neg \phi$.

Notice that the standard boolean connectives $\vee,\rightarrow, \leftrightarrow$ and the universal quantifiers can be derived as usual. Moreover, the typed equality $=_{\tau}$ can be derived as $\epsilon_1=_{\tau}\epsilon_2\equiv \forall_{\tau} \chi.( \epsilon_1\in_{\tau} \chi \leftrightarrow \epsilon_2\in_{\tau} \chi)$.
We also remark that $\in_{\tau}$ is a family of membership predicates typed over $S_{\Sigma}$ indicating that the
evaluation of a term with sort $\tau$ belongs to the evaluation of a second-order variable with the same sort

As usual, we consider formulae in context, defined as $[\Gamma, \Delta] \; \phi$, where $\phi$ is a formula of $\mF_{\Sigma}$, $\Gamma$ is a first-order context and $\Delta$ is the second-order context.

We now move to a different syntax that is equivalent to the previous one, yet  describes only those
formulae which are in positive form. Such a syntax includes derived operators in order to have
negation applied only to atomic proposition. This is a standard presentation for linear time temporal logics, and it will be pivotal for our semantics, since it allows to capture negation in terms of set complementation.

Let $\Sigma$ be a many-sorted signature, $X$ a set of first-order variables and $\mathcal{X}$ a set of second-order variables, both typed over $S_{\Sigma}$. The set $\mF_{\Sigma}$ of positive formulae of our temporal logic is generated by the rules

\[\phi:= \mathsf{tt} \; | \; %\mathsf{ff} \;|\;
\varepsilon\in_{\tau} \chi  \;|\; \neg \phi
\]

\[\psi:= \phi\;|\;\psi \vee \psi \;| \; \psi \wedge \psi \;| \;  \exists_{\tau}x. \phi \;| \; \exists_{\tau}\chi. \psi \; |\;  \;| \;  \forall_{\tau}x. \phi \; |\;\forall_{\tau}\chi. \psi \; |\; \nextoperator \psi \; |\; \psi_1 \untiloperator \psi_2  \; |\; \psi_1 \wuntiloperator \psi_2  \]

where  $\psi_1 \wuntiloperator \psi_2 $ denotes the weak until operator.

Now $ \psi_1 \wuntiloperator \psi_2$ means that $\psi_1$ has to hold at least until $\psi_2$ or, if $\psi_2$ never becomes true, $\psi_1$ must remain true forever. We will often use $\mathsf{ff}$ for $\neg \mathsf{tt}$.
In this setting, the operators $\dm$ and $\sq$ can be presented as $\dm \psi := \mathsf{tt}\untiloperator \psi$ and $\sq\psi := \psi \wuntiloperator \mathsf{ff}$.

On the following we will mostly consider just positive formulae, hence dropping the adjective whenever it is not ambiguous.

Consider again the graph signature, the counterpart model of Figure <ref>, and the typed predicates $\mathbf{present}_{\tau} (x)\equiv \exists_{\tau} y.x=_{\tau} y$ regarding the presence of an entity with sort $\tau$ in a world (the typing is usually omitted). Combining this with next operator we can speak about elements that are present at the given world and that will be present at the next step for example, i.e.  $\mathbf{present}_{\tau} (x)\wedge \nextoperator ( \mathbf{present}_{\tau} (x))$.

Instead, notice that even if $\neg \mathbf{present}_{\tau} (x)$ is a formula of our logic, it is not in positive form. An equivalent formula in positive form is $\forall_{\tau} y.x\neq_{\tau} y$, where the expression $x\neq_{\tau} y$ is equivalent to
$\exists_{\tau} \chi.( x\in_{\tau} \chi \wedge y \not \in_{\tau} \chi)$. For the sake of conciseness, we will freely use both $\neg \mathbf{present}_{\tau} (x)$ and $x\neq_{\tau} y$.

Moreover, consider the predicate $\mathbf{loop}(x) \equiv s(x) = t(x)$ characterizing the presence of a cycle. The following formulae

express different properties of our running example: $\nextoperator ( \exists_{\tau_E} x.\mathbf{loop}(x))$ states that at the next step there exists a loop, i.e. an edge whose source and target are equal. The formula $\sq (\mathbf{present}_{\tau_E} (x))$ means that for all the evolutions of our systems there exists at least an edge. The formula $\exists_{\tau_N}x. (((x\neq y) \wedge\nextoperator (x=y))$ means that given a node $y$, there exists another different node that at the next step will be identified with $y$ at the next step. Finally, the formula $ \sq (\exists_{\tau_E}e. s(e)=x\wedge t(e)=y) $ means that the nodes $x$ and $y$ will always be connected by an edge.

§ TEMPORAL STRUCTURES AND SEMANTICS

§.§ Temporal structures

The notion of hyperdoctrine was introduced by Lawvere in a series of seminal papers [23, 22] to provide a categorical framework for first order logic.

In recent years, this notion has been generalized in several settings, for example introducing elementary and existential doctrines [25, 31] and
modal hyperdoctrines [5].

In particular, in [17, 16] modal hyperdoctrines are introduced employing the notion of attribute associated to a given presheaf, or more generally, to a relational presheaf as a categorification of the model semantics. We start recalling the notion of set of classical attributes, and then we show how by simply fixing a class of morphisms of the base category of a presheaf, we can construct the main temporal operators.

Let $\relpresheaf{\mW}{X}$ be a relational presheaf. We define the set

\[ \att(X):=\{ \{A_{\omega}\}_{\omega\in \mW} \; |\; A_{\omega}\subseteq X_{\omega}\}\]

whose objects are called classical attributes.

The set of classical attributes has a natural structure of complete boolean algebra when we consider the order provided by the inclusion.
Moreover, a morphism $\freccia{X}{f}{D}$ of relational presheaves induces a morphism of boolean algebras

between the sets of classical attributes. In particular, this action is given by pulling back world-by-world, i.e. for $A\in \att (D)$, computing the pullback for every world $\omega$ as below and defining $f^*(A):=\{f_{\omega}^*(A_{\omega})\}_{\omega\in  \mW}\in \att (X)$ for each $A\in \att( D)$.

\[\xymatrix{
f_{\omega}^*(A_{\omega})\ar@{^{(}->}[r]\ar[d] & X_{\omega}\ar[d]^{f_\omega}\\
A_{\omega}\ar@{^{(}->}[r]& D_{\omega}

Given a relational presheaf $\relpresheaf{\mW}{X}$ and a classical attribute $A=\{A_{\omega}\}_{\omega\in \mW}$ of $ \att(X)$ and an element $s\in X_{\omega}$, we use the validity notation
to mean that $s\in A_{\omega}$. Therefore, writing $s\vDash^X_{\omega}A$ means that at the world or instant $\omega$, an individual $s$ of $X_{\omega}$ satisfies the property $A$.

We say that a relational presheaf  $\relpresheaf{\mW}{X}$ is equipped with a temporal structure $\mathrm{T}$, if the base category $\mW$ is considered together with a class of morphisms $\mathrm{T}$.

Given a relational presheaf $\relpresheaf{\mW}{X}$, the idea is that the class $\mathrm{T}$ represents the atomic processes or the indecomposable operations of $\mW$.

Given a temporal structure $\mathrm{T}$ on $\relpresheaf{\mW}{X}$ we denote by $\cammini{\mathrm{T}}{\omega}$ the class of sequences $\mathrm{t}:=(t_1,t_2,t_3,\dots)$ of arrows such that $t_n\in T$ and such that $\domain{t_1}=\omega$ and $\codomain{t_i}=\domain{t_{i+1}}$ for $i\geq 1$.

Given a sequence $\mathrm{t}:=(t_1,t_2,t_3,\dots)$ we denote by $\mathrm{t}_{\leq i}$ the arrow $t_it_{i-1}\cdots t_1$. Moreover we denote $\omega_i:=\codomain{t_i}$.

The intuition is that the class of arrows $\cammini{\mathrm{T}}{\omega}$ represents the $\mathrm{T}$-evolutions of the state $\omega$.

The choice of the name temporal structure is due to the fact that by simply fixing a class $\mathrm{T}$, we can define operators $\nextoperator$, $\untiloperator$, $\sq$ and $\dm$ on the complete boolean algebra $\att(X)$ of classical attributes.
Notation: we denote by $\mathrm{I}_c$ the closure under composition of the arrows of $\mathrm{I}$.

For every element $A:=\{A_{\omega}\}_{\omega\in \mW} $ of $\att (X)$ we define

* $s \vDash^X_{\omega} \nextoperator (A) $ if and only if for every arrow $\freccia{\omega}{f}{\sigma}$ arrow of $\mathrm{I}$, there exists an element $t\in X_{\sigma} $ such that $\angbr{t}{s}\in X_f$ and  $t \vDash^X_{\sigma} A $;

* $s\vDash^X_{\omega} A\untiloperator B$ if and only if there exists $C_{\omega}\subseteq X_{\omega}$ such that $s\in C_{\omega}$ and $C_{\omega}=B_{\omega} \vee (A_{\omega} \wedge \nextoperator (C)_{\omega})$;

* $s\vDash^X_{\omega}\sq A$ if and only if for every object $\sigma\in \mC$ and every arrow $\freccia{\omega}{f}{\sigma}$ of $\mathrm{I}_c$, if $\angbr{e}{s}\in X_f$ then $e\vDash^X_{\sigma}A$;

* $s\vDash_{\omega}^X \dm A$ if and only if there exists an object $\sigma$, an arrow $\freccia{\omega}{f}{\sigma}$ of $\mathrm{I}_c$, and an element $t\in X_{\sigma}$ such that $\angbr{t}{s}\in X_f$ and $t\vDash^X_{\sigma} A.$

Proposta 2 :

Let us consider a temporal structure $\mathrm{T}$ on $\relpresheaf{\mW}{X}$. For every element $A:=\{A_{\omega}\}_{\omega\in \mW} $ of $\att (X)$  and $s\in X_{\omega} $ we define

* $s \vDash^X_{\omega} \nextoperator (A) $ if and only if for every arrow $\freccia{\omega}{t}{\sigma}$ of $\mathrm{T}$, there exists an element $z\in D_{\sigma} $ such that $\angbr{z}{s}\in X_t$ and  $z \vDash^X_{\sigma} A $;

* $s\vDash^X_{\omega} A\untiloperator B$ if for every $\mathrm{t}\in \cammini{T}{\omega}$ there exists an $\bar{n}$ such that for every $i\leq \bar{n}$ there exists $z_i\in X_{\omega_i} $ such that $\angbr{z_i}{s}\in X_{t_{\leq i}}$ and $z_i \vDash^X_{\omega_i} A $ and an element $z_{\bar{n}}\in X_{\omega_{\bar{n}}} $ such that $\angbr{z_{\bar{n}}}{s}\in X_{t_{\leq \bar{n}}}$ and $z_{\bar{n}} \vDash^X_{\omega_{\bar{n}}} B $.

* $s\vDash^X_{\omega} A\wuntiloperator B$ if for every $\mathrm{t}\in \cammini{T}{\omega}$, we have that for every $i$ there exists $z_i\in X_{\omega_i} $ such that $\angbr{z_i}{s}\in X_{t_{\leq i}}$ and $z_i \vDash^X_{\omega_i} A $ or there exists an $\bar{n}$ such that for every $i\leq \bar{n}$ there exists $z_i\in X_{\omega_i} $ such that $\angbr{z_i}{s}\in X_{t_{\leq i}}$ and $z_i \vDash^X_{\omega_i} A $ and an element $z_{\bar{n}}\in X_{\omega_{\bar{n}}} $ such that $\angbr{z_{\bar{n}}}{s}\in X_{t_{\leq \bar{n}}}$ and $z_{\bar{n}} \vDash^X_{\omega_{\bar{n}}} B $.

Recall that given a relational presaheaf $\relpresheaf{\mW}{X}$, the top element of the boolean algebra $\att (X)$ is given by the attributes $\top=\{ X_{\omega}\}_{\omega\in \mW}$ and the bottom element by $\bot=\{ \emptyset_{\omega}\}_{\omega\in \mW}$ since the order of $\att (X)$ is given by the inclusion of sets.

Therefore, employing the previous notions, we can define the operators $\dm A$ and $\sq A$ as $\dm A := \top\untiloperator A$ and $\sq A := A \wuntiloperator \bot$.

Notice also that by definition, we have that  $s\vDash^X_{\omega} A\untiloperator B$ iff $s\in C_{\omega}$ for every   $C_{\omega}\subseteq X_{\omega}$ such that $C_{\omega}=B_{\omega} \vee (A_{\omega} \wedge \nextoperator (C)_{\omega})$
(and similarly for $s\vDash^X_{\omega} A\wuntiloperator B$). In other words, the set $(A\untiloperator B)_{\omega}$ can be more concisely described as the least fixed point, with respect to the order given by set inclusion,  of the function $B_{\omega} \vee (A_{\omega} \wedge \nextoperator (-)_{\omega})$

and analogously, $(A\wuntiloperator B)_{\omega}$ as the greatest fixed point of the same function
(recall that the boolean structures of attributes is given by the set theoretic inclusions, hence $\vee$ and $\wedge$ are given by the union and the intersection of sets, respectively).

Let us consider a temporal structure $\mathrm{T}$ on $\relpresheaf{\mW}{X}$. Given an attribute $A\in \att (X)$ and $s\in X_{\omega}$ it is direct to check that $\dm A$ and $\sq A $ can be directly described as follows

* $s\vDash^X_{\omega}\sq A$  if for every $\mathrm{t}\in \cammini{T}{\omega}$ and for every $i$ there exists an element $z_i\in X_{\omega_i} $ such that $\angbr{z_i}{s}\in X_{t_{\leq i}}$ and $z_i \vDash^X_{\omega_i} A $;

* $s\vDash_{\omega}^X \dm A$ if for every $\mathrm{t}\in \cammini{T}{\omega}$ there exist $\bar{n}$ and an element  $z_{\bar{n}}\in X_{\omega_{\bar{n}}} $ such that $\angbr{z_{\bar{n}}}{s}\in X_{t_{\leq {\bar{n}}}}$ and  $z_{\bar{n}} \vDash^X_{\omega_{\bar{n}}} A $.

Notice that in the definition of classical attributes, the relational structure of a given relational presheaves has no rule, while it is fundamental in defining the temporal operators embodying the fundamental idea of the counterpart semantics.

However, depending of what kind of logic we are interested in, different conditions can be imposed or required on the notion of attribute. For example, one can impose the so called stability condition with respect to the past, i.e. for every relational presheaf $\relpresheaf{\mC}{X}$, we define

\[ \relatt(X):=\{ \{A_{\omega}\}_{\omega\in \mC} \; |\; A_{\omega}\subseteq X_{\omega}\}\]

where every family $\{A_{\omega}\}_{\omega\in \mC}$ satisfies the following stability condition

\[ \freccia{\sigma}{f}{\tau}, \; \angbr{t}{s}\in X_f \mbox{ and } t\in A_{\tau} \mbox{ implies } s\in A_{\sigma}.\]

This kind of attributes are introduced in [17] to apply the relational semantics in intuitionistic logic. However, considering this notion of attributes requires a careful analysis of the interpretation of quantifiers because, for example, the usual Beck Chevalley condition in general is not satisfied in this semantics. For details we refer to [17].

A flow of time is a pair $(T,<)$ where $T$ is a non-empty set whose elements are called time points and $<$ is an irreﬂexive and transitive binary relation on $T$. Given two time points $s,u\in T$, $s<u$ intuitively means that $s$ is earlier of $u$.
Requiring that $<$ is irreﬂexive is thus motivated by the fact that no time point should be in the past or future of itself, and $<$ has to be transitive because $t$ is earlier than $u$, and $u$ earlier than $v$, then we expect $t$ to be earlier than $v$.
A flow of time is linear if given any two distinct time points in it, one is before the other, i.e. for every $s,t\in T$ such that $s\neq t$ we have that either $s<t$ or $t<s$.

A natural choice of base and temporal structure is thus a linear flow of time $(T,\leq)$ and the free category $\mW(T)$ on it. Then every relational presheaf $\relpresheaf{\mW(T)}{X}$  admits a natural temporal structure $\mathrm{T}$ provided by the set of arrows of relation $<$. We will observe in the following section that this choice allows us to obtain the standard semantics for LTL as particular case of our constructions and notions.  In particular, the interpretation of the temporal operators $\nextoperator,\dm,\sq, \untiloperator,\wuntiloperator$ coincide precisely with the usual interpretation of LTL.

The notions of Kripke frame and of flow of time are an intuitive abstraction of systems that evolve or change over instants of time. However, notice that both of them suffer of the limitation that the relation  between worlds or instants of time has to be binary. This represents a serious constraint if, for example, one want to consider a simple situation in which a system could evolve in another one through two distinct developments. Moreover, the requirement that the relation $<$ in the definition of flow of time has to be transitive and irreflexive does not allow to consider reversible process or reversible developments. This is quite natural if one has to work with time developments, but if we are interesting in a more general situation, we have to consider different notions, such as e.g. labelled transition systems. Recall that a labelled transition system (LTS) is a triple $(S,L,\rightarrow)$, where $S$ is a non-empty set of states, $L$ is the set of labels, and $\rightarrow\subset S\times L\times S$ is a relation, which is total in the first component, i.e. for every $s\in S$ there exists a label $l\in L$ and a state $s'$ such that $(s,l,s')\in \rightarrow$. Therefore, another meaningful choice for the category of worlds and the temporal structure is considering an LTS $(S,L,\rightarrow)$ and the free category $\mW(S)$ on it. Then every relational presheaf $\relpresheaf{\mW(S)}{X}$ admits a temporal structure give by the set $\mathrm{T}_S$ of arrows of the relation $\rightarrow$, where the next time operator $\nextoperator$ has exactly the intuitive meaning of it holds at every next-step of length one.

§.§ Semantics via temporal structures

In this section we show how relational presheaves and temporal structures can be employed to obtain models for our quantified temporal logic.

Recall that in the semantics of worlds, providing the interpretation of a formula means providing an interpretation of such a formula in every world.

Let $\Sigma$ be a many-sorted signature. A temporal counterpart $\mW$-model is defined by $\Tempmodel :=(\mW,\mathrm{T},\sortmodel,\functionmodel)$

* the triple $(\mW,\sortmodel,\functionmodel)$ is a counterpart $\mW$-model;

* every relational presheaf $\relpresheaf{\mW}{X}$ of $\sortmodel$ is equipped with the temporal structure $\mathrm{T}$.

The presence of a temporal structure

allows us to refine Proposition <ref> and Proposition <ref> in the context of temporal $\mW$-counterpart models, and to obtain the following correspondence with counterpart models in the sense of [13].

There is a bijective correspondence between counterpart models  $\angbr{W}{\rightsquigarrow,d}$  and temporal $\mW$-counterpart models $(\mW,\mathrm{T},\sortmodel,\functionmodel)$ where $\mW$ is freely generated by the set of objects $\mathbf{ob}(\mW)$ and the class of arrows $\mathrm{T}$ and every relational presheaf of $\sortmodel$ sends a morphism  $\freccia{\omega}{f}{\sigma}$ of  $\mW$ to a relation $\relazione{\interp{\tau}{\Relmodel}_{\sigma}}{\interp{\tau}{\Relmodel}_f}{\interp{\tau}{\Relmodel}_{\omega}}$ whose converse $\relazione{\interp{\tau}{\Relmodel}_{\omega}}{(\interp{\tau}{\Relmodel}_f)^{\dagger}}{\interp{\tau}{\Relmodel}_{\sigma}}$ is a partial function.

The construction of a temporal $\mW$-counterpart model from a counterpart model is given exactly as in Proposition <ref> with the obvious choice of the temporal structure. What changes is only the definition of a counterpart model from a temporal $\mW$-counterpart model. In fact, while in Proposition <ref> every arrow $\freccia{\omega_1}{f}{\omega_2}$ of the base category induces an element $(\omega_1,cr_f,\omega_2)\in\rightsquigarrow $, if we start from a temporal $\mW$-counterpart model as in Theorem <ref>, we define an elements $(\omega_1,cr_f,\omega_2)\in\rightsquigarrow $ only for those arrows $f\in \mathrm{T}$ of the temporal structure. It is direct to check that these two constructions provide a bijective correspondence.

Now we show how terms-in-context and formulae-in-context are interpreted in our model. We start by noticing that, by definition of temporal $\mW$-counterpart model, the interpretation of sorts, function and relation symbols is already fixed.

Therefore, for the rest of this section we fix a temporal $\mW$-counterpart model  $\Tempmodel =(\mW,\mathrm{T},\sortmodel,\functionmodel)$.

First of all, given a first-order context $\Gamma= \context{x}{\tau}{n}$,  we denote by

$$ \interp{\Gamma}{\Relmodel}:=\interp{\tau_1}{\Relmodel}\times \dots\times \interp{\tau_n}{\Relmodel}$$

the relational presheaf associated to the context $\Gamma$ via the counterpart $\mW$-model $(\mW,\sortmodel,\functionmodel)$. Then, given a second-order context $\Delta=\context{\chi}{\tau}{m}$, we denote by

$$ \interp{\Delta}{\Relmodel}:=\powerelpresheaf{\interp{\tau_1}{\Relmodel}}\times \dots \times\powerelpresheaf{\interp{\tau_m}{\Relmodel}}$$

where $\powerelpresheaf{\interp{\tau_i}{\Relmodel}}$ denotes the relational power-set presheaf of $\interp{\tau_i}{\Relmodel}$, see Definition <ref>. Therefore we define the interpretation

$$\interp{\Gamma,\Delta}{\Relmodel}=\interp{\Gamma}{\Relmodel}\times \interp{\Delta}{\Relmodel}.$$

Recall that a term in a given context $[\Gamma,\Delta]\; t:\tau $ is then interpreted as a morphism of relational presheaves, defined as

* if $t=x_i$ then $\interp{t}{\Relmodel}$ is the projection $\freccia{\interp{\Gamma,\Delta}{\Relmodel}}{\pi_i}{\interp{\tau}{\Relmodel}}$;

* if $t=f(t_1,\dots,t_k)$, then $\interp{t}{\Relmodel}$ is given by the composition

\[
\xymatrix@+2pc{
\interp{\Gamma,\Delta}{\Relmodel} \ar[rr]^{\angbr{\interp{t_1}{\Relmodel},\dots}{\interp{t_k}{\Relmodel}}}& &\interp{\Gamma' }{\Relmodel} \ar[r]^{\mI(f)}& \interp{\tau}{\Relmodel}.
} \]

The interpretation of a given formula in context $[\Gamma] \; \phi $ has to be defined for each world, in line with the usual Kripke-style semantics. Therefore, the interpretation of $[\Gamma] \; \phi $ is  defined as a classical attribute

\[\interp{[\Gamma] \; \phi}{\Tempmodel}=\{\interp{[\Gamma] \; \phi}{\Tempmodel}_{\omega}\}_{\omega\in \mW}\]

of the relational presheaf $\interp{\Gamma}{\Tempmodel}$, where every $\interp{[\Gamma] \; \phi}{\Tempmodel}_{\omega}$ is a subset of $\interp{\Gamma}{\Tempmodel}_{\omega}$. Recall that the notation $\interp{\Gamma}{\Tempmodel}_{\omega}$ indicates the set given by the evaluation $\interp{\Gamma}{\Tempmodel}$ at $\omega$.

Moreover, we start defining the interpretation of a formula at a given fixed world, and we use induction on the structure on $\phi$ as usual.

The interpretation of standard formulae at a given world $\omega$  is given as follows

* $\interp{[\Gamma,\Delta] \;\top }{\Relmodel}_{\omega}:=\interp{\Gamma,\Delta}{\Relmodel}_{\omega}$;

* $\interp{[\Gamma,\Delta] \;\bot }{\Relmodel}_{\omega}:=\emptyset$;

* $\interp{[\Gamma,\Delta] \;\varepsilon\in_{\tau} \chi }{\Relmodel}_{\omega}:= \angbr{\pi_{\varepsilon}}{\pi_{\chi}}_{\omega}^* (\in_{\interp{\tau}{\Relmodel}}(\omega))$ where $\freccia{\interp{[\Gamma,\Delta]}{\Relmodel}}{\angbr{\pi_{\varepsilon}}{\pi_{\chi}}}{\interp{[\varepsilon:\tau, \chi:\tau}{\Relmodel}}$ are the opportune projections;

* for every $\phi$, then $\interp{\Gamma,\Delta] \; \neg \phi}{\Relmodel}_{\omega}:= \overline{\interp{\Gamma,\Delta] \; \phi}{\Relmodel}_{\omega} }$ where $\overline{(-)}$ denotes the set-theoretical complements, i.e. $\interp{\Gamma,\Delta] \; \neg \phi}{\Relmodel}_{\omega} := \interp{\Gamma,\Delta}{\Relmodel}_{\omega} \setminus \interp{\Gamma,\Delta] \; \phi}{\Relmodel}_{\omega}$.

We also have that

* $\interp{[\Gamma,\Delta]\; \psi \vee \psi}{\Relmodel}_{\omega}:=\interp{[\Gamma,\Delta]\; \psi}{\Tempmodel}_{\omega}\cup \interp{[\Gamma,\Delta]\;  \psi }{\Relmodel}_{\omega}$;

* $\interp{[\Gamma,\Delta]\; \psi \wedge \psi}{\Relmodel}_{\omega}:=\interp{[\Gamma,\Delta]\; \psi}{\Tempmodel}_{\omega}\cap \interp{[\Gamma,\Delta]\;  \psi }{\Relmodel}_{\omega}$;

* $\interp{[\Gamma,\Delta]\; \forall_{\tau} y. \psi}{\Relmodel}_{\omega}:=\{ a\in \interp{\Gamma,\Delta}{\Relmodel}(\omega)\;| \forall b\in \interp{\tau}{\Relmodel}_{\omega} \mbox{ we have } (a,b)\in \interp{[\Gamma,y:\tau,\Delta]\;\psi}{\Tempmodel}_{\omega}\}$;

* $\interp{[\Gamma,\Delta]\; \forall_{\tau} \chi. \psi}{\Relmodel}_{\omega}:=\{ a\in \interp{\Gamma,\Delta}{\Relmodel}(\omega)\;| \forall b\in \powerelpresheaf{\interp{\tau}{\Relmodel}}(\omega) \mbox{ we have } (a,b)\in \interp{[\Gamma,\Delta,\chi: \tau]\;\psi}{\Tempmodel}_{\omega}\}$;

* $\interp{[\Gamma,\Delta]\; \exists_{\tau} y. \psi}{\Relmodel}_{\omega}:=\{ a\in \interp{\Gamma,\Delta}{\Relmodel}(\omega)\;| \exists b\in \interp{\tau}{\Relmodel}_{\omega} \mbox{ such that } (a,b)\in \interp{[\Gamma,y:\tau,\Delta]\;\psi}{\Tempmodel}_{\omega}\}$;

* $\interp{[\Gamma,\Delta]\; \exists_{\tau} \chi. \psi}{\Relmodel}_{\omega}:=\{ a\in \interp{\Gamma,\Delta}{\Relmodel}(\omega)\;| \exists b\in \powerelpresheaf{\interp{\tau}{\Relmodel}}(\omega) \mbox{ such that } (a,b)\in \interp{[\Gamma,\Delta,\chi: \tau]\;\psi}{\Tempmodel}_{\omega}\}$.

Finally, we have the interpretation of formulae in which temporal operators occur

* $\interp{[\Gamma,\Delta] \;\nextoperator \psi }{\Relmodel}_{\omega}:= \nextoperator\interp{[\Gamma,\Delta] \; \psi }{\Relmodel}_{\omega}$;

* $\interp{[\Gamma,\Delta] \;\psi \untiloperator \psi }{\Relmodel}_{\omega}:= \interp{[\Gamma,\Delta] \; \psi }{\Relmodel}_{\omega}\untiloperator\interp{[\Gamma,\Delta] \; \psi }{\Relmodel}_{\omega} $;

* $\interp{[\Gamma,\Delta] \;\psi \wuntiloperator \psi }{\Relmodel}_{\omega}:= \interp{[\Gamma,\Delta] \; \psi }{\Relmodel}_{\omega}\wuntiloperator\interp{[\Gamma,\Delta] \; \psi }{\Relmodel}_{\omega} $;

* $\interp{[\Gamma,\Delta] \;\sq \psi }{\Relmodel}_{\omega}:= \sq\interp{[\Gamma,\Delta] \; \psi }{\Relmodel}_{\omega}$;

* $\interp{[\Gamma,\Delta] \;\dm \psi }{\Relmodel}_{\omega}:= \dm\interp{[\Gamma,\Delta] \; \psi }{\Relmodel}_{\omega}$;

where $\nextoperator,\untiloperator,\wuntiloperator,\dm,\sq $ are the temporal operators induced by the temporal structure $\mathrm{T}$.

We conclude by comparing our semantics with that introduced for counterpart models, and we refer to [13] for all the details about that. In particular we can employ the correspondence of Theorem <ref> to conclude that the semantics introduced in [13] and the one we present for temporal counterpart models are equivalent.

A formula is satisfied by a counterpart model if and only if it is satisfied by the corresponding $\mW$-temporal counterpart model.

The notion of temporal $\mW$-counterpart model allows us to obtain as particular instance the semantics for standard LTL by considering as temporal structure the free category generated by a linear flow of time as in Example <ref>. In particular, the interpretation of the operators $\nextoperator,\dm,\sq, \untiloperator,\wuntiloperator$ coincide with the usual one of LTL.

Let us consider our running example of Figure <ref> and the temporal structure given by the morphism $\mathrm{T}:=\{f_0,f_1,f_2,f_3\}$. Now let us consider the property  $[y:\tau_N] \;\exists_{\tau_N}x. (((x\neq y) \wedge\nextoperator (x=y))$ presented in Example <ref>: we have that

* $\interp{[y:\tau_N] \;\exists_{\tau_N}x. ((x\neq y) \wedge\nextoperator (x=y)) }{\Relmodel}_{\omega_0}=\{n_0,n_2\}$ is the set of nodes of the graph $\mathbf{G}_0$ that will be identified at the next step, i.e. at the world $\omega_1$;

* $\interp{[y:\tau_N]\;\exists_{\tau_N}x. ((x\neq y) \wedge\nextoperator (x=y)) }{\Relmodel}_{\omega_1}=\{n_3,n_4\}$ is the set of nodes of the graph $\mathbf{G}_1$ that will be identified at the next step, i.e. at the world $\omega_2$;

* $\interp{[y:\tau_N] \;\exists_{\tau_N}x. ((x\neq y) \wedge\nextoperator (x=y)) }{\Relmodel}_{\omega_2}=\emptyset$ is the set of nodes of the graph $\mathbf{G}_2$ that will be identified at the next step.

Recall the toy example presented in the introduction, i.e, the model with two states $s_0$ and $s_1$. In order to describe it, consider a one-sorted signature $\Sigma=\{\tau\}$ with no function symbols, and the free category $\mathcal{S}$ generated by the following diagram

\[
\xymatrix{
s_0<EMAIL_ADDRESS>&<EMAIL_ADDRESS>\]

and the relational presheaf $\relpresheaf{\mathcal{S}}{D}$
such that $D_{s_0}=\{i \}$, $D_{s_1}=\emptyset$, and both $D_{f_0}$ and $D_{f_1}$ are the empty relation. Then consider the counterpart model $(\mathcal{S},\mathrm{T}:=\{f_0,f_1\},D,\emptyset)$.
One of the main advantages of the counterpart semantics is the possibility to deal with processes destroying elements. In this setting an interesting formula is $[x:\tau] \; \mathbf{present}(x)\wedge\nextoperator(\nextoperator \mathbf{present}(x))$, i.e. meaning that there exists an entity at a given world that has a counterpart after two steps. If we consider its interpretation at world $s_0$ in the model $(\mathcal{S},\{f_0,f_1\},D,\emptyset)$, it is direct to check that

$$\interp{[x:\tau] \; \mathbf{present}(x)\wedge\nextoperator(\nextoperator \mathbf{present}(x))}{\Tempmodel}_{s_0}=\emptyset.$$

This is exactly what expected, since it essentially means that entity $i$  has no counterpart at the world $s_0$ after two steps, even if it clearly belong to the world relative to $s_0$.

The creation and destruction of entities has attracted the interest of various authors
(e.g. [10, 32]) as a means for reasoning about the allocation and deallocation of resources or processes.
Our logic does not offer an explicit mechanism for this purpose. Nevertheless, as we have shown in
Example <ref>, we can easily derive a predicate regarding the presence of an entity in a certain world
as $ \mathbf{present}_{\tau} (x)$. Using this predicate together with the next-time modality, we can
reason about the preservation and deallocation of some entities after one step of evolution of the system as
$\mathbf{nextStepPreserved}(x)\equiv\mathbf{present}_{\tau} (x)\wedge \nextoperator ( \mathbf{present}_{\tau} (x))$
$\mathbf{nextStepDeallocated}(x)\equiv\mathbf{present}_{\tau} (x)\wedge \nextoperator (\neg \mathbf{present}_{\tau} (x))$.

Now we provide an interpretation

of these two formulae for
our running example

in Figure <ref> and the temporal structure given by the morphism $\mathrm{T}:=\{f_0,f_1,f_2,f_3\}$. Then

* $\interp{[x:\tau_E]\;\mathbf{nextstepPreserved}(x) }{\Relmodel}_{\omega_0}=\{e_0,e_1\}$ is the set of edges of $\mathbf{G}_0$ that survive at the next steps;

* $\interp{[x:\tau_E]\; \mathbf{nextstepPreserved}(x) }{\Relmodel}_{\omega_1}=\emptyset$ is the set of edges of $\mathbf{G}_1$ that survive at the next steps;

* $\interp{[x:\tau_E]\;\mathbf{nextstepPreserved}(x) }{\Relmodel}_{\omega_0}=\{e_5\}$ is the set of edges of $\mathbf{G}_2$ that survive at the next steps.

Notice that $\interp{[x:\tau_E]\; \mathbf{nextstepPreserved}(x) }{\Relmodel}_{\omega_1}=\emptyset$ because we have that $d(f_1)$ forgets the arrow $e_4$, while $d(f_2)$ forgets the arrow $e_3$. This follows from  our definition of the next step operator, where we require that a given property has to hold for every step of length one. Then, we conclude considering the case of next-step deallocation

* $\interp{[x:\tau_E]\;\mathbf{nextstepDeallocated}(x) }{\Relmodel}_{\omega_0}=\{e_2\}$ is the set of edges of $\mathbf{G}_0$ that are deallocated at the next steps;

* $\interp{[x:\tau_E]\; \mathbf{nextstepDeallocated}(x)) }{\Relmodel}_{\omega_1}=\emptyset$ is the set of edges of $\mathbf{G}_1$ that are deallocated at the next steps;

* $\interp{[x:\tau_E]\;\mathbf{nextstepDeallocated}(x) }{\Relmodel}_{\omega_0}=\emptyset$ is the set of edges of $\mathbf{G}_2$ that are deallocated at the next steps.

Notice that, as in the original presentation of hyperdoctrine, we can define the predicate

\[\equalitypredicate_A :=\Einv_{\Delta_A}(\top_A)\]

thanks to the existence of left adjoints along arbitrary maps in Definition <ref>. However, we do not require any additional condition on the left adjoints of the for $\Einv_{\id\times \Delta}$. As pointed out in several works of Ghilardi and Melloni [16, 17, 15], this choice reflects the features of presheaves  semantics for modal logic.

Let us consider a language $\modallanguage$ and a first order modal system $\modalsystem$. We define the modal hyperdoctrine of syntactic attributes as:

\[\modaldoctrine{\catcontext}{\syntdoct}\]

where $\catcontext$ is the category of lists of variables and term substitutions:

* objects of $\catcontext$ are natural number $n\geq 0$;

* a morphism $\freccia{n}{}{m}$ is a $m$-tupla of $n$-terms;

* the composition of two morphisms  is given by the substitution

The functor $\modaldoctrine{\catcontext}{\syntdoct}$ sends a natural number $n$ in the class $\syntdoct(n)$  of all well formed $n$-formulas. We say that $\psi\leq \phi$ where $\phi,\psi\in \syntdoct(n)$ if $\psi\vdash_{\modalsystem}\phi$, and then we quotient in the usual way to obtain a partial order on $\syntdoct(n)$. Given a morphism of $\mC_{\modallanguage}$

\[\freccia{n}{\vec{t}:=(t_1,\dots,t_m)}{m}\]

the functor ${\syntdoct}_{(\vec{t})}$ acts as the substitution

The category of modal hyperdoctrines $\ModalHyp$ is a 2-category, where:

* a 1-cell is a pair $(F,b)$

\[\duemorfismo{\mC}{P}{F}{b}{\mD}{R}\]

such that $\freccia{\mC}{F}{\mD}$ is a functor, and $\freccia{P}{b}{R\circ F^{\op}}$ is a natural transformation, which is also natural with respect to left adjoints;

* a 2-cell is a natural transformation $\freccia{F}{\theta}{G}$ such that for every $A$ in $\mC$ and every $\alpha$ in $P(A)$, we have

\[b_A(\alpha)\leq R_{\theta_A}(c_A(\alpha)).\]

Notice that 1-cells of the form $\freccia{\syntdoct}{(F,b)}{P}$ represent exactly categorical model of modal systems.

The following definition provides a natural specification of the notion of tripos <cit.> in the case of modal hyperdoctrines.

A modal tripos is a modal hyperdoctrine $\modaldoctrine{\mC}{P}$  such that for every object $A$ of $\mC$ there exists an object $\powersetobject{A}$ and an element $\membpredicate{A}$ in the fibre $P(A\times \powersetobject{A})$ such that for every $B$ and every $\beta$ in the fibre $P(A\times B)$ there exists a morphism $\freccia{B}{\{\beta\}}{\powersetobject{A}}$ of $\mC$ such that $P_{\id_A\times \{\beta\}}(\membpredicate{A})=\beta$.

§ KRIPKE SEMANTIC

We briefly recall from [15] the interesting presentation of the notions of world, process and individuals arising from modal logic, in terms of presheaves.

Given a category $\mC$, its objects $\sigma,\omega, \rho, \dots$ can be considered as worlds or instants of times, and the arrows $\freccia{\sigma}{f}{\omega}$ represent temporal developments or ways of accessibility. Following this line, a preshef $\presheaf{\mC}{D}$ assigns to every world $\omega$ the set $D_{\omega}:=D(\omega)$ of if individuals. Hence, if we consider an arrow
$\freccia{\sigma}{f}{\omega}$ and two elements $t\in D_{\omega}$ and $s\in D_{\sigma}$, having $s=D_f(t)$ can be read as "s is the ancestor, with respect to the development f of t".

With this intuition in mind, we recall how the Kripke semantic is formalized in terms of modal hydoctrines their morphisms.

Let $\mC$ be a small category, and let us consider the modal hyperdoctrine of semantic attributes $\modaldoctrine{\presheafcat{\mC}}{\att}$ defined as follows:

* for every presheaf $\presheaf{\mC}{D}$, we have

\[ \att(D):=\{ \{A_{\omega}\}_{\omega\in \mC} \; |\; A_{\omega}\subseteq D_{\omega}\}\]

where $D_{\omega}$ denotes the set $D(\omega)$.

* for every natural transformation $\freccia{D}{\psi}{E}$ of presheaves, then
$$\freccia{\att (E)}{\att_{\psi}}{\att (D)}$$
acts as $\{B_\omega\}_{\omega\in \mC}\mapsto \{\psi^{-1}_{\omega}(B_{\omega})\}_{\omega\in \mC}$, where $B_{\omega}\subseteq E_{\omega}$ for every $\omega$.

This is a modal hyperdoctrine when we consider the order defined by the inclusions of subsets, see [4].

The key observation due to Ghilardi and Meloni, is the result of the composition $\Subobjectdoctrine\circ (F^*)^{\op}$ where $\Subobjectdoctrine$ is the functor

$$\freccia{ \presheafcat{|\mC|}^{\op}}{\Subobjectdoctrine}{\Set}$$

where $|\mC|$ denotes the category whose objects are those of $\mC$, but whose morphisms are only identities, and

is left adjoint to the inclusion-functor $\freccia{\presheafcat{|\mC|}}{F_*}{\presheafcat{\mC}}$. In particular, one can see the presheaf $F^*(D)$ as the collection $\{D_{\omega}\;|\;\omega\in \mC\}$, and hence a subobject of $F^*(D)$ can be seen as the collection $ \att(D):=\{ \{A_{\omega}\}_{\omega\in \mC} \; |\; A_{\omega}\subseteq D_{\omega}\}$. Finally, we have that the $(F^*,F_*)$ is a geometric morphism, i.e. $F^*$ is left exact.

In this context, given a presheaves $\presheaf{\mC}{D}$, and $A\in \att(D)$, we define by $\sq A$  the maximum subpresheaf contained in $A$.

Finally, we  given a presheaf $\presheaf{\mC}{D}$ and an  element $A\in \att(D)$, we use the validity notation $s\vDash^D_{\omega}A$ to meant that $s\in A_{\omega}$.

Hence, we have that

$$s\vDash^D_{\omega}\sq A$$

if and only if for every object $\sigma\in \mC$ and every arrow $\freccia{\sigma}{f}{\omega}$, $D_f(s)\vDash^D_{\sigma}A$.

Now we show how the attribute functor, together with the notion of morphism of modal doctrines, generalized the Kripke semantic. Let us consider a 1-cell between the following of modal hyperdoctrines:

\[\duemorfismo{\catcontext}{\syntdoct}{F}{b}{\presheafcat{\mC}}{\att}\]

Since $F$ is a preserving products functor, and since the objects of $\catcontext$ are all products of $1$ (since natural numbers represents the length of a context), providing such a 1-cell of $(F,b)$ is equivalent to provide the so called presheaf Kripke model $\model=(\mC,D,\mI)$, where :

* $\mC$ is a category;

* $D$ is a presheaf $\presheaf{\mC}{D}$

* $\mI$ is an interpretation mapping every function symbol $g$ (of arity $m$) to a natural transformation $\freccia{D^m}{\mI(g)}{D}$ , and every predicate symbol $P$ to an element of $\att(D^n)$.

Now, let us consider a $n$-term $t$. Then $\freccia{D^n}{\interp{t}{\model}}{D}$ is defined by induction as usual:

* if $t=x_i$ then $\interp{t}{\model}$ is the projection $\freccia{D^n}{\pi_i}{D}$;

* if $t=f(t_1,\dots,t_k)$, then $\interp{t}{\model}$ is given by the composition

\[
\xymatrix@+2pc{
D^k\ar[rr]^{\angbr{\interp{t_1}{\model},\dots}{\interp{t_k}{\model}}}& &D^n\ar[r]^{\mI(f)}& D.
} \]

Given an $n$-formula $\phi$, we define $\interp{\phi}{\model}\in \mA(D^n)$ as follow by induction:

* if $\phi=P(t_1,\dots, t_k)$, then $\interp{\phi}{\model}:= \mA_{\angbr{\interp{t_1}{\model},\dots}{\interp{t_k}{\model}}}(\mI (P))$;

* if $\phi$ is $\phi_1 @ \phi_2$, where $@:= \wedge,\vee , \rightarrow$, then $\interp{\phi}{\model}:=\interp{\phi_1}{\model}@\interp{\phi_2}{\model}$

* if $\phi$ is $\exists x \psi $ then $\interp{\phi}{\model}:=\Einv_{\pi}(\interp{\psi}{\model})$;

* if $\phi$ is $\sq \psi$, then $\interp{\phi}{\model}:=\sq \interp{\psi}{\model}$.

A $m$-formula $\phi$  is said valid in $\model$ if and only if $\interp{\phi}{\model}=\top$.

(Graph models)
Let us consider the category $\mG$ to be

\[\xymatrix{
N \ar@/_/[r]_s \ar@/^/[r]^t& A

with two objects and two arrows. Then the category $\presheafcat{\mG}$ is the topos of graphs. Each presheaf $\presheaf{\mG}{G}$ is given by the set $G(N)$ of nodes and a set $G(A)$ of arcs. The arrows $s$ and $t$ are mapped to functions
which assign to each arc its source and target, respectively. Now we provide a concrete description of a model $\model=(\mG,G,\mI)$. Recall that the interpretation $\mI$ acts as follow:

* the interpretation $\mI$ mapping every function symbol $f$ of the language $\modallanguage$ to an arrow $\freccia{G^n}{\mI(f)}{G}$ of graphs;

* every predicate symbol $P$ is mapped to an element $\mI(P)\in \mA (G) $.

In particular, this means that every function symbol $f$ (of arity $n$) is interpreted as a pair of function $(\mI (f)_N,\mI(f)_A)$, such that the following diagrams commute

\[
\xymatrix@+1pc{ G^n(A)\ar[d]_{\mI(f)_A}\ar[r]^{G^n(t)} & G^n(N) \ar[d]^{\mI(f)_N}&& G^n(A)\ar[d]_{\mI(f)_A}\ar[r]^{G^n(s)} & G^n(N)\ar[d]^{\mI(f)_N} \\
G(A) \ar[r]_{G(t)} & G(N) &&G(A) \ar[r]_{G(s)} & G(N).
\]

Therefore, the interpretation of a $n$-term $t$ is provided by a pair

\[\interp{t}{\model}=(\interp{t}{\model}_N,\interp{t}{\model}_A)\]

of functions $\freccia{G^n(N)}{\interp{t}{\model}_N}{G(N)}$ and $\freccia{G^n(A)}{\interp{t}{\model}_A}{G(A)}$.

Similarly, every $m$- predicate symbol $P$ is interpreted as a pair $(\mA(P)_N,\mA(P)_A)$ where $\mA(P)_N\subseteq G^m(N)$ and $\mA(P)_A\subseteq G^m(A)$.

Thus, for an $n$-formula $\phi$, we have that  $\interp{\phi}{\model}\in \mA(G^n)$ will be by a pair
with $\interp{\phi}{\model}\subseteq G^n(N)$ and $\interp{\phi}{\model}_A\subseteq G^m(A)$.

(Subobject presheaf)
Let us consider the category $\Drg:=\presheafcat{\mG}$ of directed graphs and morphisms of directed graphs. Notice that, since the category $\Drg$ has finite limits, it is quite natural considering  the sub-object functor $\presheaf{\Drg}{\Subobjectdoctrine}$. Now we provide a concrete description of the model $\model=(\Drg,\Subobjectdoctrine,\mI)$.

* the interpretation $\mI$ mapping every function symbol $f$ of the language $\modallanguage$ to a natural transformation $\freccia{\Subobjectdoctrine^n}{\mI(f)}{\Subobjectdoctrine}$;

* every predicate symbol $P$ is mapped to an element $\mI(P)\in \mA (\Subobjectdoctrine) $.

Therefor, for every $n$-function symbol $f$, we have that the interpretation $\mI (f)$ can be identified with a family of functions
\[\mI (f)=\{ \freccia{\Subobjectdoctrine ^n(\omega)}{\mI(f)_{\omega}}{\Subobjectdoctrine (\omega)}\}_{ \omega\in \Drg}\]

which are natural with respect the arrows of $\Drg$.

Similarly, the interpretation of $m$-predicate symbol $P$ is given by a family indexed in $\Drg$, whose elements are sets of sub-graphs

\[\mI(P)=\{ \mI(P)_{\omega}\;| \; \mI(P)_{\omega}\subseteq \Subobjectdoctrine^m (\omega) \}_{\omega\in \Drg}\]

Hence, we get that the interpretation of a $n$-term $t$ is given by a natural transformation

\[\freccia{\Subobjectdoctrine^n}{\interp{t}{\model}}{\Subobjectdoctrine}\]

i.e. it is identified by a family of functions

\[\interp{t}{\model}=\{ \freccia{\Subobjectdoctrine ^n(\omega)}{\interp{t}{\model}_{\omega}}{\Subobjectdoctrine (\omega)}\}_{ \omega\in \Drg}\]

natural with respect to $\Drg$. Similarly, the interpretation of a $m$-formula $\phi$ is given by

\[\interp{\phi}{\model}=\{ \interp{\phi}{\model}_{\omega}\;|\;  \interp{\phi}{\model}_{\omega}\subseteq \Subobjectdoctrine^m (\omega) \}_{\omega\in \Drg}\]

Let us consider the ordinary signature $\Sigma_{Gr}=(S_{Gr},F_{Gr})$ for directed graphs, where $S_{Gr}$ consists of the sort of nodes $\tau_N$ and the sort of edges $\tau_E$, while the set $F_{Gr}$ is composed by the function symbols
$\freccia{\tau_E}{s}{\tau_N}$ and $\freccia{\tau_E}{t}{\tau_N}$, which determine, respectively, the source and the target node of an edge. Moreover, let us consider the first-order modal language on this signature. In this case, a model $\model=(\mW,N,E,\mI(s),\mI(t))$ consists of:

* a category of worlds $\mW$;

* two presheaves on the category $\mW$ of worlds: $\presheaf{\mW}{N}$ and $\presheaf{\mW}{E}$, representing, respectively, the presheaf of nodes $N$ and
that of arcs $E$

* two natural transformations $\freccia{E}{\mI(s)}{N}$ and $\freccia{E}{\mI(t)}{N}$.

The intuition is that we are assigning a directed graph $(N(\omega),E(\omega), \mI(s)_{\omega},\mI(t)_{\omega}) $ to every world $\omega$, identified by the set of nodes $N(\omega)$, the set of arcs $E(\omega)$, and the two functions $\freccia{N(\omega)}{\mI(s)_{\omega},\mI(t)_{\omega}}{E(\omega)}$.

The interpretation of sorts, contexts and functions symbols in $\model$ is defined as follow:

* $\interp{\tau_N}{\model}:=N$ and $\interp{\tau_E}{\model}:=E$;

* given a context $\Gamma:=[x_1:S_1,\dots, x_n:S_N]$ over the signature $\Sigma_{Gr}$, where $S_i$ denotes a  meta-variables to indicate sorts, i.e. $S_i=\tau_N \mbox{ or }S_i=\tau_E$ for $i=1,\dots,n$,  we have that $\interp{\Gamma}{\model}:=\interp{S_1}{\model}\times \dots\interp{S_n}{\model}$;

* $\interp{s}{\model}:=\mI(s)$ and $\interp{t}{\model}:=\mI(t)$.

A term in a given context $[\Gamma]\; f:S $ is then interpreted as a natural transformation, defined as:

* $\freccia{\interp{\Gamma}{\model}}{\pi_i}{{\interp{S_i}{\model}}}$, if $f=x_i$;

* $\freccia{\interp{\Gamma}{\model}}{\mI_s\circ\pi_{i}}{N}$ if $f=s(x_i)$;

* $\freccia{\interp{\Gamma}{\model}}{\mI_t\circ\pi_{i}}{N}$ if $f=t(x_i)$;

The interpretation of propositions at a given world $\omega$ is given as follows:

* $\interp{[\Gamma] \;\top }{\model}_{\omega}:=\interp{\Gamma}{\model}(\omega)$;

* $\interp{[\Gamma] \; x_i=_S x_j}{\model}_{\omega}:=\{(a_1,\dots,a_n)\in \interp{\Gamma}{\model}(\omega)\;| \; a_i=a_j\}$;

* $\interp{[\Gamma]\; \exists y: S \; \phi(x,y)}{\model}_{\omega}:=\{ a\in \interp{\Gamma}{\model}(\omega)\;| \exists b\in \interp{S}{\model}(\omega) \mbox{ such that } (a,b)\in \interp{[\Gamma,y:S]\;\phi}{\model}_{\omega}\}$;

* $\interp{[\Gamma]\; \phi(x,y)\wedge \psi (x,y)}{\model}_{\omega}:=\interp{[\Gamma]\; \phi(x,y)}{\model}_{\omega}\cap \interp{[\Gamma]\;  \psi (x,y)}{\model}_{\omega}$;

* $\interp{[\Gamma] \;\square \phi }{\model}_{\omega}:=\{ a\in \interp{\Gamma}{\model}\; |\; \mbox{ for every arrow } \frecciasopra{\sigma}{v}{\omega}, \; \interp{\Gamma}{\model}_v(a)\in \interp{[\Gamma] \; \phi }{\model}_{\sigma}\}$

Therefore, we can define the interpretation of a formula in context $[\Gamma] \; \phi $ as

\[\interp{[\Gamma] \; \phi}{\model}=\{\interp{[\Gamma] \; \phi}{\model}_{\omega}\}_{\omega\in \mW}.\]

In this setting, let us consider the formula $[y: \tau_N]\; \exists x: \tau_{E} \; s(x)=y  $. Then we have that

\[\interp{\exists x: \tau_{E} \; s(x)=y \; [y: \tau_N] }{\model}_{\omega}= \{ n\in N(\omega): \exists a\in E(\omega), \; \mI(s)_{\omega}(a)=n\}\]

and then

\[\interp{\exists x: \tau_{E} \; s(x)=y \; [y: \tau_N] }{\model}=\{\interp{\exists x: \tau_{E} \; s(x)=y \}}{\model}_{\omega}\}_{\omega\in \mW}\]

We conclude this section showing that the semantic attribute doctrines is rich enough to interpret higher order constructors, i.e. it is a tripos.

Let us consider two categories $\mC$ and $\mD$ with finite products. let $F\dashv G$ be an adjunction such that $\freccia{\mD}{F}{\mC}$ preserves finite products. Then, for every modal tripos $\modaldoctrine{\mC}{P}$ , we have that $P\circ F^{\op}$ is a modal tripos.

We assume that $F$ preserves strictly the products in order to simplify the notation and the proof. Let $A$ be an object of $\mD$. We define the object $\powersetobject{A}$ in $\mD$ as  $\powersetobject{A}:=G(\powersetobject{FA})$, and the element $\membpredicate{A}$ as

$$\membpredicate{A}:= P_{\id_{FA}\times \varepsilon_{\powersetobject{FA}}}(\membpredicate{FA})$$

where $\varepsilon$ is the counit of the adjunction $F\dashv G$. Now let $\beta \in PF(A\times B)$. Then, since $P$ is a tripos, there exists an arrow $\freccia{FB}{\{\beta\}}{\powersetobject{FA}}$ in $\mC$ such that $P_{\id_{FA}\times \{\beta\}}(\membpredicate{FA})=\beta$. Therefore, since $F$ is left adjoint to $G$, there exists a unique morphism $\freccia{B}{g}{\powersetobject{FA}}$ such that $\{\beta\}=F(g)\varepsilon_{\powersetobject{FA}}$. Hence

$$\beta=(PF^{\op})_{(\id_A\times g)}(\membpredicate{A})$$

§ RELATIONAL PRESHEAVES

In the previous section we have seen how  the presheaf semantic generalizes the Kripke semantic in the context of modal hyperdoctrines. However, notice that the choice of presheaves for the semantic carry on some restrictions: given a presheaf $\presheaf{\mC}{D}$, and a temporal development $\freccia{\sigma}{f}{\tau}$, i.e. an arrow $f$ of $\mC$, the connection $D_f$ represents a temporal connection between individuals living in $D_{\tau}$ and $D_{\sigma}$, but since $D_f$ is totally defined on $D_{\tau}$, this forces that an individual $t$ living of the world $\tau$ necessarily exists also in the world $\sigma$ with respect to the development $\freccia{\sigma}{f}{\tau}$. This means that individuals cannot be born from nothing or cannot die.

If we are interested in modelling a more general kind of development, we the case in which

\[\relazione{D_{\tau}}{D_f}{D_{\sigma}}\]

is an arbitrary relation. This allows us, for example, to deal with partial functions, and to avoid the previous situation. Therefore, we recall the notion of relational presheaf.

A relational presheaf is a functor $\relpresheaf{\mC}{X}$, where $\Rel$ denotes the category of sets and relations.

Relational presheaves form a category (with left limits) if as arrows we consider the families of set functions $\psi:=\{\freccia{X_{\sigma}}{f_{\sigma}}{U_{\sigma}}\}_{\sigma\in \mC}$ such that for every $\freccia{\sigma}{g}{\tau}$ of the base category, we have that
\[\angbr{s}{t}\in X_{g}\Rightarrow\angbr{f_{\sigma}(s)}{f_{\tau}(t)}\in U_{f}\]

where $s\in X_{\sigma}$ and $t\in X_{\tau}$.

Therefore, the presheaves semantic defined in Section <ref> can be restated considering relational presheaves.

Let $\mC$ be a small category, and let us consider the modal hyperdoctrine of semantic relational-attributes $\modaldoctrine{\relpresheafcat{\mC}}{\relatt}$ defined as follows:

* for every relational presheaf $\relpresheaf{\mC}{X}$, we have that

\[ \relatt(X):=\{ \{A_{\omega}\}_{\omega\in \mC} \; |\; A_{\omega}\subseteq X_{\omega}\}\]

where every family $\{A_{\omega}\}_{\omega\in \mC}$ satisfies the following stability condition with respect to the past:

\[ \freccia{\sigma}{f}{\tau}, \; \angbr{s}{t}\in X_f \mbox{ and } t\in A_{\tau} \mbox{ implies } s\in A_{\omega}.\]

* The action of $\relatt$ on the arrows of $\relpresheafcat{\mC}$  is defined as for the functor $\att$.

Notice that in this case we have

\[s\vDash^{X}_{\omega} \sq A\]

if and only if for every $\sigma$, and every arrow $\freccia{\sigma}{f}{\omega}$ and $r\in X_{\sigma}$, if $\angbr{r}{s}\in X_{f}$ then $r\vDash^{X}_{\sigma}  A.$

Now we show how to construct a canonical model with relational presheaves. The idea is that the generic model with relational presheaves is build up from classical models. Notice that by classical model we meant a model such that the base category is provided by a single objects and its products, and without any condition requested for the validity of model operator.

Therefore, consider a category $\mC$ having as objects classical models and having as arrows between a pair of classical models all the relations $\psi \subseteq D_{\sigma}\times E_{\omega}$ which are stable under substitutions. The idea is that the elements of a relation $\psi$ are pairs of elements which are classical interpretation of farmulae in the classical models $D_\sigma$ and $E_{\omega}$. What we are going to require is that the relation must be stable we apply substitutions. In details: for every $n\geq 0$, for every $s\in D^n_{\sigma}$ and $e\in E^n_{\omega}$, with $\angbr{s_k}{e_k}\in \psi$ for $k=1,\dots,n$, then $\angbr{D_{\sigma}(t)s}{E_{\omega}(t)e}\in \psi$.

(Proposta prefascio relazionale)
Let us consider the category of directed graphs and partial morphisms denoted by $\ParDrg$. We consider the relational presheaf

\[\relpresheaf{\ParDrg}{\nuovopf}\]

defined as follow:

* $\nuovopf(\omega)=\omega_N\cup \omega_A$, i.e. the set of individuals $\nuovopf(\omega)$ associated to the directed graph $\omega$ is the set of nodes and arcs.

* given a partial map $\freccia{\omega}{f}{\tau}$, the relation  $\relazione{\nuovopf_{\tau}}{\nuovopf_f}{\nuovopf_{\omega}}$ is defined as the set

\[\{(a,b) \; | \;  \mbox{is defined on } b\mbox{ and } f(b)=a\}\subseteq \nuovopf(\tau)\times \nuovopf (\omega)\]

\[ \relatt(\nuovopf):=\{ \{A_{\omega}\}_{\omega\in \ParDrg} \; |\; A_{\omega}\subseteq \nuovopf_{\omega}\}\]

\[\interp{\phi}{\model}=\{A_{\omega}\}_{\omega\in \ParDrg}\]

\[\interp{x=y}{\model}=\{A_{\omega}\}_{\omega\in \ParDrg}, \; A_\omega\subseteq\Delta_{\Psi_{\omega}}\]

\[\mI(s):=\{ \freccia{\Psi_{\omega}}{s_{\omega}}{\Psi_{\omega}}\}_{\omega \in \ParDrg}\]

(Counterpart model)
Let us consider the ordinary signature $\Sigma_{Gr}=(S_{Gr},F_{Gr})$ for directed graphs, where $S_{Gr}$ consists of the sort of nodes $\tau_N$ and the sort of edges $\tau_E$, while the set $F_{Gr}$ is composed by the function symbols
$\freccia{\tau_E}{s}{\tau_N}$ and $\freccia{\tau_E}{t}{\tau_N}$, which determine, respectively, the source and the target node of an edge. Moreover, let us consider the first-order modal language on this signature. A counter part model
$$\model=(\mW,N,E,\mI(s),\mI(t), \rightsquigarrow)$$
consists of:

* a category of worlds $\mW$;

* two presheaves on the category $\mW$ of worlds: $\presheaf{\mW}{N}$ and $\presheaf{\mW}{E}$, representing, respectively, the presheaf of nodes $N$ and
that of arcs $E$

* two natural transformations $\freccia{E}{\mI(s)}{N}$ and $\freccia{E}{\mI(t)}{N}$.

* a relational presheaf $\freccia{\mW^{\op}}{\rightsquigarrow}{\ParDrg}$ such that
\[\rightsquigarrow(\omega)=(N(\omega), E(\omega),\mI(t)_{\omega},\mI(s)_{\omega}).\]

Again the intuition is that we are assigning a directed graph $(N(\omega),E(\omega), \mI(s)_{\omega},\mI(t)_{\omega}) $ to every world $\omega$, identified by the set of nodes $N(\omega)$, the set of arcs $E(\omega)$, and the two functions $\freccia{N(\omega)}{\mI(s)_{\omega},\mI(t)_{\omega}}{E(\omega)}$.

The relational presheaf $\rightsquigarrow$ identify the accessibility relation.

§ CONCLUSIONS AND FUTURE WORKS

In the paper we presented a counterpart semantics for (linear time) temporal logics that is based on relational presheaves.

Starting points were previous works on modal logics, namely the set-theoretical counterpart semantics in [13] and the functional presheaves model for Kripke frames in [15], and indeed they are both recovered in our framework.

Counterpart semantics offers a suitable solution to the trans-world identity problem, which we have argued to be relevant also from a practitioner point of view. The use of preshaves allows us to easily recover it, as well as to model second-order quantification.

The choice of linear time temporal logics asked for some ingenuity in the way to model the next step operator, with the introduction of what we called temporal structures, as well as in the treatment of negation, which required the use of a syntax for positive formulae. Our presheaf framework may as well recover the semantics of other temporal logics, and in fact we believe that it is general enough that it could be adapted to many different formalisms: indeed, with respect to our focus on partial ones, relational presheaves allows for a very general notion of morphism between worlds, which could e.g. be pivotal for formalisms where non-determinism plays a central role.

From a categorical perspective, our results open two challenging lines for future works: the first one regards the problem of proving a result of completeness. The choice of relational presheaves makes this task tricky to pursue, but it certainly deserves future investigations.

The second regards the study of formal criteria for the semantics of quantified temporal logic in the spirit of categorical logic, where models are thought of as opportune morphisms. A possible solution could be presenting temporal models as morphisms of opportune Lawvere doctrines. This is also a non-trivial problem that we are going to deal with in future work.

[1]
S. Awodey, K. Kishida, and H. Kotzsch.
Topos semantics for higher-order modal logic.
Logique et Analyse, 57(228):591–636, 2014.

[2]
P. Baldan, A. Corradini, B. König, and A. Lluch-Lafuente.
A temporal graph logic for verification of graph transformation
In J. L. Fiadeiro and P. Schobbens, editors, WADT 2006, volume
4409 of LNCS, pages 1–20. Springer, 2006.

[3]
F. Belardinelli.
Quantified Modal Logic and the Ontology of Physical Objects.
PhD thesis, Scuola Normale Superiore of Pisa, 2006.

[4]
P. Blackburn, J. F. A. K. van Benthem, and F. Wolter, editors.
Handbook of Modal Logic, volume 3.
North-Holland, 2007.

[5]
T. Braüner and S. Ghilardi.
First-order modal logic.
In Blackburn et al. [4], pages 549–620.

[6]
L. Cardelli, P. Gardner, and G. Ghelli.
A spatial logic for querying graphs.
In P. Widmayer, S. Eidenbenz, F. Triguero, R. Morales, R. Conejo, and
M. Hennessy, editors, ICALP 2002, pages 597–610. Springer, 2002.

[7]
B. Courcelle.
The monadic second-order logic of graphs. I. Recognizable sets of
finite graphs.
Information and Computation, 85(1):12–75, 1990.

[8]
B. Courcelle.
The expression of graph properties and graph transformations in
monadic second-order logic.
In G. Rozenberg, editor, Handbook of Graph Grammars and
Computing by Graph Transformations, Volume 1: Foundations, pages 313–400.
World Scientific, 1997.

[9]
A. Dawar, P. Gardner, and G. Ghelli.
Expressiveness and complexity of graph logic.
Information and Computation, 205(3):263–310, 2007.

[10]
D. Distefano, A. Rensink, and J. Katoen.
Model checking birth and death.
In R. A. Baeza-Yates, U. Montanari, and N. Santoro, editors, IFIP TCS 2002, volume 223 of IFIP Conference Proceedings, pages
435–447. Kluwer, 2002.

[11]
E. Franconi and D. Toman.
Fixpoint extensions of temporal description logics.
In D. Calvanese, G. D. Giacomo, and E. Franconi, editors, DL
2003, volume 81 of CEUR Workshop Proceedings. CEUR-WS.org, 2003.

[12]
P. Freyd and A. Scedrov.
Categories, Allegories.
Elsevier, 1990.

[13]
F. Gadducci, A. Lluch Lafuente, and A. Vandin.
Counterpart semantics for a second-order $\mu$-calculus.
Fundamenta Informaticae, 118(1-2):177–205, 2012.

[14]
P. H. Gardiner, C. E. Martin, and O. de Moor.
An algebraic construction of predicate transformers.
Science of Computer Programming, 22(1):21–44, 1994.

[15]
S. Ghilardi and G. Meloni.
Modal and tense predicate logic: Models in presheaves and categorical
In F. Borceux, editor, Categorical Algebra and its
Applications, volume 1348 of Lecture Notes in Mathematics, pages
130–142. Springer, 1988.

[16]
S. Ghilardi and G. Meloni.
Relational and topological semantics for temporal and modal
predicative logic.
In G. Corsi and G. Sambin, editors, Nuovi problemi della logica
e della scienza II, pages 59–77. CLUEB, 1990.

[17]
S. Ghilardi and G. Meloni.
Relational and partial variable sets and basic predicate logic.
Journal of Symbolic Logic, 61(3):843–872, 1996.

[18]
A. Hazen.
Counterpart-theoretic semantics for modal logic.
The Journal of Philosophy, 76(6):319–338, 1979.

[19]
I. M. Hodkinson, F. Wolter, and M. Zakharyaschev.
Monodic fragments of first-order temporal logics: 2000-2001 A.D.
In R. Nieuwenhuis and A. Voronkov, editors, LPAR 2001, volume
2250 of LNCS, pages 1–23. Springer, 2001.

[20]
B. Jacobs.
Many-sorted coalgebraic modal logic: A model-theoretic study.
RAIRO–Theoretical Informatics and Applications, 35:31–59,

[21]
B. Jacobs.
The temporal logic of coalgebras via Galois algebras.
Mathematical Structures in Computer Science, 12(6), 2002.

[22]
F. Lawvere.
Adjointness in foundations.
Dialectica, 23:281–296, 1969.

[23]
F. Lawvere.
Diagonal arguments and cartesian closed categories.
In P. J. Hilton, editor, Category Theory, Homology Theory and
their Applications II, volume 92 of Lecture Notes in Mathematics, page
134–145. Springer, 1969.

[24]
D. K. Lewis.
Counterpart theory and quantified modal logic.
The Journal of Philosophy, 65(5):113–126, 1968.

[25]
M. Maietti and G. Rosolini.
Quotient completion for the foundation of constructive mathematics.
Logica Universalis, 7(3):371–402, 2013.

[26]
J. Meseguer.
The temporal logic of rewriting: A gentle introduction.
In P. Degano, R. D. Nicola, and J. Meseguer, editors, Concurrency, Graphs and Models, volume 5065 of LNCS, pages 354–382.
Springer, 2008.

[27]
S. Niefield.
Lax presheaves and exponentiability.
Theory and Applications of Categories, 24(12):288–301, 2010.

[28]
A. Pnueli.
The temporal logic of programs.
In FOCS 1977, pages 46–57. IEEE Computer Society, 1977.

[29]
J. H. Reif and A. P. Sistla.
A multiprocess network logic with temporal and spatial modalities.
Journal of Computer and System Science, 30(1):41–53, 1985.

[30]
A. Rensink.
Model checking quantified computation tree logic.
In C. Baier and H. Hermanns, editors, CONCUR 2006, volume 4137
of LNCS, pages 110–125. Springer, 2006.

[31]
D. Trotta.
The existential completion.
Theory and Applications of Categories, 35:1576–1607, 2020.

[32]
E. Yahav, T. Reps, M. Sagiv, and R. Wilhelm.
Verifying temporal heap properties specified via evolution logic.
Logic Journal of the IGPL, 14(5):755–783, 2006.