Michell Guzmán

Salim Perchy

Camilo Rueda

Frank D Valencia

Characterizing Right Inverses for Spatial Constraint Systems with Applications to Modal Logic $

Keywords: constraint systems, concurrent constraint programming, concurrency theory, modal logic, inverse operators

Spatial constraint systems are algebraic structures from concurrent constraint programming to specify spatial and epistemic behavior in multi-agent systems. In this paper spatial constraint systems are used to give an abstract characterization of the notion of normality in modal logic and to derive right inverse/reverse operators for modal languages. In particular, a necessary and sufficient condition for the existence of right inverses is identified and the abstract notion of normality is shown to correspond to the preservation of finite suprema. Furthermore, a taxonomy of normal right inverses is provided, identifying the greatest normal right inverse as well as the complete family of minimal right inverses. These results are applied to existing modal languages such

Introduction

In this paper we give an abstract characterization of the notion of normality in modal logic and derive right inverse operators for modal languages. We shall do this by using spatial constraint systems [START_REF] Knight | Spatial and epistemic modalities in constraint-based process calculi[END_REF]. Spatial Constraint Systems. Constraint systems are algebraic structures for the semantics of process calculi from concurrent constraint programming (CCP) [START_REF] Saraswat | Semantic foundations of concurrent constraint programming[END_REF][START_REF] Boer | Nondeterminism and infinite computations in constraint programming[END_REF][START_REF] Knight | Spatial and epistemic modalities in constraint-based process calculi[END_REF][START_REF] Fages | Linear concurrent constraint programming: Operational and phase semantics[END_REF][START_REF] Réty | Distributed concurrent constraint programming[END_REF][START_REF] Nielsen | Temporal concurrent constraint programming: Denotation, logic and applications[END_REF]. They specify the domain and elementary operations and partial information upon which programs (processes) of these calculi may act. In this paper we shall study constraint systems as semantic structures for modal logic.

A constraint system (CS) can be formalized as a complete lattice (Con, ). The elements of Con represent partial information and we shall think of them as being assertions. The elements of Con are traditionally referred to as constraints since they naturally express partial information (e.g., x > 42). The order corresponds to entailment between constraints, c d means c can be derived from d, or that d represents as much information as c. Consequently, the order , the join , the bottom true and the top false of the lattice correspond respectively to entailment, conjunction, the empty information and the join of all (possibly inconsistent) information.

A distinctive property of CCP processes is that they can be interpreted as both concurrent computational entities and logic specifications (e.g., process composition can be seen as parallel execution and conjunction). The CCP operations and their logical counterparts typically have a corresponding elementary construct or operation on the elements of the constraint system. In particular, parallel composition and conjunction correspond to the join operation while local variables and existential quantification correspond to a cylindrification operation on the set of constraints [START_REF] Saraswat | Semantic foundations of concurrent constraint programming[END_REF] that project away the information of a given existential (or local) variable.

Similarly, the notion of computational space and the epistemic notion of belief in the spatial concurrent constraint programming (SCCP) process calculi [START_REF] Knight | Spatial and epistemic modalities in constraint-based process calculi[END_REF] correspond to a family of functions [•] i : Con → Con on the elements of the constraint system Con that preserve the join operation. These functions are called space functions. A CS equipped with space functions is called a spatial constraint system (SCS). From a computational point of view, given c ∈ Con, the assertion (constraint) [c] i specifies that c resides within the space of agent i. From an epistemic point of view, the assertion [c] i specifies that agent i considers c to be true (i.e. that in the world of agent i assertion c is true). Both intuitions convey the idea of c being local (subjective) to agent i.

The Extrusion Problem. Given a space function [•] i , the extrusion problem consists in finding/constructing a right inverse of [•] i , called extrusion function, satisfying some basic requirements (e.g., preservation of the join operation). By right inverse of [•] i we mean a function ↑ i : Con → Con such that [ ↑ i c ] i = c. The computational interpretation of ↑ i is that of a process being able to extrude any c from the space [•] i .

The extruded information c may not necessarily be part of the information residing in the space of agent i. For example, using properties of space and extrusion functions we

shall see that [ d ↑ i c ] i = [ d ] i c
specifying that c is extruded (while d is still in the space of i). The extruded c could be inconsistent with d (i.e., c d = false), it could be related to d (e.g., c d), or simply unrelated to d. From an epistemic perspective, we can use ↑ i to express utterances by agent i and such utterances could be intentional lies (i.e., inconsistent with their beliefs), informed opinions (i.e., derived from the beliefs), or simply arbitrary statements (i.e., unrelated to their beliefs). One can then think of extrusion/utterance as the right inverse of space/belief. Modal Logic. Modal logics [START_REF] Popkorn | First steps in modal logic[END_REF] extend propositional logic with n ≥ 1 operators 1 , 2 , . . . , n , expressing modalities. Depending on the intended meaning of the modalities, a particular modal logic can be used to reason about space, knowledge, belief or time, among others. For example, in doxastic modal logic, the logic of belief, the formula i φ (often written as B i φ) specifies that agent i believes φ and the formula i ¬ j ψ specifies that agent i believes that the agent j does not believe ψ. We shall also be interested in inverse modalities. An operator -1 i is a (right) inverse modality for i if the formula i -1 i φ is logically equivalent to φ. Inverse operators arise as, among others, past operators in temporal logic [START_REF] Ryan | Counterfactuals and updates as inverse modalities[END_REF], utterances in epistemic logic [START_REF] Haar | An algebraic view of space/belief and extrusion/utterance for concurrency/epistemic logic[END_REF], and backward moves in modal logic for concurrency [START_REF] Phillips | A logic with reverse modalities for history-preserving bisimulations[END_REF] Kripke Semantics. The most representative semantic models for modal logics are Kripke Structures (KS) [START_REF] Fagin | Reasoning about knowledge[END_REF]. A KS M can be represented as a state graph with n ≥ 1 transition relations 1 -→ M , 2 -→ M , . . . , n -→ M and a function π M that specifies the set of propositions π M (s) that are true at each state (or world) s of M . A pointed KS is a pair (M, s) where s is a state of M . We shall say that (M, s) is model of (or satisfies) a propositional formula p if p ∈ π M (s). Boolean operators are defined as usual; (M, s) is a model of φ ∧ ψ if it is a model of both φ and ψ, and it is a model of ¬φ if it is not model of φ. For the modal case, (M, s) is said to be a model of i φ if (M, t) is a model of φ for every t reachable from s through an i-labelled transition; i.e. s i -→ M t.

We shall use [[ φ ]] to denote the set of all models of φ. Different families of KS give rise to different modal logics. For example, the theorems of the S5 epistemic logic are those modal formulae that are satisfied by all pointed KS whose transition relations are equivalences.

Normal Modal Operators. In modal logic one is often interested in normal modalities: Roughly, a modal operator i is normal in a given modal logic system if [START_REF] Knight | Spatial and epistemic modalities in constraint-based process calculi[END_REF] i φ is a theorem whenever φ is a theorem, and (2) i (φ ⇒ ψ) ⇒ ( i φ ⇒ i ψ) is a theorem.

Normal modalities are ubiquitous in logic; e.g., the box operator in the the logic system K and its extensions [START_REF] Fagin | Reasoning about knowledge[END_REF], and the always and next operators as well as the weak past operator from temporal logic [START_REF] Pnueli | The temporal logic of reactive and concurrent systems[END_REF], the necessity operator from Hennessy-Milner (HM) logic [START_REF] Hennessy | Algebraic laws for nondeterminism and concurrency[END_REF], the knowledge operator from epistemic logic, the belief operator from doxastic logic [START_REF] Hintikka | Knowledge and belief[END_REF] are all normal. In fact, any operator i whose models are defined with the above-mentioned Kripke semantics, is normal.

This paper. Although the notion of spatial constraint system is intended to give an algebraic account of spatial and epistemic assertions, we shall show in this paper that it is sufficiently robust to give an algebraic account of more general modal logic assertions.

The main focus of this paper is the study of the above-mentioned extrusion problem for meaningful families of SCS's called Kripke spatial constraint systems introduced in [START_REF] Knight | Spatial and epistemic modalities in constraint-based process calculi[END_REF].

The constraints (or elements) of Kripke SCS's are sets of pointed KS, i.e., models of modal logics formulae, ordered by reversed inclusion. Consequently, they can be used as semantic domains for modal logic in a natural way. For example, let us suppose that the set of models [[ φ ]] is a constraint in a Kripke SCS. The set [[ i φ ]] can be compositionally obtained, using the space function [•] i of agent i, as the constraint

[ [[ φ ]]
] i in the Kripke SCS. Furthermore, if there exists an extrusion function ↑ i for the space function [•] i (see extrusion problem above) then we can derive an inverse

modality -1 i for i by defining [[ -1 i φ ]] as ↑ i [[ φ ]] .
Contributions. This paper contributes to the theory of constraint systems [START_REF] Saraswat | Semantic foundations of concurrent constraint programming[END_REF] by giving an algebraic characterization of the notion of normal modalities as space functions and by providing a complete taxonomy of extrusion functions from Kripke SCS's. It also contributes to the theory of modal logic by using this characterization and taxonomy to prove new expressiveness results for various modal systems and related notions. More precisely, our contributions are the following:

1. We give an algebraic characterization of the notion of normality in modal logic by building upon work on Geometric Logic [START_REF] Vickers | Topology via logic[END_REF] and show that this abstract notion corresponds exactly to preservation of the join operation.

2. We derive a complete characterization for the existence of right inverses of space functions: The weakest restriction on the elements of the constraint systems (i.e., KS's) that guarantees the existence of right inverses.

3. We give a characterization and derivations of extrusion functions that are normal (and thus they correspon to normal inverse modalities). In particular we identify the maximum normal extrusion function and a family of minimal normal extrusion functions.

4. Finally we discuss the application of our results in the context of specific modal systems and related concepts such as the minimal logic system K [START_REF] Fagin | Reasoning about knowledge[END_REF], the modal logic of linear-time temporal logic (LTL) [START_REF] Pnueli | The temporal logic of reactive and concurrent systems[END_REF], and bisimilarity. In particular, we prove that there is no reverse modality for the box operator of the logic system K nor for the always operator of LTL and we also derive existing inverse modalities for the next operator of LTL. We use our taxonomy results to show that, unlike HM-logic formulae, bisimilarity is not preserved by formulae in HM-logic extended with a reverse modality for the necessity operator: I.e., there are bisimilar pointed KS that do not satisfy the same formulae. This shows that the extended logic is more expressive than HM-logic.

This submission is the extended and revised version of [START_REF] Guzman | Deriving Inverse Operators for Modal Logic[END_REF] for the special issue of selected papers from ICTAC 2016. In this version we have included all proofs as well as new material in Section 5 corresponding to the derivation of all minimal normal right inverses. The work in [START_REF] Guzman | Deriving Inverse Operators for Modal Logic[END_REF] does not study minimal right inverses. This submission thus offers a complete taxonomy of normal right inverses. The new material is also used in the Applications section to prove an expressiveness result in the context of bisimilarity invariance in Section 6.4.

In previous work [START_REF] Haar | An Algebraic View of Space/Belief and Extrusion/Utterance for Concurrency/Epistemic Logic[END_REF] and its extended version [START_REF] Guzman | Belief, knowledge, lies and other utterances in an algebra for space and extrusion[END_REF] the authors derived an inverse modality but only for the specific case of a logic of belief and only a sufficient (but not necessary) condition was identified. Unlike the present work, [START_REF] Haar | An Algebraic View of Space/Belief and Extrusion/Utterance for Concurrency/Epistemic Logic[END_REF][START_REF] Guzman | Belief, knowledge, lies and other utterances in an algebra for space and extrusion[END_REF] were neither concerned with giving a complete characterization of the existence of right inverses, a complete taxonomy of extrusion functions, nor deriving normal inverses.

Organization.

This article is structured as follows. In Section 2 we recall the notions of constraint system and spatial constraint system. In Section 3 we give an algebraic characterization of the notion of normality in modal logic and show that this abstract notion is equivalent to preservation of finite joins. Section 4 and Section 5 are the core sections of the paper.

In Section 4 we identify necessary and sufficient conditions for the existence of right inverses of space functions. In Section 5 we turn our attention to the derivation and classification of normal right inverses. Finally, in Section 6 we discuss and apply our results in the context of the modal system K, LTL, and bisimilarity.

For the sake of clarity and readability this paper includes an index table for notation and a table of contents.

Background: Spatial Constraint Systems

In this section we recall the notion of basic constraint system [START_REF] Boer | Nondeterminism and infinite computations in constraint programming[END_REF] and the more recent notion of spatial constraint system [START_REF] Knight | Spatial and epistemic modalities in constraint-based process calculi[END_REF]. We presuppose basic knowledge of order theory and modal logic [START_REF] Abramsky | Domain theory[END_REF][START_REF] Popkorn | First steps in modal logic[END_REF][START_REF] Fagin | Reasoning about knowledge[END_REF][START_REF] Blackburn | Modal Logic[END_REF].

The concurrent constraint programming model of computation [START_REF] Saraswat | Semantic foundations of concurrent constraint programming[END_REF] is parametric in a constraint system (CS) specifying the structure and interdependencies of the partial information that computational agents can ask of and post in a shared store.

We shall use the following notions and notations from order theory. We shall now describe two typical concrete constraint systems taken from [START_REF] Guzman | Belief, knowledge, lies and other utterances in an algebra for space and extrusion[END_REF][START_REF] Boer | Nondeterminism and infinite computations in constraint programming[END_REF][START_REF] Saraswat | Semantic foundations of concurrent constraint programming[END_REF]. 2 Recall CS's can also be used a semantic domains for concurrent constraint programming (CCP) languages. The restriction to algebraic lattices is for semantic purposes and a full discussion of this technical issue is beyond the scope of this paper (the reader is referred to [START_REF] Boer | Nondeterminism and infinite computations in constraint programming[END_REF]). Briefly speaking, CCP programs can post or query constraints but these constraints must be compact (finite). The result of a possibly infinite computation is the join of all the (compact) constraints posted during the computation. Algebraicity of constraint systems [START_REF] Boer | Nondeterminism and infinite computations in constraint programming[END_REF] means that any constraint is the join of compact constraints below it. This assumption is needed for correspondence results between the denotational semantics and their operational counterpart.

(equivalence class of) finite sets of equalities. The LUB is the (equivalence class of) set union.

In the above example constraints are represented as set of equations and thus the join (LUB) of constraints corresponds to the equivalent class of union of their equations. We can also view a constraint c as a representation of a set of variable assignments [START_REF] Aristizábal | Deriving labels and bisimilarity for concurrent constraint programming[END_REF].

For instance a constraint x > 42 can be thought of as the set of assignments mapping x to a value greater than 42; i.e., the solutions to (or models of) x > 42. In this case the join of constraints naturally corresponds to the intersection of their assignments, false as the empty set of assignments, and true as the set of all assignments.

Example 2.4 (Boolean Constraint System [START_REF] Guzman | Belief, knowledge, lies and other utterances in an algebra for space and extrusion[END_REF][START_REF] Aristizábal | Deriving labels and bisimilarity for concurrent constraint programming[END_REF]). Let Φ be a set of primitive propositions. A boolean (or truth) assignment π over Φ is a total map from Φ to the set {0, 1}. We use A(Φ) to denote the set of all such boolean assignments. We can now define the Boolean CS B(Φ) as (P(A(Φ)), ⊇): The powerset of assignments ordered by ⊇. Thus constraints in Con are sets of assignments, is ⊇, false is ∅, true is A(Φ), the join operator is ∩, and the meet operator is

∪. A constraint c in B(Φ) is compact iff A(Φ) \ c is a finite set.
Notice that logic propositions can be straightforwardly interpreted as constraints in B(Φ). Let L 0 (Φ) be the propositional language built from Φ by the grammar φ, ψ, . . .

:= p | φ ∧ ψ | ¬φ (1)
where p ∈ Φ. We shall use the classical abbreviations φ ∨ ψ for ¬(¬φ ∧ ¬ψ), φ ⇒ ψ for ¬φ ∨ ψ, ff for p ∧ ¬p, and tt for ¬ff . A boolean assignment π satisfies φ iff π |= φ

where |= is defined inductively as follows:

π |= p iff π(p) = 1, π |= φ ∧ ψ iff π |= φ
and π |= ψ, and π |= ¬φ iff π |= φ. We interpret each formula φ as the constraint

B φ def = {π ∈ A(Φ) | π |= φ} in B(Φ). Clearly B φ B ψ holds iff ψ ⇒ φ is valid, i.e.
, satisfied by every truth assignment.

Spatial Constraint Systems. The authors of [START_REF] Knight | Spatial and epistemic modalities in constraint-based process calculi[END_REF] extended the notion of CS to account for distributed and multi-agent scenarios where agents have their own space for keeping their local information and performing their computations.

Let G = {1, . . . , n} be an underlying set of agents. Intuitively, each agent i ∈ G has a space function [•] i from constraints to constraints. Recall that constraints can be viewed as assertions. Thus, given a constraint c, we can think of [c] i as an assertion stating that c is a piece of information residing within a space attributed to agent i.

An alternative epistemic logic interpretation of [c]

i is an assertion stating that agent i believes c or that c holds within the space of agent i (but it may not hold elsewhere).

Both interpretations convey the idea that c is local to agent i. Similarly, [[c] j ] i is a hierarchical spatial specification stating that c holds within the local space the agent i attributes to agent j. Nesting of spaces can be of any depth. We can think of a constraint of the form [c] i [d] j as an assertion specifying that c and d hold within two parallel spaces that belong to agents i and j, respectively. From a computational/ concurrency point of view, we think of as parallel composition. As mentioned before, from a logic point of view the join of information corresponds to conjunction.

Definition 2.5 (Spatial Constraint System [START_REF] Knight | Spatial and epistemic modalities in constraint-based process calculi[END_REF]). An n-agent (n > 0) spatial constraint system (n-SCS) C is a CS (Con, ) equipped with n self-maps We refer the reader to Section 4.1 to see Kripke SCS's in full detail.

Extrusion and utterance. We can also equip each agent i with an extrusion function ↑ i : Con → Con. Intuitively, within a space context [•] i , the assertion ↑ i c specifies that c must be posted outside of agent i's space. This is captured by requiring the following extrusion axiom:

(E.1) [ ↑ i c ] i = c. (2)
In other words, we view extrusion/utterance as the right inverse of space/belief (and thus space/belief as the left inverse of extrusion/utterance).

Definition 2.8 (Extrusion). Given an n-SCS (Con, , [•] 1 , . . . , [•] n ), we say that ↑ i is an extrusion function for the space [•] i iff ↑ i is a right inverse of [•] i , i.e., iff Axiom E.1
in Eq. 2 is satisfied.

From the above definitions it follows that [c Example 2.9.

↑ i d] i = [c] i d.
Let e = [c ↑ i [a] j ] i [d] j .
The constraint e specifies that agent i has c and wishes to transmit, via extrusion, a addressed to agent j. Agent j has d in their space. Indeed, with the help of E.1 and S.2, we can derive e [d a] j thus stating that e entails that a will be in the space of j.

The Extrusion/Right Inverse Problem. A legitimate question is: Given space [•] i can we derive an extrusion function ↑ i for it ? From set theory we know that there is an extrusion function (i.e., a right inverse)

↑ i for [•] i iff [•] i is surjective. Recall that the pre-image of y ∈ Y under f : X → Y is the set f -1 (y) = {x ∈ X | y = f (x)}.
Thus the extrusion ↑ i can be defined as a function, called choice function, that maps each element c to some element from the pre-image of c under [•] i .

The existence of the above-mentioned choice function assumes the Axiom of Choice.

The next proposition from [START_REF] Haar | An algebraic view of space/belief and extrusion/utterance for concurrency/epistemic logic[END_REF] gives some constructive extrusion functions. It also identifies a distinctive property of space functions for which a right inverse exists.

If [•]

i is surjective and preserves arbitrary suprema then

↑ i : c → [c] -1 i is a right inverse of [•]
i and preserve arbitrary infima.

If [•]

i is surjective and preserves arbitrary infima then

↑ i : c → [c] -1
i is a right inverse of [•] i and preserve arbitrary suprema.

We have presented spatial constraint systems as algebraic structures for spatial and epistemic behaviour as that was their intended meaning. Nevertheless, we shall see that they can also provide an algebraic structure to reason about Kripke models with applications to modal logics.

In Section 4 we shall study the existence, constructions and properties of right inverses for a meaningful family of SCS's; the Kripke SCS's. The importance of such a study is the connections we shall establish between right inverses and reverse modalities which are present in temporal, epistemic and other modal logics. Property (1) in Proposition 2.10 can be used as a test for the existence of a right inverse. The space functions of Kripke SCS's preserve arbitrary suprema, thus Property (2) will be useful. They do not preserve in general arbitrary (or even finite) infima so we will not apply Property (3).

It is worth noticing that the derived extrusion ↑ i in Property (3) preserves arbitrary suprema; this implies ↑ i is normal in a sense we shall make precise next. Normal self-maps give an abstract characterization of normal modal operators, a fundamental concept in modal logic. We will be therefore interested in deriving normal inverses.

The notion of normality is important because it is in normal modal logics where the axiom K (i.e. i (φ → ψ) → ( i φ → i ψ)) is satisfied, which allow us to provide modal logics with a Kripke semantics.

Constraint Frames and Normal Self Maps

Spatial constraint systems are algebraic structures for spatial and mobile behavior. By building upon ideas from Geometric Logic and Heyting Algebras [START_REF] Vickers | Topology via logic[END_REF] we can also make them suitable as semantics structures for modal logic. In this section we give an algebraic characterization of the concept of normal modality as the maps preserving finite suprema.

We can define a general form of implication by adapting the corresponding notion from Heyting Algebras to constraint systems. Intuitively, a Heyting implication c → d in our setting corresponds to the weakest constraint one needs to join c with to derive d. Similarly, the negation of a constraint c, written ∼ c, can be seen as the weakest constraint inconsistent with c. The following basic properties of Heyting implication are immediate consequences of the above definitions.

Proposition 3.2. Let (Con, ) be a constraint frame. For every c, d, e ∈ Con:

1. c (c → d) = c d 2. c (d → e) iff c d e 3. c → d = true iff c d
Proof. The proof proceeds as follows:

1. c (c → d) = c d
This is proved in Lemma 1 (Modus Ponens) of [START_REF] Guzman | Belief, knowledge, lies and other utterances in an algebra for space and extrusion[END_REF]. For self-containedness we have included the proof of this item.

We From a computational point of view, we can think of c → d as a process that triggers d if c is present in the space the process is placed. We illustrate this next. Example 3.4. A more complex example involves extrusion from i to j and back from j to i by letting a to be the conditional

d → ↑ j [d] i in the constraint e = [c ↑ [a] j ] i
[d] j defined in Example 2.9. Intuitively the agent i sends a conditional process a to the space of j. Once in this space, d is entailed and thus d is sent to the space of i via extrusion. Indeed one can verify that e [a d] i .

Normal Self-Maps

In modal logics one is often interested in normal modal operators. The formulae of a modal logic are those of propositional logic extended with modal operators. Roughly speaking, a modal logic operator m is normal iff (1) the formula m(φ) is a theorem (i.e., true in all models for the underlying modal language) whenever the formula φ is a theorem, and (2) the implication formula m(φ

⇒ ψ) ⇒ (m(φ) ⇒ m(ψ)) is a theorem.
Since constraints can be viewed as logic assertions, we can think of modal operators as self-maps on constraints. Thus, using Heyting implication 3 , we can express the normality condition in constraint frames as follows. and let f be a self-map on Con. Then f is normal if and only if f preserves finite suprema.

Proof. It suffices to show that for any bottom preserving self-map f , ∀c, d ∈ Con :

f (c → d ) → (f (c) → f (d )) = true iff ∀c, d ∈ Con : f (c d) = f (c) f (d).
(Both conditions require f to be bottom preserving, i.e., f (true) = true, and preservation of non-empty finite suprema is equivalent to the preservation of binary suprema.)

• Assume that ∀c, d ∈ Con : f (c → d ) → (f (c) → f (d )) = true. Take two arbitrary c, d ∈ Con. We first prove f (c d) f (c) f (d).
From the assumption and Proposition 3.2(3) we obtain We now prove

f ((c d) → d) f (c d) → f (d). (3)
f (c) f (d) f (c d).
From the assumption and Proposition 3.2(3) we have

f (c → (d → c d)) f (c) → f (d → c d). (4)
f (d → c d) f (d) → f (c d). We then have f (c) f (d → c d) f (d) → f (c d). Thus f (c) f (d) → f (c d)
(c → d) f (c) = f (c (c → d)) = f (c d) = f (c) f (d) f (d) as wanted.
It then follows from the above theorem that space functions from constraint frames are indeed normal self-maps, since they preserve finite suprema. Another immediate consequence of the above theorem is that every normal self-map is also monotone.

Summary

In this section we have characterized the notion of normal self-maps as those that preserve finite LUBs. This characterization will be useful in the next section when we turn our attention to normal right-inverse self-maps.

Extrusion Problem for Kripke Constraint Systems

This and the next section are the main and more technical parts of the paper. We will study the extrusion/right inverse problem for a meaningful family of spatial constraint systems (SCS); the Kripke SCS. In particular we shall derive and give a complete characterization of normal extrusion functions as well as identify the weakest condition on the elements of the SCS under which extrusion functions may exist. To illustrate the importance of this study it is convenient to give some intuition first. where s is a state of the KS M . In particular, in modal logics with one or more modal (box) operators i , the formula i φ is equated to

i φ = {(M, s) | ∀t : s i -→ M t, (M, t) ∈ φ }.
Analogously, in a Kripke SCS each constraint c is equated to a set of pairs (M, s) of pointed KS. Furthermore, for each space

[•] i we have [c] i = {(M, s) | ∀t : s i -→ M t, (M, t) ∈ c}.
This means that formulae can be interpreted as constraints and in

particular i can be interpreted by [•] i as i φ = [ φ ] i .
Inverse modalities -1 i , also known as a reverse modalities, are used in many modal logics. In tense logics they represent past operators [START_REF] Prior | Past, present and future[END_REF] and in epistemic logic they represent utterances [START_REF] Haar | An algebraic view of space/belief and extrusion/utterance for concurrency/epistemic logic[END_REF]. The basic property of a (right) inverse modality is given by the axiom i ( -1 i φ) ⇔ φ. In fact, given a modal logic one may wish to see if it can be extended with reverse modalities (e.g., is there a reverse modality for the always operator of temporal logic?).

Notice that if we have an extrusion function ↑ i for [•] i we can provide the semantics for inverse modalities -1 i by letting

-1 i φ = ↑ i ( φ ) (thus i ( -1 i φ) = φ
). Therefore deriving extrusion functions and establishing the weakest conditions under which they exist is a relevant issue. Furthermore, the algebraic structure of Kripke SCS may help us establish desirable properties of the reverse modality such as that of being normal (Definition 3.5).

KS and Kripke SCS

We begin by recalling some notions and notations related to Kripke models.

Definition 4.1 (Kripke Structures). An n-agent (n > 0) Kripke Structure (KS) M over a set of primitive propositions Φ is a tuple (S, π, R 1 , . . . , R n ) where
• S is a non-empty set of states,

• π : S → (Φ → {0, 1}) is an interpretation associating with each state a truth assignment to the primitive propositions in Φ, and

• R i is a binary relation on S.
A pointed KS is a pair (M, s) where M is a KS and s, called the actual world, is a state of M .

We shall use the following notation in the rest of the paper. Notation 4.2. Each R i is referred to as the accessibility relation for agent i. We shall use i -→ M to refer to the accessibility relation of agent i in M . We write We now define the Kripke SCS w.r.t. a set S n (Φ) of pointed KS. Notice that in Example 2.4 constraints represented sets of boolean assignments, which allowed us to interpret each propositional formula as a constraint (i.e. the set of assignments satisfying the formula). Similarly, in a Kripke SCS constraints are sets of (pointed) KS models. This will allows us to interpret each modal formula as constraints.

s i -→ M t to denote (s, t) ∈ R i . We use i (M, s) = {(M, t) | s i -→ M t}
Definition 4.3 (Kripke Spatial Constraint Systems [START_REF] Knight | Spatial and epistemic modalities in constraint-based process calculi[END_REF]). Let S n (Φ) be a (non-empty) set of n-agent Kripke structures over a set of primitive propositions Φ. Let ∆ be the set of all pointed Kripke structures (M, s) such that M ∈ S n (Φ).

A Kripke n-SCS for S n (Φ) is a SCS K(S n (Φ)) = (Con, , [•] 1 , . . . , [•] n )
where Con = P(∆), = ⊇, and for every i ∈ {1, . . . , n} :

[ c ] i def = {(M, s) ∈ ∆ | i (M, s) ⊆ c} (5)
In the Kripke-based semantics of modal logic (Section 6) every pointed KS is a model of the constant true and no pointed KS is a model of the constant false. This is consistent with the reversed inclusion = ⊇ order of Kripke constraint systems. We clarify this in the following remark. Notice that K(S n (Φ)) is a frame since meets are unions and LUBs are intersections so the requirement of distributivity is satisfied. Furthermore, each [•] i preserves arbitrary suprema (intersection) and thus, from Theorem 3.6 it is a normal self-map.

Proposition 4.5 ([18]). Let K(S n (Φ)) = (Con, , [•] 1 , . . . , [•] n ) as in Definition 4.3. 1. K(S n (Φ)
) is an n-agent spatial constraint frame.

Each [•]

i preserves arbitrary suprema.

Complete Characterization of the Existence of Right Inverses

We now address the question of whether a given Kripke constraint system can be extended with extrusion functions. We shall identify a sufficient and necessary condition on accessibility relations for the existence of an extrusion function ↑ i given the space

[•] i . We also give explicit right inverse constructions.

Notation 4.6. For notational convenience, we take the set Φ of primitive propositions and n to be fixed from now on and omit them from the notation. E.g., we write M instead of M n (Φ).

The following notions play a key role in our complete characterization, in terms of classes of KS, of the existence of right inverses for Kripke space functions. The following proposition gives an alternative definition of determinant states. First, we need the following notation. of states as i (M, S) = s∈S i (M, s). Furthermore, we shall write s i M t to mean that s uniquely determines t w.r.t. Proof. The proof proceeds as follows :

i i i i i i i i i i i i i i (ii) M2 u1 u2 u3 . . . i i i (iii) M3 u1 u2 u3 . . . i i i i i i i (iv) M4 v i (v) M5
• Assume that s ∈ S M is determinant w.r.t. i -→ M .
Let us proceed by contradiction and assume that there exists an S ⊆ S M such that i (M, s)

⊆ i (M, S ) and s ∈ S . Since s is determinant w.r.t. i -→ M there must ex- ist a t such that s i -→ M t and s i -→ M t for any s ∈ S . By definition of i , (M, t) ∈ i (M, s) and (M, t) ∈ i (M, S ) which is a contradiction since i (M, s) ⊆ i (M, S ).
• Assume for every S ⊆ S M , if i (M, s) ⊆ i (M, S ) then s ∈ S . To reach a contradiction, let us suppose that s is not determinant w.r.t.

i -→ M . By our assumption that s is not determinant w.r.t.

i -→ M it follows that for any t i such that s i -→ M t i there must be s i = s such that s i i -→ M t i . Now, take S = {s 1 , s 2 , . . . }. Notice that i (M, s) ⊆ i (M, S ). Applying the assumption, we conclude s ∈ S , a contradiction.

The following theorem provides a complete characterization, in terms of classes of KS, of the existence of right inverses for space functions.

-1 i = {d | c = [d] i } denotes the pre-image of c under [•] i . Definition 4.13 (Maximum Right Inverse). Let K(S) = (Con, , [•] 1 , . . . , [•] n ) be a
Kripke SCS over S ⊆ M D . We define ↑ M i as the following self-map on Con:

↑ M i : c → [c] -1 i .

It follows from Proposition 2.10.2 that ↑ M

i is a right inverse of [•] i , and furthermore, from its definition it is clear that ↑ M i is the maximum right inverse of [•] i w.r.t. .

Summary

In this section we singled out determinacy-completeness as a necessary and sufficient condition on KS's to guarantee the existence of right inverses (Theorem 4.11). In the rest of the paper M D is used to denote the class of KS's whose accessibility relations are determinant-complete; M D is thus the largest class for which space functions of a Kripke SCS have right inverses. We shall also assume Kripke SCS's K(S) = (Con,

, [•] 1 , . . . , [•] n ) with S ⊆ M D .
We also derived ↑ M i as the maximum right inverse of [•] i w.r.t. the underlying Kripke SCS order. As shown next, however, ↑ M i is not necessarily normal in the sense of Definition 3.5. In the next section we shall derive and classify normal right inverses.

Deriving Normal Right-Inverses

This section is devoted to provide a complete taxonomy, based on the underlying SCS order, of right inverse constructions that are normal. As discussed in Section 6 the Kripke semantics of several inverse modalities in the literature corresponds to normal right inverses of space functions. The notion of indeterminacy and multiple determinacy introduced in Definition 5.1 will play a central role.

Let us first extend the terminology in Definition 4.7.

Definition 5.1 (Indeterminacy and Multiple Determinacy). Let S and R be the set of states and an accessibility relation of a KS M , respectively. Given t ∈ S, we say that t is determined w.r.t. R if there is s ∈ S such that s determines t w.r.t. R, else we say that t is indetermined (or initial) w.r.t. R. Similarly, we say that t is multiply, or ambiguously, determined if it is determined by at least two different states in S w.r.t. R. Additionally, we shall say that t is uniquely determined if it is determined by only one state in S w.r.t. R.

(As in Definition 4.7, we shall often omit "w.r.t. R" when no confusion can occur.)

The following statement and Theorem 3.6 lead us to conclude that the presence of indetermined/initial states or multiple-determined states causes ↑ M i not to be normal.

Proposition 5.2. Let K(S) = (Con, , [•] 1 , . . . , [•] n ) and ↑ M i as in Definition 4.13. Let nd(S) = {(M, t) | M ∈ S & t is indetermined w.r.t. i -→ M } and md(S) = {(M, t) | M ∈ S & t is multiply determined w.r.t. i -→ M }: • If nd(S) = ∅ then ↑ M i (true) = true. • If md(S) = ∅ then ↑ M i (c d) = ↑ M i (c) ↑ M i (d) for some c, d ∈ Con.
Proof.

• If nd(S) = ∅ then ↑ M i (true) = true.
Assume nd(S) = ∅. Take c to be the complement of nd(S) in Con. Using Equation 5we have [START_REF] Knight | Spatial and epistemic modalities in constraint-based process calculi[END_REF] [c] i = true and from the assumption (2) c = true (recall that true is the set of all pointed KS, see Remark 4.4). From ( 1) and (2) we have

↑ M i (true) = [c] -1 i = true. • If md(S) = ∅ then ↑ M i (c d) = ↑ M i (c) ↑ M i (d) for some c, d ∈ Con.
Suppose md(S) = ∅. Take t ∈ md(S), then there exist s, s s.t. s i -→ M t and

s i -→ M t. Let c = {(M, s)} and d = {(M, s )}. Recall that ↑ M i is a right inverse of [•] i . Because of this any constraint e = [↑ M i (e)] i = {(M, s ) | i (M, s ) ⊆ ↑ M i (e)}, therefore (M, t) ∈ ↑ M i (c) ∩ ↑ M i (d). Now, ↑ M i (c ∩ d) = ↑ M i (false) = false because Proposition 2.10 and ↑ M i (false) = [false] -1 i
(recall that false is the empty set, see Remark 4.4). We therefore conclude

↑ M i (c d) = ↑ M i (c ∩ d) = ↑ M i (c) ∩ ↑ M i (d) = ↑ M i (c) ↑ M i (d).
The following central lemma provides distinctive properties of any normal right inverse.

Lemma 5.3. Let K(S) = (Con, , [•] 1 , . . . , [•] n ) be the Kripke SCS over S ⊆ M D .
Suppose that f is a normal right inverse of [•] i . Then for every M ∈ S, c ∈ Con:

1. i (M, s) ⊆ f (c) if (M, s) ∈ c, 2. {(M, t)} ⊆ f (c) if t is multiply determined w.r.t.
i -→ M , and 3. true ⊆ f (true).

Proof. The proof proceeds as follows : Then, we know f (false) ⊆ f (c) therefore {(M, t)} ⊆ f (c) as wanted.

1. i (M, s) ⊆ f (c) if (M, s) ∈ c. Assume (M, s) ∈ c. By definition of i we have i (M, s) = {(M, t) | s i -→ M t}. Then for every (M, t) belonging to i (M, s) t is determined w.r.t. i -→ M . Given that f is a right inverse of [•] i , it must satisfy [f (c)] i = c. By Definition 4.3 we have [c] i = {(M, s) | i (M, s) ⊆ c}, then [f (c)] i = {(M, s) | i (M, s) ⊆ f (c)}. Therefore, since [f (c)] i = c = {(M, s) | i (M, s) ⊆ f (c)} then i (M, s) ⊆ f (c) as wanted. 2. {(M, t)} ⊆ f (c) if t is multiply determined w.r.t. i -→ M . Assume t is multi- ply determined w.r.t.
3. true ⊆ f (true). Trivial from the assumption that f is a normal-right inverse.

As stated in the above lemma, for every normal right inverse f , f (c) must necessarily include every (M, t) such that t is multiply determined w.r.t.

i -→ M , as well as every (M, t) where t is uniquely determined w.r.t.

↑ MN i (c) def =    true if c = true {(M, t) | t is determined w.r.t. i -→ M & ∀s : s i M t, (M, s) ∈ c} (6)
(Recall that s i M t means that s uniquely determines t w.r.t.

i -→ M .)

The following theorem states that

↑ MN i (c) is indeed the maximum normal right inverse of [•] i w.r.t. . Theorem 5.5. Let K(S) = (Con, , [•] 1 , . . . , [•] n ) and ↑ MN i as in Definition 5.4. • The self-map ↑ MN i is a normal right inverse of [•] i , • For every normal right inverse f of [•] i , we have f ↑ MN i .
Proof.

• The self-map

↑ MN i is a normal right inverse of [•] i .
To prove it is a right inverse we prove [↑ MN i (c)] i = c. From Theorem 3.6 to prove that is a normal map it suffices to show that ↑ MN i (true) = true and

↑ MN i (c d) = ↑ MN i (c) ↑ MN i (d) (equivalent to proving ↑ MN i (c ∩ d) = ↑ MN i (c) ∩ ↑ MN i (d)).
- -↑ MN i (true) = true. By definition of ↑ MN i .

[↑ MN i (c)] i = c. Suppose (M, s) ∈ [↑ MN i (c)] i . Then i (M, s) ⊆ ↑ MN i (c) from Definition 4.3. Since s is determinant w.r.t. i -→ M , there exists t s.t.
-

↑ MN i (c ∩ d) = ↑ MN i (c) ∩ ↑ MN i (d
(c ∩ d) ⊆ ↑ MN i (c) ∩ ↑ MN i (d). Because c ∩ d ⊆ c and c ∩ d ⊆ d. Then ↑ MN i (c ∩ d) ⊆ ↑ MN i (c) and ↑ MN i (c ∩ d) ⊆ ↑ MN i (d) by monotonicity of ↑ MN i . Thus ↑ MN i (c ∩ d) ⊆ ↑ MN i (c) ∩ ↑ MN i (d). * ↑ MN i (c)∩↑ MN i (d) ⊆ ↑ MN i (c∩d). Suppose (M, t) ∈ ↑ MN i (c)∩↑ MN i (d). Then from the definition of ↑ MN i , t is determined w.r.t. i -→ M of ↑ MN i . If there exists s s.t. s i M t, then (M, s) ∈ c and (M, s) ∈ d. Suppose there exists such state s. Then (M, s) ∈ c∩d and (M, t) ∈ ↑ MN i (c∩d). If not, then t is multiply determined w.r.t. i -→ M hence (M, t) ∈ ↑ MN i (c ∩ d) by definition of ↑ MN i .
• For every normal right inverse f of [•] i , we have f

↑ MN i .
Suppose f is a normal right inverse. We then need to prove Notice that ↑ MN i (c) excludes indetermined states if c = true. It turns out that we can add them and still obtain a normal right inverse. We shall see in the next section that this kind of normal right inverse arises in the context of linear-time temporal logic. Definition 5.6 (A Normal-Right Inverse). Let K(S) = (Con, ) be a Kripke SCS over

↑ MN i (c) ⊆ f (c) for every c. Keep in mind that is ⊇ in K(S). It suffices to prove that if (M, t) ∈ ↑ MN i (c) then (M, t) ∈ f (c).
S ⊆ M D . Define ↑ N i : Con → Con as ↑ N i (c) def = {(M, t) | ∀s : s i M t, (M, s) ∈ c}.
Clearly ↑ N i (c) includes every (M, t) such that t is indetermined w.r.t.

i -→ M . We now show that it is indeed a normal right inverse.

Theorem 5.7. Let K(S) = (Con, , [•] 1 , . . . , [•] n ) and ↑ N i as in Definition 5.6. The self-map ↑ N i is a normal right inverse of [•] i . Proof. To prove that ↑ N i is a right inverse we prove [↑ N i (c)] i = c.
To prove that it is a normal map, by Theorem 3.6, it suffices to prove ↑ N i (true) = true and

↑ N i (c d) = ↑ N i (c) ↑ N i (d) (equivalent to proving ↑ N i (c ∩ d) = ↑ N i (c) ∩ ↑ N i (d)). • [↑ N i (c)] i = c. Suppose (M, s) ∈ [↑ N i (c)] i . Then i (M, s) ⊆ ↑ N i (c) from Def- inition 4.
(M, s) ∈ [↑ N i (c)] i . • ↑ N i (true) = true. We have ↑ N i (true) = {(M , t) | ∀s : s i M t, (M , s) ∈ true}. Since (M, s) ∈ true trivially holds, (M, t) ∈ ↑ N i (true) for any (M, t). Thus ↑ N i (true) = true. • ↑ N i (c ∩ d) = ↑ N i (c) ∩ ↑ N i (d). We first prove monotonicity (i.e. if c ⊆ d then ↑ N i (c) ⊆ ↑ N i (d)). For this, suppose c ⊆ d and (M, t) ∈ ↑ N i (c). If there exists a state s with (M, s) ∈ c s.t. s i M t then (M, s) ∈ d, thus (M, t) ∈ ↑ N i (d). If such state does not exist, then (M, t) ∈ ↑ N i (d).
We now proceed with the proof.

-

↑ N i (c ∩ d) ⊆ ↑ N i (c) ∩ ↑ N i (d). We know c ∩ d ⊆ c and c ∩ d ⊆ d. Then, by monotonicity of ↑ N i , ↑ N i (c ∩ d) ⊆ ↑ N i (c) and ↑ N i (c ∩ d) ⊆ ↑ N i (d). Therefore ↑ N i (c ∩ d) ⊆ ↑ N i (c) ∩ ↑ N i (d).
-

↑ N i (c) ∩ ↑ N i (d) ⊆ ↑ N i (c ∩ d). Suppose (M, t) ∈ ↑ N i (c) ∩ ↑ N i (d).
(M, t) ∈ ↑ N i (c ∩ d) by definition of ↑ N i .

Deriving Minimal Normal-Right Inverses

In Definition 5.6 we included in ↑ N i (c) all indetermined states. We did not include, however, the states that are uniquely determined by states not in c. It turns out that, under certain conditions, we can add all but one of them to ↑ N i (c) and obtain a minimal normal right inverse.

We shall see that not adding all uniquely determined is a necessary condition to guarantee that the resulting self-map is still a right inverse. We shall use choice functions to select the uniquely-determined states that are not added. Nevertheless, we shall also show that such selection must obey certain conditions to guarantee that the resulting right inverse self-map is still normal.

Remark 5.8. A map m is a choice function (or selector) for a collection of nonempty sets if it maps each set S in the collection to some element m(S) of S. Recall that £ i (M, s) denotes the set of all (M, t) such that s uniquely determines t w.r.t. Below we define a minimal right inverse ↑ mN i,s , where s is a family of selectors, following the above intuitions. Given c ∈ Con, we shall use a selector s c ∈ s that chooses an element in each set in the collection { £ i (M, s) } (M,s) / ∈c . These selected elements are not included in ↑ mN i,s (c). Definition 5.9

(Minimal Normal-Right Inverse). Let K(S) = (Con, , [•] 1 , . . . , [•] n )
be a Kripke SCS over S ⊆ M D . Define ↑ mN i,s : Con → Con as

↑ mN i,s (c) def = {(M, t) | ∀s : s i M t, (M, s) ∈ c} ∪ (7) (M,s) / ∈c £ i (M, s) \ {s c ( £ i (M, s) )} ( 8
)
where s is a family

{ s c } c∈Con such that (1) s c is a selector for { £ i (M, s) } (M,s) / ∈c , and (2) if c ⊆ d then s c(£ i (M, s)) = s d(£ i (M, s)) for every (M, s) ∈ d.
From the above definition of ↑ mN i,s (c) it is easy to see that :

• (7) includes the indetermined states, the multiply determined states and the uniquely determined states by any state s such that (M, s) ∈ c, and

• (8) includes uniquely determined states by any s such that (M, s ) / ∈ c but it excludes uniquely determined states selected by the choice function s c in Definition 5.9 (1).

In the following example we will illustrate that if we were to include these selected states, ↑ mN i,s (c) would not be a right inverse of [•] i . Let s be a family of selectors that includes s d and s c. Assume that

i i i i i i i i i i i c d
s d(£ i (M, s 1 )) = (M, t 1 ), s d(£ i (M, s 2 )) = (M, t 3 ) and s c(£ i (M, s 3 )) = (M, t 5
). From Definition 5.9

we obtain

↑ mN i,s (c) = {(M, t 1 ), (M, t 2 ), (M, t 3 ), (M, t 4 )}.
Let us now consider h(c) = ↑ mN i,s (c) ∪ s c(£ i (M, s 3 )) to be ↑ mN i,s (c) plus the pointed KS from £ i (M, s 3 ) selected by the choice function s c. We would then obtain h(c) = {(M, t 1 ), (M, t 2 ), (M, t 3 ), (M, t 4 ), (M, t 5 )}.

Notice that any self-map g such that g(c) = h(c) cannot be a right inverse for [•] i .

From Definition 4.3 we would have

[g(c)] i = {(M, s 1 ), (M, s 2 ), (M, s 3 )} = c.
Notice that the selection of elements that are not included in ↑ mN i,s (c) need to obey Condition (2) in Definition 5.9. This condition is needed for the normality of ↑ mN i,s (c). We illustrate this in the following example. Let s be a family of selectors that includes s c, s d and s c∩d . Suppose that s c(£ i (M, s 1 )) = (M, t 1 ) = s c∩d (£ i (M, s 1 )), s c(£ i (M, s 3 )) = (M, t 5 ) = s c∩d (£ i (M, s 3 )), and

i i i i i i i i i i i i d c
s d(£ i (M, s 3 )) = (M, t 6 ).
We have c ⊆ d but s c(£ i (M, s 3 )) = s d(£ i (M, s 3 )) hence s does not satisfy Condition

(2) in Definition 5.9.

Notice that if we were to drop Condition (2) in Definition 5.9 we would obtain the following.

↑ mN i,s (c) ={(M, t 3 ), (M, t 4 ), (M, t 2 ), (M, t 6 )} ↑ mN i,s (d) ={(M, t 1 ), (M, t 2 ), (M, t 3 ), (M, t 4 ), (M, t 5 )} ↑ mN i,s (c ∩ d) = ↑ mN i,s (c) ={(M, t 3 ), (M, t 4 ), (M, t 2 ), (M, t 6 )} And since ↑ mN i,s (c) ∩ ↑ mN i,s (d) = {(M, t 3
), (M, t 4 ), (M, t 2 )} then we would conclude

↑ mN i,s (c) ∩ ↑ mN i,s (d) = ↑ mN i,s (c ∩ d).
Then ↑ mN i,s would not be a normal right inverse of [•] i (Theorem 3.6)

Now we prove that the function ↑ mN i,s (•) presented in Definition 5.9 is a normal right inverse of the space function [•] i . Theorem 5.12. Let K(S) = (Con, , [•] 1 , . . . , [•] n ) and ↑ mN i,s as in Definition 5.9. The self-map

↑ mN i,s is a normal right inverse of [•] i .
Proof. To prove that ↑ mN i,s is a right inverse we prove [↑ mN i,s (c)] i = c. To prove that it is a normal map, by Theorem 3.6, it suffices to prove ↑ mN i,s (true) = true and

↑ mN i,s (c d) = ↑ mN i,s (c) ↑ mN i,s (d) (equivalent to proving ↑ mN i,s (c ∩ d) = ↑ mN i,s (c) ∩ ↑ mN i,s (d)).
• [↑ mN i,s (c)] i = c. The proof of this equality is similar to corresponding one in the proof of Theorem 5.7. Suppose (M, s)

∈ [↑ mN i,s (c)] i . Then i (M, s) ⊆ ↑ mN i,s (c) from Definition 4.3. Since every state from K(S) is determinant w.r.t. i -→ M , there must be t s.t. s i M t and (M, t) ∈ ↑ mN i,s (c)
. Therefore by definition of ↑ mN i,s , (M, s) ∈ c. Now suppose (M, s) ∈ c, then for all states in i (M, s), they are either uniquely determined by s or multiply determined w.r.t. • ↑ mN i,s (true) = true. The proof of this equality is also similar to corresponding one in the proof of Theorem 5.7. Recall that true is the set of all pointed KS's (M, s) (with M ∈ S) while false is the empty set. Thus ∅ = (M,s) / ∈true £ i (M, s) \ {s c(£ i (M, s))}. From Definition 5.9 we obtain ↑ mN i,s (true) = {(M , t) | ∀s :

s i M t, (M , s) ∈ true} = true. • ↑ mN i,s (c ∩ d) = ↑ mN i,s (c) ∩ ↑ mN i,s (d). We first prove monotonicity of ↑ mN i,s : If c ⊆ d then ↑ mN i,s (c) ⊆ ↑ mN i,s (d). Suppose c ⊆ d and (M, t) ∈ ↑ mN i,s (c)
. We want to prove that (M, t) ∈ ↑ mN i,s (d). If t is indetermined or multiply determined w.r.t.

i -→ M then trivially, from Definition 5.9, (M, t) is included ↑ mN i,s (d). Otherwise, t is uniquely determined and thus we must have an s such that s i M t. If (M, s) ∈ c then since c ⊆ d, we have (M, s) ∈ d and thus (M, t) ∈ ↑ mN i,s (d) by Definition 5.9. Otherwise (M, s) / ∈ c and since (M, t) ∈ ↑ mN i,s (c) we conclude from Definition 5.9 that

(M, t) ∈ £ i (M, s) \ {s c(£ i (M, s))}. If (M, s) ∈ d, then (M, t) ∈ {(M, t) | ∀s : s i M t, (M, s) ∈ d} and (M, t) ∈ ↑ mN i,s (d).
Otherwise (M, s) / ∈ d and then from Condition (2) in Definition 5.9 we conclude that (M, t) ∈ £ i (M, s) \ {s d(£ i (M, s))}. Hence from Definition 5.9

we conclude (M, t) ∈ ↑ mN i,s (d) as wanted.

We now proceed to prove

↑ mN i,s (c ∩ d) = ↑ mN i,s (c) ∩ ↑ mN i,s (d). The direction ↑ mN i,s (c ∩ d) ⊆ ↑ mN i,s (c) ∩ ↑ mN i,s (d) is an immediate consequence of the the monotonicity of ↑ mN i,s (•). To show that ↑ mN i,s (c) ∩ ↑ mN i,s (d) ⊆ ↑ mN i,s (c ∩ d)
it is convenient to define the following sets:

A 1 ={(M, t) | ∀s : s i M t, (M, s) ∈ c}, A 1 ={(M, t) | ∀s : s i M t, (M, s) ∈ d}, A 2 = (M,s) / ∈c £ i (M, s) \ {s c(£ i (M, s))}, A 2 =A 1 , A 3 = A 1 , A 3 = (M,s) / ∈d £ i (M, s) \ {s d(£ i (M, s))}, A 4 =A 2 , A 4 = A 3 .
And

B 1 ={(M, t) | ∀s : s i M t, (M, s) ∈ c ∩ d}, B 2 = (M,s) / ∈c∩d £ i (M, s) \ {s c∩d (£ i (M, s))}.
From Definition 5.9 we have

↑ mN i,s (c ∩ d) = B 1 ∪ B 2 .
Using Definition 5.9 and distributive set laws we obtain

↑ mN i,s (c) ∩ ↑ mN i,s (d) = (A 1 ∪ A 2 ) ∩ (A 1 ∪ A 3 ) = i∈I A i where A i = A i ∩ A i for i ∈ I = {1, 2, 3, 4}. It is easy to verify that A 1 ⊆ B 1 and A 4 ⊆ B 2 .
Using Condition (2) in Definition 5.9 we conclude

A 2 ⊆ B 2 and A 3 ⊆ B 2 . Thus, A 2 ⊆ A 2 ⊆ B 2 , A 3 ⊆ A 3 ⊆ B 2 . Therefore ↑ mN i,s (c) ∩ ↑ mN i,s (d) ⊆ ↑ mN i,s (c ∩ d) as wanted.
We shall show that the family of normal right inverses in Definition 5.9 are minimal Proof. We prove that there is no other normal right inverse g(•) for the space function

[•] i such that g(c) ↑ mN i,s (c) for every c ∈ Con. Recall that g(c) ↑ mN i,s (c) is equivalent to ↑ mN i,s (c) ⊆ g(c) (Remark 4.12).
By way of contradiction let us assume that there exists a normal right inverse g(•) for

[•] i , different from ↑ mN i,s (•), such that ↑ mN i,s (c) ⊆ g(c)
for all c ∈ Con. Thus there must be (M, t) and c ∈ Con such that (M, t) ∈ g(c) and (M, t) / ∈ ↑ mN i,s (c).

Since (M, t) / ∈ ↑ mN i,s (c), we can use Lemma 5.3 and Definition 5.9 to show that

(M, s) / ∈ c and that (M, t) = s c(£ i (M, s)) (9)
where s uniquely determines t in M (i.e., s i M t).

From Equation 9and Definition 5.9 it follows that £ i (M, s) \ {(M, t)} is included in

↑ mN i,s (c). But ↑ mN i,s (c) ⊆ g(c) and (M, t) ∈ g(c) thus £ i (M, s) ⊆ g(c). (10)
From Lemma 5.3(2) and the assumption that g is a normal right inverse, g(c) includes all (M, t) such that t is multiply determined w.r.t. Proof. Given a normal right inverse g of [•] i we will show the existence of a minimal right inverse ↑ mN i,s of [•] i for some s such that for every c ∈ Con if (M, t) ∈ g(c) then (M, t) ∈ ↑ mN i,s (c) (see Remark 4.12).

From Theorem 5.12, Lemma 5.3 and Definition 5.9, ↑ mN i,s (c) includes every (M, t) such that t is multiply determined or indetermined w.r.t.

i -→ M as well as every (M, t) such that t is uniquely determined w.r.t.

i -→ M by some s with (M, s) ∈ c. Consequently, it suffices to prove that for every (M, t) such that t is uniquely determined by some s with (M, s) / ∈ c if (M, t) ∈ g(c) then (M, t) ∈ ↑ mN i,s (c). More precisely, it suffices to prove that there exists a family of selectors s such that the following holds for any c ∈ Con:

If (M, t) ∈ g (c) then (M, t) ∈ ↑ mN i,s (c) (12)
where g (e) def = g(e) ∩ (M,s) / ∈e £ i (M, s).

We need to prove some properties about g . The first property is the following:

If (M, s) / ∈ c then £ i (M, s) \ g (c) = ∅. (13)
This property follows from the fact that g is normal and a right inverse. We prove something stronger: 13.

If (M, s) / ∈ c then g (c) ⊂ £ i (M, s). Notice that if (M, s) / ∈ c then g (c) ⊆ £ i (M,
The second property we claim about g is the following:

If c ⊆ d and (M, s) ∈ d then £ i (M, s) \ g (d) ⊆ £ i (M, s) \ g (c) (14)
To prove this property, suppose that c ⊆ d, (M, s) ∈ d, and (M, t)

∈ £ i (M, s) \ g (d)
. To conclude the proof we now identify a minimal normal right inverse ↑ mN i,s that satisfies Equation 12. Let s to be a family of choice functions {s c} c∈Con such that (I)

Thus (M, t) ∈ £ i (M,
s c(£ i (M, s)) ∈ £ i (M, s) \ g (c) and (II) s c(£ i (M, s)) = s d(£ i (M, s))
for every (M, s) ∈ d whenever c ⊆ d. Notice that because of Equation 13 condition (I) can be fulfilled. Similarly, with the help of Equations 13 and 14, condition (II) can also be fulfilled. Clearly s satisfies the selection conditions in Definition 5.9. Thus we have

↑ mN i,s ↑ mN i,s (c) = {(M, t) | ∀s : s i M t, (M, s) ∈ c} ∪ (M,s) / ∈c £ i (M, s) \ {s c(£ i (M, s))}
Because of (I), this minimal right inverse ↑ mN i,s is easily seen to satisfy Equation 12 which concludes the proof.

Summary

In this section we derived normal right inverses and classified them according to the underlying Kripke SCS order. We focused on normal right inverses, because as we shall illustrate in the next section, they are ubiquitous in modal logic. We identified the maximum normal right inverse ↑ MN i , a normal right inverse ↑ N i and the family of all minimal right inverses, denoted as {↑ mN i,s }. The following corollary summarizes our classification.

Corollary 5.15 (Taxonomy). Fix a Kripke SCS K(S) = (Con, ,

[•] 1 , . . . , [•] n ) with S ⊆ M D . Then 1. ↑ mN i,s ↑ N i ↑ MN i
for every s as in Definition 5.9, and 2. for every normal right inverse g of [•] i , there exists s as in Definition 5.9 such that

↑ mN i,s g ↑ MN i (i.e., ↑ mN i,s (c) ⊇ g(c) ⊇ ↑ MN i (c) for every c ∈ Con.)
where ↑ MN i , ↑ N i and ↑ mN i,s are given as in Definitions 5.4, 5.6 and 5.9 w.r.t. K(S).

The upper and lower bounds in Corollary 5.15 [START_REF] Saraswat | Semantic foundations of concurrent constraint programming[END_REF] are useful to prove whether some e is in a given normal-right inverse g. Thus if e ∈ ↑ MN i (c) then e ∈ g(c) and if e / ∈ ↑ mN i,s (c) for every s then e / ∈ g(c). We shall use these properties in the next section.

The following table summarizes the right inverses presented in Corollary 5.15 .

Maximum Right Inverse

Applications

In this section we will illustrate and briefly discuss the results obtained in the previous sections in the context of modal logic.

Modal formulae can be interpreted as constraints in the SCS K(S n (Φ)). First we recall the notion of modal language. Bisimilarity is a central equivalence in concurrency theory [START_REF] Milner | Communication and concurrency[END_REF]. Bisimilarity-invariance. The well-known result of bisimilarity-invariance of modal satisfiability [START_REF] Hennessy | Algebraic laws for nondeterminism and concurrency[END_REF] implies that if (M, s) ∼ s (N, t) then (M, s) and (M, t) satisfy exactly the same formulae in L n (Φ).

Modal logics are typically interpreted over different classes of KS's obtained by imposing conditions on their accessibility relations. Let S n (Φ) be a non-empty set of n-agent Kripke structures over a set of primitive propositions Φ. A modal formula φ is said to be valid in S n (Φ) iff (M, s) |= φ for each (M, s) such that M ∈ S n (Φ).

We can interpret modal formulae as constraints in a given Kripke SCS C = K(S n (Φ))

as follows.

Definition 6.3 (Kripke Constraint Interpretation). Let C be a Kripke SCS K(S n (Φ)).

Given a modal formula φ in the modal language L n (Φ), its interpretation in the Kripke SCS C is the constraint C φ inductively defined as follows: It is easy to verify that the constraint C φ includes those pointed KS (M, s), where

C p = {(M, s) | π M (s)(p) = 1} C φ ∧ ψ = C φ C ψ C ¬φ = ∼ C φ C i φ = [ C φ ] i Remark
M ∈ S n (Φ), such that (M, s) |= φ. Thus, φ is valid in S n (Φ) if and only if C φ = true.
Notice that from Proposition 4.5 and Theorem 3.6, each space function

[•] i of K(S n (Φ))
is a normal self-map. From Definitions 3.5 and 6.3 we can derive the following standard property stating that i is a normal modal operator:

1. (Necessitation) If φ is valid in S n (Φ) then i φ is valid in S n (Φ), and 2
. (Distribution) i (φ ⇒ ψ) ⇒ ( i φ ⇒ i ψ) is valid in S n (Φ).

Right-Inverse Modalities

Reverse modalities, also known as inverse modalities, arise naturally in many modal logics. For example in temporal logics they are past operators [START_REF] Pnueli | The temporal logic of reactive and concurrent systems[END_REF], in modal logics for concurrency they represent backward moves [START_REF] Phillips | A logic with reverse modalities for history-preserving bisimulations[END_REF], in epistemic logic they correspond to utterances [START_REF] Haar | An algebraic view of space/belief and extrusion/utterance for concurrency/epistemic logic[END_REF].

To illustrate our results in the previous sections, let us fix a modal language L n (Φ)

(whose formulae are) interpreted in an arbitrary Kripke SCS C = K(S n (Φ)). Suppose we wish to extend it with modalities -1 i , called reverse modalities also interpreted over the same set of KS's S n (Φ) and satisfying some minimal requirement. The new language is given by the following grammar. Definition 6.5 (Modal Language with Reverse Modalities). Let Φ be a set of primitive propositions. The modal language L +r n (Φ) is given by the following grammar:

φ, ψ, . . . := p | φ ∧ ψ | ¬φ | i φ | -1 i φ
where p ∈ Φ and i ∈ {1, . . . , n}.

The minimal semantic requirement for each -1 i is that, regardless of the interpretation we give to -1 i φ, we should have:

i -1 i φ ⇔ φ valid in S n (Φ). (15)
We then say that -1 i is a right-inverse modality for i (by analogy to the notion of right inverse function).

Since C i φ = [ C φ ] i , we can use the results in the previous sections to derive semantic interpretations for -1 i φ by using a right inverse ↑ i for the space function [•] i in Definition 6.3. Assuming that such a right inverse exists, we can then interpret the reverse modality in C as

C -1 i φ = ↑ i ( C φ ). (16)
Since each ↑ i is a right inverse of [•] i , it is easy to verify that the interpretation satisfies the requirement in Equation 15. Furthermore, from Theorem 4.11 we can conclude that for each M ∈ S n (Φ), i -→ M must necessarily be determinant-complete.

Normal Inverses Modalities

We can choose ↑ i in Equation 16 from the set {↑ N i , ↑ MN i , ↑ M i , ↑ mN i,s } of right inverse constructions in Section 4.3. Assuming that ↑ i is a normal self-map (e.g., either ↑ N i , ↑ MN i , or ↑ mN i,s ), we can show from Definition 3.5 and Equation 16that -1 i is itself a normal modal operator in the following sense:

(1) If φ is valid in S n (Φ) then -1 i φ is valid in S n (Φ), and (2) -1 i (φ ⇒ ψ) ⇒ ( -1 i φ ⇒ -1 i ψ) is valid in S n (Φ).

Inconsistency Invariance

We can conclude from Proposition 2.10(1) that since we assumed a right inverse of [•] i , we should have

¬ i ff valid in S n (Φ). (17)
Indeed using the fact that [•] i is a normal self-map with an inverse ↑ i and Theorem 3.6, we can verify the following:

C i ff = C i (ff ∧ -1 i ff ) = C i (ff )∧ i ( -1 i ff ) = C i (ff )∧ff = C ff .
This implies i ff ⇔ ff is valid in S n (Φ) and this amounts to say that ¬ i ff is valid in S n (Φ).

Modal systems such K n or HM [START_REF] Hennessy | Algebraic laws for nondeterminism and concurrency[END_REF] where ¬ i ff is not an axiom cannot be extended with a reverse modality satisfying Equation 15 (without restricting their models). The issue is that the axiom ¬ i ff , typically needed in epistemic, doxastic and temporal logics, would require the accessibility relations of agent i to be serial (recall that determinant-complete relations are necessarily serial). In fact i ff is used in HM logic to express deadlocks w.r.t. i; (M, s) |= i ff iff there is no s such that s i -→ M s .

Clearly there cannot be state deadlocks w.r.t. i if i -→ M is required to be serial for each M .

Bisimilarity Invariance

Recall that bisimilarity invariance states that bisimilar pointed KS's satisfy the same formulae in L n (Φ). The addition of a reverse modality -1 i may violate this invariance, in the sense that bisimilar pointed KS's may not longer satisfy the same formulae in L +r n (Φ). This can be viewed as saying that the addition of inverse modalities increases the distinguishing power of the original modal language. We prove this next as an application of our taxonomy of normal right inverses in Section 5.

Let us suppose that the chosen right inverse ↑ i in Equation 16is any normal self-map whatsoever. Now take v and s 4 as in Figure 4. Suppose that π M5 (v) = π M1 (s i ) for every s i in the states of M 1 . Clearly (M 1 , s 4 ) ∼ s (M 5 , v). Since s 4 is multiply determined then from Definition 5.4 (m, s 4 ) ∈ ↑ MN i (false). Using Corollary 5.15(2) we obtain (m, s 4 ) ∈ ↑ i (false), and thus (M 1 , s 4 ) |= -1 i ff .

Since v is uniquely determined, applying Definition 5.9 we conclude that (M Thus, from the bounds for normal right inverses provided in this paper we have shown that regardless of the normal interpretation of -1 i , the formula -1 i ff can tell uniquely determined states from multiply determined ones but bisimilarity cannot tell them appart.

Temporal Operators

We conclude this section with a brief discussion on some right inverse linear-time modalities. Let us suppose that we have two agents n = 2 in our modal language L n (Φ) under consideration. Thus, we can interpret them in Kripke SCS as C = K(S 2 (Φ)).

Assume further that the intended meaning of the two modalities 1 and 2 are the next operator ( ) and the henceforth/always operator (P), respectively, in a linear-time temporal logic. In order to obtain the intended meaning we take S 2 (Φ) to be the largest set such that: If M ∈ S 2 (Φ), where M is a 2-agent KS, the accessibility relation , we obtain -1 1 = , which corresponds to a past modality known in the literature as the strong previous operator [START_REF] Pnueli | The temporal logic of reactive and concurrent systems[END_REF]. Formally, the operator is given by (M, t) |= φ iff there exists s such that s M -→ 1 t and (M, s) |= φ.

If we take ↑ i to be the normal right inverse ↑ N i , we obtain -1 1 = the past modality known as weak previous operator [START_REF] Pnueli | The temporal logic of reactive and concurrent systems[END_REF]. The formal definition of the operator is given by (M, t) |= φ iff for every s if s M -→ 1 t then (M, s) |= φ. Notice that the only difference between the two operators is the following: If s is an indetermined/initial state w.r.t. 15.

By analogy to the above-mentioned past operators, one may think that the past operator it-has-always-been [START_REF] Ryan | Counterfactuals and updates as inverse modalities[END_REF] may provide a reverse modality for P in the sense of Equation 15. The operator is given by (M, t) |= φ iff (M, s) |= φ for every s such that s 2 -→ M t. Clearly P φ ⇒ φ is valid in S 2 (Φ) but φ ⇒ P φ is not.

Concluding Remarks and Related Work

We gave an algebraic counterpart of the notion of normality from modal logic: A self-map is normal if and only if it preserves finite suprema. We then studied the existence and derivation of right inverses (extrusion) of space functions for the Kripke spatial constraint systems. We showed that being determinant-complete is the weakest condition on KS's that guarantees the existence of such right inverses. We identified the maximum normal right inverse as well as all minimal right inverses of any given space function. To illustrate our results we applied them to modal logic by using space functions and their right inverses as the semantic counterparts of box modalities and their right inverse modalities. We discussed their implications in the context of modal concepts such as bisimilarity invariance, inconsistency invariance and temporal modalities.

Most of the related work was discussed in the previous sections. The constraint systems in this paper can be seen as a modal extension of geometric logic [START_REF] Vickers | Topology via logic[END_REF]. Modal logic has also been studied from an algebraic perspective by using modal extensions of boolean and Heyting algebras in [START_REF] Macnab | Modal operators on heyting algebras[END_REF][START_REF] Blackburn | Modal Logic[END_REF][START_REF] Chagrov | of oxford logic guides[END_REF]. These works, however, do not address issues related to inverse modalities. Inverse modalities have been used in temporal, epistemic and logic for concurrency. In [START_REF] Ryan | Counterfactuals and updates as inverse modalities[END_REF] the authors discuss inverse temporal and epistemic modalities from a proof theory perspective. The work in [START_REF] Phillips | A logic with reverse modalities for history-preserving bisimulations[END_REF][START_REF] De Nicola | Observational logics and concurrency models[END_REF][START_REF] Goltz | Propositional temporal logics and equivalences[END_REF] uses modal logic with reverse modalities for specifying true concurrency and [START_REF] De Nicola | Back and forth bisimulations[END_REF][START_REF] De Nicola | Three logics for branching bisimulation[END_REF] use backward modalities for characterizing branching bisimulation. None of these works are concerned with an algebraic approach or with deriving inverse modalities for modal languages.

Residuation theory [START_REF] Blyth | Residuation Theory[END_REF] can be used for elegant characterizations of minimal information and inverse operators. In fact it has been used in the context of soft concurrent constraint programming, e.g. to allow for non-idempotent tell/post operations [START_REF] Gadducci | A labelled semantics for soft concurrent constraint programming[END_REF].

Soft CCP requires a richer notion of constraint system based on residuation theory. As future work, it is natural to consider spatial extensions of the constraint systems from [START_REF] Gadducci | A labelled semantics for soft concurrent constraint programming[END_REF] towards a more general framework of spatial soft CCP.

In the present paper we used spatial constraint systems (SCS's) as an abstract representation of modal logics. This helped us to prove new expressiveness results for these logics. As future work we plan to use SCS's as an abstract representation of process calculi. We expect to use this representation to prove expressiveness results similar to those in [START_REF] Palamidessi | On the Expressiveness of Linearity vs Persistence in the Asychronous Pi-Calculus[END_REF][START_REF] Cacciagrano | Linearity, Persistence and Testing Semantics in the Asynchronous Pi-Calculus[END_REF] which are inspired by the close connection between processes and formulae.

Index

, entailment, order relation, 9

, , join, LUB, supremum, 9 , it-has-always-been operator, 48

Notation 2 . 1 (

 21 Lattices and Limit Preservation). Let C be a partially ordered set (poset) (Con, ). We shall use S to denote the least upper bound (LUB) (also called supremum or join) of the elements in S if it exists, and similarly S is the greatest lower bound (GLB) (also called infimum or meet) of the elements in S if it exists. We say that C is a complete lattice iff each subset of Con has a LUB and a GLB in Con. A non-empty set S ⊆ Con is directed iff every finite subset of S has an upper bound in S. Also c ∈ Con is compact iff for any directed subset D of Con, c D implies c d for some d ∈ D. A complete lattice C is said to be algebraic iff for each c ∈ Con, the set of compact elements below it forms a directed set and the LUB of this directed set is c. A self-map on Con is a function f : Con → Con. Let (Con, ) be a complete lattice. The self-map f on Con preserves the LUB of a set S ⊆ Con iff f ( S) = {f (c) | c ∈ S}. The preservation of the GLB of a set is defined analogously. We say f preserves finite/infinite suprema iff it preserves the LUB of arbitrary finite/infinite sets. Preservation of finite/infinite infima is defined similarly. The order extends naturally to self-maps; we shall write f g, where f and g are self-maps on Con if and only if f (c) g(c) for every c ∈ Con. Constraint systems can be formalized as complete algebraic lattices [3] 1 . The elements of the lattice, the constraints, represent (partial) information. A constraint c can be viewed as an assertion. The lattice order is meant to capture (reverse) entailment of information: c d, alternatively written d c, means that the assertion d represents at least as much information as c. Thus we may think of c d as saying that d entails c or that c can be derived from d. The least upper bound (LUB) operator represents join of information; c d, the least element in the underlying lattice above c and d. Thus c d can be seen as an assertion stating that both c and d hold. The top element represents the LUB of all, possibly inconsistent, information, hence it is referred to as false. The bottom element true represents the empty information. Definition 2.2 (Constraint Systems [3]). A constraint system (CS) C is a complete algebraic 2 lattice (Con, ). The elements of Con are called constraints. The symbols , true and false will be used to denote the least upper bound (LUB) operation, the bottom, and the top element of C, respectively.

Example 2 . 3 (

 23 Herbrand Constraint System[START_REF] Saraswat | Semantic foundations of concurrent constraint programming[END_REF][START_REF] Boer | Nondeterminism and infinite computations in constraint programming[END_REF][START_REF] Guzman | Belief, knowledge, lies and other utterances in an algebra for space and extrusion[END_REF]). The Herbrand CS captures syntactic equality between terms t, t , . . . built from a first-order alphabet L with variables x, y, . . ., function symbols, and equality =. The constraints are (equivalent classes of) sets of equalities over the terms of L: E.g., {x = t, y = t} is a constraint. The relation c d holds if the equalities in c follow from those in d: E.g., {x = y} {x = t, y = t}. The constraint false is the set of all term equalities in L and true is (the equivalence class of) the empty set. The compact elements are the1 An alternative syntactic characterization of CS, akin to Scott information systems, is given in[START_REF] Saraswat | Semantic foundations of concurrent constraint programming[END_REF].

  From a spatial point of view, agent i extrudes d from its local space. From an epistemic view this can be seen as an agent i that believes c and utters d to the outside world. If d is inconsistent with c, i.e., c d = false, we can see the utterance as an intentional lie by agent i: The agent i utters an assertion inconsistent with their own beliefs.

Proposition 2 .

 2 10 ([9]). Let [•] i be a space function of SCS. Then 1. If [false] i = false then [•] i does not have any right inverse.

Definition 3 . 1 (

 31 Constraint Frames). A constraint system (Con, ) is said to be a constraint frame iff its LUBs distribute over arbitrary meets: For every c ∈ Con and S ⊆ Con we have c S = {c e | e ∈ S}. Given a constraint frame (Con, ) and c, d ∈ Con, define Heyting implication c → d as {e ∈ Con | c e d } and Heyting negation as ∼ c def = c → false.

•• 2 .•

 2 need to prove c {e | d e c} = c d. Recall that by definition LUBs distribute over arbitrary meets in any frame. First we prove c {e | d e c} c d. Let S = {e | d e c}. Since d ∈ S, we conclude S d. Thus, c S c d as wanted. We now prove c d c {e | d e c}. Let S = {e | d e c}. Distributing the LUB over the meet we obtain c S = {c e | e ∈ S}. Since each c e d for every e ∈ S then d {c e | e ∈ S} = c (d → e) iff c d e Assume c (d → e). Then we have c d (d → e) d. Therefore, from Proposition 3.2 (1) (modus ponens) we obtain c d d e and c d e as wanted. • Suppose c d e. Because d → e = S where S = {a | a d e}, and c ∈ S, then c (d → e).

3 .

 3 c → d = true iff c d. By Proposition 3.2 (2), we know that e (c → d) iff e c d. Let us take e = true. Then, true (c → d ) iff true c d. Therefore, true = (c → d ) iff c d as wanted.

Example 3 . 3 .

 33 A simple example can be obtained by taking d = a → b in Example 2.9, i.e., e = [c ↑ i [a] j ] i [a → b] j . We can use Proposition 3.2 item 1, S.2, and E.1 to obtain e [a b] j . Thus i can send a to j and cause b to be triggered in the space of j.

Definition 3 . 5 (

 35 Normal Maps). Let (Con, ) be a constraint frame. A self-map m on Con is said to be normal if (1) m(true) = true and (2) m(c → d) → (m(c) → m(d)) = true for each c, d ∈ Con. We now prove that the normality requirement is equivalent to the requirement of preserving finite suprema. The next theorem states that Condition (2) in Definition 3.5 is equivalent to the seemingly simpler condition: m(c d) = m(c) m(d).

Theorem 3 . 6 (

 36 Normality & Finite Suprema). Let C be a constraint frame (Con, )

From Proposition 3 . 2 ( 3 )

 323 (c d) → d = true. Since f (true) = true we have f ((c d) → d) = true. We must then have, from Equation 3, f (c d) → f (d) = true as well. Using Proposition 3.2(3) we obtain f (c d) f (d). In a similar fashion, by exchanging c and d in Equation 3, we can obtain f (d c) f (c). We can then conclude f (c d) f (c) f (d) as wanted.

  Using Proposition 3.2 one can verify that c → (d → c d) = true. Since f (true) = true we have f (c → (d → c d)) = true. From Equation 4, we must then have f (c) → f (d → c d) = true and by using Proposition 3.2(3) we conclude f (c) f (d → c d). From the assumption and Proposition 3.2(3)

  and then using Proposition 3.2(2) we obtain f (c) f (d) f (c d) as wanted. • Assume that ∀c, d ∈ Con : f (c d) = f (c) f (d). Take two arbitrary c, d ∈ Con. We shall prove f (c → d) → (f (c) → f (d)) = true. From Proposition 3.2(2-3) it suffices to prove f (c → d) f (c) f (d). Using the the assumption and Proposition 3.2(1) we obtain f

Corollary 3 . 7 .

 37 Let C be a constraint frame (Con, ) and let f be a normal self-map on Con. If c d then f (c) f (d).

  Kripke structures (KS) are a fundamental mathematical tool in logic and computer science. They can be seen as transition systems and they are often used to give semantics to modal logics. A KS M provides a relational structure with a set of states and one or more accessibility relations i -→ M between them: s i -→ M t can be seen as a transition, labelled with i, from s to t in M . Broadly speaking, a model-based Kripke semantics equates each modal formula φ to a certain set φ of pairs (M, s), called pointed KS's,

  to denote the pointed KS reachable through R i from the pointed KS (M, s). The interpretation function π tells us what primitive propositions are true at a given world: p holds at state s iff π(s)(p) = 1. We shall use S M and π M to denote the set of states and interpretation function of M .

Remark 4 . 4 .

 44 The structure K(S n (Φ)) = (Con, , [•] 1 , . . . , [•] n ) is a complete algebraic lattice given by a powerset ordered by reversed inclusion ⊇[START_REF] Knight | The epistemic view of concurrency theory[END_REF]. The LUB (join) is set intersection, the meet is set union, the top element false is the empty set ∅, and bottom true is the set ∆ of all pointed Kripke structures (M, s) with M ∈ S n (Φ).

Tree-like accessibility

  relations where all paths are infinite are determinant-complete (Figure 1.(ii) and Figure 1.(iii)). Also some non-tree like structures such as Figure 1.(i) and Figure 1.(v).Figure 1.(iv) shows a non determinate-complete accessibility relation by taking the transitive closure of Figure 1.(iii).

Notation 4 . 9 .

 49 Recall that i (M, s) = {(M, t) | s i -→ M t} where i -→ M denotesthe accessibility relation of agent i in the KS M . We extend this definition to sets

Figure 1 :

 1 Figure 1: Accessibility relations for an agent i. In each sub-figure we omit the corresponding KS M k from the edges and draw s i -→ t whenever s i -→ M k t.

i

  -→ M . Analogously, we define £ i (M, s) def = {(M, t) | s i M t}. Proposition 4.10. Let s ∈ S M . The state s is determinant w.r.t. i -→ M if and only if for every S ⊆ S M : If i (M, s) ⊆ i (M, S ) then s ∈ S .

Theorem 4 .•

 4 11 (Completeness). Let [•] i be a space function of a Kripke SCS K(S). Then [•] i has a right inverse if and only if for every M ∈ S the accessibility relation i -→ M is determinant-complete. Proof. Suppose that for every M ∈ S, i -→ M is determinant-complete. By the Axiom of Choice, [•] i has a right inverse if [•] i is surjective. Thus, it suffices to show that for every set of pointed KS d, there exists a set of pointed KS c such that [c] i = d. Take an arbitrary d and let c = i (M , S ) where S = {s | (M, s) ∈ d}. From Definition 4.3 we conclude d ⊆ [c] i . It remains to prove d ⊇ [c]. Suppose d ⊇ [c]. Since d ⊆ [c] we have d ⊂ [c]. Then there must be an (M , s ), with M ∈ S, such that (M , s ) ∈ d and (M , s ) ∈ [c]. But if (M , s ) ∈ [c] i then from Definition 4.3 we conclude that i (M , s ) ⊆ c = i (M , S ). Furthermore (M , s ) ∈ d implies s ∈ S . It then follows from Proposition 4.10 that s is not determinant w.r.t. i -→ M . This leads us to a contradiction since i -→ M is supposed to be determinant-complete. • Suppose [•] i has a right inverse. By the Axiom of Choice, [•] i is surjective. We claim that i -→ M is determinant-complete for every M ∈ S. To show this claim let us assume there is M ∈ S such that i -→ M is not determinant-complete. From Proposition 4.10 we should have s ∈ S and S ⊆ S such that i (M , s) ⊆ i (M , S ) and s ∈ S . Since [c ] i is surjective, there must be a set of pointed KS c such that {(M , s ) | s ∈ S } = [c ] i . We can then verify, using Definition 4.3, that i (M, S ) ⊆ c . Since i (M , s) ⊆ i (M , S ) then i (M , s) ⊆ c . It then follows from Definition 4.3 that (M , s) ∈ [c ] i . But [c ] i = {(M , s ) | s ∈ S } then s ∈ S , a contradiction. Henceforth we use M D to denote the class of KS's whose accessibility relations are determinant-complete. It follows from Theorem 4.11 that S = M D is the largest class for which space functions of a Kripke K(S) have right inverses. 4.3. Deriving Maximum Right-Inverse Let K(S) = (Con, , [•] 1 , . . . , [•] n ) be the Kripke SCS. The Axiom of Choice and Theorem 4.11 tell us that each [•] i has a right inverse (extrusion function) if and only if S ⊆ M D . We are interested, however, in explicit constructions of the right inverses. Remark 4.12. Recall, from Remark 4.4, that any Kripke SCS K(S) = (Con, , [•] 1 , . . . , [•] n ) is ordered by reversed inclusion (i.e., = ⊇). Thus, for example, saying that some f is the least function w.r.t. ⊆ satisfying certain conditions is equivalent to saying that f is the maximum function w.r.t. satisfying the same conditions. As usual given two self-maps f and g over Con we define f g iff f (c) g(c) for every c ∈ Con. Since any Kripke SCS space function preserve arbitrary suprema (Proposition 4.5), we can apply Proposition 2.10.2 to obtain the following canonical maximum right-inverse construction. Recall that [c]

  i -→ M . Therefore we know that if there exists s, s withs = s such that s i -→ M t and s i -→ M t. From Corollary 3.7 we know if c ⊆ d then f (c) ⊆ f (d). Then it follows that false ⊆ d and f (false) ⊆ f (d ).Thus, it suffices to prove that (M, t) ∈ f (false). From the assumption that f is a normal right inverse then by Theorem 3.6 it preserves suprema f ({(M, s)} ∩ {(M, s )}) = f ({(M, s)}) ∩ f ({(M, s )}). Since s = s then {(M, s)} ∩ {(M, s )} = ∅. From Lemma 5.3 (1) s i -→ M t and s i -→ M t we know {(M, t)} ⊆ f ({(M, s)}) ∩ f ({(M, s )}). Therefore by Corollary 3.7, {(M, t)} ⊆ f ({(M, s)} ∩ {(M, s )}) which is the same as {(M, t)} ⊆ f (false).

i-→

  M by some s with (M, s) ∈ c. 5.1. Deriving Maximum Normal Right Inverse Lemma 5.3 above tells us what sets should necessarily be included in every f (c) if f is to be both normal and a right inverse of [•] i . It turns out that it is sufficient to include exactly those sets to obtain a normal right inverse of [•] i . In other words Lemma 5.3 gives us a complete set of conditions for normal right inverses. In fact, the least selfmap f w.r.t. ⊆, i.e., the maximum one w.r.t. the lattice order , satisfying Conditions 1,2 and 3 in Lemma 5.3 is indeed a normal right inverse. We shall call such a function the maximum normal right inverse ↑ MN i . Definition 5.4 (Maximum Normal-Right Inverse). Let K(S) = (Con, , [•] 1 , . . . , [•] n ) be a Kripke SCS over S ⊆ M D . We define the maximum normal right inverse for agent i, ↑ MN i as the following self-map on Con:

M

  t and (M, t) ∈ ↑ MN i (c). Therefore by definition of ↑ MN i , (M, s) ∈ c. Now suppose (M, s) ∈ c, then for all states in i (M, s), they are either uniquely determined by s or multiply determined w.r.t. i -→ M , therefore i (M, s) ⊆ ↑ MN i (c), and consequently (M, s) ∈ [↑ MN i (c)] i .

3 .

 3 As s is determinant w.r.t. i -→ M , there exists t s.t. s i M t and (M, t) ∈ ↑ N i (c). Therefore by definition of ↑ N i , (M, s) ∈ c. Now suppose (M, s) ∈ c, then for all states in i (M, s), they are either uniquely determined by s or multiply determined w.r.t. i -→ M , therefore i (M, s) ⊆ ↑ N i (c), and consequently

  4.9). Notice that £ i (M, s) = ∅ since we are assuming that each (M, s) must be determining w.r.t.i -→ M .

Figure 2 :

 2 Figure 2: Accessibility relations corresponding to the KS M for an agent i. Example 5.10. Consider Figure 2 with c = {(M, s 1 ), (M, s 2 )} and d = {(M, s 3 )}.

Figure 3 :

 3 Figure 3: Accessibility relations corresponding to the KS M for an agent i.

i-→

  M , therefore i (M, s) ⊆ ↑ mN i,s (c), and consequently (M, s) ∈ [↑ mN i,s (c)] i by Definition 4.3.

  (w.r.t. ) normal right inverses for the space function [•] i in the sense that there are no normal right inverses below them. More precisely, h is a minimal normal right inverse of [•] i iff h is a normal right inverse of [•] i and there is no other normal right inverse g(•) of [•] i such that g h. Theorem 5.13. Let K(S) = (Con, , [•] 1 , . . . , [•] n ) and ↑ mN i,s as in Definition 5.9. Then ↑ mN i,s is a minimal normal right inverse of [•] i .

i-→

  M . Consequently, using Equation 10 we conclude i (M, s) ⊆ g(c). (11) Since we assumed that g is a right inverse of [•] i we have [g(c)] i = c. We can use Equation 11 and Definition 4.3 to conclude (M, s) ∈ [g(c)] i . Hence (M, s) ∈ c, a contradiction with Equation 9. The above theorem identifies a family of minimal normal right inverses indexed by collections of choice functions. The next theorem tell us that the family is complete in the sense that every normal right inverse is bounded from below by some minimal right inverse ↑ mN i,s . Theorem 5.14. Let K(S) = (Con, , [•] 1 , . . . , [•] n ) as in Definition 5.9. Suppose that g is a normal right inverse of the space function [•] i . Then there exists a minimal normal right inverse ↑ mN i,s as in Definition 5.9 such that ↑ mN i,sg.

  s) since the sets £ i (M, s ) of states uniquely-determined by s are mutually exclusive. Then by way of contradiction suppose (M, s) / ∈ c andg (c) = £ i (M, s). Since g (c) ⊆ g(c) we would have £ i (M, s) ⊆ g(c). From Lemma 5.3(2)and the assumption that g is a normal right inverse, g(c) includes all (M, t) such that t is multiply determined w.r.t. i -→ M . Since £ i (M, s) ⊆ g(c) we then conclude i (M, s) ⊆ g(c). But g is a right inverse of [•] i thus [g(c)] i = c. Using Definition 4.3 we would then conclude (M, s) ∈ [g(c)] i . Hence (M, s) ∈ c, a contradiction with the assumption in Equation

iiA

  The maximum right inverse for the space function [•] i wrt (⊇).↑ M i (c) is the minimum set (wrt ⊆) of pointed Kripke structures such that [↑ M i (c)] i = c. The function ↑ M i is not normal (Definition 3.The maximum normal right inverse of [•] i wrt (⊇). The function↑ MN i is normal and ↑ MN i (c) is the minimum set (wrt ⊆) of pointed Kripke structures such that [↑ MN i (c)] i = c. inverse of [•] i . The function ↑ N i is normal and the set ↑ N i (c) is given by ↑ MN i (c)plus those pointed Kripke structures (M, t) such that t is indetermined w.r.t. minimal normal right inverse of [•] i wrt (⊇). The function ↑ mN i ,s is normal and ↑ mN i ,s (c) is a maximal set (wrt ⊆) of pointed Kripke structures, determined by a choice function sc, such that [↑ MNi (c)] i = c. Definition 5.9.

Definition 6 . 1 (

 61 Modal Language). Let Φ be a set of primitive propositions. The modal language L n (Φ) is given by the following grammar: φ, ψ, . . . := p | φ ∧ ψ | ¬φ | i φ where p ∈ Φ and i ∈ {1, . . . , n}. We shall use the abbreviations φ∨ψ for ¬(¬φ∧¬ψ), φ ⇒ ψ for ¬φ ∨ ψ, φ ⇔ ψ for (φ ⇒ ψ) ∧ (ψ ⇒ φ), the constant false ff for p ∧ ¬p, and the constant tt for ¬ff . We say that a pointed KS (M, s) satisfies φ iff (M, s) |= φ where |= is defined inductively as follows: (M, s) |= p iff π M (s)(p) = 1 (M, s) |= φ ∧ ψ iff (M, s) |= φ and (M, s) |= ψ (M, s) |= ¬φ iff (M, s) |= φ (M, s) |= i φ iff (M, t) |= φ for every t such that s i -→ M t.

6 . 4 .

 64 One can verify that for any Kripke SCS K(S n (Φ)), the Heyting negation ∼ c (Def. 3.1) is ∆ \ c where ∆ is the set of all pointed Kripke structures (M, s) such that M ∈ S n (Φ) (i.e., boolean negation). Similarly, Heyting implication c → d is equivalent to (∼ c) ∪ d (i.e., boolean implication).

Figure 4 :

 4 Figure 4: Accessibility relations for an agent i. In each sub-figure we omit the corresponding KS M k from the edges and draw s i -→ t whenever s i -→ M k t.

1 -→ 2 -→ M is the reflexive and transitive closure of 1 -→ M . The relation 1 - 1 -

 12111 M is isomorphic to the successor relation on the natural numbers and → M is intended to capture the linear flow of time. Intuitively, s 1 -→ M t means that the state t is the only next state for s. Similarly, s 2 -→ M t, with s = t, is intended to capture the fact that t is one of the infinitely many future states for s.Let us first consider the modality 1 to be the next operator 1 = . Notice that the accessibility relation → M is determinant-complete, because this is isomorphic to the successor relation, therefore every state is uniquely determining its successor, and by Theorem 4.11 there exists a right inverse of [•] i . If we apply Equation 16 taking as the inverse ↑ 1 = ↑ M 1 , i.e., the maximum right inverse of [•] 1

1 -→ 2 - 1 -→ M s 1 1 - 2 -→ M s j we also have s 0 2 -

 121122 M then (M, s) |= φ and (M, s) |= φ for any φ. It follows that is not a normal operator, since tt is not valid in S 2 (Φ) but tt is. Now consider the modality 2 to be the always operator 2 = P. Notice that the accessibility relation → M is not determinant-complete because there are not determinant states in the structure. Take any increasing chain s 0 → M . . . Then, state s 1 is not determinant because for every s j such that s 1 → M s j . Theorem 4.11 tell us that there is no right inverse ↑ 2 of [•] i that can give us an operator -1 2 satisfying Equation

  MN i (d). If such state does not exist, then t is multiply determined w.r.t. We now proceed with the proof. * ↑ MN i

	). We first prove monotonicity (i.e. if c ⊆ d
	then ↑ MN i (c) ⊆ ↑ MN i (d)). For this, suppose c ⊆ d. If (M, t) ∈ ↑ MN i (c) then
	by definition of ↑ MN i t is determined w.r.t.
	i -→ M and
	consequently (M, t) ∈ ↑ MN i (d).

i -→ M . If there exists a state s with (M, s) ∈ c s.t. s i M t then (M, s) ∈ d, thus (M, t) ∈ ↑

  If there exists s s.t. s i M t, then (M, s) ∈ c and (M, s) ∈ d. Now suppose there exists such s, therefore (M, s) ∈ c ∩ d and (M, t) ∈ ↑ N i (c ∩ d).If this is not the case, then t is not determined w.r.t.

i

-→ M by any other state, hence

  s) and (M, t) ∈ g (d). Since (M, s) ∈ d we have (M, t) ∈

	(M,s) / ∈d £ i (M, s). But (M, t) ∈ g (d), and we must have (M, t) / ∈ g(d). Since g is
	normal it is monotone (Corollary 3.7), consequently c ⊆ d and (M, t) / ∈ g(d) implies
	(M, t) / ∈ g(c). (M, t) / ∈ g (c). It follows that (M, t) ∈ £ i (M, s) \ g (c) as
	wanted.

Logical (boolean) implication is a particular instance of Heyting implication[START_REF] Vickers | Topology via logic[END_REF].

$ This work has been partially supported by the Colciencias project 125171250031 CLASSIC, STIC Am-Sud