Nick Bezhanishvili
Title:
Generalized Esakia duality
Abstract:
I will introduce partial Esakia morphisms, well partial Esakia
morphisms, and strong partial Esakia morphisms between Esakia spaces and
show that they provide the dual description of
$(\wedge,\to)$-homomorphisms, $(\wedge,\to,0)$-homomorphisms, and
$(\wedge,\to,\vee)$-homomorphisms between Heyting algebras, thus
establishing a generalization of Esakia duality.
Achim Jung
Title:
Stone Duality for bitopological spaces
Abstract:
Samson Abramsky promoted the idea to use Stone duality to
connect denotational semantics for programming languages with program
logics. He developed a fairly specialised theory that was applicable to
so-called Scott-domains (and SFP objects). In joint work with Drew
Moshier, we found that the theory becomes much more elegant if carried out
for stably compact spaces. More recently, we discovered that our duality
(and the resulting logic) can usefully be expressed for bitopological
spaces. This sheds new light on the logical set-up but, surprisingly, also
on the classical dualities of Stone for Boolean algebras and distributive
lattices.
Christian Kissig
Title:
Trace Logics for Semiring Monads
(Joint work with Alexander Kurz)
Abstract:
Recently, coalgebraic logics have seen much attention as means to characterise points in Set-based coalgebras precisely up to bisimilarity. With the introduction of a uniform definition of trace semantics for coalgebras structured in the branching type given by a monad, the question was raised for a logic which describes points in such coalgebras adequately and expressively up to trace equivalence.
In this talk I will present recent work with Alexander Kurz on this question. We consider coalgebras on Set with branching given by evaluation in a fixed semiring, which defines a semiring monad. The trace semantics of such coalgebras is given by final sequence induction in the Kleisli-category, which in this case happens to be the category of freely generated semimodules. We then obtain trace logics and its semantics as transposes of respectively final coalgebra and final coalgebra morphism along the Morita adjunction induced by the semiring under consideration.
Clemens Kupke
Title:
Final Coalgebras and the Hennessy-Milner property
(Joint work with Raul Leal)
Abstract:
The notion of behavioural equivalence is central to the
theory of coalgebras. In my talk will relate three different, but
equivalent, ways to
characterise behavioural equivalence for set coalgebras. These are:
using final coalgebras, using coalgebraic languages that have the Hennessy-
Milner property and using coalgebraic languages that have ``logical
congruences''.
In particular, I will present a straightforward construction of the final
T-coalgebra of a set functor using a given logical language
that has the Hennessy-Milner property with respect to the class of
T-coalgebras.
Finally I will discuss generalizations to coalgebras over other categories.
Alexander Kurz
Title:
Towards Universal Algebra for Nominal Sets
(Joint work with Daniela Petrisan)
Abstract:
Starting from the observation that nominal sets (in
the sense of Gabbay and Pitts) are a full reflective subcategory of a
category of algebras, we propose to use standard universal algebra to
do algebra over nominal sets. For example, it is possible to adapt the
standard proof of Birkhoff's HSP theorem to nominal algebra. We
compare this with J.M.Gabbay's Nominal Algebra and the HSP-theorem.
Rob Myers
Title:
Coalgebraic Tableaux
Abstract:
Formulae of multisorted coalgebraic modal logics, which may contain
fixpoints, universal programs, nominals or other features, are often
thought of as partial observations satisfied in some model. However we
note that they may also be seen as elements of the respective final
coalgebra, in the sense that coalgebraic tableaux algorithms construct
satisfying models from these formulae. Recently Silva, Bosangue and
Rutten have presented generic fixpoint expressions together with a
generalisation of both Kleene's theorem for regular expressions and the
complete equational logic of Kleene algebra; this covers Mealy machines
and Kleene algebras with tests amongst others. We will show that this
work is an instantiation of this observation, thereby obtaining a
generic decision procedure and a considerable generalisation beyond the
Kripke polynomial coalgebra case they presented. We will also discuss
the framework of multisorted coalgebraic hybrid logic with the universal
modality, which amongst other things provides a generic framework for
Description Logic (DL) and even appears to provide a new "canonical"
tableaux for the well-studied relational case. An example application
outside DL lies in the area of norm-governed multi-agent systems.
Dirk Pattinson
Title:The Coalgebraic mu-calculus
(Joint work with Corina Cirstea and Clemens Kupke)
Abstract:
The coalgebraic approach to modal logic provides a uniform framework
that captures the semantics of a large class of structurally
different modal logics, including e.g. graded and probabilistic
modal logics and coalition logic. In this paper, we introduce the
coalgebraic μ-calculus, an extension of the general
(coalgebraic) framework with fixpoint operators. Our main results
are completeness of the associated tableau calculus and EXPTIME
decidability. Technically, this is achieved by reducing
satisfiability to the existence of non-wellfounded tableaux, which
is in turn equivalent to the existence of winning strategies in
parity games.
Our results are parametric in the underlying class of models and
yield, as concrete applications, previously unknown complexity
bounds for the probabilistic μ-calculus and for an extension of
coalition logic with fixpoints.
Daniela Petrisan
Title:
A Duality Theorem for Real Commutative C* Algebras
(Joint Work with Drew Moshier)
Abstract:
Real commutative C* algebras have come under attention in theoretical computer science as an abstraction of the notion of ``test'' or ``observation.'' Another way to think about observations has a longer history in domain theory. The open sets of a Scott topology are regarded as forming a logic of observable properties. The two approaches are related via the two Stone duality theorems: C* algebras vs. compact Hausdorff spaces on one hand, and Boolean algebras vs. Stone spaces on the other. We investigate the connections between the `logical' view and the `real ring' view, giving a direct proof for the equivalence between the category of C* algebras and the category of skew frames with negation. The latter appears in the work of Jung and Moshier on the bitopological nature of Stone duality. Consequently, we can prove that the category of C* algebras and the category of proximity lattices with negation are dually equivalent, without going through the construction of spaces.
