Pointers for CS applications of logic

Question

I'm a grad student in math with a solid background in logic. I've taken a year-long graduate course in logic together with graduate courses on finite model theory and another on forcing and set theory. Most CS texts seem to assume only a very modest background in logic, which mostly covers basics of propositional logic and first-order logic.

I'd like to get some pointers on where to go for CS applications where heavier material from logic is being used. One interest of mine would be type theory and formal methods in general. Could anyone suggest some good readings past the introductory books on model checking and programming languages?

Answer 1

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.

1. Finite Model Theory, Ebbinghaus and Flum
2. Elements of Finite Model Theory, Libkin
3. On winning strategies in Ehrenfeucht-Fraisse games, Arora and Fagin, 1997.
4. 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.

1. Results on the propositional $\mu$-calculus, Kozen, 1983
2. Rudiments of $\mu$-calculus Arnold and Niwinski, 2001
3. Completeness of Kozen's Axiomatisation of the Propositional $\mu$-Calculus, Walukiewicz 1995
4. Modal logics and $\mu$-calculi, Bradfield and Stirling, 2001
5. The modal mu-calculus alternation hierarchy is strict, Bradfield, 1996
6. 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.

1. The temporal logic of programs, Pnueli 1977
2. From Church and Prior to PSL, Vardi, 2008
3. An automata-theoretic approach to linear temporal logic, Vardi and Wolper, 1986
4. The Temporal Logic of Reactive and Concurrent Systems: Specification, Manna and Pnueli
5. 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.

1. "Sometimes" and "not never" revisited: on branching versus linear time temporal logic, Emerson and Halpern, 1986
2. On the Expressive Power of CTL, Moller, Rabinovich, 1999
3. Computation tree logic CTL* and path quantifiers in the monadic theory of the binary tree, Hafer and Thomas, 1987
4. 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.

1. Infinite Words: Automata, Semigroups, Logic and Games, Perrin and Pin, 2004
2. $\omega$-Languages, Staiger, 1997
3. Beyond $\omega$-Regular Languages, Bojanczyk, 2010
4. 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.

1. Decidability of Second-Order Theories and Automata on Infinite Trees, Rabin, 1969
2. Automata on infinite objects, Thomas, 1988
3. 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.

1. Deciding the winner in parity games is in UP ∩ co-UP, Jurdzinski, 1998
2. Games for the μ-calculus, Niwinski and Walukiewicz, 1996
3. An Exponential Lower Bound for the Parity Game Strategy Improvement Algorithm as We Know it, Friedmann, 2009

Answer 2

Edmund M. Clarke, Orna Grumberg, Doron A. Peled: Model Checking. MIT Press 1999, is a nice book (for me) on model checking.

Glynn Winskel: The Formal Semantics of Programming Languages: an introduction. MIT Press 1994, is one of the standard textbooks on programming languages.

Mordechai Ben-Ari: Mathematical logic for computer science. Springer 2001, is perhaps what you are looking for.

Answer 3

Database theory is a sprawling field providing many applications of logic. Descriptive complexity and finite model theory are closely associated fields. As far as I can tell, these areas all tend to use algebraic styles of logic (following in the footsteps of Birkhoff and Tarski) rather than proof-theoretic. However, some of the work of Peter Buneman, Leonid Libkin, Wenfei Fan, Susan Davidson, Limsoon Wong, Atsushi Ohori, and other researchers who were working at UPenn in the 1980s-90s, did seek to unite programming language theory and databases. This seems to require being comfortable with both styles of logic. The same goes for more recent work by James Cheney and Philip Wadler.

In terms of specific references, the standard textbook is available online for convenient reference:

• Serge Abiteboul, Richard Hull, Victor Vianu. Foundations of Databases, 1995. http://webdam.inria.fr/Alice/

Unfortunately I don't know any up to date general textbooks or surveys covering this fast-moving field. I have found two older surveys useful. First,

• Jan Van den Bussche, Applications of Alfred Tarski's Ideas in Database Theory, CSL 2001. doi:10.1007/3-540-44802-0_2

shows how to connect the dots between Tarski and a specific subfield, constraint databases. Second,

• Victor Vianu, Databases and Finite-Model Theory, Descriptive Complexity and Finite Models: Proceedings of a DIMACS Workshop, 1996. http://leo.saclay.inria.fr/publifiles/gemo/GemoReport-107.ps.gz

pitches (1996-style) database theory to finite model theorists, and in the process highlights many interesting applications of logic in databases. For more recent work (such as the theory of XML, provenance, streaming models, or graph databases) reading highly-cited research papers is a reasonable approach.

Answer 4

Michael Huth and Mark Ryan: Logic in computer science, Cambridge University Press, 2004.

I recommend this book highly as a general introduction on how logic plays a role in computer science.

Answer 5

A key use of logic in CS is program logics, also called Hoare logics.

One good way of thinking about program logics is to see them as sub-calculi of ZFC set-theory (or whatever your preferred foundation of maths might be, e.g. second-order logic) that are just expressive enough to reason about programs in a given programming language, but not more. You can always reason about programs in ZFC set theory, but set theory has too much expressive power in the sense that it contains many formulae that are not really relevant for reasoning about programs (e.g. $2 \in \sqrt(\pi^{17})$ is a valid formula in ZFC that may or may not be true, depending on how you code up real numbers as sets). The superfluous expressive power is a disadvantage when thinking about program correctness because (simplifying a bit) it increases formula and proof size. So what we are looking for in the study of program logics are logics with succinct formulae and proofs.

A similar situation obtains in the study of modal logics which (simplfying a bit again) are not as expressive as first-order logic, but what they can express, they do express with shorter formulae and proofs.

Identifying suitable fragments of ZFC is not hard for simple programming languages, but gets rapidly more challenging as programming languages acquire more features. The last couple of years have seen substantial progress in this endeavour.

The paper An Axiomatic Basis for Computer Programming by T. Hoare is often seen as founding the study of program logics in earnest, is easy to read, and probably a good way to start venturing into the field. The same logic is studied in more detail in Winskel's book "Formal Semantics of Programming Languages" menioned by @vb le.

Type theory can be seen in a similar light. The key selling point of type-theory is the identification of proofs with (purely functional) programs, leading to a great economy of concepts and to powerful automation (in the form of type-inference and interactive theorem provers). The price for type theory's being an elegant way of organising proofs is that it does not appear to work all that well with programming languages that are not purely functional.

A recent and throughly modern text that introduces program logic in a type-theoretic tinged way is Software Foundations by Pierce et al. It'll lead you right near the (a) cutting edge of research in program verification and, as a textbook, probably gives a glimpse of how computer science and maths will be taught in the future.

Once a program logic has been developed for a language, the next step is automation, or partial automation: constructing proofs for non-trivial programs is labour intensive, and we would like machines to do as much of it as possible. Much current research in formal methods to do with such automation.

Answer 6

There is a very strong tradition of logic in computer science. The problems we study and the aesthetics of the computational logic community is not identical to that of the mathematical logic community. You are absolutely right that significant developments in model theory, the meta-theory of first-order logic and of set theory are not commonly used in computational logic. One can successfully research computational logi without seeing or using ultrafilters, non-standard analysis, forcing, the Paris-Harrington theorem, and a host of other fascinating concepts which are considered important in classical logic.

Just as one applies mathematical ideas to study logic as well as logical ideas to study mathematics, we apply logic to study computer science and as well as applying computational perspectives to study logic. This different focus has rather dramatic consequences for the types of results that are important for us.

Here is a quotation from John Baez about logic and computer science. I do not hold exactly the same view because I am not very familiar with advanced mathematical logic.

When I was an undergraduate I was quite interested in logic and the foundations of mathematics --- I was always looking for the most mind-blowing concepts I could get ahold of, and Goedel's theorem, the Loewenheim-Skolem theorem, and so on were right up there with quantum mechanics and general relativity as far as I was concerned. [...] I remember feeling at the time that logic had become less revolutionary than in it was in the early part of the century. It seemed to me that logic had become a branch of mathematics like any other, studying obscure properties of models of the Zermelo-Fraenkel axioms, rather than questioning the basic presumptions implicit in those axioms and daring to pursue new, different approaches. [...]

Anyway, it's now quite clear to me that I just hadn't been reading the right stuff. I think Rota has said that the really interesting work in logic now goes under the name of "computer science',[...] --Week 40, This Week's Find, John Baez

Logic in computer science is a vast and rapidly developing field. I find that every perspective of classical logic can be modified to derive some perspective on computational logic. The Wikipedia entry on mathematical logic splits the field into set theory, model theory, proof theory and recursion theory. You can esssentially take these areas and add a computational flavour to them and obtain a sub-field of computational logic.

Model Theory We like to study the model theory of non-classical logics and non-classical models of classical logic. By that I mean that we study modal, temporal and sub-structural logics, and that we study logics over trees, words, and finite models, as opposed to classical models like algebras. The two fundamental problems are satisfiability and model checking. Both have immense practical and theoretical significance. In contrast, these problems are less central in classical logic.

Proof theory We study the complexity and efficiency with which we can generate proofs in classical proof systems, as well as developing new, non-classical proof systems that are sensitive to complexity and efficiency considerations. Automated deduction studies machine-supported proof generation, broad speaking. The process may involve human interaction or be completely automatic. There is a lot of work on developing decision procedures for logical theories. Proof complexity focuses on the size of proofs and the computational complexity of generating proofs. There is a fascinating line of work relating programs to proofs, which combines with work descending from linear logic to develop proof systems, and consequently programming languages, that are resource sensitive.

Recursion theory Our recursion theory is complexity theory. Rather than studying what is computable we study how efficiently we can compute. There are many analogues of recursion theory in complexity theory, but the results and separations of recursion theory do not always hold for their complexity theoretic analogues. Instead of computable sets and an arithmetic hierarchy, we have polynomial time, the polynomial time hierarchy and polynomial space enclosing the hierarchy. Instead of bounded quantification in the arithmetic hierarchy, we have satisfiability and quantified Boolean formulae and bounded quantification of Boolean formulae.

The survey article

On the Unusual Effectiveness of Logic in Computer Science

is a good starting point to get a very high-level view of computational logic. I am going to list several, logically oriented fields of computer science. I hope that others will edit this answer and add to that list here, and possibly add a link to an answer on this page.

1. Finite model theory
2. Proof complexity
3. Algorithmic deduction (decision procedures for logical theories)
4. Logics of programs
5. Dynamic logic
6. Linear Temporal logic and its variants
7. Computational Tree Logic and its variants
8. Epistemic logic
9. Database theory
10. Type theory
11. Automata over infinite words
12. Categorical logic
13. Concurrency theory and process algebra
14. Domain theory
15. Linear logic
16. Descriptive Complexity
17. Model Checking
18. Fixed Point calculi and transitive closure logics

Answer 7

an area of strong overlap between logic and computer science is automated theorem proving, eg [4]. also eg ref [1] is the use of the Boyer-Moore theorem prover to check/verify Godels theorem. another recent major/impressive result is the recent completion of software verification of the four color theorem (and others such as Odd Order and Feit-Thompson [3]) at Microsoft research by Gonthier.[2]

[1] Metamathematics, Machines and Gödel's Proof (Cambridge Tracts in Theoretical Computer Science by Shankar

[2] A computer-checked proof of the Four Colour Theorem Georges Gonthier

[3] Interesting algorithms in the formalization of the Feit-Thompson theorem? tcs.se

[4] Where and how did computers help prove a theorem? tcs.se