Duality for Logics of Transition Systems

Marcello M. Bonsangue^{1}^{⋆} Alexander Kurz^{2}^{⋆⋆}

1 LIACS, Leiden University, The Netherlands 2 Department of Computer Science, University of Leicester, UK

Abstract. We present a general framework for logics of transition systems based on Stone duality. Transition systems are modelled as coalgebras for a functor T on a category X. The propositional logic used to reason about state spaces from X is modelled by the Stone dual A of X (e.g. if X is Stone spaces then A is Boolean algebras and the propositional logic is the classical one). In order to obtain a modal logic for transition systems (i.e. for T -coalgebras) we consider the functor L on A that is dual to T . An adequate modal logic for T -coalgebras is then obtained from the category of L-algebras which is, by construction, dual to the category of T -coalgebras. The logical meaning of the duality is that the logic is sound and complete and expressive (or fully abstract) in the sense that non-bisimilar states are distinguished by some formula. We apply the framework to Vietoris coalgebras on topological spaces, using the duality between spaces and observation frames, to obtain adequate logics for transition systems on posets, sets, spectral spaces and Stone spaces.

Keywords: transition systems, coalgebras, Stone duality, topological dualities, modal logic

1 Introduction

The framework presented in this paper aims at a general theory of logics for transition systems built on Stone duality. The relationship between these notions can be displayed as follows.

systems  coalgebras logics  algebras_{Stone duality}

The upper row refers to the theory of coalgebras as laid out by Rutten [22] which proposes coalgebras as a general framework allowing to treat a large variety of different (transition) systems in a uniform way.

The lower row refers to the connection between logics and algebras as familiar from propositional logic/Boolean algebras or intuitionistic logic/Heyting algebras. The

⋆ The research of Dr. Bonsangue has been made possible by a fellowship of the Royal Netherlands Academy of Arts and Sciences

⋆⋆ Partially supported by NWO/British Council.

modal logics that are the basis for most logics of transition systems have similar algebraic counterparts [3].

The connection between the two rows will be provided by Stone duality (Johnstone [13]). Stone duality provides set-theoretic representations of algebras, or, in other words, provides a state-based semantics for the logics described as algebras. It has been used, for example, in the ground breaking work of Jónnson and Tarski [15] and Goldblatt [11] in modal logic and Abramsky [1, 2] in domain theory.

Lifting a Stone Duality via Dual Functors In this paper we show that there is a simple general principle underlying all these works. It can be formalised in a framework parametric in the basic duality and the type of the transition structure. The key role in this framework will be provided by a suitable duality between a category X (e.g. Stone spaces [13]) and a category of algebras A (e.g. Boolean algebras). This duality extends to a duality between relational structures on X (e.g. descriptive general frames [11]) and modal algebras on A whenever there are dual endofunctors T :X → X and L:A → A.

[figure: X; T; A; L]

The relational semantics is given by T -coalgebras and the algebraic semantics is given by L-algebras. The respective categories Coalg(T ) and Alg(L) are dually equivalent by construction. Informally speaking, T encodes the possible next-step transitions a T -coalgebra may engage in; and L describes how to construct, up to logical equivalence, modal formulae of depth 1 from propositional formulae. We show in Theorem 5 that under fairly general circumstances dual functors on dual categories automatically give rise to a modal logic and an adequate relational semantics (i.e. the logic is sound, complete, and expressive).

Instantiating the Framework with a Powerdomain for T_{0}-spaces We instantiate the above framework to show that a number of modal logics arise in a uniform way if we take X above to be a suitable category of topological spaces and T to be a variant of the powerset functor. In particular, we want to be able to characterise the relational structure providing an adequate semantics to positive modal logic with infinite joins and infinite meets. This builds on the work of [6] since such a characterisation will require a duality between T_{0} topological spaces and so-called spatial observation frames. As a novel result, we present a functor L defining the modal algebras dual to the relational structures induced by T . It is a non-trivial extension of the Vietoris functor on locales as defined in [14].

By considering suitable subcategories of topological spaces we obtain modal logics with an adequate relational semantics on transition systems over posets, sets, spectral spaces, and Stone spaces. The last two cases give us well known modal logics, namely the positive and the classical ones, with Alg(L) being positive modal algebras and Boolean algebras with operators, respectively, and Coalg(T ) being the K^{+}-spaces of [8] and the descriptive general frames of [11], respectively. This unifies and extends recent work [21, 17] showing that K^{+}-spaces and descriptive general frames can be described as Coalg(T ) for an appropriate functor T . Compared to [21], which uses Priestley spaces, our description of K^{+}-spaces as coalgebras is simpler in that the definition of the Vietoris functor on spectral spaces avoids taking a quotient identifying indistinguishable subsets.

Related Work The idea of relating constructions on algebras and topological spaces is extensively discussed in [23] and, for a specific class of topological spaces, in [1]. Our approach is more general since it also treats logics with infinitary conjunctions. Moreover, the models we are interested in are not only the solutions of recursive domain equations (final coalgebras) but any coalgebras. On the other hand, we only deal here with categories that do not accommodate the function spaces important in domain theory.

Our algebraic description of the Vietoris construction is a generalisation of that presented in [13, 14], since it allows for equations involving infinite conjunctions. However, when these are not necessary, the two constructions coincide. The equations for spectral spaces of Section 5, for example, are the same as those presented in [14].

Soundness and completeness of an infinitary modal logic for transition systems has been proved in [7] using a topological duality. Completeness, however, is obtained by significantly restricting the class of transition systems under consideration. For example, they form a subclass of the descriptive general frames. Our result here incorporates the above as a special case, obtained by considering a specific category of topological spaces. Furthermore, by applying our framework to the category of posets, we obtain completeness for a larger class of transition systems including the descriptive general frames. To our knowledge, this is the first such result for a positive infinitary modal logic.

Overview We proceed as follows. The next section introduces some basic notions on coalgebras, algebras and their presentation by generators and relations. In Section 3 we describe the framework for the use of dualities for a coalgebraic semantics of modal logic. In Section 4, we introduce a duality for topological spaces and set up, in Section 5, the necessary ingredients for finally applying in Section 6 the above framework to obtain sound, complete, and expressive modal logics for transition systems. We conclude with a discussion on possible future directions in Section 7.

2 Preliminaries

Although category theory does not play a major role in this paper, we will have to assume some basic notions. As usual, Set denotes the category of sets and functions.

Algebras and Coalgebras for a Functor Roughly speaking, coalgebras for a functor generalise transition systems, whereas algebras for a functor generalise the ordinary algebras for a signature where carriers are not sets but taken from some category. Further, (co-)algebras for a functor give rise to the principle of (co-)induction [22].

Given a functor T :X → X on a category X, a T -coalgebra (X , ξ) consists of an object X ∈ X and an arrow ξ:X → TX . A coalgebra morphism f :(X , ξ) → (X′, ξ′) is an arrow f :X → X′ such that ξ′ ∘ f = Tf ∘ ξ. Dually, an L-algebra on a category A is given by an arrow α:LA → A, and an algebra morphism f :(A, α) → (A′, α′) is an arrow f :A → A′ such that α′ ∘ Lf = f ∘ α. The respective categories are denoted by Coalg(T ) and Alg(L).

If the category X has a forgetful (i.e. faithful) functor V :X → Set then we can talk about the elements of a coalgebra. In particular, we have a canonical notion of behavioural equivalence (or bisimulation). Explicitly, given T -coalgebras (X , ξ), (X′, ξ′) and elements x ∈ VX , x′ ∈ VX′, we say that x and x′ are behaviourally equivalent or bisimilar, denoted x ≃ x′, if there is a coalgebra (Y , ν) and there are coalgebra morphisms f :(X , ξ) → (Y , ν) and f′:(X′, ξ′) → (Y , ν) such that Vf (x) = Vf′(x′).

Example 1. If X is the category Set of sets and functions and T = P is the powerset functor (mapping a set to its powerset and a function to the direct image function), then Coalg(T ) is the category of Kripke frames with bounded morphisms (also called p-morphisms [11]). Kripke models w.r.t. a given set Prop of atomic propositions are (P(Prop) × P)-coalgebras. Behavioural equivalence yields the standard notion of bisimulation in both cases.

The Final and Initial Sequences The intuition that T describes the possible next-step transitions can be made precise using the final (coalgebra) sequence. Moreover, in cases were the final coalgebra does not exist, one can still work with the final sequence. We just outline the basics, for further information see e.g. [25].

The final sequence (or terminal sequence) of T :X → X

\xymatrix{T_{0} & T_{1} \ar[l]_{p_{0}^{1}} & … \ar[l] & T_{n} & T_{n+1} \ar[l]_{p_{n}^{n+1}} & … \ar[l]}

is an ordinal indexed sequence of objects T_{n} in X together with a family (p_{m}^{n})_{m≤n} of arrows p_{m}^{n}:T_{n} → T_{m} for all ordinals m ≤ n such that

– T_{n+1} = T (T_{n}) and p_{m+1}^{n+1} = T (p_{m}^{n}) for all m ≤ n,

– p_{n}^{n} = id_{T_{n}} and p_{k}^{n} = p_{k}^{m} ∘ p_{m}^{n} for k ≤ m ≤ n,

– the cone (T_{n}, (p_{m}^{n}))_{m<n} is limiting whenever n is a limit ordinal.

Here we are assuming that X has the necessary limits (in particular, a final object T_{0}). The initial sequence of an endofunctor is defined dually.

Intuitively, T_{n} represents behaviours that can be observed in n steps. This can be formalised by observing that, for every coalgebra (X , ξ), there are arrows

ξ_{n}:X → T_{n}

where ξ_{n}:X → T_{n} is T (ξ_{m}) ∘ ξ if n = m + 1 and ξ_{n} is the unique map satisfying ξ_{m} = p_{m}^{n} ∘ ξ_{n} for all m < n if n is a limit ordinal. If V :X → Set is the forgetful functor we now consider V ξ_{n} as the map assigning to each state x its n-step behaviour, that is, for (X , ξ), (X′, ξ′) and x ∈ VX , x′ ∈ VX′ define x, x′ to be n-step equivalent, denoted by x ≃_{n} x′, if ξ_{n}(x) = ξ′_{n}(x′).

The final sequence is said to converge if there is an ordinal n for which p_{n}^{n+1} is iso. Then the inverse (p_{n}^{n+1})^{−1} is the final T -coalgebra. In this case, two states are behaviourally equivalent if and only if they are identified by the (unique) morphisms into the final coalgebra, that is, x ≃_{n} x′ for all ordinals n.

Example 2. Let X = Set. If TX is the powerset PX of X , then n-step equivalence coincides with the notion of bounded bisimulation as e.g. in [10]. The final coalgebra does not exist (as an object in Coalg(T )) since its carrier is not a set but a proper class.

Presenting Algebras by Generators and Relations A category A is algebraic when it comes with a monadic functor U :A → Set [18]. In this case, the functor U has a left adjoint F :Set → A, mapping every set S to the free algebra FS. Furthermore, every object of A can be presented by generators and relations, that is, for each A ∈ A we can find a set S (the elements of which are called generators in this context) and a set R ⊆ FS × FS (the elements of which are called relations in this context) such that A is the quotient FS/R. Algebraically speaking, objects of A can be identified with algebras of an (infinitary) algebraic theory^{3}. Clearly, every presentation A⟨S|R⟩ by generators S and relations R defines an algebra in A.

Example 3. A frame is a complete lattice L that satisfies the infinite distributive law a ∧ ⋁ C = ⋁{a ∧ c | c ∈ C } for all a ∈ L and all subsets C ⊆ L. Frames with functions preserving arbitrary joins and finite meets form a category called Frm. The forgetful functor from Frm to Set mapping each frame to its underlying set is monadic. Hence the infinitary algebra Frm⟨S|R⟩ presented by a set of generators S and a set of relations R presents a frame and every frame can be presented by generators and relations. In particular, the free frame over a set S can be presented as Frm⟨S|∅⟩.

A model of a presentation A⟨S|R⟩ is a pair ⟨B, f :S → UB⟩ such that B ∈ A and f^{†}(e_{l}) = f^{†}(e_{r}), where (e_{l}, e_{r}) ∈ R and f^{†}:FS → B is the unique extension of f such that f^{†}(η(s)) = f (s) for each s ∈ S, with η the unit of the adjunction between F and U . It follows that presentations are canonical: if A⟨S|R⟩ is a presentation of A ∈ A then it comes equipped with a function [[−]]_{A}:S → UA such that for every other model ⟨B, f :S → UB⟩ there exists a unique function f^{‡}:A → B with the property that f^{‡}([[s]]_{A}) = f (s) for each s ∈ S.

Example 4. A complete lattice L is a completely distributive lattice (cdl) if, for all sets C of subsets of L, it holds that ⋀{⋁ C | C ∈ C} = ⋁{⋀ f (C) | f ∈ Φ(C)}, where f (C) denotes the set {f (C ) | C ∈ C} and Φ(C) is the set of all functions f : C → ⋃ C such that f (C ) ∈ C for all C ∈ C. Completely distributive lattices with functions preserving both arbitrary meets and arbitrary joins form a category, denoted by CDL. Also the forgetful functor from CDL to Set mapping each completely distributive lattice to its underlying set is monadic.

Since every cdl is a frame we have that CDL⟨S|R⟩ together with the function [[−]]_{F} is a model of F = Frm⟨S|R⟩. Therefore, the identity function over a set S can be uniquely extended to a frame morphism from Frm⟨S|R⟩ to CDL⟨S|R⟩ for each set of frame relations R. In other words, CDL⟨S|R⟩ is the presentation of the free cdl over the frame presented by Frm⟨S|R⟩.

3 The converse is, in general, false. For example, there is no free complete Boolean algebra over a set of two generators.

3 The Framework: Dualities for Modal Logic

This section describes a general framework for the use of dualities in modal logic. Consider the following situation

[figure: X; T; O; V; A; Pt; L; U; Set; Set; F]

where O and Pt are a dual equivalence (or duality, for short) between the categories X and A, i.e. O and Pt are contravariant functors and there are isomorphisms X → PtOX , A → OPtA, for all X ∈ X , A ∈ A. Further, V is a faithful functor from X to Set, and L and T are dual functors in the sense that there is an isomorphism PtL → T^{op}Pt. Clearly, Alg(L) and Coalg(T ) are dual categories.

We assume that A is a category of algebras over Set, that is, categorically speaking, the functor U :A → Set is monadic. In particular, for any set Prop the free algebra F (Prop) ∈ A exists. We call UF (Prop) the set of propositional formulae in variables (or atomic propositions) Prop. Since algebras can be represented by generators and relations we can find, for each algebra A, a set of generators GA and a surjective algebra morphism τ_{A}:FGA → LA. We assume G to be a functor from A → Set and τ_{A} to be natural in A.^{4}

These ingredients allow us to define modal formulae and their algebraic semantics. Consider the diagram

\xymatrix{L′_{0} \ar[r] \ar[d]^{q_{0}} & FGL′_{0} \ar[d]^{q_{1}} \ar[r] & … & FGL′_{n} \ar[d]^{q_{n+1}} \ar[r] & … \\ L′_{0} \ar[r] & L′_{1} \ar[r] & … & L′_{n+1} \ar[r] & …}

where the lower row is the initial sequence (Section 2) of the functor L′ = L+F (Prop), that is, L′_{0} is the initial object in A, L′_{n+1} = L(L′_{n}) + F (Prop). The elements of FGL′_{n} are the modal formulae of depth n + 1. The horizontal arrows allow us to consider a formula of depth n as a formula of depth m for any m ≥ n. The vertical arrows q_{n} assign to each formula of depth n its algebraic semantics (which is an equivalence class of modal formulae) and are given by τ_{L′_{n}} composed with the left injection into L(L′_{n}) + F (Prop). By naturality of τ, the above diagram commutes. If the sequence converges, the colimit of FGL′_{n} is the set of all modal formulas and the colimit of the L′_{n} is the Lindenbaum-Tarski algebra of the logic. In many interesting cases, the sequence will converge (even after ω steps), but since we also want to cover infinitary logics we can not assume this.

4 For example, we can take G:A → Set to be the functor GA = ∐_{B∈A} ULFUB × A(FUB, A) and τ_{A}(f , g) = ULg(f ). But often, as in the case studied in this paper, a much more economical presentation is possible.

In this paper, the objects of A will always be (distributive) lattices, that is, although all objects are equipped with a partial order ≤ they may lack implication. This means that we cannot reduce consequence ϕ ⊢ ψ to theoremhood ⊢ ϕ → ψ. We define

ϕ ⊢ ψ ⇔ q_{n}(ϕ) ≤ q_{n}(ψ) for some ordinal n, n ≥ depth of ϕ, ψ

On the semantic side, in this paper, the objects of X will be T_{0}-spaces and O maps continuous functions to their inverse image functions. We can now describe the coalgebraic semantics for the logic. Let ξ:X → TX be a coalgebra and x in X . Due to the duality, L′_{n} is dual to T′_{n} where T′ = T × Pt(F (Prop)), that is, there are isomorphisms j_{n}:L′_{n} → O(T′_{n}). Note that a T′-coalgebra (X , ⟨ξ, v⟩) is a T -coalgebra (X , ξ) together with a valuation v:X → Pt(F (Prop)). That is, for each T -coalgebra (X , ξ) together with a valuation v:X → Pt(F (Prop)) there are arrows ⟨ξ, v⟩_{n}:X → T′_{n} (see Section 2). The situation is summarised in

\xymatrix{FGL′_{n−1} \ar[r]_{q_{n}} & L′_{n} \ar[r]_{j_{n}} & O(T′_{n}) \ar[r]_{⟨ξ,v⟩_{n}^{−1}} & OX}

We define the semantics ⊩ of ⊢ w.r.t. a coalgebra ⟨ξ, v⟩ as follows. ϕ ⊩_{⟨ξ,v⟩} ψ if for some ordinal n, n ≥ depth of ϕ, ψ,

⟨ξ, v⟩_{n}^{−1}(j_{n}(q_{n}(ϕ))) ⊆ ⟨ξ, v⟩_{n}^{−1}(j_{n}(q_{n}(ψ)))  (1)

Intuitively, ⟨ξ, v⟩_{n}^{−1}(j_{n}(q_{n}(ϕ))) is the set of elements of X that satisfy the formula ϕ under valuation v. As usual, ϕ ⊩ ψ means ϕ ⊩_{⟨ξ,v⟩} ψ for all coalgebras ξ and valuations v. We can now prove soundness, completeness, invariance under bisimilarity and expressiveness.

The theorem can be proved under two different assumptions. This paper employs the theorem under the first assumption, the second assumption will be useful to treat the non-compact powerspace.

Theorem 5. In the situation described above assume that either

1. the final T′-coalgebra exists or

2. T′ weakly preserves limits of n-chains for all limit ordinals n.

Then the modal logic is sound and complete w.r.t. its coalgebraic semantics, that is, ϕ ⊩ ψ ⇔ ϕ ⊢ ψ. Moreover, formulae are invariant under behavioural equivalence and the logic is expressive in the sense that any non-bisimilar points are separated by some formula.

Proof. We first sketch the proof under Assumption 2 which means that all arrows in the final sequence of T′ are surjective (split epi). Soundness: Assume ϕ ⊢ ψ, i.e. q_{n}(ϕ) ≤ q_{n}(ψ). Since ⟨ξ, v⟩_{n}^{−1} ∘ j_{n} is a morphism and therefore monotone it follows ϕ ⊩ ψ. Completeness: Assume ϕ ⊬ ψ, i.e. q_{n}(ϕ) ≰ q_{n}(ψ). Since j_{n}:L′_{n} → O(T′_{n}) is an injective morphism, there is t ∈ j_{n}(ϕ)) such that t ∉ j_{n}(ψ). It follows from assumption 2 that each arrow p_{n}^{n+1}:T′(T′_{n}) → T′_{n} in the final sequence has a rightinverse ζ. ζ is a T′-coalgebra for which ϕ ⊮_{ζ} ψ, the (counter)example being t. Invariance: It is immediate from the definition that formulae are invariant under ≃_{n}.

Expressiveness: If ⟨ξ, v⟩, ⟨ξ′, v′⟩ are two coalgebras and x, x′ are two elements with ⟨ξ, v⟩_{n}(x) ≠ ⟨ξ′, v′⟩_{n}(x′) then, by surjectivity of j_{n} (and the spaces being T_{0}), there must be some ϕ such that j_{n}(q_{n}(ϕ)) contains one of {x, x′} but not the other. Hence ϕ separates x and x′. Under Assumption 1, the proof is essentially the same. One replaces q_{n} by the morphism to the initial L′-algebra, ⟨ξ, v⟩_{n} by the morphism to the final T′-coalgebra and ζ by the final coalgebra itself.

Remark 6. Expressiveness of the logic can also be considered as full abstractness of the final semantics.

Example 7. We briefly illustrate the notions with a well-known example. Let A be the category of Boolean algebras and X the category of Stone spaces. VPtA = A(A, 2) is the set of ultrafilters over A. (Similarly, writing 2_{X} for the two-element Stone space, we have that U OX = X (X , 2_{X}) is the set of clopens of X .) If we take GA = A and τ_{A}(a) = □a and LA to be the quotient of FGA defined by the equations expressing that □ preserves meets, then Alg(L) is the category of modal algebras (Boolean algebras with operators). GL′_{n} = {□ϕ | ϕ ∈ L′_{n}} and FGL′_{n} is the closure of GL′_{n} under propositional operations (modulo Boolean equations). The functor T dual to L is the Vietoris functor and Coalg(T ) is the category of descriptive general frames. The continuity of a valuation v:X → Pt(F (Prop)) ≅ ∏_{Prop} 2_{X} means that the extension of a propositional variable in Prop has to be a clopen set. See [17] for details.

4 Topological Duality

In this section we set up the necessary ingredients for applying the above framework. In particular we will briefly introduce a duality for topological spaces, generalising the Stone duality considered in the previous example.

Recall that a topological space is a set X together with a collection of subsets of X , called opens, closed under arbitrary unions and finite intersections. A function between two sets X and Y is continuous if its inverse maps opens of Y to opens of X .

Each topological space X induces a closure operator mapping each subset S of X to the least (w.r.t. subset inclusion) subset \overline{X} such that X \ \overline{X} is open. Each topological space induces also a pre-order on X defined by x ≤ y if and only if x ∈ o implies y ∈ o for each open o of X . A space X is said to be T_{0} when the above pre-order is a partial order. We denote by Top_{0} the category of all T_{0} topological spaces with continuous functions as morphisms.

For the category of algebras we consider the category OFrm of observation frames, a structure introduced in [6] for representing topological spaces abstractly. An observation frame is an order-reflecting frame morphisms α:F → L between a frame F and a completely distributive lattice L such that

q = ⋀{o ∈ α(F ) | q ≤ o}

for every element q of L. A morphism between two observation frames α:F → L and β:G → H is a pair ⟨f , g⟩ consisting of a frame morphism f :F → G and a cdlmorphism g:L → H such that g ∘ α = β ∘ f .

Example 8. Each topological space X defines an observation frame OX as the inclusion map between the frame O(X ) of all open subsets of X and the cdl Q(X ) of all upclosed subsets of X . Furthermore, O can be extended to a functor by mapping a continuous function f :X → Y to ⟨f^{−1}:O(Y ) → O(X ), f^{−1}:Q(Y ) → Q(X )⟩.

The functor U :OFrm → Set mapping an observation frame α:F → L to α(F ) is monadic [5]. Therefore every observation frame α:F → L can be presented as OFrm⟨S|R⟩ for some set S of generators and set R of relations e_{l} = e_{r}. Here e_{l} and e_{r} are expressions formed by applying the infinite meet operator ⋀ to expressions formed from the generators in S by applying the infinite join operator ⋁ and finite meet operator ∧. In particular, L is isomorphic in CDL to CDL⟨S|R⟩, whereas F is isomorphic in Frm to Frm⟨S|R^{−}⟩, where R^{−} is the subset of R obtained by considering relations involving only finite meet and infinite join operators. Since ⟨L, [[−]]_{L}⟩ is a model for the presentation of F , the frame morphism α:F → L is obtained as the canonical extension of the identity on S. Similarly, every presentation OFrm⟨S|R⟩ presents an observation frame.

Next we show that the functor O:Top_{0} → OFrm^{op} has a right adjoint. Let 2 be the two-element cdl with ⊤_{2} as top element and ⊥_{2} as bottom one, and 2 be the identity morphism on 2. For an observation frame α:F → L we denote by Pt(α) the topological space given by the set OFrm(α, 2) together with a topology with open sets defined, for every x ∈ F , by △(x) = {⟨f , g⟩:α → 2 | f (x) = ⊤_{2}}.

Theorem 9 ([6]). For every observation frame α, the assignment α ↦ Pt(α) can be extended to a functor from OFrm^{op} to Top_{0} which is right adjoint of O.

For every T_{0} topological space X , the unit η_{X} :X → Pt(O(X )) of the above adjunction is an isomorphism, whereas for each observation frame α:F → L the counit △(−):F → O(Pt(α)) is injective. We say that α is spatial when △ is an isomorphism. The above adjunction thus restricts to an equivalence between Top_{0} and the full subcategory SOFrm of spatial observation frames [6].

5 Two Vietoris Functors

In order to apply the duality framework introduced in Section 3 we define two endofunctors P_{c} and V on Top_{0} and OFrm, respectively, and prove that they are dual functors using the duality introduced in the previous section.

We call a subset c of a topological space X convex if c = c↑∩ \overline{c}, where c↑ is the upclosure of c w.r.t. the pre-order induced by X whereas \overline{c} is its topological closure.

Definition 10. Given a space X , define the Vietoris hyperspace P_{c}(X ) to be the set of all convex compact subsets of X equipped with the topology generated by the sub-basic sets

{c ∈ P_{c}(X ) | c ⊆ o} and {c ∈ P_{c}(X ) | c ∩ o ≠ ∅}

for each o ∈ O(X ).

The restriction to convex subsets in the definition of P_{c}(X ) guarantees that the hyperspace P_{c}(X ) is T_{0} if X is a T_{0} space [19]. P_{c} extends to an endofunctor on Top_{0}.

Example 11. If X is a set, i.e. a discrete topological space, then P_{c}(X ) is the set of all finite subsets of X taken with the discrete topology. Also, if X is an ω-algebraic complete partial order equipped with the Scott topology, then P_{c}(X ) coincides with the Plotkin powerdomain.

For the definition of the endofunctor V on OFrm it is enough to define a presentation of V(α) for each observation frame α. Its set of generators is

G(α) = {□a | a ∈ α(F )} ∪ {♢a | a ∈ α(F )}

and the relations are given by the following rule schemes

(□ − ⋀) \frac{⋀_{I} a_{i} ≤ b}{⋀_{I} □a_{i} ≤ □b}  (♢ − ⋁) ♢ ⋁_{I} a_{i} = ⋁_{I} ♢a_{i}
(□ − ∨) □(a ∨ b) ≤ □a ∨ ♢b  (♢ − ⋀) \frac{⋀_{I} a_{i} ∧ b ≤ c}{⋀_{I} □a_{i} ∧ ♢b ≤ ♢c}
(COM ) □ ⋁_{I} a_{i} = ⋁_{J∈Fin(I )} □ ⋁_{J} a_{i} ,

where Fin(I ) is the set of all finite subsets of I . Rules (□ − ⋀) and (♢ − ⋀) generalise corresponding rules for the Vietoris locale [14] basically by imposing the □ operator to distribute over all meets of F which are preserved by α as meet of L. The scheme (COM ) corresponds to restricting to compact subsets in the definition of P_{c} as in [14, 23] and states that □ distributes over directed joins.

Theorem 12. For every T_{0} space X , PtVOX ≅ P_{c}X .

If α is a spatial observation frame then α ≅ OPtα and it follows PtVα ≅ P_{c}Ptα. Hence the functors P_{c} and V were dual if SOFrm was closed under V. This is not the case in general [14], but we will see below that it is true for many important subcategories of SOFrm to which we then apply the framework of Section 3.

Posets The category PoSet of posets with monotone functions can be characterised as the full subcategory of Top_{0} that has as objects those topological spaces where open sets are closed under arbitrary intersections (the Alexandroff topology). The category PoSet is closed under the Vietoris functor P_{c}. The adjunction in Theorem 9 restricts to a duality between the category PoSet and AlgCDL, the category of algebraic cdl’s. AlgCDL is equivalent to the full sub-category of OFrm whose objects are observation frames α:F → L with α(F ) = L and L algebraic [5]. The duality implies that these observation frames are spatial.

The category AlgCDL is closed under the Vietoris functor V. To see this one can first note that because α(F ) = L the presentation of Vα can be simplified by replacing the schemes (□ − ⋀) and (♢ − ⋀) with the following two:

(□ − ⋀′) ⋀_{I} □a_{i} = □ ⋀_{I} a_{i}  (♢ − ∧) □a ∧ ♢b ≤ ♢(a ∧ b) .

That the cdl presented by Vα is algebraic (and hence spatial) follows from the following lemma, similar to one in [2, 24].

Lemma 13. Let α:F → L be an observation frame and X a subset of α(F ). In the observation frame Vα we have □ ⋁_{I} a_{i} = ⋁_{J∈Fin(I )}(□ ⋁_{J} a_{i} ∧ ⋀_{J} ♢a_{i}) .

Summarising, the categories PoSet and AlgCDL are dual and closed under the two Vietoris functors P_{c} and V, respectively. Furthermore, the two functors are also dual, and the category AlgCDL is algebraic.

Sets The category Set of sets and functions is a full subcategory of PoSet. It can be characterised as the full subcategory of Top_{0} with as objects the topological spaces with open sets closed under arbitrary intersections and complement (the discrete topology). We have already seen that Set is closed under the Vietoris functor P_{c}. The duality between the categories PoSet and AlgCDL restricts to a duality between Set and CABool the full sub-category of AlgCDL with objects equivalent to observation frames α:F → L with α(F ) = L and L an algebraic boolean algebra. Note that algebraic complete boolean algebras are just complete atomic boolean algebras.

If α:F → L is an observation frame as above then in the observation frame Vα it holds

(□ − ¬) □a ∨ ♢¬a = ⊤ and (♢ − ¬) □a ∧ ♢¬a = ⊥ .

for each a ∈ α(F ) with complement ¬a ∈ α(F ). Hence ♢¬a is the complement of □a. The presentation of Vα can thus be simplified by replacing the schemes (□ − ⋀), (□ − ∨) and (♢ − ⋀) with (□ − ⋀′), (□ − ¬) and (♢ − ¬). By applying the framework described in Section 3 we obtain an infinitary modal logic (with negation) that is sound and complete w.r.t. its coalgebraic semantics.

Spectral Spaces The category Spec of spectral spaces is a subcategory of Top_{0} with as objects topological spaces with compact open sets closed under finite intersections and forming a base for the topology. Morphisms in Spec are continuous functions with inverse preserving compact opens. As for the other categories above, Spec is closed under the Vietoris functor P_{c} [13, 23]. The adjunction in Theorem 9 restricts to a duality between the category Spec and DLat, the category of distributive lattices, equivalent to the full sub-category of OFrm whose objects are observation frames α:F → L with F an algebraic arithmetic frame and L the free completely distributive lattice over F . Equivalently, observation frames in DLat can be presented by relations using only finite meet and finite join operators, because they are equivalent to distributive lattices. It follows that observation frames in DLat are spatial.

The category DLat is closed under the Vietoris functor V, because if α:F → L is an observation frame in DLat, then the presentation of Vα can be simplified by using the following relations:

(□ − ∧) □(a ∧ b) = □a ∧ □b (□ − ⊤) □⊤ = ⊤
(♢ − ∨) ♢(a ∨ b) = ♢a ∨ ♢b  (♢ − ⊥) ♢⊥ = ⊥
(□ − ∨) □(a ∨ b) ≤ □a ∨ ♢b (♢ − ∧) □a ∧ ♢b ≤ ♢(a ∧ b) .

Note that these axioms are precisely those which have to be added to distributive lattices to define positive modal algebras, see e.g. [8]. It follows that Alg(V), with V restricted to DLat, is (isomorphic to) the category of positive modal algebras. From Section 3, it follows that Coalg(P_{c}), with P_{c} restricted to spectral spaces, provides an adequate relational semantics for positive modal logic. Compared to [21] this yields an alternative description of K^{+}-spaces ([8]) as coalgebras.

Stone Spaces Stone spaces are spectral spaces with compact opens closed under complement. Let Stone be the full subcategory of Spec with Stone spaces as objects. We can restrict the duality between Spec and DLat to a duality between Stone and Bool, the full subcategory of DLat with as object boolean algebras. If α:F → L is an observation frame equivalent to a boolean algebra then in the observation frame Vα both (□ − ¬) and (♢ − ¬) hold. Hence the presentation of Vα for DLat can be simplified by replacing the schemes (□ − ∨) and (♢ − ∧) with (□ − ¬) and (♢ − ¬). We can further simplify by reducing the set of generators to G(α) = {□a | a ∈ α(F )} and the relations to

(□ − ∧) □(a ∧ b) = □a ∧ □b (□ − ⊤) □⊤ = ⊤

Note that these axioms are precisely those which have to be added to Boolean algebras to define modal algebras (Boolean algebras with operator). It follows that Alg(V), with V restricted to Bool, is (isomorphic to) the category of modal algebras. The category Coalg(P_{c}), with P_{c} restricted to Stone, is isomorphic to the category of descriptive general frame and has also been described in [17].

6 Modal Logics for Transition Systems

In order to obtain sound, complete, and expressive modal logics, we now apply the framework of Section 3 to the dualities obtained in the previous section. For all four dualities

[figure: X; P_{c}; A; V]

the final coalgebra of the functor P_{c} exists, so that we can apply Theorem 5. The corresponding propositional logic is obtained in the following way.

For a description of A via signature Σ and equations E take the formulae to be the terms built from the signature Σ plus the two unary operation symbols □ and ♢. The calculus is given by the calculus for equational logic plus the equations E plus the rules describing the functor V (some of the rules have been given as inequations, but ϕ ≤ ψ can be considered a shorthand for ϕ ∧ ψ = ψ).

As it is well-known, such an equational calculus can be translated into a propositional modal calculus. Since our algebras are lattices we can use inequations instead of equations. We write ϕ ⊢ ψ for ϕ ≤ ψ. That is, ϕ ⊢ ψ corresponds to the equation ϕ ∧ ψ = ψ and, conversely, an equation ϕ = ψ to inequations ϕ ⊢ ψ, ψ ⊢ ϕ.

As it is apparent from (1) in Section 3, the semantics of ϕ ⊢ ψ is the so-called local consequence of modal logic. In classical modal logic, local consequence can be formulated as theorem-hood because ϕ ⊢ ψ is equivalent to ⊢ ϕ → ψ. But as in e.g. [1, 7, 8], not all our logics have ‘→’. We will detail below the modal calculi arising in the way just described from the four dualities of the previous section.

Posets and Spectral Spaces The first is the infinitary version of the second. In both cases, the modal operators will obey the rule schemes

\frac{ϕ ⊢ ψ}{□ϕ ⊢ □ψ}  \frac{ϕ ⊢ ψ}{♢ϕ ⊢ ♢ψ}  (2)

Posets The signature Σ is {⋁, ⋀} and these operators are axiomatised according to the laws of completely distributive lattices (i.e. , negation free infinitary propositional logic).^{5} The axiom schemes for the modal operators are the following.

⋀_{I} □ϕ_{i} ⊢ □ ⋀_{I} □ϕ_{i}  ♢ ⋁_{I} ϕ_{i} ⊢ ⋁_{I} ♢ϕ_{i}
□(ϕ ∨ ψ) ⊢ □ϕ ∨ ♢ψ  □ϕ ∧ ♢ψ ⊢ ♢(ϕ ∧ ψ)
□ ⋁_{I} ϕ_{i} ⊢ ⋁_{J∈Fin(I )} □ ⋁_{J} ϕ_{i}

Spectral Spaces The signature Σ is {⊤, ⊥, ∨, ∧} and these operators are axiomatised according to the laws of distributive lattices (i.e. , negation free propositional logic). The axiom schemes for the modal operators are the following.

□(a ∧ b) ⊢ □a ∧ □b ⊤ ⊢ □⊤
♢a ∨ ♢b ⊢ ♢(a ∨ b) ♢⊥ ⊢ ⊥
□(a ∨ b) ⊢ □a ∨ ♢b □a ∧ ♢b ⊢ ♢(a ∧ b) .

In the previous section some of the inequalities above are presented as equalities. The ‘missing’ directions follow from the monotonicity rules (2).

Sets and Stone spaces The first is the infinitary version of the second. Since we have classical implication, we only need to axiomatise ⊤ ⊢ ϕ which we abbreviate by ⊢ ϕ. Since we have negation, we need only one modal operator, say □.

Sets The signature Σ is {⋀, ¬} and these operators are axiomatised according to the laws of completely distributive lattices with negation (i.e. , classical propositional logic). In order to stay close to the equational axiomatisation it is convenient to choose as a rule scheme

\frac{⊢ ϕ ↔ ψ}{⊢ □ϕ ↔ □ψ}  (3)

(which is the congruence rule of equational logic for □) and as axiom schemes

⊢ ⋀ □ϕ_{i} ↔ □ ⋀ ϕ_{i}  ⊢ ⊤ ↔ □⊤
⊢ □ ⋁_{I} ϕ_{i} ↔ ⋁_{J∈Fin(I )} □ ⋁_{J} ϕ_{i}

Stone Spaces The signature Σ consists of the operators ⊤, ∨, ¬ which are axiomatised according to the laws of boolean algebra (i.e. classical propositional logic). In order

5 The category A of Section 3 is AlgCDL whereas the category described by the signature is CDL. But since V preserves algebraic cdls, the initial sequence for V remains in AlgCDL.

to stay close to the standard calculus of modal logic, it is convenient to choose the following rule and axiom scheme

\frac{⊢ ϕ}{⊢ □ϕ} ⊢ □(ϕ → ψ) → (□ϕ → □ψ)

These schemes correspond to the equations from the previous section because they are equivalent to the rule 3 together with ⊢ □(ϕ ∧ ψ) ↔ □ϕ ∧ □ψ and ⊢ □⊤ ↔ ⊤.

7 Conclusion and Further Work

We have presented a general framework relating modal logics and their relational (i.e. coalgebraic) semantics. It can be read in two directions: describe a given logic as a functor L and work out the adequate relational semantics by describing the dual functor T ; or, for a given notion of transitions systems as T -coalgebras, work out the adequate logic by describing the dual of T via generators and relations. To apply this idea and equip the coalgebraic logic of Moss [20] with modal operators (given by the generators) and a complete axiomatisation is one of many directions for future research.

Another one is to look at other functors T than the compact hyperspace. An obvious candidate is the non-compact hyperspace which is expected to give interesting infinitary logics for the categories of posets and sets (the infinitary counterparts of spectral and Stone spaces, respectively). Further candidates are the Kripke-polynomial functors of Jacobs [12].

Furthermore, it would be interesting to determine the range of the framework of Section 3. Apart from generalising some of the specific assumptions, there is also the question which logics can be described by categories of algebras that admit a duality, leading to connections with algebraic logic [9].

References

1. S. Abramsky. Domain theory in logical form. Annals of Pure and Applied Logic, 5:1–77, 1991.

2. S. Abramsky. A domain equation for bisimulation. Inf. and Comp., 92, 1991.

3. J. van Benthem, J. van Eijck, and V. Stebletsova. Modal Logic, Transition Systems and Processes. Journal of Logic and Computation, 4:811–855, 1994.

4. P. Blackburn, M. de Rijke, and Y. Venema. Modal Logic. CSLI, 2001.

5. M.M. Bonsangue. Topological Dualities in Semantics. Vol. 8 of ENTCS, Elsevier, 1996.

6. M.M. Bonsangue, B. Jacobs, and J.N. Kok. Duality beyond sober spaces: topological spaces and observation frames. Theor. Comp. Sci. 15(1):79–124, 1995.

7. M.M. Bonsangue and J.N. Kok. Towards an infinitary logic of domains: Abramsky logic for transition systems. Inf. and Comp. 155:170–201, 1999.

8. S. Celani and R. Jansana. Priestley duality, a Sahlqvist theorem and a Goldblatt-Thomason theorem for positive modal logic. Logic Journ. of the IGPL, 7:683–715, 1999.

9. J.M. Font, R. Jansana, and D. Pigozzi. A Survey of Abstract Algebraic Logic. Studia Logica, 74:13–97, 2003.

10. J. Gerbrandy. Bisimulations on Planet Kripke. PhD thesis, Univ. of Amsterdam, 1999.

11. R.I. Goldblatt. Metamathematics of modal logic I. Rep. on Math. Logic, 6, 1976.

12. B. Jacobs. Many-sorted coalgebraic modal logic: a model-theoretic study. Theoretical Informatics and Applications, 35(1):31–59, 2001.

13. P.T. Johnstone. Stone Spaces. Cambridge University Press, 1982.

14. P.T. Johnstone. The Vietoris monad on the category of locales. In Continuous Lattices and Related Topics, pp. 162–179, 1982.

15. B. Jónsson and A. Tarski, Boolean algebras with operators, part I. American Journal of Mathematics, 73:891–939, 1951.

16. M. Kracht. Tools and Techniques in Modal Logic. Vol. 142 of Studies in Logic, Elsevier, 1999.

17. C. Kupke, A. Kurz, and Y. Venema. Stone coalgebras. Theoret. Comput. Sci., 327:109–134, 2004.

18. E.G. Manes. Algebraic Theories. Springer-Verlag, 1976.

19. E. Michael. Topologies on spaces of subsets. Trans. Amer. Math. Soc., 71, 1951

20. L. Moss. Coalgebraic logic. Annals of Pure and Applied Logic, 96:277–317, 1999.

21. A. Palmigiano. A coalgebraic semantics for positive modal logic. Theoret. Comput. Sci., 327:175–195, 2004.

22. J.J.M.M. Rutten. Universal coalgebra: A theory of systems. Theoret. Comput. Sci., 249:3–80, 2000.

23. S. Vickers. Topology via Logic. Cambridge University Press, 1989.

24. S. Vickers. Information systems for continuous posets. Theoret. Comp. Sci., 114, 1993.

25. J. Worrell. Terminal sequences for accessible endofunctors. In Coalgebraic Methods in Computer Science (CMCS’99), vol. 19 of ENTCS, Elsevier, 1999.