Constructive completeness for the linear-time µ-calculus

• Main Author: Doumane, Amina
• Other Authors: Preuves, Programmes et Systèmes (PPS), Université Paris Diderot - Paris 7 (UPD7)-Centre National de la Recherche Scientifique (CNRS), Design, study and implementation of languages for proofs and programs (PI.R2), Université Paris Diderot - Paris 7 (UPD7)-Centre National de la Recherche Scientifique (CNRS)-Institut de Recherche en Informatique Fondamentale (IRIF (UMR_8243)), Université Paris Diderot - Paris 7 (UPD7)-Centre National de la Recherche Scientifique (CNRS)-Université Paris Diderot - Paris 7 (UPD7)-Centre National de la Recherche Scientifique (CNRS)-Inria de Paris, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)
• Format: Conference Object
• Language: English
• Published: HAL CCSD 2017
• Subjects: [INFO]Computer Science [cs]; Iceland
• Online Access: https://hal.archives-ouvertes.fr/hal-01430737; https://hal.archives-ouvertes.fr/hal-01430737/document; https://hal.archives-ouvertes.fr/hal-01430737/file/MAIN.pdf

International audience 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.