# A Proof Theory for Model Checking: An Extended Abstract

## TL;DR

This paper introduces a proof-theoretic foundation for model checking using sequent calculus, employing focused proof systems to handle state exploration and verification tasks more naturally.

## Contribution

It develops a focused proof system that combines additive and multiplicative inference rules to improve the theoretical foundation of model checking.

## Key findings

- Provides a proof-theoretic framework for reachability and non-reachability
- Enables direct state exploration through synthetic rules
- Supports bisimulation and winning strategies analysis

## Abstract

While model checking has often been considered as a practical alternative to building formal proofs, we argue here that the theory of sequent calculus proofs can be used to provide an appealing foundation for model checking. Since the emphasis of model checking is on establishing the truth of a property in a model, we rely on the proof theoretic notion of additive inference rules, since such rules allow provability to directly describe truth conditions. Unfortunately, the additive treatment of quantifiers requires inference rules to have infinite sets of premises and the additive treatment of model descriptions provides no natural notion of state exploration. By employing a focused proof system, it is possible to construct large scale, synthetic rules that also qualify as additive but contain elements of multiplicative inference. These additive synthetic rules -- essentially rules built from the description of a model -- allow a direct treatment of state exploration. This proof theoretic framework provides a natural treatment of reachability and non-reachability problems, as well as tabled deduction, bisimulation, and winning strategies.