Sections:
Here is the PDF text (300kB).
Here is a gzipped PostScript preprint.
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
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.
Here is the published version (PDF) (280 kB), and the current version (gzipped PostScript) (150kB), which fixes a couple of minor errors.
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.
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).
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 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).
gzipped PostScript text (126 kB).
gzipped PostScript text (47 kB).
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).
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).
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 text here is not quite what appeared in LNCS---it contains fewer typos and better notation!
gzipped PostScript text (85 kB).
We show that Niwinski's fixpoint hierarchy on tree algebras with intersection is strict.gzipped PostScript text (47 kB).
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).
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).
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).
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).
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).
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).
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.