Publications and Presentations

This page lists papers and talks in my various areas of interest. Because I tend to work on the borders between areas, it's hard to split the topics up meaningfully. However, one clear distinction, at least by intended audience, is between computer science and mathematics on the one hand, and my recent (and, I hope, future) forays into natural language on the other, so those are the two divisions.

Within each major division, the organization is reverse chronological.

To indicate the general type of the papers and talks, I use the following codes:

Rather few of the slides from my talks are currently up here, as I only recently came round to the idea of making slides generally available -- if you remember a talk that I gave and would like to see the slides, drop me an email.

For things published in the last decade or so, I took care to retain publication rights. For very old materials, the copies here may be a technical violation of the publishers' copyrights. I don't suppose they care any more than I do. In the case of published papers, the file here is usually the last version I sent, rather than the published version -- there should be no differences other than formatting and the publisher's logo.

Recent papers are all PDF; older papers may be gzipped PostScript.

Natural Language

(UC) New data on !Xoon A-raising

Poster at OCP21 in Leipzig, February 2024.

(J) The Sound of a Spherical Cow

This article, which appeared in Phonology 34(2) 347-362 (2017), is a methodological essay on the use of simulations in phonology. It looks at some old and more recent work by others, and my own simulations from some of the conference presentations below, to articulate how one should apply standard scientific practice in phonological simulations. The abstract is
I consider the use of computational simulations in phonology, and the benefits and dangers of making abstractions, or failing to make abstractions. I argue that the potential of simulation studies is not yet realized as it could be.
The not-quite-final preprint is SphericalCow.pdf.

The offical published version is here.

(J) Clicks, Concurrency, and Khoisan

This paper, which appeared in Phonology 31(1) 1-49 (2014), is the article arising from the MFM talk below. The abstract is
I propose that the notions of segment and phoneme be enriched to allow, even in classical theories, some concurrent clustering. My main application is the Khoisan language ǃXóõ, where by treating clicks as phonemes concurrent with phonemic accompaniments, the inventory size is radically reduced, so solving the problems of many unsupported contrasts. I show also how phonological processes of ǃXóõ can be described more elegantly in this setting, and provide support from metalinguistic evidence and experiment evidence of production tasks. I describe a new allophony in ǃXóõ. I go on to discuss other, some rather speculative, applications of the concept of concurrent phoneme. The article also provides a comprehensive review of the segmental phonetics and phonology of ǃXóõ, together with previous analyses.
This version is not quite the version sent to the journal; it has minor differences in typography, and one or two additional paragraphs and tables that were cut to save space. It's available in three formats:

clickscon-a4.pdf is suitable for printing on A4 paper.
clickscon-2up.pdf is formatted for A5 paper and then arranged 2-up on A4 -- the type is larger than that obtained by doubling up the previous version, so should be comfortable to read in print.
clickscon-a5.pdf is the single page A5 format, and is probably the most comfortable for reading on screen.

The published official version is here.

(UC) Stress-testing GP - the phonology of Taa

This poster was presented at the 20th Manchester Phonology Meeting in May 2012.

This is a different take on !Xoo or Taa - here I wonder what it looks like trying to do a GP-based analysis. The tentative conclusion (the work is early) is that the representation does not raise serious problems, but describing the phonological processes is challenging.

Here is the poster.

(UC) Where's the contrast?

This poster was presented at the 19th Manchester Phonology Meeting in May 2011.

It's a simple simulation experiment, aiming to show that effects that have been claimed to require features, can instead arise from purely phonetic effects. It is a development of part of the following talk.

Here is the poster.

(UC) Phonetic Universals - Abstraction vs detail and -etics vs -ology

This was a talk at the conference on Phonetic Universals conference in Leipzig in November 2010. It discussed aspects of simulation, and some experiments also presented in the poster above. Slides are available, but not very useful as the presentation relied on live simulations.

(UC) Acquisition and Complexity of Phonemes and Inventories

This poster was presented at the workshop on Computational Modelling of Sound Pattern Acquisition in Edmonton (February 2010), and then at the 18th Manchester Phonology Meeting in May 2010

It's a follow-up to the talk at the previous MFM. Using simulations, it looks at how the difficulty of learning large vowel systems (such as that of !Xoo) depends on whether they are learned simply as lots of vowels, or with internal structure (such as the voice qualities used in the !Xoo system). This gives some support to the claim that the !Xoo vowel system is just too complicated to learn, if given the traditional analysis.

Here is the poster.

(UC) OT or not OT - is that a question?

This talk was presented at the 7th Old World Conference on Phonology in Nice (January 2010). It's a talk designed for the end of a long day (as it was scheduled), which goes through some (well known) arguments for and against OT, and then looks at how these apply to OT's original poster child, Imdlawn Tashlhiyt Berber syllabification. It concludes with a simple re-writing account of ITB syllabification that encapsulates what, in my view, is a very plausible account of how speakers might actually do syllabification (as opposed to solving a constraint set over several million candidates).

Here are the slides.

(UC) Clicks, Concurrency and the Complexity of Khoisan

This talk was presented at the 17th Manchester Phonology Meeting in May 2009. It argues that the notoriously large consonant and vowel inventories of Khoisan languages are really due to an inappropriate analysis: rather, one should slightly broaden the notion of phoneme to include segments that occur concurrently with other segments as well as sequentially. A fair part of the argument is, of course, aesthetic, but phonological and psycholinguistic arguments are also adduced.

Here is the printed handout; the jokes won't make too much sense without the context of voice-over and conference, and you can't see the gratuitous special effects, but the argument should be clear. A formal article is in progress - if you are interested in seeing (and commenting on!) the draft, send me an email.

(UC) Modelling, Formality and the Phonetics-Phonology Interface

Originally, this was to be a talk at the 14th MFM, but owing to illness I was unable to present it. Instead, it became a poster (A4 version, really needs colour) presented at the 5th Old World Conference on Phonology in Toulouse (January 2008). It's really a reply to the Port and Leary paper ‘Against Formal Phonology’, but is also an indication of things I might do. (See above for a concrete instantiation.) There is also a four page abstract which goes into a little more detail, but still without any actual applications.

(MS) The Absurdity of Vastness

In 1984, Terence Langendoen and Paul Postal published The Vastness of Natural Languages. I only came across it in 2008, and read it with ever increasing surprise. As catharsis, I wrote a long article giving my mathematician's view of its arguments, and in the process found out a lot more about both the history of set theory and my own attitude to it. I put it here in case anybody might stumble across it and find it interesting. It might possibly make an interesting read for a graduate seminar in theoretical linguistics - if you want to use it for such a purpose, or indeed for any other, please get in touch. It is still very much a manuscript, so please don't distribute other than via this page.

Here is the PDF.

Computer Science, Logic, Mathematics

(RC) Team building in dependence

This paper appeared in CSL'13.
Hintikka and Sandu's Independence-Friendly Logic was introduced as a logic for partially ordered quantification, in which the independence of (existential) quantifiers from previous (universal) quantifiers is written by explicit syntax. It was originally given a semantics by games of imperfect information; Hodges then gave a (necessarily) second-order Tarskian semantics. More recently, Väänänen (2007) has proposed that the many curious features of IF logic can be better understood in his Dependence Logic, in which the (in)dependence of variables is stated in atomic formula, rather than by changing the definition of quantifier; he gives semantics in Tarskian form, via imperfect information games, and via a routine second-order perfect information game. He then defines Team Logic, where classical negation is added to the mix, resulting in a full second-order expressive logic. He remarks that no game semantics appears possible (other than by playing at second order).

In this article, we explore an alternative approach to game semantics for DL, where we avoid imperfect information, yet stay locally apparently first-order, by sweeping the second-order information into longer games (infinite games in the case of countable models). Extending the game to Team Logic is not possible in standard games, but we conjecture a move to transfinite games may achieve a `natural' game for Team Logic.

Here is the official version.

For those who find the LIPICS style distasteful, here is a version (with identical content) in my standard format for A4 paper: backtrack.pdf.

(RC) Recursive checkonly QVT-R transformations with general when/ and where/ clauses via the modal mu calculus

This paper, with Perdita Stevens, discusses and solves a problem with the semantics of recursive relations in the modelling language QVT-R. It appeared in FASE 2012.
In earlier work we gave a game-based semantics for checkonly QVT-R transformations. We restricted when and where clauses to be conjunctions of relation invocations only, and like the OMG standard, we did not consider cases in which a relation might (directly or indirectly) invoke itself recursively. In this paper we show how to interpret checkonly QVT-R - or any future model transformation language structured similarly - in the modal mu calculus and use its well-understood model-checking game to lift these restrictions. The interpretation via fixpoints gives a principled argument for assigning semantics to recursive transformations. We demonstrate that a particular class of recursive transformations must be ruled out due to monotonicity considerations. We demonstrate and justify a corresponding extension to the rules of the QVT-R game.
Here is the PDF.

(TR) Fixpoint alternation and the Wadge Hierarchy

This paper, written with Sandra Quickert and Jacques Duparc, takes up a problem raised in the TIA paper below. It will be (we hope) the journal version of the CSL paper below; however, it currently relies on unpublished results of Duparc, and we would like to wait until those are published before submitting.

It is perhaps worth warning that this is a long and very difficult paper, especially the second part, which has been greatly expanded since the conference version. If you just want to know the results, go to the conference paper.

In earlier work Bradfield found a link between finite differences formed by Σ02 sets and the mu-arithmetic introduced by Lubarski. 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 Σ02 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. In the second part, we use the more refined Wadge hierarchy to understand further the links established in the first part, by connecting game-theoretic operations to operations on Wadge degrees.
Here is the paper.

This version can be cited as:
Bradfield, J., Duparc, J. and Quickert, S.: Fixpoint Alternation and the Wadge Hierarchy, University of Edinburgh Informatics Report Series EDI-INF-RR-1366 (2010).

(J) A general definition of malware

This paper, with Simon Kramer, uses temporal logic to try to characterize the notion of malware (as in computer viruses). Note that Simon is the main and corresponding author, so if you have queries contact him - unless they're about the formal details, in which case you can also ask me.
We propose a general, formal definition of the concept of malware (malicious software) as a single sentence in the language of a certain modal logic. Our definition is general thanks to its abstract formulation, which, being abstract, is independent of—but nonetheless generally applicable to—the manifold concrete manifestations of malware. From our formulation of malware, we derive equally general and formal definitions of benware (benign software), anti-malware (“antibodies” against malware), and medware (medical software or “medicine” for affected software). We provide theoretical tools and practical techniques for the detection, comparison, and classification of malware and its derivatives. Our general defining principle is causation of (in)correctness.
Here is the published paper, which is available on open access from SpringerLink.

The reference is:
Kramer, S. and Bradfield, Julian C.: A general definition of malware. Journal in Computer Virology 6(2): 105-114 (2010).

(RC) Model-checking games for fixpoint logics with partial order models

This paper, with Julian Gutierrez, discusses model-checking for the logic SFL that Julian develops in his Ph.D. A journal version is in final revision.
We introduce model-checking games that allow local second-order power on sets of independent transitions in the underlying partial order models wh ere the games are played. Since the one-step interleaving semantics of such models is not considered, some problems that may arise when using interleaving semantics are avoided and new decidability results for partial orders are achieved. The games are shown to be sound and complete, and therefore determined. While in the interleaving case they coincide with the local model-checking games for the μ-calculus (Lμ), in a non-interleaving setting they verify properties of Separation Fixpoint Logic (SFL), a logic that can specify in partial orders properties not expressible with Lμ. The games underpin a novel decision procedure for model-checking all temporal properties of a class of infinite and regular event structures, thus improving previous results in the literature.

Here is the preprint.

The reference is:
Gutierrez, J. and Bradfield, J.: Model-checking games for fixpoint logics with partial order models, in: Bravetti, M. and Zavattaro, G. (Eds.): Proc. CONCUR 2009 LNCS 5710, Springer 2009, 354-368.

(J) 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).
A preliminary version appeared as the CSL '05 paper below; this version was published in the post-proceedings of a meeting on Infinite Games in the series Foundations of the Formal Sciences.

Here is the published PDF file.

The reference is:
Bradfield, J. and Kreutzer, S.: The complexity of independence-friendly fixpoint logic, in: Stefan Bold, Benedikt Löwe, Thoralf Räsch, Johan van Benthem (eds.), Foundations of the Formal Sciences V, Infinite Games 39-62. [Studies in Logic 11]. London: College Publications (2007).

(BC) Modal Mu-Calculi

This is a chapter for the (very expensive) Handbook of Modal Logic, 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).

The reference is:
Bradfield, Julian and Stirling, Colin. Modal mu-calculi. In: P. Blackburn, J. van Benthem and F. Wolter (eds.), The Handbook of Modal Logic pp. 721-756. Elsevier (2006).

(J) Independence: logics and concurrency

This is a considerably revised and expanded version of the CSL '00 paper below. It appeared 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.

The reference is:
Independence: logics and concurrency. In: Tuomo Aho and Ahti-Veikko Pietarinen (eds). Truth and Games: Essays in Honour of Gabriel Sandu (Acta Philosophica Fennica 78) 47-70. Helsinki: Societas Philosophica Fennica. (2006)

(RC) 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 [Bra03] Bradfield found a link between finite differences formed by Σ02 sets and the mu-arithmetic introduced by Lubarski [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 Σ02. 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 reference is:
Bradfield, J. C., Duparc, J. and Quickert, S., Transfinite extension of the mu-calculus. In: Proc. 14th Int. Conf. on Computer Science Logic (CSL '05)} LNCS 3634 384-396. Springer (2005).

A much expanded version is currently available as a technical report.

(RC) The complexity of independence-friendly fixpoint logic

This paper, in CSL '05 (proceedings in LNCS), was the extended abstract of the full paper above, with some simplications to the logic. Please work from the full paper. For the record, here is the gzipped PostScript text of the conference version.

(J) 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. The paper 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.

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

The reference is:
Bradfield, J. C. On independence-friendly fixpoint logics. Philosophiae Scientiae 8(2) 125-144 (2004).

(RC) 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 the preliminary version of the full paper immediately above. Please work from the journal version. For the record, here is the gzipped PostScript text of the conference version.

(J) Fixpoints, games and the difference hierarchy

This 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 Δ02. 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.
The problem of transfinite fixpoint hierarchies was finally dealt with in the CSL '05 paper above.

Here is the gzipped PostScript text (139 kB).

The reference is:
Bradfield, J. C. Fixpoints, games and the difference hierarchy. Theoretical Informatics and Applications 37 1-15 (2003).

(J) 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.
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).

The reference is:
Bradfield, J. C. and Fröschle, S. B. Independence-friendly modal logic and true concurrency. Nordic Journal of Computing 9 102-117 (2002).

(RC) Enriching OCL using observational mu-calculus

This paper, with Juliana Küster Filipe (now Juliana Bowles) 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).

The reference is:
Bradfield, J.C., Küster Filipe, J. and Stevens, P. Enriching OCL using observational mu-calculus, Proc. of the 5th International Conference on Fundamental Approaches to Software Engineering (FASE) (R.-D. Kutsche and H. Weber, eds.), LNCS 2306 203--217 (2002).

(RW) 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. Please work from the journal version. Here is the original workshop paper, as gzipped PostScript text.

(RW) 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. The questions were answered in the CSL '05 paper above. Here is the gzipped PostScript text.

(RC) Independence: logic and concurrency

This paper appeared in CSL 2000, published in LNCS. A considerably revised and expanded version appeared several years later as the Sandu Festschrift paper above - please work from that. Here is the original conference paper, as gzipped PostScript text.

(BC) Modal logics and mu-calculi: an introduction

This is a preprint of a chapter by Colin Stirling and myself in the (very expensive) Handbook of Process Algebra, published by Elsevier.
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!

Here is the text (144 kB).

The reference is:
Bradfield, J. C. and Stirling, C. P. Modal logics and mu-calculi: an introduction. In Handbook of Process Algebra (eds. J. Bergstra, A. Ponse and S. Smolka) 293--330. Elsevier (2001).

(J) Fixpoint alternation: Arithmetic, transition systems, and the binary tree

This paper 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).

The reference is:
Bradfield, J.C. Fixpoint alternation: Arithmetic, transition systems, and the binary tree. Theoretical Informatics and Applications 33(4/5) 341-356 (1999).

(RC) 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).

(RW) Fixpoint alternation on trees

This short paper appeared in the Fixpoints in Computer Science workshop in Brno, 1999. It was absorbed into the TIA journal paper above. Here is the original gzipped PostScript text.

(RC) Simplifying the modal mu-calculus alternation hierarchy

This paper, which appeared in STACS 98, provided the simple basis for the proof of the alternation hierarchy theorem that I had unaccountably failed to see in the original paper. A journal version appeared as the TIA paper above - please work from that. Here is the original gzipped PostScript text.

(J) The modal mu-calculus alternation hierarchy is strict

This paper settles one of the (then) three major open problems 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.
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.
This paper should be read in conjunction with the TIA paper above, which removes the quite unnecessary use in this paper of a very technical theorem of Lubarsky.

Here is gzipped PostScript text (111 kB).

The reference is:
Bradfield, J.C. The modal mu-calculus alternation hierarchy is strict. Theoretical Computer Science 195 133-153 (1998).

(RC) 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. 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).

The reference for the published version is:
Bradfield, J. C., Esparza, J. and Mader, A. An effective tableau system for the linear time mu-calculus, Proc. 25th Int. Coll. on Automata, Languages and Programming (ICALP '96) LNCS 1099 98--109 (1996).

(RC) The modal mu-calculus alternation hierarchy is strict

This CONCUR '96 paper was the conference announcement. It is an extended abstract of the TCS paper. For old time's sake, here is the conference version as gzipped PostScript.

(RC) 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 Δ12). 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.
Within a couple of months of submission, this paper became redundant when I finally proved the alternation hierarchy theorem. So it's here purely for historical interest.

The tech report was gzipped PostScript text (55 kB).

The reference for the conference version is:
Bradfield, J.C. On the expressivity of the modal mu-calculus. Proc. 13th Annual Symposium on Theoretical Aspects of Computer Science (STACS '96) LNCS 1046 479-490 (1996).

(MS) 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 in the early 1990s.
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).

(RC) A proof assistant for symbolic model checking

This paper, presented at CAV '92 (Proceedings: Springer LNCS 663, 316-329), describes a brief excursion into actual implementation. 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).

The reference is:
Bradfield, J.C. A proof assistant for symbolic model-checking. Proc. Int. Conf. on Computer Aided Verification '92. LNCS 663 316-329 (1993).

(J) 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).

The reference is:
Bradfield, J.C. and Stirling, C.P. Local model checking for infinite state spaces. Theoret. Comput. Sci. 96 157--174 (1992).

(Book) Verifying Temporal Properties of Systems

This is my thesis, subsequently published. It has its own page.

(RC) 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).

(J) 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).

The reference is:
Bradfield, J. C. Proving temporal properties of Petri nets Advances in Petri Nets 1991 LNCS 524 29--47 (1991).