My main research interests originate in the use of temporal logics in
system verification, but spread to cover many connected areas.
A central area of my research for the last twenty years has been
fixpoint logics, and particularly the modal mu-calculus. These provide
a foundational logic for verification using the temporal logic
paradigm, and also have a wealth of intrinsically interesting
As a consequence of this interest, I have also become interested in
fixpoints in general, which has led to some forays into (mostly quite
elementary!) descriptive set theory.
A long-standing interest is theories and models of true
concurrency, in which causality and the independence of parallel
components are taken seriously.
In the last few years, I have been working on modal analogues of Hintikka's
Independence-Friendly Logic. This was inspired by its intuitively
obvious links with concurrency - an intuition which takes a while to
I have always been interested in natural language, particularly
phonology, and recently I have started to do a little real
work in the area, something which I hope to continue and deepen.
Papers and preprints
Here are a few recent and/or popular publications:
Most of my papers and preprints are online,
accompanied by a short description and notes about dependencies.
- A journal paper on the use of
simulation in phonology.
- The journal paper on the
phonology of clicks in Khoisan.
- A CSL paper with a new game semantics
for dependence logic.
- A poster about the difficulty of
learning complex vowel systems.
- A preprint of a chapter on
mu-calculi in the Handbook of Modal Logic.
The journal version of two papers on
fixpoints and parity conditions in descriptive set theory, and a
conference paper dealing with
one of the problems raised there.
- A full version of a paper on fixpoint
extensions of independence-friendly logic, and a full paper on the complexity of such logics.
A paper in a Festschrift for
considering the use of Henkin quantification in modal logic.
- A preprint of an introduction
to modal mu-calculus, appearing as a chapter in the Handbook of
The journal version of the original paper
establishing the strictness of the modal mu-calculus alternation
hierarchy, and a journal version of two conference papers,
simplifying the proof, and addressing the issue of Niwinski's fixpoint
algebras on trees.
Slides from talks
My talks page has the slides from some of my
seminar etc. talks. This material will be moved into the publications
page, but is currently separate.