This page is in the process of being replaced. Very recent material is in that page instead, which will take over from this one.

Sections:

(Preprints of) Published Papers

Most recent papers first. All texts of papers are either gzipped PostScript or PDF.
The files here are generally the last preprint before publication, rather than the actual published version. The content is usually the same.

Modal Mu-Calculi

This is a chapter for the Handbook of Modal Logic to be published by Elsevier in 2006. It is written together with
Colin Stirling. While it includes some considerable chunks from the Handbook of Process Algebra chapter, it is more concerned with logical, game and automata theoretic issues in mu-calculi than with applications to processes. It covers: background; syntax and semantics of modal mu-calculus; expressive power; satisfiability; axiomatization; alternation; bisimulation invariance; generalized mu-calculi.

Here is the PDF text (300kB).


Independence: logics and concurrency

This is a considerably revised and expanded version of the
CSL '00 paper below, to appear in a Festschrift for Gabriel Sandu. It concentrates more on `design issues' around the application of IF concepts to modal logics than on the mathematical properties of such logics, though it includes and extends some of the results from the CSL paper.

Here is a gzipped PostScript preprint.


Transfinite extension of the mu-calculus

This paper, written with
Sandra Quickert and Jacques Duparc, takes up a problem raised in the TIA paper below. It appeared in in CSL '05 (proceedings in LNCS).
In \cite{Bra03} Bradfield found a link between finite differences formed by $\ks ^0_2$ sets and the mu-arithmetic introduced by Lubarski \cite{Lub93}. We extend this approach into the transfinite: in allowing countable disjunctions we show that this kind of extended mu-calculus matches neatly to the transfinite difference hierarchy of $\ks^0_2$ sets. The difference hierarchy is intimately related to parity games. When passing to infinitely many priorities, it might not longer be true that there is a positional winning strategy. However, if such games are derived from the difference hierarchy, this property still holds true.
gzipped PostScript text

The complexity of independence-friendly fixpoint logic

This paper, written with
Stephan Kreutzer, studies what it says.
We study the complexity of model-checking for the fixpoint extension of Hintikka and Sandu's independence-friendly logic. We show that this logic captures \EXPTIME; and by embedding PFP, we show that its combined complexity is \EXPSPACE-hard, and moreover the logic includes second order logic (on finite structures).
The full version will appear in a volume of Proceedings of FotFS V: Infinite Games; here is the gzipped PostScript preprint.

An extended abstract, with a slightly simpler logic, appeared in CSL '05 (proceedings in LNCS). Here is the gzipped PostScript text.


On independence-friendly fixpoint logics

This is the somewhat revised and expanded journal version of the
CSL'03 paper below, invited for an issue of Philosophia Scientiae devoted to Logic and Game Theory.

Here is the published version (PDF) (280 kB), and the current version (gzipped PostScript) (150kB), which fixes a couple of minor errors.


Parity of Imperfection or Fixing Independence

The cutesy title was a feeble attempt at recalling the spirit of the 18th century with some even feebler punning. Oh well.
This paper, which appeared in CSL '03 (proceedings in
LNCS) is part of the programme of developing modal and temporal version of independence-friendly logic. It is mostly concerned with the difficulties of adding fixpoint constructors to IF logics.
We introduce a fixpoint extension of Hintikka and Sandu's IF (independence-friendly) logic. We obtain some results on its complexity and expressive power. We relate it to parity games of imperfect information, and show its application to defining independence-friendly modal mu-calculi.
Some typos in the published version have been fixed.
A journal version is given above.
gzipped PostScript text (136 kB).

Fixpoints, games and the difference hierarchy

This paper appeared in Theoretical Informatics and Applications 37 1-15 (2003). It is the journal version of the
CSL '99 and FICS '01 papers, without significant changes.
Drawing on an analogy with temporal fixpoint logic, we relate the arithmetic fixpoint definable sets to the winning positions of certain games, namely games whose winning conditions lie in the difference hierarchy over $\Delta^0_2$. This both provides a simple characterization of the fixpoint hierarchy, and refines existing results on the power of the game quantifier in descriptive set theory. We raise the problem of transfinite fixpoint hierarchies.
gzipped PostScript text (139 kB).

Independence-friendly modal logic and true concurrency

This paper, with
Sibylle Fröschle, studies the relationships between traditional concurrent equivalences and those induced by a modal analogue of independence-friendly logic. It is the extended journal version of the EXPRESS paper below, and appeared in Nordic Journal of Computing 9 102-117 (2002).
We consider modal analogues of Hintikka et al.'s `independence-friendly first-order logic', and discuss their relationship to equivalences previously studied in concurrency theory.
gzipped PostScript text (134 kB).

Enriching OCL using observational mu-calculus

This paper, with
Juliana Küster Filipe and Perdita Stevens, was presented at FASE 2002, with proceedings published in LNCS.
The Object Constraint Language is a textual specification language which forms part of the Unified Modelling Language\cite{UML1.4}. Its principal uses are specifying constraints such as well-formedness conditions (e.g. in the definition of UML itself) and specifying \emph{contracts} between parts of a system being modelled in UML. Focussing on the latter, we propose a systematic way to extend OCL with temporal constructs in order to express richer contracts. Our approach is based on observational mu-calculus, a two-level temporal logic in which temporal features at the higher level interact cleanly with a domain specific logic at the lower level. Using OCL as the lower level logic, we achieve much improved expressiveness in a modular way. We present a unified view of invariants and pre/post conditions, and we show how the framework can be used to permit the specification of liveness properties.
gzipped PostScript text (162kB).

On logical and concurrent equivalences

This paper, with
Sibylle Fröschle, appeared in the EXPRESS '01 workshop in Aalborg; its journal version is the NJC paper above (q.v.).

gzipped PostScript text (126 kB).


Some remarks on transfinite fixpoint alternation

A note for the Fixpoints in Computer Science 2001 workshop in Florence. It asks questions about how transfinite fixpoint alternation might be defined, and points out some problematic issues. It was included (with improvements) as the final section of the
TIA paper above.

gzipped PostScript text (47 kB).


Independence: logic and concurrency

This paper appeared in CSL 2000, published in
LNCS. The version here is the one that appeared in the proceedings; a full version is still in progress.
We consider Hintikka et al.'s `independence-friendly first-order logic'. We apply it to a modal logic setting, defining a notion of `independent' modal logic, and we examine the associated fixpoint logics.
gzipped PostScript text (95 kB).

Modal logics and mu-calculi: an introduction

This is a preprint (February 2000) of a chapter by
Colin Stirling and myself in the Handbook of Process Algebra, to be published by Elsevier in 2000 or 2001.
Abstract: We briefly survey the background and history of modal and temporal logics. We then concentrate on the modal mu-calculus, a modal logic which subsumes most other commonly used logics. We provide an informal introduction, followed by a summary of the main theoretical issues. We then look at model-checking, and finally at the relationship of modal logics to other formalisms.
The style of this article is relatively high-level and untechnical: my aim while writing was to make it as much like bedtime reading as the subject can manage! Comments on the success, failure, desirability etc. of this aim would be much appreciated, to inform the next time I try to write a survey.

Here is the text (144 kB).


Fixpoint alternation: Arithmetic, transition systems, and the binary tree

This paper is in Theoretical Informatics and Applications Vol 33 no. 4/5 1999, pp. 341-356. It is the journal version of the
STACS 98 and FICS papers.
We provide an elementary proof of the fixpoint alternation hierarchy in arithmetic, which in turn allows us to simplify the proof of the modal mu-calculus alternation hierarchy. We further show that the alternation hierarchy on the binary tree is strict, resolving a problem of Niwinski.
gzipped PostScript text (95 kB).

Fixpoint alternation and the game quantifier

This paper appeared in CSL '99, published in
LNCS. It's essentially filling in a link that has been more or less implicit for a long time; not deep, but quite pretty, I think. Some of the open questions are quite interesting. This version has been superseded by the journal version above.

The text here is not quite what appeared in LNCS---it contains fewer typos and better notation!

gzipped PostScript text (85 kB).


Fixpoint alternation on trees

This short paper appeared in the Fixpoints in Computer Science workshop in Brno, 1999.
We show that Niwinski's fixpoint hierarchy on tree algebras with intersection is strict.
gzipped PostScript text (47 kB).

Simplifying the modal mu-calculus alternation hierarchy

This paper, a version of which appeared in STACS 98, provides a significant improvement to the next paper. It is more or less self-contained, but will be easier to read if you've already read the main paper.
In [the next paper], the strictness of the modal mu-calculus alternation hierarchy was shown by transferring a hierarchy from arithmetic; the latter was a corollary of a deep and highly technical analysis by Lubarsky. In this paper, we show that the alternation hierarchy in arithmetic can be established by entirely elementary means; further, simple examples of strict alternation depth n formulae can be constructed, which in turn give very simple examples to separate the modal hierarchy. Moreover, these examples turn out to be exactly the properties defining the existence of winning strategies in parity games.
gzipped PostScript text (80 kB).

The modal mu-calculus alternation hierarchy is strict

The ideas of the STACS 96 paper actually achieve something in this paper, an earlier version of which appeared in CONCUR '96, which settles an open problem about the modal mu-calculus, namely, whether the alternation hierarchy is a strict hierarchy in expressive power. The file given here is a preprint of the journal version that appeared in Theoretical Computer Science 195 133-153 (1998).
ABSTRACT: One of the open questions about the modal mu-calculus is whether the alternation hierarchy collapses; that is, whether all modal fix-point properties can be expressed with only a few alternations of least and greatest fix-points. In this paper, we resolve this question by showing that the hierarchy does not collapse.
gzipped PostScript text (111 kB).

An effective tableau system for the linear time mu-calculus

This paper appeared in ICALP '96. The text given here is a slightly earlier tech report (ECS-LFCS-95-337). The paper was written with Javier Esparza and Angelika Mader of the
Technische Universität München. It describes - well, the title says it all. Probably only of interest to the specialist.
ABSTRACT: We present a tableau system for the model checking problem of the linear time mu-calculus. It improves the system of Stirling and Walker by simplifying the success condition for a tableau. In our system success for a leaf is determined by the path leading to it, whereas Stirling and Walker's method requires the examination of a potentially infinite number of paths extending over the whole tableau.
gzipped PostScript text (59 kB).

On the expressivity of the modal mu-calculus

The paper published in STACS '96 was a shortened version of a technical report, the text of which is given here. The differences are that in the published version, all references to Petri nets have been removed, and replaced by non-deterministic register machines---this reduces the number of definitions required, but also removes one or two mildly entertaining propositions.
ABSTRACT: We analyse the complexity of the sets of states, in certain classes of infinite systems, that satisfy formulae of the modal mu-calculus. Improving on some of our earlier results, we establish a strong upper bound (namely \Delta^1_2). We also establish various lower bounds and restricted upper bounds, incidentally providing another proof that the mu-calculus alternation hierarchy does not collapse at level 2.
gzipped PostScript text (55 kB).

Verifying temporal properties of systems

This text was provided to accompany two lectures given at the XXI-st International Winter School on Theoretical and Practical Aspects of Computer Science (SOFSEM), Milovy (Czech Republic) in December 1994. It is basically an updated version of the
next paper, concentrating on the practical side, but also giving more explanation of the underlying theory. It is probably the best quick introduction to the theory and practice of tableau model-checking as practised at Edinburgh.
ABSTRACT: The modal mu-calculus is a powerful logic with which to express properties of concurrent systems. There are algorithms which allow one to check whether a finite system satisfies a formula of this logic; but many interesting systems are infinite, or at least potentially infinite. In this paper we present an approach to verifying infinite systems. The method is a tableau style proof system, using the modal mu-calculus as the logic. We also describe a software tool to assist humans in using the method.
gzipped PostScript text (78 kB).

A proof assistant for symbolic model checking

This paper, presented at CAV '92 (Proceedings: Springer LNCS 663, 316-329), is currently the only published description of the software tool I am developing to assist people in the use of tableau verification techniques. See also
the previous paper.
ABSTRACT: We describe a prototype of a tool to assist in the model-checking of infinite systems by a tableau-based method. The tool automatically applies those tableau rules that require no user intervention, and checks the correctness of user-applied rules. It also provides help with checking the well-foundedness conditions required to prove liveness properties. The tool has a general tableau-manager module, and may use different reasoning modules for different models of systems; a module for Petri nets has been implemented.
gzipped PostScript text (70 kB).

Local model checking for infinite state spaces

This paper, written with
Colin Stirling, appeared in Theoretical Computer Science 96 (1992) 157-174. It is our standard journal reference for the technique of verifying modal mu-calculus properties by tableau-style local model-checking. It contains (most of) the material in the Advances in Petri Nets paper and in the CONCUR '90 paper.

If you're interested in the soundness and completeness proofs for the tableau system, this paper contains Stirling's versions of the proofs; my versions are (tersely) in the Advances paper and (verbosely) in my thesis. Some people prefer one, some the other...

ABSTRACT: We present a sound and complete tableau proof system for establishing whether a set of elements of an arbitrary transition system model has a property expressed in (a slight extension of) the modal mu-calculus. The proof system, we believe, offers a very general verification method applicable to a wide range of computational systems.
gzipped PostScript text (81 kB).

Verifying temporal properties of processes

This paper, written with
Colin Stirling, was presented at CONCUR '90 (Proceedings: ed. Baeten and Klop, Springer LNCS 458, 115-125). It describes the tableau system for local model-checking as applied to CCS processes. It is strictly contained in the TCS paper. (I'm afraid the typography is fairly disgusting, as the paper was written in LaTeX, and that was years before I switched to LaTeX and coerced it into producing something reasonable.)

gzipped PostScript text (57 kB).


Proving Temporal Properties of Petri Nets

This paper was published in Advances in Petri Nets 1991, (ed. G. Rozenberg), Springer LNCS 524. It is strictly contained in my
thesis.
ABSTRACT: We present a sound and complete tableau system for proving temporal properties of Petri nets, expressed in a propositional modal mu-calculus which subsumes many other temporal logics. The system separates the checking of fix-points from the rest of the logic, which allows the use of powerful reasoning, perhaps specific to a class of nets or an individual net, to prove liveness and fairness properties. Examples are given to illustrate the use of the system. The proofs of soundness and completeness are given in detail.

KEYWORDS: Petri nets, temporal logic, tableau systems, model-checking.

Here is the text (80 kB).

Preprints; tech reports not otherwise published; miscellany