Classical approach to verification and design

Verification and design - Logic and automata-theoretic methods have been used for the specification, design and verification of computer systems for decades. Seminal works in the 1960s, by Büchi, Rabin, and others on automata theory and logic have made those applications possible. The model-checking technology is based on these foundations, and has seen substantial developments in the last two decades. The approach is most effective when applied to relatively unstructured and control-intensive processes in which the system being analyzed is accurately modeled as a finite-state automaton. This technology is now an important part of the design cycle in companies such as Intel or IBM.

Limitations - In contrast, the application of these techniques to computer software, complex systems like embedded systems or distributed systems has been less successful. The reasons for that are multiple:

1. Automata-based models do not faithfully capture the complex interactive behaviour of modern interactive and computational systems. We need formalisms where components are first class citizens and where complex interactions between computational systems can be accurately modelled;
2. Current verification or synthesis algorithms are, in general, not yet efficient enough for realistic applications. We need more efficient algorithms and good heuristics to bridge the gap between theory and practice;
3. The success of model checking applies, to a large extent, to systems with a finite state-space only. Verification and synthesis algorithms for richer models are needed. We need to be able to handle efficiently infinite state spaces where time, data, or quantities can be modelled.

CRP aims & objectives: Pushing the game-theoretic approach

We strongly believe that the limitations identified above cannot be overcome by merely fine-tuning the conceptual framework. Our approach is to generalize transition systems and automata – models of computation of the classical approach to verification – by the more flexible (and mathematically deeper) game-theoretic framework. There are initial results in this area, and our aim is to advance them towards a usable framework and methodology in the verification and design of complex systems. Our objectives are complementary to fields like game theoretic semantics in logic and the theory of programming. With the proposed approach, we also aim to contribute to a convergence of our community with the important community of control theory that deals with the behavior of dynamical systems.

Objectives and motivations - Our long term objective is the definition of a modern systems theory where systems are modeled as interacting processes that are potential collaborators or adversaries, and where important aspects like communication, timing information, data, probability, etc. can be adequately modeled.

As computer systems are deployed more and more in safety critical environments, there is a need for a methodology to design, synthesize and formally verify complex interacting computational systems. This modern systems theory should help the designers to model complex computer based systems in a rigorous way and allow them to reason formally about their correctness. Our research should contribute substantially to the creation of such a methodology.