Keywords

1 Introduction

Constraint systems (cs’s) provide the basic domains and operations for the semantic foundations of several declarative models and process calculi from concurrent constraint programming (ccp) [3, 8, 9, 11, 15, 18, 23, 25]. In these calculi, processes can be thought of as both concurrent computational entities and logic specifications (e.g., process composition can be seen as parallel execution and conjunction). All ccp process calculi are parametric in a cs that specifies partial information upon which programs (processes) may act.

A cs is often represented as a complete algebraic lattice (Con, \(\sqsubseteq \)). The elements of Con, the constraints, represent partial information and we shall think of them as being assertions. The intended meaning of \(c \sqsubseteq d\) is that d specifies at least as much information as c (i.e., d entails c). The join operation \(\sqcup \), the bottom \({\textit{true}}\) and the top \({\textit{false}}\) of the lattice (Con, \(\sqsubseteq \)) correspond to conjunction, the empty information and the join of all information, respectively. 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, and existential quantification and local variables correspond to a cylindrification operation on the set of constraints [25].

Similarly, the notion of computational space and the epistemic notion of belief in the sccp process calculi [15] correspond to a family of functions \({\varvec{[}}{\cdot }{\varvec{]}}_i:\,\,\) Con \(\rightarrow \) Con on the elements of the constraint system Con that preserve finite suprema. 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 the assertion (constraint) \({\varvec{[}}{c}{\varvec{]}}_i\) specifies that c resides within the space of agent i. From an epistemic point of view, the assertion \({\varvec{[}}{c}{\varvec{]}}_i\) specifies that agent i considers c to be true (i.e. that in the world of agent i the assertion c is true). Both intuitions convey the idea of c being local to agent i.

The Extrusion Problem. Given a space function \({\varvec{[}}{\cdot }{\varvec{]}}_i\), the extrusion problem consists in finding/constructing a right inverse of \({\varvec{[}}{\cdot }{\varvec{]}}_i\), called extrusion function, satisfying some basic requirements (e.g., preservation of finite suprema). By right inverse of \({\varvec{[}}{\cdot }{\varvec{]}}_i\) we mean a function \({\uparrow }{}{_i}:\,\,\) Con \(\rightarrow \) Con such that \({\varvec{[}}{{\uparrow }{}{_i c}}{\varvec{]}}_i = c\). From a computational point of view, the intended meaning of \({\varvec{[}}{{\uparrow }{}{_i c}}{\varvec{]}}_i = c\) is that within a space context \({\varvec{[}}{\cdot }{\varvec{]}}_i\), \({\uparrow }{}{_i c}\) extrudes c from agent i’s space. From an epistemic point of view, we can use \({\varvec{[}}{{\uparrow }{}{_i c}}{\varvec{]}}_i \) to express utterances by agent i, i.e., to specify that agent i wishes to say c to the outside world. One can then think of extrusion/utterance as the right inverse of space/belief.

Modal logics [21] extend classical logic to include operators 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. Some modal logics have been extended with inverse modalities to specify, for example, past tense assertions in temporal logic [24], utterances in epistemic logic [13], and backward moves in modal logic for concurrency [19], among others. Although the notion of spatial constraint system is intended to give an algebraic account of spatial and epistemic assertions, we shall show that it is sufficiently robust to give an algebraic account of more general modal assertions.

Contributions. We shall study the extrusion problem for a meaningful family of scs’s that can be used as semantic structures for modal logics. These scs’s are called Kripke spatial constraint systems because its elements are Kripke structures. We shall show that the extrusion functions of Kripke scs’s, i.e. the right inverses of the space functions, correspond to right inverse modalities in modal logic. We shall derive a complete characterization for the existence of right inverses of space functions: The weakest restriction on the elements of Kripke scs’s that guarantees the existence of right inverses. We shall also give an algebraic characterization of the modal logic notion of normality as maps that preserve finite suprema. We then give a complete characterization and derivations of extrusion functions that are normal (and thus they correspond to normal inverse modalities). Finally, we use the above-mentioned contributions to the problem of whether a given modal language can be extended with right inverse operators. We discuss the implications of our results for specific modal languages and modal concepts such the minimal modal logic \(K_n\) [10], Hennessy-Milner logic [14], a modal logic of linear-time [20], and bisimulation.

2 Background: Spatial Constraint Systems

In this section we recall the notion of basic constraint system [3] and the more recent notion of spatial constraint system [15]. We presuppose basic knowledge of order theory and modal logic [1, 2, 10, 21].

The concurrent constraint programming model of computation [25] 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. This information is represented as assertions traditionally referred to as constraints.

Constraint systems can be formalized as complete algebraic lattices [3]Footnote 1. The elements of the lattice, the constraints, represent (partial) information. A constraint c can be viewed as an assertion (or a proposition). The lattice order \(\sqsubseteq \) is meant to capture entailment of information: \(c \sqsubseteq d\), alternatively written \(d \sqsupseteq c\), means that the assertion d represents as much information as c. Thus we may think of \(c \sqsubseteq d\) as saying that d entails c or that c can be derived from d. The least upper bound (lub) operator \(\sqcup \) represents join of information; \(c \ \sqcup \ d\), the least element in the underlying lattice above c and d. Thus \(c \ \sqcup \ 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 \({\textit{false}}\). The bottom element \({\textit{true}}\) represents the empty information.

Definition 1

(Constraint Systems [3]). A constraint system (cs) \(\mathbf {C}\) is a complete algebraic lattice (Con, \(\sqsubseteq \)). The elements of Con are called constraints. The symbols \(\sqcup \), \({\textit{true}}\) and \({\textit{false}}\) will be used to denote the least upper bound (lub) operation, the bottom, and the top element of \(\mathbf {C},\) respectively.

We shall use the following notions and notations from order theory.

Notation 1 (Lattices)

Let \(\mathbf {C}\) be a partially ordered set (poset) (Con, \(\sqsubseteq \)). We shall use \(\bigsqcup S\) to denote the least upper bound (lub) (or supremum or join) of the elements in S, and is the greatest lower bound (glb) (infimum or meet) of the elements in S. We say that \(\mathbf {C}\) is a complete lattice iff each subset of Con has a supremum and an infimum in Con. A non-empty set \(S \subseteq \) Con is directed iff every finite subset of S has an upper bound in S. Also \(c\in \) Con is compact iff for any directed subset D of Con, \(c \sqsubseteq \bigsqcup D\) implies \(c \sqsubseteq d\) for some \(d\in D\). A complete lattice \(\mathbf C\) is said to be algebraic iff for each \(c \in \) 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 \(\rightarrow \) Con. Let (Con, \(\sqsubseteq \)) be a complete lattice. The self-map f on Con preserves the supremum of a set \(S \subseteq \) Con iff \(f(\bigsqcup S) = \bigsqcup \{ f(c)\mid c \in S \}\). The preservation of the infimum of a set is defined analogously. We say f preserves finite/infinite suprema iff it preserves the supremum of arbitrary finite/infinite sets. Preservation of finite/infinite infima is defined similarly.

Spatial Constraint Systems. The authors of [15] extended the notion of cs to account for distributed and multi-agent scenarios where agents have their own space for local information and for performing their computations.

Intuitively, each agent i has a space function \({\varvec{[}}{\cdot }{\varvec{]}}_i\) from constraints to constraints. Recall that constraints can be viewed as assertions. We can then think of \( {\varvec{[}}{c}{\varvec{]}}_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 \({\varvec{[}}{c}{\varvec{]}}_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, \({\varvec{[}}{{\varvec{[}}{c}{\varvec{]}}_j}{\varvec{]}}_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 \( {\varvec{[}}{c}{\varvec{]}}_i \ \sqcup \ {\varvec{[}}{d}{\varvec{]}}_j \) as an assertion specifying that c and d hold within two parallel/neighboring spaces that belong to agents i and j, respectively. From a computational/ concurrency point of view, we think of \(\sqcup \) as parallel composition. As mentioned before, from a logic point of view the join of information \(\sqcup \) corresponds to conjunction.

Definition 2

(Spatial Constraint System [15]). An n-agent spatial constraint system (n-scs) \(\mathbf {C}\) is a cs \((\textit{Con}, \sqsubseteq )\) equipped with n self-maps \({\varvec{[}}{\cdot }{\varvec{]}}_1,\ldots ,{\varvec{[}}{\cdot }{\varvec{]}}_n\) over its set of constraints \({{\textit{Con}}}\) such that: (S.1) \({\varvec{[}}{{\textit{true}}}{\varvec{]}}_i = {\textit{true}},\) and (S.2) \({\varvec{[}}{c \ \sqcup \ d}{\varvec{]}}_i = {\varvec{[}}{c}{\varvec{]}}_i \ \sqcup \ {\varvec{[}}{d}{\varvec{]}}_i \ \ \text { for each } c,d \in {\textit{Con}}.\)

Axiom S.1 requires space functions to be strict maps (i.e. bottom preserving). Intuitively, it states that having an empty local space amounts to nothing. Axiom S.2 states that the information in a given space can be distributed. Notice that requiring S.1 and S.2 is equivalent to requiring that each \({\varvec{[}}{\cdot }{\varvec{]}}_i\) preserves finite suprema. Also S.2 implies that each \({\varvec{[}}{\cdot }{\varvec{]}}_i\) is monotonic: I.e., if \(c \sqsupseteq d\) then \({\varvec{[}}{c}{\varvec{]}}_i \sqsupseteq {\varvec{[}}{d}{\varvec{]}}_i.\)

Extrusion and utterance. We can also equip each agent i with an extrusion function \({\uparrow }{}{_i }:{\textit{Con}}\rightarrow {\textit{Con}}\). Intuitively, within a space context \({\varvec{[}}{\cdot }{\varvec{]}}_i\), the assertion \({\uparrow }{}{_i c}\) specifies that c must be posted outside of (or extruded from) agent i’s space. This is captured by requiring the extrusion axiom \( {\varvec{[}}{\ {\uparrow }{}{_i c}\ }{\varvec{]}}_i = c. \) 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 3 (Extrusion)

Given an n-scs \(({{\textit{Con}}},\sqsubseteq ,{\varvec{[}}{\cdot }{\varvec{]}}_1,\ldots ,{\varvec{[}}{\cdot }{\varvec{]}}_n)\), we say that \({\uparrow }{}{_i}\) is extrusion function for the space \({\varvec{[}}{\cdot }{\varvec{]}}_i\) iff \({\uparrow }{}{_i}\) is a right inverse of \({\varvec{[}}{\cdot }{\varvec{]}}_i\), i.e., iff \( {\varvec{[}}{\ {\uparrow }{}{_i c}\ }{\varvec{]}}_i = c. \)

From the above definitions it follows that \({\varvec{[}}{c \sqcup {\uparrow }{}{_i d}}{\varvec{]}}_i = {\varvec{[}}{c }{\varvec{]}}_i \sqcup d.\) 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\sqcup d = {\textit{false}}\), we can see the utterance as an intentional lie by agent i: The agent i utters an assertion inconsistent with their own beliefs.

The Extrusion/Right Inverse Problem. A legitimate question is: Given space \({\varvec{[}}{\cdot }{\varvec{]}}_i\) can we derive an extrusion function \({\uparrow }{}{_i}\) for it? From set theory we know that there is an extrusion function (i.e., a right inverse) \({\uparrow }{}{_i}\) for \({\varvec{[}}{\cdot }{\varvec{]}}_i\) iff \({\varvec{[}}{\cdot }{\varvec{]}}_i\) is surjective. Recall that the pre-image of \(y \in Y\) under \(f : X \rightarrow Y\) is the set \(f^{-1}(y) = \{ x \in X \mid y = f(x) \}\). Thus the extrusion \({\uparrow }{}{_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 \({\varvec{[}}{\cdot }{\varvec{]}}_i.\)

The existence of the above-mentioned choice function assumes the Axiom of Choice. The next proposition from [13] gives some constructive extrusion functions. It also identifies a distinctive property of space functions for which a right inverse exists.

Proposition 1

Let \({\varvec{[}}{\cdot }{\varvec{]}}_i\) be a space function of scs. Then

  1. 1.

    If \({\varvec{[}}{{\textit{false}}}{\varvec{]}}_i\ne {\textit{false}}\) then \({\varvec{[}}{\cdot }{\varvec{]}}_i\) does not have any right inverse.

  2. 2.

    If \({\varvec{[}}{\cdot }{\varvec{]}}_i\) is surjective and preserves arbitrary suprema then \({\uparrow }{}{_i}: c \mapsto \bigsqcup {\varvec{[}}{c}{\varvec{]}}_i^{-1}\) is a right inverse of \({\varvec{[}}{\cdot }{\varvec{]}}_i\) and preserve arbitrary infima.

  3. 3.

    If \({\varvec{[}}{\cdot }{\varvec{]}}_i\) is surjective and preserves arbitrary infima then \({\uparrow }{}{_i}: c \mapsto \sqcap {\varvec{[}}{c}{\varvec{]}}_i^{-1}\) is a right inverse of \({\varvec{[}}{\cdot }{\varvec{]}}_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 Sect. 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 1 can be used as a test for the non-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 to point out that the derived extrusion \({\uparrow }{}{_i}\) in Property (3), preserves arbitrary suprema, this implies \({\uparrow }{}{_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.

3 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 [26] 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 those maps that preserve 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 \rightarrow d\) in our setting corresponds to the weakest constraint one needs to join c with to derive d: i.e., the greatest lower bound \(\sqcap \{ e \mid e \ \sqcup \ c \sqsupseteq d \}.\) Similarly, the negation of a constraint c, written \(\thicksim \! c\), can be seen as the weakest constraint inconsistent with c, i.e., the greatest lower bound \(\sqcap \{ e \mid e \ \sqcup \ c \sqsupseteq {\textit{false}} \} = c \rightarrow {\textit{false}}.\)

Definition 4 (Constraint Frames)

A constraint system \(({\textit{Con}}, \sqsubseteq )\) is said to be a constraint frame iff its joins distribute over arbitrary meets: More precisely, \(c \ \sqcup \ \sqcap S = \sqcap \{ c \ \sqcup \ e \mid e \in S\}\) for every \(c \in {\textit{Con}}\) and \(S \subseteq {\textit{Con}}\). Given a constraint frame \(({\textit{Con}}, \sqsubseteq )\) and \(c,d \in {\textit{Con}}\), define Heyting implication \(c \rightarrow d\) as \(\sqcap \{ e \in {\textit{Con}}\mid c \ \sqcup \ e \sqsupseteq d \}\) and Heyting negation \(\thicksim \! c\) as \(c \rightarrow {\textit{false}}.\)

The following basic properties of Heyting implication are immediate consequences of the above definitions.

Proposition 2

Let \(({\textit{Con}}, \sqsubseteq )\) be a constraint frame. For every \(c,d,e \in {\textit{Con}}\) we have: (1) \(c \sqcup (c \rightarrow d) = c \sqcup d\), (2) \(c \sqsupseteq (d \rightarrow e)\) iff \(c \sqcup d \sqsupseteq e\), and (3) \(c \rightarrow d = {\textit{true}}\) iff \(c \sqsupseteq d.\)

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\((\phi )\) is a theorem (i.e., true in all models for the underlying modal language) whenever the formula \(\phi \) is a theorem, and (2) the implication formula m(\(\phi \Rightarrow \psi \)) \(\Rightarrow \) (m(\(\phi \)) \(\Rightarrow \) m(\(\psi \))) 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, we can express the normality condition in constraint frames as follows.

Definition 5 (Normal Maps)

Let \(({\textit{Con}}, \sqsubseteq )\) be a constraint frame. A self-map m on \({\textit{Con}}\) is said to be normal if (1) \(m({\textit{true}})={\textit{true}}\) and (2) \(m(c \rightarrow d) \rightarrow (m (c) \rightarrow m(d)) = {\textit{true}}\) for each \(c,d \in {\textit{Con}}.\)

We now prove that the normality requirement is equivalent to the requirement of preserving finite suprema. The next theorem basically states that Condition (2) in Definition 5 is equivalent to the seemingly simpler condition: \(m(c \sqcup d) = m (c) \sqcup m(d).\)

Theorem 1 (Normality & Finite Suprema)

Let \(\mathbf {C}\) be a constraint frame \(({\textit{Con}}, \sqsubseteq )\) and let f be a self-map on \({\textit{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, \(\forall c,d \in {\textit{Con}}:f{\varvec{(}}{c \rightarrow d}{\varvec{)}} \rightarrow (f{\varvec{(}}{c}{\varvec{)}} \rightarrow f{\varvec{(}}{d}{\varvec{)}})={\textit{true}}\) iff \(\forall c,d\in {\textit{Con}}:\) \(f(c \sqcup d)=f(c) \sqcup f(d)\). (Both conditions require f to be bottom preserving, i.e., \(f({\textit{true}})={\textit{true}}\), and preservation of non-empty finite suprema is equivalent to the preservation of binary suprema.) Here we show the only-if direction (the other direction is simpler).

Assume that \(\forall c,d\in {\textit{Con}}:f(c \rightarrow d) \rightarrow (f{(c)} \rightarrow f{(d)})={\textit{true}}\). Take two arbitrary \(c,d\in {\textit{Con}}.\) We first prove \(f({c}\sqcup {d}) \sqsupseteq f({c})\sqcup (d)\). From the assumption and Proposition 2(3) we obtain

$$\begin{aligned} f{\varvec{(}}{(c \sqcup d) \rightarrow d}{\varvec{)}} \sqsupseteq f{\varvec{(}}{c \sqcup d}{\varvec{)}} \rightarrow f{\varvec{(}}{d}{\varvec{)}}. \end{aligned}$$
(1)

From Proposition 2(3) \((c \sqcup d) \rightarrow d = {\textit{true}}.\) Since \(f({\textit{true}})={\textit{true}}\) we have \(f{\varvec{(}}{(c \sqcup d) \rightarrow d}{\varvec{)}} = {\textit{true}}.\) We must then have, from Eq. 1, \(f{\varvec{(}}{c \sqcup d}{\varvec{)}} \rightarrow f{\varvec{(}}{d}{\varvec{)}} = {\textit{true}}\) as well. Using Proposition 2(3) we obtain \(f({c \sqcup d}) \sqsupseteq f(d).\) In a similar fashion, by exchanging c and d in Eq. 1, we can obtain \(f{\varvec{(}}{d \sqcup c}{\varvec{)}} \sqsupseteq f{\varvec{(}}{c}{\varvec{)}}.\) We can then conclude \(f{\varvec{(}}{c \ \sqcup \ d}{\varvec{)}} \sqsupseteq f{\varvec{(}}{c}{\varvec{)}} \ \sqcup \ f{\varvec{(}}{d}{\varvec{)}}\) as wanted.

We now prove \(f{\varvec{(}}{c}{\varvec{)}} \ \sqcup \ f{\varvec{(}}{d}{\varvec{)}} \sqsupseteq f{\varvec{(}}{c \ \sqcup \ d}{\varvec{)}}\). From the assumption and Proposition 2(3) we have

$$\begin{aligned} f{\varvec{(}}{c \rightarrow (d \rightarrow c \sqcup d)}{\varvec{)}} \sqsupseteq f{\varvec{(}}{c}{\varvec{)}} \rightarrow f{\varvec{(}}{d \rightarrow c \sqcup d}{\varvec{)}}. \end{aligned}$$
(2)

Using Proposition 2 one can verify that \(c \rightarrow (d \rightarrow c \sqcup d) = {\textit{true}}.\) Since \(f{\varvec{(}}{{\textit{true}}}{\varvec{)}} = {\textit{true}}\) then \(f{\varvec{(}}{c \rightarrow (d \rightarrow c \sqcup d)}{\varvec{)}} = {\textit{true}}.\) From Eq. 2, we must then have \(f{\varvec{(}}{c}{\varvec{)}} \rightarrow f{\varvec{(}}{d \rightarrow c \sqcup d}{\varvec{)}} = {\textit{true}}\) and by using Proposition 2(3) we conclude \(f{\varvec{(}}{c}{\varvec{)}} \sqsupseteq f{\varvec{(}}{d \rightarrow c \sqcup d}{\varvec{)}}.\) From the assumption and Proposition 2(3) \(f{\varvec{(}}{d \rightarrow c \sqcup d}{\varvec{)}} \sqsupseteq f{\varvec{(}}{d}{\varvec{)}} \rightarrow f{\varvec{(}}{c \sqcup d}{\varvec{)}}\). We then have \(f{\varvec{(}}{c}{\varvec{)}} \sqsupseteq f{\varvec{(}}{d \rightarrow c \sqcup d}{\varvec{)}} \sqsupseteq f{\varvec{(}}{d}{\varvec{)}} \rightarrow f{\varvec{(}}{c \sqcup d}{\varvec{)}}.\) Thus \(f{\varvec{(}}{c}{\varvec{)}} \sqsupseteq f{\varvec{(}}{d}{\varvec{)}} \rightarrow f{\varvec{(}}{c \sqcup d}{\varvec{)}}\) and then using Proposition 2(2) we obtain \(f{\varvec{(}}{c}{\varvec{)}} \sqcup f{\varvec{(}}{d}{\varvec{)}} \sqsupseteq f{\varvec{(}}{c \sqcup d}{\varvec{)}}\) as wanted.   \(\square \)

By applying the above theorem, we can conclude that space functions from constraint frames are indeed normal self-maps, since they preserve finite suprema.

4 Extrusion Problem for Kripke Constraint Systems

This is the main and more technical part of the paper. Here we will study the extrusion/right inverse problem for a meaningful family of spatial constraint systems (scs’s); 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 Kripke scs’s under which extrusion functions may exist. To illustrate the importance of this study it is convenient to give some intuition first.

Kripke structures (KS) [16] are a fundamental mathematical tool in logic and computer science. They can be seen as transition systems and they are 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 \(\overset{i}{\longrightarrow }_{M}\) between them: \(s \overset{i}{\longrightarrow }_{M} t\) can be seen as a transition, labelled with i, from s to t in M. Broadly speaking, the Kripke semantics interprets each modal formula \(\phi \) as a certain set \(\llbracket \phi \rrbracket \) of pairs (M, s), called pointed KS’s, where s is a state of the KS M. In modal logics with one or more modal (box) operators \(\square _i\), the formula \(\square _i \phi \) is interpreted as \(\llbracket \square _i \phi \rrbracket = \{(M,s) \ | \ \forall t: s\overset{i}{\longrightarrow }_{M}t, (M,t) \in \llbracket \phi \rrbracket \}.\)

Analogously, in a Kripke scs each constraint c is equated to a set of pairs (M, s) of pointed KS. Furthermore, we have \({\varvec{[}}{c}{\varvec{]}}_i = \{ (M,s) \ | \ \forall t: s\overset{i}{\longrightarrow }_{M}t, (M,t) \in c\}\). This means that formulae can be interpreted as constraints and in particular \(\square _i\) can be interpreted by \({\varvec{[}}{\cdot }{\varvec{]}}_i\) as \(\llbracket \square _i \phi \rrbracket = {\varvec{[}}{\ \llbracket \phi \rrbracket \ }{\varvec{]}}_i.\)

Inverse modalities \(\square _i^{-1}\), also known as reverse modalities, are used in many modal logics. In tense logics they represent past operators [22] and in epistemic logic they represent utterances [13]. The basic property of a (right) inverse modality is given by the axiom \(\square _i(\square _i^{-1} \phi ) \Leftrightarrow \phi .\) 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 \({\uparrow }{}{_i}\) for \({\varvec{[}}{\cdot }{\varvec{]}}_i\) we can provide the semantics for inverse modalities \(\square _i^{-1}\) by letting \(\llbracket \square _i^{-1} \phi \rrbracket = {\uparrow }{}{_i(\ \llbracket \phi \rrbracket \ ) }\). We then have \(\llbracket \square _i(\square _i^{-1} \phi ) \rrbracket = \llbracket \phi \rrbracket \) thus validating the axiom \(\square _i(\square _i^{-1} \phi ) \Leftrightarrow \phi .\) This illustrates the relevance of deriving extrusion functions and establishing the weakest conditions under which they exist. Furthermore, the algebraic structure of Kripke scs may help us stating derived properties of the reverse modality such as that of being normal (Definition 5).

4.1 KS and Kripke SCS

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

Definition 6 (Kripke Structures)

An n-agent Kripke Structure (KS) M over a set of atomic propositions \(\varPhi \) is a tuple \((S, \pi , \mathcal {R}_1, \ldots , \mathcal {R}_n)\) where S is a nonempty set of states, \(\pi :S \rightarrow (\varPhi \rightarrow \{0,1\}) \) is an interpretation associating with each state a truth assignment to the primitive propositions in \(\varPhi \), and \(\mathcal {R}_i\) is a binary relation on S. A pointed KS is a pair (M, s) where M is a KS and s is a state of M.

We shall use the following notation in the rest of the paper.

Notation 2

Each \(\mathcal {R}_i\) is referred to as the accessibility relation for agent i. We shall use \(\overset{i}{\longrightarrow }_{M}\) to refer to the accessibility relation of agent i in M. We write \(s \overset{i}{\longrightarrow }_{M} t\) to denote \((s,t) \in \mathcal {R}_i.\) We use \(\rhd _i(M,s) = \{ (M,t) \mid s \overset{i}{\longrightarrow }_{M} t \}\) to denote the pointed KS reachable from the pointed KS (M, s). The interpretation function \(\pi \) tells us what primitive propositions are true at a given state: p holds at state s iff \(\pi (s)(p)=1\). We shall use \(S_M\) and \(\pi _M\) to denote the set of states and interpretation function of M.

We now define the Kripke scs wrt a set \(\mathcal {S}_n(\varPhi )\) of pointed KS.

Definition 7

(Kripke Spatial Constraint Systems [15]). Let \(\mathcal {S}_n(\varPhi )\) be a non-empty set of n-agent Kripke structures over a set of primitive propositions \(\varPhi \) and let \(\varDelta \) be the set of all pointed Kripke structures (M, s) such that \(M \in { \mathcal {S}_n(\varPhi ) }.\) We define the Kripke n-scs for \(\mathcal {S}_n(\varPhi )\) as \(\mathbf{K}(\mathcal {S}_n(\varPhi )) = ({{\textit{Con}}},\sqsubseteq ,{\varvec{[}}{\cdot }{\varvec{]}}_1,\ldots ,{\varvec{[}}{\cdot }{\varvec{]}}_n)\) where \({\textit{Con}}= \mathcal {P}(\varDelta )\), \( \sqsubseteq \ = \ \supseteq \), and

$$\begin{aligned} {\varvec{[}}{c}{\varvec{]}}_i \mathop {=}\limits ^{\texttt {def} }\{(M,s) \in \varDelta \mid \rhd _i(M,s) \subseteq c \}. \end{aligned}$$
(3)

The structure \(\mathbf{K}(\mathcal {S}_n(\varPhi )) = ({{\textit{Con}}},\sqsubseteq ,{\varvec{[}}{\cdot }{\varvec{]}}_1,\ldots ,{\varvec{[}}{\cdot }{\varvec{]}}_n)\) is a complete algebraic lattice given by a powerset ordered by reversed inclusion \(\supseteq \). The join \( \ \sqcup \ \) is set intersection, the meet \(\sqcap \) is set union, the top element \({\textit{false}}\) is the empty set \(\emptyset \), and bottom \({\textit{true}}\) is the set \(\varDelta \) of all pointed Kripke structures (M, s) with \(M \in { \mathcal {S}_n(\varPhi ) }\). Notice that \(\mathbf{K}(\mathcal {S}_n(\varPhi ))\) is a frame since meets are unions and joins are intersections so the distributive requirement is satisfied. Furthermore, each \({\varvec{[}}{\cdot }{\varvec{]}}_i\) preserves arbitrary suprema (intersection) and thus, from Theorem 1 it is a normal self-map.

Proposition 3

Let \(\mathbf{K}(\mathcal {S}_n(\varPhi )) = ({{\textit{Con}}},\sqsubseteq ,{\varvec{[}}{\cdot }{\varvec{]}}_1,\ldots ,{\varvec{[}}{\cdot }{\varvec{]}}_n)\) as in Definition 7. Then (1) \(\mathbf{K}(\mathcal {S}_n(\varPhi ))\) is a spatial constraint frame and (2) each \({\varvec{[}}{\cdot }{\varvec{]}}_i\) preserves arbitrary suprema.

4.2 Existence of Right Inverses

We shall 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 \({\uparrow }{}{}_i\) given the space \({\varvec{[}}{\cdot }{\varvec{]}}_i\). We shall also give explicit right inverse constructions.

Notation 3

For notational convenience, we take the set \(\varPhi \) of primitive propositions and n to be fixed from now on and omit them from the notation. E.g., we write \(\mathcal {M}\) instead of \(\mathcal {M}_n(\varPhi ).\)

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.

Definition 8 (Determinacy and Unique-Determinacy)

Let S and \(\mathcal {R}\) be the set of states and an accessibility relation of a KS M, respectively. Given \(s,t \in S\), we say that s determines t wrt \(\mathcal {R}\) if \((s,t) \in \mathcal {R}\). We say that s uniquely determines t wrt \(\mathcal {R}\) if s is the only state in S that determines t wrt \(\mathcal {R}\). A state \(s \in S\) is said to be determinant wrt \(\mathcal {R}\) if it uniquely determines some state in S wrt \(\mathcal {R}\). Furthermore, \(\mathcal {R}\) is determinant-complete if every state in S is determinant wrt \(\mathcal {R}\).

Fig. 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 \overset{i}{\longrightarrow }_{} t\) whenever \(s \overset{i}{\longrightarrow }_{M_k} t\).

Full size image

Example 1

Figure 1 illustrates some typical determinant-complete accessibility relations for agent i. Notice that any determinant-complete relation \(\overset{i}{\longrightarrow }_{M}\) is necessarily serial (or left-total): i.e., For every \(s \in S_M\), there exists \(t \in S_M\) such that \(s\overset{i}{\longrightarrow }_{M}t\). Tree-like accessibility relations where all paths are infinite are determinant-complete (Fig. 1(ii) and (iii)). Also some non-tree like structures such as Fig. 1(i) and (v). Figure 1(iv) shows a non determinate-complete accessibility relation by taking the transitive closure of Fig. 1(iii).

We need to introduce some notation.

Notation 4

Recall that where denotes the accessibility relation of agent i in the KS M. We extend this definition to sets of states as follows Furthermore, we shall write to mean that s uniquely determines t wrt \(\overset{i}{\longrightarrow }_{M}\).

The following proposition gives an alternative definition of determinant states.

Proposition 4

Let \(s \in S_M\). The state s is determinant wrt \(\overset{i}{\longrightarrow }_{M}\) if and only if for every \(S' \subseteq S_M\): If \(\rhd _i(M,s)\subseteq \rhd _i(M,S')\) then \(s \in S'.\)

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

Theorem 2 (Completeness)

Let \({\varvec{[}}{\cdot }{\varvec{]}}_i\) be a spatial function of a Kripke scs \(\mathbf{K}(\mathcal {S}).\) Then \({\varvec{[}}{\cdot }{\varvec{]}}_i\) has a right inverse if and only if for every \(M \in \mathcal {S}\) the accessibility relation \(\overset{i}{\longrightarrow }_{M}\) is determinant-complete.

Proof

  • Suppose that for every \(M \in \mathcal {S}\), \(\overset{i}{\longrightarrow }_{M}\) is determinant-complete. By the Axiom of Choice, \({\varvec{[}}{\cdot }{\varvec{]}}_i\) has a right inverse if \({\varvec{[}}{\cdot }{\varvec{]}}_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 \({\varvec{[}}{c}{\varvec{]}}_i = d\). Take an arbitrary d and let \(c =\,\rhd _i(M',S')\) where \(S' = \{ s \ | \ (M,s) \in d \}\). From Definition 7 we conclude \(d \subseteq {\varvec{[}}{c}{\varvec{]}}_i\). It remains to prove \(d \supseteq [ c ]\). Suppose \(d\not \supseteq {\varvec{[}}{c}{\varvec{]}}\). Since \(d \subseteq {\varvec{[}}{c}{\varvec{]}}\) we have \(d \subset {\varvec{[}}{c}{\varvec{]}}.\) Then there must be a \((M',s')\), with \(M' \in \mathcal {S}\), such that \((M',s')\not \in d\) and \((M',s') \in {\varvec{[}}{c}{\varvec{]}}.\) But if \((M',s') \in {\varvec{[}}{c}{\varvec{]}}_i\) then from Definition 7 we conclude that \( \rhd _i(M',s') \subseteq c = \rhd _i(M',S')\). Furthermore \((M',s')\not \in d\) implies \(s' \not \in S'.\) It then follows from Proposition 4 that \(s'\) is not determinant wrt \(\overset{i}{\longrightarrow }_{M'}\). This leads us to a contradiction since \(\overset{i}{\longrightarrow }_{M'}\) is supposed to be determinant-complete.

  • Suppose \({\varvec{[}}{\cdot }{\varvec{]}}_i\) has a right inverse. By the Axiom of Choice, \({\varvec{[}}{\cdot }{\varvec{]}}_i\) is surjective. We claim that \(\overset{i}{\longrightarrow }_{M}\) is determinant-complete for every \(M \in \mathcal {S}\). To show this claim let us assume that there is \(M' \in \mathcal {S}\) such that \(\overset{i}{\longrightarrow }_{M}\) is not determinant-complete. From Proposition 4 we should have \(s \in S\) and \(S'\subseteq S\) such that \(\rhd _i(M',s)\subseteq \rhd _i(M',S')\) and \(s \not \in S'.\) Since \({\varvec{[}}{c'}{\varvec{]}}_i\) is surjective there must be a set of pointed KS \(c'\) such that \(\{ (M',s') \ | \ s'\in S' \}={\varvec{[}}{c'}{\varvec{]}}_i.\) We can then verify, using Definition 7, that \(\rhd _i(M,S') \subseteq c' \). Since \(\rhd _i(M',s)\subseteq \rhd _i(M',S')\) then \(\rhd _i(M',s) \subseteq c'.\) It then follows from Definition 7 that \((M',s) \in {\varvec{[}}{c'}{\varvec{]}}_i.\) But \({\varvec{[}}{c'}{\varvec{]}}_i = \{ (M',s') \ | \ s'\in S' \}\) then \(s \in S'\), a contradiction.   \(\square \)

Henceforth we use \(\mathcal {M}^{{\texttt {D}}}\) to denote the class of KS’s whose accessibility relations are determinant-complete. It follows from Theorem 2 that \(\mathcal {S} = \mathcal {M}^{{\texttt {D}}}\) is the largest class for which space functions of a Kripke scs \(\mathbf{K}(\mathcal {S})\) have right inverses.

4.3 Right Inverse Constructions

Let \(\mathbf{K}(\mathcal {S}) = ({{\textit{Con}}},\sqsubseteq ,{\varvec{[}}{\cdot }{\varvec{]}}_1,\ldots ,{\varvec{[}}{\cdot }{\varvec{]}}_n)\) be the Kripke scs. The Axiom of Choice and Theorem 2 tell us that each \({\varvec{[}}{\cdot }{\varvec{]}}_i\) has a right inverse (extrusion function) if and only if \(\mathcal {S} \subseteq \mathcal {M}^{{\texttt {D}}}.\) We are interested, however, in explicit constructions of the right inverses.

Remark 1

Recall that any Kripke scs \(\mathbf{K}(\mathcal {S}) = ({{\textit{Con}}},\sqsubseteq ,{\varvec{[}}{\cdot }{\varvec{]}}_1,\ldots ,{\varvec{[}}{\cdot }{\varvec{]}}_n)\) is ordered by reversed inclusion (i.e., \(c \sqsubseteq d\) iff \(d \subseteq c\)). Thus, for example, saying that some f is the least function wrt \(\subseteq \) satisfying certain conditions is equivalent to saying that f is the greatest function wrt \(\sqsubseteq \) satisfying the same conditions. As usual given two self-maps f and g over \({\textit{Con}}\) we define \(f \sqsubseteq g \) iff \(f(c) \sqsubseteq g(c)\) for every \(c\in {\textit{Con}}\).

Since any Kripke scs space function preserve arbitrary suprema (Proposition 3), we can apply Proposition 1.2 to obtain the following canonical greatest right-inverse construction. Recall that the pre-image of c under \({\varvec{[}}{\cdot }{\varvec{]}}_i\) is given by \({\varvec{[}}{c}{\varvec{]}}_i^{-1}= \{ d \mid c = {\varvec{[}}{d}{\varvec{]}}_i \}.\)

Definition 9 (Max Right Inverse)

Let \(\mathbf{K}(\mathcal {S}) = ({{\textit{Con}}},\sqsubseteq ,{\varvec{[}}{\cdot }{\varvec{]}}_1,\ldots ,{\varvec{[}}{\cdot }{\varvec{]}}_n)\) be a Kripke scs over \(\mathcal {S} \subseteq \mathcal {M}^{{\texttt {D}}}\). We define \({\uparrow }{}{_{_i}^{{\texttt {M} }}}\) as the following self-map on \({\textit{Con}}\): .

It follows from Proposition 1.2 that \({\uparrow }{}{_{_i}^{{\texttt {M} }}}\) is a right inverse for \({\varvec{[}}{\cdot }{\varvec{]}}_i\), and furthermore, from its definition it is clear that \({\uparrow }{}{_{_i}^{{\texttt {M} }}}\) is the greatest right inverse of \({\varvec{[}}{\cdot }{\varvec{]}}_i\) wrt \(\sqsubseteq \).

Nevertheless, as stated in the following proposition, \({\uparrow }{}{_{_i}^{{\texttt {M} }}}\) is not necessarily normal in the sense of Definition 5. To state this more precisely, let us first extend the terminology in Definition 8.

Definition 10 (Indeterminacy and Multiple Determinacy)

Let S and \(\mathcal {R}\) be the set of states and an accessibility relation of a KS M, respectively. Given \(t \in S\), we say that t is determined wrt \(\mathcal {R}\) if there is \(s \in S\) such that s determines t wrt \(\mathcal {R}\), else we say that t is indetermined (or initial) wrt \(\mathcal {R}.\) Similarly, we say that t is multiply, or ambiguously, determined if it is determined by at least two different states in S wrt \(\mathcal {R}\).

The following statement and Theorem 1 lead us to conclude that the presence of indetermined/initial states or multiple-determined states causes \({\uparrow }{}{_{_i}^{{\texttt {M} }}}\) not to be normal.

Proposition 5

Let \(\mathbf{K}(\mathcal {S}) = ({{\textit{Con}}},\sqsubseteq ,{\varvec{[}}{\cdot }{\varvec{]}}_1,\ldots ,{\varvec{[}}{\cdot }{\varvec{]}}_n)\) and \({\uparrow }{}{_{_i}^{{\texttt {M} }}}\) as in Definition 9. Let \( {\texttt {nd} }(\mathcal {S}) = \{ (M,t) \ | \ M \in \mathcal {S} \ \& \ t \text { is indetermined wrt } \overset{i}{\longrightarrow }_{M} \}\) and \( {\texttt {md} }(\mathcal {S}) = \{ (M,t) \ | \ M \in \mathcal {S} \ \& \ t \text { is multiply determined wrt } \overset{i}{\longrightarrow }_{M} \}\):

  • If \({\texttt {nd} }(\mathcal {S})\ne \emptyset \) then \({\uparrow }{}{_{_i}^{{\texttt {M} }}}({\textit{true}}) \ne {\textit{true}}.\)

  • If \({\texttt {md} }(\mathcal {S})\ne \emptyset \) then \({\uparrow }{}{_{_i}^{{\texttt {M} }}}(c \sqcup d) \ne {\uparrow }{}{_{_i}^{{\texttt {M} }}}(c) \sqcup {\uparrow }{}{_{_i}^{{\texttt {M} }}}(d)\) for some \(c,d \in {\textit{Con}}.\)

In what follows we shall identify right inverse constructions that are normal. The notion of indeterminacy and multiply determinacy we just introduced in Definition 10 will play a central role.

4.4 Normal Right Inverses

The following central lemma provides distinctive properties of any normal right inverse.

Lemma 1

Let \(\mathbf{K}(\mathcal {S}) = ({{\textit{Con}}},\sqsubseteq ,{\varvec{[}}{\cdot }{\varvec{]}}_1,\ldots ,{\varvec{[}}{\cdot }{\varvec{]}}_n)\) be the Kripke scs over \(\mathcal {S} \subseteq \mathcal {M}^{{\texttt {D}}}\). Suppose that f is a normal right-inverse of \({\varvec{[}}{\cdot }{\varvec{]}}_i.\) Then for every \(M \in \mathcal {S}\), \(c \in {\textit{Con}}\):

  1. 1.

    \(\rhd _i(M,s) \subseteq f(c)\) if \((M,s) \in c\),

  2. 2.

    \(\{ (M,t) \} \subseteq f(c)\) if t is multiply determined wrt \(\overset{i}{\longrightarrow }_{M}\), and

  3. 3.

    \({\textit{true}}\subseteq f({\textit{true}}).\)

The above property tell us what sets should necessarily be included in every f(c) if f is to be both normal and a right inverse of \({\varvec{[}}{\cdot }{\varvec{]}}_i.\) It turns out that it is sufficient to include exactly those sets to obtain a normal right inverse of \({\varvec{[}}{\cdot }{\varvec{]}}_i.\) In other words the above lemma gives us a complete set of conditions for normal right inverses. In fact, the least self-map f wrt \(\subseteq \), i.e., the greatest one wrt the lattice order \(\sqsubseteq \), satisfying Conditions 1, 2 and 3 in Lemma 1 is indeed a normal right-inverse. We call such a function the max normal right inverse \({\uparrow }{}{_{_i}^{{\texttt {MN} }}}\) and is given below.

Definition 11 (Max Normal-Right Inverse)

Let \(\mathbf{K}(\mathcal {S}) = ({{\textit{Con}}},\sqsubseteq , {\varvec{[}}{\cdot }{\varvec{]}}_1,\ldots ,{\varvec{[}}{\cdot }{\varvec{]}}_n)\) be a Kripke scs over \(\mathcal {S} \subseteq \mathcal {M}^{{\texttt {D}}}\). We define the max normal right inverse for agent i, \({\uparrow }{}{_{_i}^{{\texttt {MN} }}}\) as the following self-map on \({\textit{Con}}\):

(4)

(Recall that means that s uniquely determines t wrt \(\overset{i}{\longrightarrow }_{M}\).)

We now state that \({\uparrow }{}{_{_i}^{{\texttt {MN} }}}{(c)}\) is the greatest normal right inverse of \({\varvec{[}}{\cdot }{\varvec{]}}_i\) wrt \(\sqsubseteq \).

Theorem 3

Let \(\mathbf{K}(\mathcal {S}) = ({{\textit{Con}}},\sqsubseteq ,{\varvec{[}}{\cdot }{\varvec{]}}_1,\ldots ,{\varvec{[}}{\cdot }{\varvec{]}}_n)\) and \({\uparrow }{}{_{_i}^{{\texttt {MN} }}}\) as in Definition 11.

  • The self-map \({\uparrow }{}{_{_i}^{{\texttt {MN} }}}\) is a normal right inverse of \({\varvec{[}}{\cdot }{\varvec{]}}_i\),

  • For every normal right-inverse f of \({\varvec{[}}{\cdot }{\varvec{]}}_i,\) we have \(f \sqsubseteq {\uparrow }{}{_{_i}^{{\texttt {MN} }}}{}\).

Notice that \({\uparrow }{}{_{_i}^{{\texttt {MN} }}}(c)\) excludes undetermined states if \(c \ne {\textit{true}}\). It turns out that we can add them and obtain a more succinct normal right inverse:

Definition 12 (Normal Inverse)

Let \(\mathbf{K}(\mathcal {S}) = ({{\textit{Con}}},\sqsubseteq ,{\varvec{[}}{\cdot }{\varvec{]}}_1,\ldots ,{\varvec{[}}{\cdot }{\varvec{]}}_n)\) be a Kripke scs over \(\mathcal {S} \subseteq \mathcal {M}^{{\texttt {D}}}\). Define \({\uparrow }{}{_{_i}^{{\texttt {N} }}}:{\textit{Con}}\rightarrow {\textit{Con}}\) as .

Clearly \({\uparrow }{}{_{_i}^{{\texttt {N} }}}(c)\) includes every (M, t) such that t is indetermined wrt \(\overset{i}{\longrightarrow }_{M}\).

Theorem 4

Let \(\mathbf{K}(\mathcal {S}) = ({{\textit{Con}}},\sqsubseteq ,{\varvec{[}}{\cdot }{\varvec{]}}_1,\ldots ,{\varvec{[}}{\cdot }{\varvec{]}}_n)\) and \({\uparrow }{}{_{_i}^{{\texttt {N} }}}\) as in Definition 12. The self-map \({\uparrow }{}{_{_i}^{{\texttt {N} }}}\) is a normal right inverse of \({\varvec{[}}{\cdot }{\varvec{]}}_i\).

We conclude this section with the order of the right-inverses we identified.

Corollary 1

Let \(\mathbf{K}(\mathcal {S}) = ({{\textit{Con}}},\sqsubseteq ,{\varvec{[}}{\cdot }{\varvec{]}}_1,\ldots ,{\varvec{[}}{\cdot }{\varvec{]}}_n)\) be a Kripke scs over \(\mathcal {S} \subseteq \mathcal {M}^{{\texttt {D}}}.\) Let \({\uparrow }{}{_{_i}^{{\texttt {M} }}},{\uparrow }{}{_{_i}^{{\texttt {MN} }}},\) and \({\uparrow }{}{_{_i}^{{\texttt {N} }}}\) as in Definitions 9, 11 and 12, respectively. Then \({{\uparrow }{}{_{_i}^{{\texttt {N} }}}\sqsubseteq {\uparrow }{}{_{_i}^{{\texttt {MN} }}} \sqsubseteq {\uparrow }{}{_{_i}^{{\texttt {M} }}}}.\)

5 Applications

In this section we will apply and briefly discuss the results obtained in the previous section in the context of modal logic. First we recall the notion of modal language.

Definition 13 (Modal Language)

Let \(\varPhi \) be a set of primitive propositions. The modal language \(\mathcal {L}_n(\varPhi )\) is given by the following grammar: \(\phi , \psi ,\ldots \ := \ p \mid \phi \wedge \psi \mid \lnot \phi \mid \square _i \phi \) where \(p \in \varPhi \) and \(i \in \{1,\ldots ,n \}.\) We shall use the abbreviations \(\phi \vee \psi \) for \(\lnot (\lnot \phi \wedge \lnot \psi )\), \(\phi \Rightarrow \psi \) for \(\lnot \phi \vee \psi \), \(\phi \Leftrightarrow \psi \) for \((\phi \Rightarrow \psi ) \wedge (\psi \Rightarrow \phi )\), the constant false \({\textit{ff}}\) for \( p \wedge \lnot p\), and the constant \({\textit{tt}}\) for \(\lnot {\textit{ff}}\).

We say that a pointed KS (M, s) satisfies \(\phi \) iff \((M,s)\ \models \ \phi \) where \(\models \) is defined inductively as follows: \((M,s)\ \models \ p\) iff \(\pi _M(s)(p)=1\), \((M,s)\ \models \ \phi \wedge \psi \) iff \((M,s)\ \models \ \phi \) and \((M,s)\ \models \ \psi \), \((M,s)\ \models \ \lnot \phi \) iff , and \((M,s)\ \models \ \square _i \phi \) iff \((M,t)\ \models \ \phi \) for every t such that \(s \overset{i}{\longrightarrow }_{M} t\). This notion of satisfiability is invariant under a standard equivalence on Kripke structures: Bisimilarity, itself a central equivalence in concurrency theory [14].

Definition 14 (Bisimilarity)

Let \(\mathcal {B}\) be a symmetric relation on pointed KS’s. The relation is said to be a bisimulation iff for every \(((M,s),(N,t)) \in \mathcal {B}\): (1) \(\pi _M(s) = \pi _N(t)\) and (2) if \(s \overset{i}{\longrightarrow }_{M} s'\) then there exists \(t'\) s.t. \(t \overset{i}{\longrightarrow }_{N} t'\) and \(((M,s'),(N,t')) \in \mathcal {B}.\) We say that (M, s) and (N, t) are bisimilar, written \((M,s) \sim (N,t)\) if there exists a bisimulation \(\mathcal {B}\) such that \(((M,s),(N,t)) \in \mathcal {B}.\)

The well-known result of bisimilarity-invariance for modal satisfiability implies that (M, s) and (M, t) satisfy the same formulae in \(\mathcal {L}_n(\varPhi )\) whenever \((M,s) \sim (N,t)\) [14].

Modal logics are typically interpreted over different classes of KS’s obtained by imposing conditions on their accessibility relations. Let \(\mathcal {S}_n(\varPhi )\) be a non-empty set of n-agent Kripke structures over a set of primitive propositions \(\varPhi \). A modal formula \(\phi \) is said to be valid in \(\mathcal {S}_n(\varPhi )\) iff \((M,s)\ \models \phi \) for each (M, s) such that \(M \in { \mathcal {S}_n(\varPhi ) }.\)

We can interpret modal formulae as constraints in a given Kripke scs \(\mathbf {C}= \mathbf{K}(\mathcal {S}_n(\varPhi ))\) as follows.

Definition 15 (Kripke Constraint Interpretation)

Let \(\mathbf {C}\) be a Kripke scs \(\mathbf{K}(\mathcal {S}_n(\varPhi )).\) Given a modal formula \(\phi \) in the modal language \(\mathcal {L}_n(\varPhi )\), its interpretation in the Kripke scs \(\mathbf {C}\) is the constraint \(\mathbf {C}\llbracket \phi \rrbracket \) inductively defined as follows:

$$\begin{aligned} \mathbf {C} \llbracket p \rrbracket= & {} \{ (M,s) \ \mid \ \pi _M(s)(p) = 1 \} \\ \mathbf {C} \llbracket \phi \wedge \psi \rrbracket= & {} \mathbf {C} \llbracket \phi \rrbracket \sqcup \mathbf {C} \llbracket \psi \rrbracket \\ \mathbf {C} \llbracket \lnot \phi \rrbracket= & {} \sim { \mathbf {C} \llbracket \phi \rrbracket } \\ \mathbf {C} \llbracket \square _i \phi \rrbracket= & {} {\varvec{[}}{\ \mathbf {C} \llbracket \phi \rrbracket \ }{\varvec{]}}_i \end{aligned}$$

Remark 2

One can verify that for any Kripke scs \(\mathbf{K}(\mathcal {S}_n(\varPhi ))\), the Heyting negation \(\sim c\) (Definition 4) is \(\varDelta \setminus c\) where \(\varDelta \) is the set of all pointed Kripke structures (M, s) such that \(M \in { \mathcal {S}_n(\varPhi ) }\) (i.e., boolean negation). Similarly, Heyting implication \(c \rightarrow d\) is equivalent to \((\sim c) \cup d\) (i.e., boolean implication).

It is easy to verify that the constraint \(\mathbf {C}\llbracket \phi \rrbracket \) includes those pointed KS (M, s), where \(M\in \mathcal {S}_n(\varPhi ),\) such that \((M,s)\ \models \ \phi .\) Thus, \(\phi \) is valid in \(\mathcal {S}_n(\varPhi )\) if and only if \(\mathbf {C}\llbracket \phi \rrbracket = {\textit{true}}\).

Notice that from Proposition 3 and Theorem 1, each space function \({\varvec{[}}{\cdot }{\varvec{]}}_i\) of \(\mathbf{K}(\mathcal {S}_n(\varPhi ))\) is a normal self-map. From Definitions 5 and 15 we can derive the following standard property stating that \(\square _i\) is a normal modal operator: (Necessitation) If \(\phi \) is valid in \(\mathcal {S}_n(\varPhi )\) then \(\square _i\phi \) is valid in \(\mathcal {S}_n(\varPhi )\), and (Distribution) \(\square _i( \phi \Rightarrow \psi ) \Rightarrow (\square _i \phi \Rightarrow \square _i\psi )\) is valid in \(\mathcal {S}_n(\varPhi ).\)

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 [20], in modal logics for concurrency they represent backward moves [19], in epistemic logic they correspond to utterances [13].

To illustrate our results in the previous sections, let us fix a modal language \(\mathcal {L}_n(\varPhi )\) (whose formulae are) interpreted in an arbitrary Kripke scs \(\mathbf {C}=\mathbf{K}(\mathcal {S}_n(\varPhi )).\) Suppose we wish to extend it with modalities \(\square _{i}^{-1}\), called reverse modalities also interpreted over the same set of KS’s \(\mathcal {S}_n(\varPhi )\) and satisfying some minimal requirement. The new language is given by the following grammar.

Definition 16 (Modal Language with Reverse Modalities)

Let \(\varPhi \) be a set of primitive propositions. The modal language \(\mathcal {L}_n^{+r}(\varPhi )\) is given by the following grammar: \( \phi , \psi ,\ldots \ := \ p \mid \phi \wedge \psi \mid \lnot \phi \mid \square _i \phi \mid \square _i^{-1} \phi \) where \(p \in \varPhi \) and \(i \in \{1,\ldots ,n \}.\)

The minimal semantic requirement for each \(\square _{i}^{-1}\) is that, regardless of the interpretation we give to \(\square _{i}^{-1} \phi \), we should have:

$$\begin{aligned} \ \square _{i}\square _{i}^{-1}\phi \ \Leftrightarrow \ \phi \ \ \ \text { valid in } \mathcal {S}_n(\varPhi ).\end{aligned}$$
(5)

We then say that \(\square _{i}^{-1}\) is a right-inverse modality for \(\square _{i}\) (by analogy to the notion of right-inverse of a function).

Since \(\mathbf {C} \llbracket \square _i \phi \rrbracket = {\varvec{[}}{\ \mathbf {C} \llbracket \phi \rrbracket \ }{\varvec{]}}_i\), we can use the results in the previous sections to derive semantic interpretations for \(\square _{i}^{-1} \phi \) by using a right inverse \({\uparrow }{}{_i}\) for the space function \({\varvec{[}}{\cdot }{\varvec{]}}_i\) in Definition 15. Assuming that such a right inverse exists, we can then interpret the reverse modality in \(\mathbf {C}\) as

$$\begin{aligned} \mathbf {C} \llbracket \square _i^{-1} \phi \rrbracket = {\uparrow }{}{_i ( \ \mathbf {C} \llbracket \phi \rrbracket \ ) }. \end{aligned}$$
(6)

Since each \({\uparrow }{}{_i}\) is a right inverse of \({\varvec{[}}{\cdot }{\varvec{]}}_i\), it is easy to verify that the interpretation satisfies the requirement in Eq. 5. Furthermore, from Theorem 2 we can conclude that for each \(M \in \mathcal {S}_n(\varPhi )\), \(\overset{i}{\longrightarrow }_{M}\) must necessarily be determinant-complete.

Normal Inverse Modalities. We can choose \({\uparrow }{}{_i}\) in Eq. 6 from the set \(\{ {\uparrow }{}{_{_i}^{{\texttt {N} }}}, {\uparrow }{}{_{_i}^{{\texttt {MN} }}}, {\uparrow }{}{_{_i}^{{\texttt {M} }}} \}\) of right-inverse constructions in Sect. 4.3. Assuming that \({\uparrow }{}{_i}\) is a normal self-map (e.g., either \({\uparrow }{}{_{_i}^{{\texttt {N} }}}\) or \({\uparrow }{}{_{_i}^{{\texttt {MN} }}}\)), we can show from Definition 5 and Eq. 6 that \(\square _i^{-1}\) is itself a normal modal operator in the following sense: (1) If \(\phi \) is valid in \(\mathcal {S}_n(\varPhi )\) then \(\square _i^{-1}\phi \) is valid in \(\mathcal {S}_n(\varPhi )\), and (2) \(\square _i^{-1}( \phi \Rightarrow \psi ) \Rightarrow (\square _i^{-1} \phi \Rightarrow \square _i^{-1}\psi )\) is valid in \(\mathcal {S}_n(\varPhi ).\)

Inconsistency Invariance. Since we assumed a right inverse for \({\varvec{[}}{\cdot }{\varvec{]}}_i\), from Proposition 1(1) we should have

$$\begin{aligned} \lnot \square _{i}{\textit{ff}} \text{ valid } \text{ in } \mathcal {S}_n(\varPhi ) \end{aligned}$$
(7)

(recall that \({\textit{ff}}\) is the constant false). Indeed using the fact that \({\varvec{[}}{\cdot }{\varvec{]}}_i\) is a normal self-map with an inverse \({\uparrow }{}{_i}\) and Theorem 1, we can verify the following:

$$\begin{aligned} \mathbf {C}\llbracket \square _{i}{\textit{ff}} \rrbracket =\mathbf {C}\llbracket \square _{i}( {\textit{ff}}\wedge \square _{i}^{-1}{\textit{ff}}) \rrbracket = \mathbf {C}\llbracket \square _{i}{\textit{ff}}\wedge \square _{i}\square _{i}^{-1}{\textit{ff}} \rrbracket = \mathbf {C}\llbracket \square _{i}{\textit{ff}}\wedge {\textit{ff}} \rrbracket = \mathbf {C}\llbracket {\textit{ff}} \rrbracket \end{aligned}$$

This implies \(\square _{i}{\textit{ff}}\Leftrightarrow {\textit{ff}}\) is valid in \(\mathcal {S}_n(\varPhi )\) and this means that \(\lnot \square _{i}{\textit{ff}}\) is valid in \(\mathcal {S}_n(\varPhi ).\)

Modal systems such \(K_n\) or Hennessy-Milner logic [14] where \(\lnot \square _{i}{\textit{ff}}\) is not an axiom cannot be extended with a reverse modality satisfying Eq. 5 (without restricting their models). The issue is that the axiom \(\lnot \square _{i}{\textit{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 \(\square _{i}{\textit{ff}}\) is used in HM logic to express deadlocks wrt to i; \((M,s)\ \models \ \square _{i}{\textit{ff}}\) iff there is no \(s'\) such that \(s\overset{i}{\longrightarrow }_{M}s'\). Clearly there cannot be state deadlocks wrt i if \(\overset{i}{\longrightarrow }_{M}\) is required to be serial for each M.

Bisimilarity Invariance. Recall that bisimilarity invariance says that bisimilar pointed KS’s satisfy the same formulae in \(\mathcal {L}_n(\varPhi ).\) The addition of a reverse modality \(\square _{i}^{-1}\) may violate this invariance: Bisimilar pointed KS’s may not longer satisfy the same formulae in \(\mathcal {L}_n^{+r}(\varPhi ).\) 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.

Let us suppose that the chosen right inverse \({\uparrow }{}{_i}\) in Eq. 6 is any normal self-map whatsoever. It follows from Lemma 1(2) and Eq. 6 that if t is multiply-determined wrt \(\overset{i}{\longrightarrow }_{M}\) then \((M,t)\ \models \ \square _i^{-1}{\textit{ff}}.\) We can use Lemma 1(1) and Eq. 6 to show that if t is uniquely determined wrt \(\overset{i}{\longrightarrow }_{M}\) then

Now take v and \(s_4\) as in Fig. 1. Suppose that \(\pi _{M_5}(v)=\pi _{M_1}(s_i)\) for every \(s_i\) in the states of \(M_1\). Clearly \((M_1,s_4)\sim (M_5,v)\). Since \(s_4\) is multiply determined and v is uniquely determined, we conclude that \((M_1,s_4)\ \models \ \square _i^{-1}{\textit{ff}}\) but Thus \(\square _i^{-1}{\textit{ff}}\) can tell uniquely determined states from multiply determined ones but bisimilarity cannot.

Temporal Operators. We conclude this section with a brief discussion on some right-inverse linear-time modalities. Let us suppose that \(n=2\) in our modal language \(\mathcal {L}_n(\varPhi )\) under consideration (thus interpreted in Kripke scs \(\mathbf {C}=\mathbf{K}(\mathcal {S}_2(\varPhi )).\) Assume further that the intended meaning of the two modalities \(\square _1\) and \(\square _2\) are the next operator () and the henceforth/always operator (\(\Box \)), respectively, in a linear-time temporal logic. To obtain the intended meaning we take \(\mathcal {S}_2(\varPhi )\) to be the largest set such that: If \(M \in \mathcal {S}_2(\varPhi )\), M is a 2-agent KS where \(\overset{1}{\longrightarrow }_{M}\) is isomorphic to the successor relation on the natural numbers and \(\overset{2}{\longrightarrow }_{M}\) is the reflexive and transitive closure of \(\overset{1}{\longrightarrow }_{M}\). The relation \(\overset{1}{\longrightarrow }_{M}\) is intended to capture the linear flow of time. Intuitively, \(s\overset{1}{\longrightarrow }_{M}t\) means t is the only next state for s. Similarly, \(s\overset{2}{\longrightarrow }_{M}t\) for \(s \ne t\) is intended to capture the fact that t is one of the infinitely many future states for s.

Let us first consider the next operator Notice that \(\overset{1}{\longrightarrow }_{M}\) is determinant-complete. If we apply Eq. 6 with \({\uparrow }{}{_1}={\uparrow }{}{_{_1}^{{\texttt {M} }}}\), i.e., the greatest right inverse of \({\varvec{[}}{\cdot }{\varvec{]}}_1\), we obtain \(\square _1^{-1} = \circleddash \), a past modality known in the literature as strong previous operator [20]. The operator is given by iff there exists s such that and . If we take to be the normal right inverse , we obtain the past modality known as weak previous operator [20]. The operator is given by iff for every s if then . Notice that the only difference between the two operators is the following: If s is an indetermined/initial state wrt \(\overset{1}{\longrightarrow }_{M}\) then and for any \(\phi \).

Let us now consider the always operator \(\square _2 = \Box .\) Notice that \(\overset{2}{\longrightarrow }_{M}\) is not determinant-complete: Take any sequence \(s_0 \overset{1}{\longrightarrow }_{M} s_1 \overset{1}{\longrightarrow }_{M} \ldots \) The state \(s_1\) is not determinant because for every \(s_j\) such that \(s_1\overset{2}{\longrightarrow }_{M}s_j\) we have \(s_0\overset{2}{\longrightarrow }_{M}s_j.\) Theorem 2 says that there is no right-inverse of \({\varvec{[}}{\cdot }{\varvec{]}}_i\) that can give us a \(\square _2^{-1}\) satisfying Eq. 5.

By analogy to the above-mentioned past operators, one may think that the past operator it-has-always-been \(\boxminus \) [24] may provide a reverse modality for \(\Box \) in the sense of Eq. 5. The operator is given by \((M,t)\ \models \ \boxminus \phi \) iff \((M,s)\ \models \ \phi \) for every s such that \(s \overset{2}{\longrightarrow }_{M}t.\) Clearly \(\Box \boxminus \phi \ \Rightarrow \ \phi \) is valid in \(\mathcal {S}_2(\varPhi )\) but \(\phi \Rightarrow \ \Box \boxminus \ \phi \) is not.

6 Concluding Remarks and Related Work

We 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 greatest normal right inverse of any given space function. We applied these results 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 our results 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. In previous work [13] the authors derived an inverse modality but only for the specific case of a logic of belief. The work was neither concerned with giving a complete characterization of the existence of right inverse nor deriving normal inverses. The constraint systems in this paper can be seen as modal extension of geometric logic [26]. Modal logics have also been studied from an algebraic perspective by using modal extensions of boolean and Heyting algebras in [2, 4, 17]. These works, however, do not address issues related to inverse modalities. Inverse modalities have been used in temporal, epistemic and logic for concurrency. In [24] the authors discuss inverse temporal and epistemic modalities from a proof theory perspective. The works [5, 12, 19] use modal logic with reverse modalities for specifying true concurrency and [6, 7] use backward modalities for characterizing branching bisimulation. None of these works is concerned with an algebraic approach or with deriving inverse modalities for modal languages.