Within each major division, the organization is reverse chronological.

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

**J**article refereed to journal standards (whether in a journal or a one-off book).**BC**book chapter in surveys, handbooks etc.**RC/RW**refereed full conference or workshop paper.**IC/IW**invited conference or workshop talk/paper.**UC/UW**unrefereed conferences or workshops, including those with selection only by short abstract. This also includes Dagstuhl Seminar presentations.**TR**technical report, usually an incipient journal paper.**S**presentations given as departmental/faculty seminars in various institutions -- including recreational or tutorial talks.**MS**anything else, whether ultimately intended to become a journal article, or just something I felt like writing.

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.

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.

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.

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.

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.

Here are the slides.

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.

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).Here is the official version.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.

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

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.

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 ΣHere is the paper.^{0}_{2}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 Σ^{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. 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.

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

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

We introduce model-checking games that allowlocalsecond-order power onsetsof 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.

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

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

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)

In [Bra03] Bradfield found a link between finite differences formed by Σgzipped PostScript text^{0}_{2}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 Σ^{0}_{2}. 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.

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.

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

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.

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

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

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

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

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

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

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

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

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 Δ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.^{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.

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

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

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

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

gzipped PostScript text (57 kB).

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.Here is the text (80 kB).KEYWORDS: Petri nets, temporal logic, tableau systems, model-checking.

The reference is:

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