Constructive completeness for the linear-time µ-calculus

Amina Doumane (1, 2)

1 PPS - Preuves, Programmes et Systèmes
2 PI.R2 - Design, study and implementation of languages for proofs and programs

Modal µ-calculus is one of the central logics for verification. In his seminal paper, Kozen proposed an axiomati-zation for this logic, which was proved to be complete, 13 years later, by Kaivola for the linear-time case and by Walukiewicz for the branching-time one. These proofs are based on complex, non-constructive arguments, yielding no reasonable algorithm to construct proofs for valid formulas. The problematic of constructiveness becomes central when we consider proofs as certificates, supporting the answers of verification tools. In our paper, we provide a new completeness argument for the linear-time µ-calculus which is constructive, i.e. it builds a proof for every valid formula. To achieve this, we decompose this difficult problem into several easier ones, taking advantage of the correspondence between the µ-calculus and automata theory. More precisely, we lift the well-known automata transformations (non-determinization for instance) to the logical level. To solve each of these smaller problems, we perform first a proof-search in a circular proof system, then we transform the obtained circular proofs into proofs of Kozen's axiomatization.

Domaines: Informatique [cs]

Amina Doumane. Constructive completeness for the linear-time µ-calculus. Conference on Logic in Computer Science 2017, Jun 2017, Reykjavik, Iceland. ⟨hal-01430737⟩