On the proof theory of regular fixed points

David Baelde

Description

Niveau: Supérieur, Doctorat, Bac+8
On the proof theory of regular fixed points David Baelde INRIA & LIX / Ecole Polytechnique Abstract. We consider encoding finite automata as least fixed points in a proof- theoretical framework equipped with a general induction scheme, and study au- tomata inclusion in that setting. We provide a coinductive characterization of in- clusion that yields a natural bridge to proof-theory. This leads us to generalize these observations to regular formulas, obtaining new insights about inductive theorem proving and cyclic proofs in particular. 1 Introduction The automated verification of systems that have only finitely many possible behaviors is obviously decidable, although possibly complex. More interestingly, many proper- ties are still decidable in the much richer class where infinitely many behaviors can be described by a finite number of states. There are several reasons for considering these questions from a proof-theoretical angle. Obviously, proof-theory provides well- structured proof objects that can be considered as verification certificates; the fact that proofs can be composed by cut is of particular interest here. Taking the opposite point of view, complex but decidable problems can also be good examples to test and illuminate the design of rich logics. In particular, we are interested in the treatment of finite-state behaviors in first- order logic extended with least fixed points. While the finite behavior case is trivially handled in the proof-theory of such logics, finite-state behaviors are not so well under- stood.

• ?n when there


• least fixed


• multi-simulation


• p?


• µbt µbt


• then ?


• finite state

Sujets

• Philippus Baldaeus
• École polytechnique
• Finite-state machine

Informations

• Publié par: profil-zyak-2012
• Nombre de lectures: 25
• Langue: English

Extrait

Ontheprooftheoryofregularfixedpoints DavidBaelde IN d R a I v A id & .b L a I e X l / de E ´ @ co e l n e s P - o l l y yt o e n c . h o ni r q g ue Abstract.Weconsiderencodingfiniteautomataasleastfixedpointsinaproof- theoreticalframeworkequippedwithageneralinductionscheme,andstudyau- tomatainclusioninthatsetting.Weprovideacoinductivecharacterizationofin- clusionthatyieldsanaturalbridgetoproof-theory.Thisleadsustogeneralize theseobservationstoregularformulas,obtainingnewinsightsaboutinductive theoremprovingandcyclicproofsinparticular. 1Introduction Theautomatedverificationofsystemsthathaveonlyfinitelymanypossiblebehaviors isobviouslydecidable,althoughpossiblycomplex.Moreinterestingly,manyproper- tiesarestilldecidableinthemuchricherclasswhereinfinitelymanybehaviorscan bedescribedbyafinitenumberofstates.Thereareseveralreasonsforconsidering thesequestionsfromaproof-theoreticalangle.Obviously,proof-theoryprovideswell- structuredproofobjectsthatcanbeconsideredasverificationcertificates;thefactthat proofscanbecomposedbycutisofparticularinteresthere.Takingtheoppositepointof view,complexbutdecidableproblemscanalsobegoodexamplestotestandilluminate thedesignofrichlogics. Inparticular,weareinterestedinthetreatmentoffinite-statebehaviorsinfirst- orderlogicextendedwithleastfixedpoints.Whilethefinitebehaviorcaseistrivially handledintheproof-theoryofsuchlogics,finite-statebehaviorsarenotsowellunder- stood.Finitebehaviorscanbetreatedbyonlyunfoldingfixedpointsonbothpositive andnegativepositions.Applyinganexhaustiveproof-searchstrategyalongtheselines, theBedwyrsystem[14,2]providesapurelysyntacticapproachtomodel-checking. Althoughsimple,thisstrategyallowstotreatcomplexproblemslikebisimulationfor finite π -calculus,thankstotheseamlessintegrationofgenericquantification[8,13].In ordertodealwithfinite-statebehaviors,anaturalattemptistodetectcyclesinproof- searchandcharacterizethosewhichreflectasoundreasoning.Followingthatgeneral idea,tableau[5]andcyclic[10,12,4]proofsystemshavebeenexploredunderseveral angles.Thesesystemsaresimple,especiallynaturalfromasemanticpointofview, butnotentirelysatisfactory.Notably,theydonotenjoycut-elimination(exceptforthe propositionalframeworkof[10])and,inthefirst-order,intuitionisticorlinearcases, theircut-freeproofsarenotexpressiveenoughforcapturingfinite-statebehaviors. Inthispaper,wefirststudytheproof-theoreticaltreatmentoffiniteautomatainclu- sion,acentralprobleminmodel-checking,inalogicequippedwithageneral,explicit inductionprinciple.Wetranslateafiniteautomaton,orrathertheacceptanceofaword