COALA: Coalgebraic Logics and Applications
Coalgebraic semantics offers
a generic framework to study a
class of (typically non-normal) modal logic in a uniform
way including, besides extensions of the logic K,
- The logic of neighbourhood frames and montone modal logics
- Coalition Logic
- Probabilistic and Graded Modal Logic, Majority Logic
- several different Conditional Logics
and many others. Results for particular logics are then
obtained by simple instantiations of the coalgebraic framework.
The tutorial presents an overview of the state-of-the-art in
coalgebraic logics, grouped around for main themes:
- Modelling with Coalgebraic Logics
- An introduction to coalgebras
from the perspective of modal logic. Examples of
coalgebraic models: Kripke models, (monotone) neighbourhood frames,
game frames, probabilistic and labelled transition systems,
weighted multigraphs, selection function models. Syntax and Semantics of coalgebraic logics,
bisimulation and the Hennessy-Milner property.
- Reasoning in Coalgebraic Logics
- Axiom systems for coalgebraic logics, completeness and the
finite model property in the general coalgebraic framework and
applied to the examples above.
- Complexity of Coalgebraic Logics
- Generic sequent / tableaux
systems for coalgebraic logics leading to uniform complexity bounds
for the satisfiability problem of coalgebraic logics and a
prototypical implementation, examples as above.
- Combining Coalgebraic Logics
- Construction principles for coalgebraic semantics, modular aspects of the Hennessy-Milner
property, modular completeness and modular algorithms. Examples:
Segala Systems and alternating systems (different combinations of
probabilities and non-determinism), games with quantitative
uncertainty (game frames with probabilistic information), logics of
probabilistic knowledge.
Why Coalgebraic Logics?
Coalgebraic logics exhibit three major traits that make them a
useful tool for modal reasoning:
- Genericity
- The tools and techniques developed in a
coalgebraic framework are simultaneously applicable to a large class
of logics
- Compositionality
- Coalgebraic techniques lend
themselves to modular construction of systems with the same level of
modularity at the logical level
- Algorithms
-
Both genericity and compositionality
manifest themselves also in the
to the modular construction of decision procedures.
We hope that attendees will
be able to identify and subsequently exploit coalgebraic aspects in
their own research in the context of modelling, reasoning and
mechanising modal logics, and profit from the large number of
off-the-shelf results established in the coalgebraic framework.
Prerequisites
The tutorial provides an introduction to, and an overview of
coalgebraic techniques in modal logics equally suitable for
beginning PhD students and more experienced researchers. In
particular, no prerequisite knowledge on coalgebras will be assumed.
Literature
A reader covering the four main themes of the tutorial will be
provided.
- General Theory of Coalgebras
-
- Coalgebras and Modal Logic
-
- A. Kurz,
Specifying coalgebras with modal logic
- D. Pattinson,
Coalgebraic Modal Logic: Soundness, Completeness and Decidability
- D. Pattinson,
Expressive logics for coalgebras via terminal sequence induction
- L. Schröder,
A Finite Model Construction for Coalgebraic Modal Logic
- L. Schroeder, D. Pattinson,
PSPACE-Bounds for Rank-1 Modal Logics
- L. Schröder, D. Pattinson,
Modular Algori thms for Heterogeneous Modal Logics
- C. Cirstea and D. Pattinson,
Modular proof systems for coalgebraic logics
- L. Schröder and D. Pattinson,
Rank-1 logics are coalgebraic
