Taming non-determinism in infinite-state systems using games

• Applicant: Dr. Patrick Totzke
• Subject Area: Theoretical Computer Science
• Term: since 2024
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 524989976

Formal Verification is used to ensure that computer systems behave as intended. Whilst desirable in all software, manual verification is only practical in small cases, and automatic verification is typically computationally expensive, often impossible, and only employed in critical applications to avoid catastrophe. Developing tractable verification techniques is an active area of research which develops an understanding of the limits of computation and designs new techniques to make verification accessible. When modelling computer systems for formal analysis, most formalisms incorporate some form of non-determinism that allows to over-approximate algorithmic workflows, to state specifications concisely, and to model uncontrollable external environments. However, the presence of non-determinism in our models means that many formal analysis techniques first require a costly determinization step that is often the main barrier to efficient procedures. Moreover, verifying realistic systems relies upon models with infinitely many possible system states. For those, the impact of non-determinism is even more pronounced: it often gives the models more expressive power, but it can make their analysis impossible. History-determinism (HD) is an intermediate notion that allows non-determinism, but only if it can be resolved step-by-step, that is, without knowledge of the future input. This restriction has been studied extensively in the past decade and has been shown to enable tractable verification for wider classes of models and specifications. In this project we will advance our knowledge of history-determinism in two directions. First, we will study HD variants of key computational formalisms that are widely employed to model concurrency, recursive programs, and real-time systems. Our hypothesis is that, compared to deterministic variants, HD ones recognize larger classes of languages to be used in specifications, yet retain the decidability or decent worst-case complexity of common verification problems. We will study the extent to which history-determinism limits expressivity, whether the property can be detected and the improvements to fundamental verification procedures that can be obtained under the property. As a second direction, we will explore variations of history-determinism to maximize expressivity and minimize computational resources required for verification. We will do this by varying the degree of information available to, or guarantees demanded of, both opponents in the game-based characterizations. We will moreover consider further restrictions resulting from imposing strong assumptions, for example on the topology (demanding some form of compositionality of the automata structure), or on the internal complexity of player strategies. We expect that our activities will provide new theoretical insights and have practical impact by enabling new, efficient implementations.

• DFG Programme: Research Grants