Formal methods involve classical disciplines such as game and automata theory as well as algebraic techniques. These disciplines are at the basis of virtually all processes of automatic formal verification.

Automata

Automata serve as both system models and as tools for deciding logical theories (a technique going back to Büchi, Elgot, and Trakhtenbrot in the 1960s). Logical formulas as well as automata, in turn, may be interpreted as games, which indeed provide a natural model of reactive systems, as they naturally reflect the interaction of a system with an environment.

Games of infinite duration

In the algorithmic analysis of such games, one is interested in reasoning about the existence of winning strategies, and also about the structure of such strategies. This is especially important in the context of multi-player games of imperfect information where players may have a partial view of game states. These games have applications to control and synthesis in distributed systems, and there is a rich theory currently being developed on definability of strategies in zero-sum perfect information games. Corresponding notions are as yet unclear in the more general context of imperfect information. Automata theory of concurrency has given us rich insights into the structure and behavior of agents in distributed systems and we plan to explore how such understanding can be used in the game theoretic context as well.

Automata-based and algebraic techniques

Algebraic approaches, such as the use of semigroup/monoid theory, have been successfully used in the study of (subclasses of) regular languages of words. This provided algorithmic results which led to classification of the regular languages. Other structures, such as series-parallel and forest algebras have been developed to model trees, posets and other complex structures. Elgot, Bloom, Esik, Meseguer, Montanari, Stefanescu and others have advocated even more general structures such as categories to model richer behaviours that arise in computation. A weakness of this latter work is that, while it relies on elegant mathematics, algorithmic aspects have been largely ignored. We propose to revisit this work and develop it on an algorithmic and automata-theoretic footing, with a view to applications in computer science.