I briefly reviewed some areas here, trying to focus on ideas that would appeal to someone with a background in advanced mathematical logic.
Finite Model Theory
The simplest restriction of classical model theory from the viewpoint
of computer science is to study structures over a finite universe.
These structures occur in the form of relational databases, graphs,
and other combinatorial objects arising everywhere in computer
science. The first observation is that several fundamental theorems of
first-order model theory fail when restricted to finite models. These
include the compactness theorem, Godel's completeness theorem, and
ultraproduct constructions. Trakhtenbrot showed that unlike classical
first order logic, satisfiability over finite models is undecidable.
The fundamental tools in this area are Hanf locality, Gaifman
locality, and numerous variations on Ehrenfeucht-Fraisse games. The
topics studied include infinitary logics, logics with counting, fixed
point logics, etc. always with a focus on finite models. There is work
focusing on expressivity in finite-variable fragments of first-order
logic and these logics have characterisations via pebble-games. Another direction of enquiry is to identify properties of classical logics that survive the restriction to finite models. A recent result in that direction from Rossman shows that certain homomorphism preservation theorems still hold over finite models.
- Finite Model Theory, Ebbinghaus and Flum
- Elements of Finite Model Theory, Libkin
- On winning strategies in Ehrenfeucht-Fraisse games, Arora
and Fagin, 1997.
- Homomorphism preservation theorems, Rossman
The propositional $\mu$-calculus
A line of work from the late 60s showed that numerous properties of
programs could be expressed in extensions of propositional logic that
supported reasoning about fixed points. The modal-$\mu$ calculus is
one logic developed in this period that has found a wide range of
applications in automated formal methods. A lot of formal methods is
connected to temporal logic, or Hoare-style logics and much of this
can be viewed in terms of the $\mu$-calculus. In fact, I have heard it
said that the $\mu$-calculus is the assembly language of temporal
logics.
In his paper introducing the $\mu$-calculus, Kozen gave an
axiomatization and only proved it sound and complete for a restricted
fragment of the logic. The completeness proof was one of the great
open problems in logical computer science until Walukiewicz gave a
proof (based on infinite automata). The model theory of the
$\mu$-calculus has many rich results. Similar to van Benthem's theorem
for modal logic, Janin and Walukiewicz proved that the $\mu$-calculus
is expressively equivalent to the bisimulation invariant fragment of
monadic second order logic. The $\mu$-calculus has also been
characterised in terms of parity games and automata over infinite
trees. The satisfiability problem for this logic is EXPTIME complete
and Emerson and Jutla showed that the logic has the small model
property. Bradfield showed that the alternation hierarchy of the $\mu$-calculus is strict, while Berwanger showed that the variable hierarchy is also strict. Important classical tools used in this area are Rabin's theorem and
Martin's determinacy theorem.
- Results on the propositional $\mu$-calculus, Kozen, 1983
- Rudiments of $\mu$-calculus Arnold and Niwinski, 2001
- Completeness of Kozen's Axiomatisation of the Propositional
$\mu$-Calculus, Walukiewicz 1995
- Modal logics and $\mu$-calculi, Bradfield and Stirling, 2001
- The modal mu-calculus alternation hierarchy is strict, Bradfield, 1996
- The variable hierarchy of the mu-calculus is strict, Berwanger, E. Grädel, and G. Lenzi, 2005
Linear Temporal Logic
Linear temporal logic was adopted from philosophical logic into
computer science for reasoning about the behaviour of computer
programs. It was considered a good logic because it could express
properties such as invariance (absence of errors) and termination. The
proof theory of temporal logic was developed by Manna and Pnueli (and
others, later) in their articles and books. The model checking and the
satisfiability problem for LTL can both be solved in terms of automata
over infinite words.
Pnueli also proved fundamental resuls about LTL in his original paper
introducing the logic for reasoning about programs. Vardi and Wolper
gave a much simpler compilation of LTL formulae into Buchi automata.
The connection to temporal logic has led to intense study of
algorithms for efficiently deriving automata from LTL, and for
determinization and complementation of Buchi automata. Kamp's theorem
shows that LTL with since and until modalities is expressively
equivalent to monadic first-order logic with an order relation. There
is ongoing work extending these results to logics over dense linear
orders and time intervals. Etessami and Wilke developed a variation of Ehrenfeucht-Fraisse games for LTL and used them to show that the until hierarchy is strict. Another line of work is to extend LTL to express arbitrary $\omega$-regular properties. This leads to the linear-time $\mu$-calculus, a linear-time counterpart of the modal $\mu$-calculus. Unlike the modal counterpart, the linear-time alternation hierarchy collapses at level 2.
- The temporal logic of programs, Pnueli 1977
- From Church and Prior to PSL, Vardi, 2008
- An automata-theoretic approach to linear temporal logic,
Vardi and Wolper, 1986
- The Temporal Logic of Reactive and Concurrent Systems:
Specification, Manna and Pnueli
- An Until hierarchy and other applications of an Ehrenfeucht-Fraïssé game for temporal logic, Etessami and Wilke, 2000
Computational-Tree Logics
Instead of a linear notion of time, the behaviour of a computer
program can be understood as a tree, leading to the notion of
computational tree logics. The simplest such logic, Computational Tree
Logic can be viewed as an alternation-free fragment of the
$\mu$-calculus. The difference between LTL and CTL led Emerson and
Halpern to develop CTL*, which allows reasoning about both properties
of states and traces.
The model checking problem for CTL over finite structures is in
polynomial time. The model checking problem for CTL* is EXPTIME
complete. The axiomatization of CTL* was a challenging open problem
that was finally resolved by Reynolds 2001. The analogue of van
Benthem's theorem for modal logic and Kamp's theorem for LTL is given
for CTL* by a theorem of Hafer and Thomas showing that CTL*
corresponds to a fragment of monadic second order logic over binary
trees. A later characterisation by Hirschfeld and Rabinovich is that
CTL* is expressively equivalent to the bisimulation-invariant fragment
of MSO with path quantification.
- "Sometimes" and "not never" revisited: on
branching versus linear time temporal logic, Emerson and Halpern,
1986
- On the Expressive Power of CTL, Moller, Rabinovich, 1999
- Computation tree logic CTL* and path quantifiers in the monadic
theory of the binary tree, Hafer and Thomas, 1987
- An Axiomatization of Full Computation Tree Logic, Reynolds,
2001
Languages of Infinite Words
The connection to LTL and the necessicity of modelling infinite
behaviour led to an intense study of $\omega$-languages, which are languages in which words are defined as functions from natural numbers to a finite alphabet. The community has studied properties of regular languages over infinite
words and developed several results analogous to the finite-word case. There are several surprises that show up, so we cannot just lift the finite-word results to the infinite-word case.
Some of my favourite results are the characterisiation of $\omega$-regular languages in terms of regular languages and analogues of the
Myhill-Nerode theorems. Staiger showed that you do not just get infinite word automata from an appropriately defined equivalence relation. This holds only for a specific sub-family of $\omega$-regular languages. Alpern and Schneider formalised the intuitive notions of safety and liveness of computer programs in terms of prefix-closed and limit-closed sets of $\omega$-words. Moreover, using elementary topology, they showed that every linear-time property can be expressed as the intersection of a safety and a liveness property. This result has significant practical consequences because it means that rather than build complex property checkers, it suffices to build a safety and a liveness checker. A further reduction shows that it is enough to build an invariance checker and a termination checker. The safety-liveness characterisation was extended to trees by Manolios and Trefler and more recently to sets of traces, in the hyperproperties framework, by Clarkson and Schneider.
- Infinite Words: Automata, Semigroups, Logic and Games, Perrin and Pin, 2004
- $\omega$-Languages, Staiger, 1997
- Beyond $\omega$-Regular Languages, Bojanczyk, 2010
- On syntactic congruences for ω—languages, Maler and Staiger, 1993
Automata on Infinite Words
Where there are languages, computer scientists will have automata. Enter the theory of automata over infinite words and infinite trees. It is extremely sad that although automata over infinite words appeared within two years of automata on finite words, this fundamental topic is rarely covered in standard computer science curricula. Automata over infinite words and trees provide a very robust approach to prove decidability of satisfiability for a very rich family of logics.
A fundamental result is that the different acceptance criteria for
infinite word automata are all equivalent. The basic problems of
union, intersection, and complement for $\omega$-automata are more
involved than their finite word counterparts and the details differ
with the acceptance criterion used. Safra gave a famously complex determinization algorithm for Buchi automata and significant work has been devoted to deriving a new and simpler construction. Rabin famously proved that the monadic second order theory of the binary tree is decidable. His proof uses automata and the cornerstone result is the determinization of Rabin automata. I have heard tell that Rabin's theorem is the mother of all decidability results in program verification.
- Decidability of Second-Order Theories and Automata on Infinite Trees, Rabin, 1969
- Automata on infinite objects, Thomas, 1988
- Automata: From Logics to Algorithms, Vardi, 2007
Infinite Games
Logical and infinite games are an active area of research. Games-theoretic notions show up in computer science all over the place in the duality between non-determinism and parallelism (alternation), a program and its environment, universal and existential quantification, box and diamond modalities, etc. Games turned out to be a great way to study properties of the various types of non-classical logics listed above.
As with acceptance criteria for automata, we have different winning conditions for games and many can be shown to be equivalent. Since you asked about classical results, the Borel Determinacy theorem and Gale-Stewart games often lie discreetly in the background of several game models we study. One pressing question of our times has been about the complexity of solving parity games. Jurdzinski gave a strategy-improvement algorithm and showed that deciding the winner was in the intersection of the complexity classes UP and coUP. The precise complexity of Jurdzinski's algorithm was open until Friedmann gave it an exponential-time lower bound in 2009.
- Deciding the winner in parity games is in UP ∩ co-UP, Jurdzinski, 1998
- Games for the μ-calculus, Niwinski and Walukiewicz, 1996
- An Exponential Lower Bound for the Parity Game Strategy Improvement Algorithm as We Know it, Friedmann, 2009
