We investigate mathematical models of computation, which is a necessary precondition to understand and explain the behaviour of AI systems and other computer programs.
Cyber-physical systems increasingly affect most aspects of our lives: they are used in pacemakers, manage factory supply chains, trade in stocks and autonomously pilot modern planes and cars. Software deficiencies can have serious economic and life-threatening consequences. While traditional methods of testing and simulations can be effective for finding errors, they are hopelessly inadequate for showing their absence. A more promising approach is to use mathematical arguments to prove that a system behaves as intended, in all possible situations. Verification is the area of research based on this idea. It is truly interdisciplinary and has fascinating connections to Artificial Intelligence, Discrete Mathematics and Software Engineering.
To prove the correctness of some system one starts with a formal model of the system itself as well as a specification that defines what correctness means. In model-checking, for instance, we model systems as a finite-state machine and the specifications as temporal logic formulae. Correctness then ammounts to the fact that the finite-state machine satisfies the formula, which can often be verified automatically. Naturally, there are many different ways to formalize systems and specifications, and some formalisms are more expressive than others.
Current methods are very good at analysing models with only finitely many internal configurations, such as microchips or hardware drivers. However, if we move to more expressive models we quickly go beyond the reach of known techniques or even cross theoretical limits. At this point the research frontier is on so-called infinite-state models, which enable us to argue directly about unbounded quantities such as realtime constraints, recursion depth or simultaneous user requests.
For example, imagine a network server that can receive any number of requests concurrently and which should eventually respond to all of them. The total number of requests is not determined in advance and so it is necessary to incorporate it into the model, which consequently has infinitely many possible internal configurations. However, we do have good finite representations, such as Counter Machines or Pushdown Automata, that can be used in such situations. The result is a trade-off between the expressibility of these formalisms and the feasibility of their verification.
A key mathematical tool for correctness checks and decision making in the presence of environmental uncertainty are games between antagonistic players, who try to cause and prevent errors, respectively. Closely related formalisms are used in Economics, Biology, Chemistry and other sciences, in the form of Markov Chains and Markov Decision Processes.
Correctness here corresponds to the existence of winning strategies, which tell their player how to move in order to secure a win. Winning strategies are important not only because they act as correctness certificates but also because they can often be directly translated into executable code.
Our research seeks to understand more general, infinitary strategies, which are often necessary for realistic specifications. We will investigate the mathematical structure, internal complexity, and thus the cost of winning strategies. Advancing our understanding of strategies promises to yield better finite representations, which in turn makes it easier to verify that winning strategies exist (checking correctness) as well as automatically generating and executing them.
Our research leads to a deeper understanding of the nature of computation and decision making and provides new and improved methods for automated program verification.
|