Des automates aux preuves cycliques : algorithmes d’équivalence et complexité descriptive
Laureline Pinault · HAL (Le Centre pour la Communication Scientifique Directe) · 2021
Computational models allow us to reason about programs by abstracting their operatingprocess. The choice of a suitable model for a given situation takes into account both itsexpressivity and properties such as the complexity of the associated problems. This thesisstudies computational models in order to develop tools for conception and analysis ofprograms.First we consider the language equivalence problem for automata, which has variousapplications especially in the formal verification field. Our starting point is a coinductivealgorithm HKC developed by Bonchi and Pous that exploits up-to techniques to comparefinite automata. We present a version of this algorithm that works in a slighty extendedsetting, so we can adapt it to Büchi automata. We also give a linear version of a test usedas a subroutine in HKC and a framework based on automata learning to evaluate theefficiency of equivalence algorithms.Secondly we explore the expressivity of a cyclic proof system seen as a calculation deviceby comparing it with existing computational models (multiheads automata and Gödel’sSystem T). This proof system corresponds to a type system for functional programs.If we restrict ourselves to functions from words to boolean, we get exactly the regularlanguages in the affine subsystem, and Logspace if we add the contraction rule. Withoutthis restriction the system coincides with System T on natural functions: the primitiverecursive functions in the affine case et the Peano definable functions with the contraction.