Actualités
  Période
semaine
ou mois
aucune période


  Thèmes:
Thèses
Colloques
Autres
Groupes
Tous les thèmes

   
  Liens:
Voir les thèses

Voir les colloques

Voir les autres événements

Voir la page des groupes

Accéder à l'intranet

Intitulé:   
Constructive completeness for the linear-time mu-calculus
du groupe Séminaire Méthodes Formelles

Date 2017-10-24  11:00-12:00
TitreConstructive completeness for the linear-time mu-calculus 
RésuméModal mu-calculus is one of the central logics for verification. In his seminal paper, Kozen proposed an axiomatization 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. We provide a new completeness argument for the linear-time mu-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 mu-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 in Kozen's axiomatization. This yields a constructive proof for the full linear-time mu-calculus. 
Lieu178 
OrateurAmina Doumane 
Emailhttps://www.irif.fr/~doumane/ 
UrlLIP - ENS Lyon 



Aucun document lié à cet événement.

Retour
Retour à l'index