Computation is employed to incredible success in a massive variety of applications, and yet it is difficult to formally state what our computations are. Finding a way to model computations is not only valuable to understanding them, but central to automatic manipulations and formal verification. Often the most interesting computations are not functions with inputs and outputs, but ongoing systems that continuously react to user input. In the automata-theoretic approach, computations are modeled as words, a sequence of letters representing a trace of a computation. Each automaton accepts a set of words, called its language. To model reactive computation, we use Büchi automata: automata that operate over infinite words. Although the computations we are modeling are not infinite, they are unbounded, and we are interested in their ongoing properties. For thirty years, Büchi automata have been recognized as the right model for reactive computations. In order to formally verify computations, however, we must also be able to create specifications that embody the properties we want to prove these systems possess. To date, challenging algorithmic problems have prevented Büchi automata from being used as specifications. I address two challenges to the use of Buechi automata as specifications in formal verification. The first, complementation, is required to check program adherence to a specification. The second, determination, is used in domains such as synthesis, probabilistic verification, and module checking. I present both empirical analysis of existing complementation constructions, and a new theoretical contribution that provides more deterministic complementation and a full determination construction.

Computation is employed to incredible success in a massive variety of applications, and yet it is difficult to formally state what our computations are. Finding a way to model computations is not only valuable to understanding them, but central to automatic manipulations and formal verification. Often the most interesting computations are not functions with inputs and outputs, but ongoing systems that continuously react to user input. In the automata-theoretic approach, computations are modeled as words, a sequence of letters representing a trace of a computation. Each automaton accepts a set of words, called its language. To model reactive computation, we use Büchi automata: automata that operate over infinite words. Although the computations we are modeling are not infinite, they are unbounded, and we are interested in their ongoing properties. For thirty years, Büchi automata have been recognized as the right model for reactive computations. In order to formally verify computations, however, we must also be able to create specifications that embody the properties we want to prove these systems possess. To date, challenging algorithmic problems have prevented Büchi automata from being used as specifications. I address two challenges to the use of Buechi automata as specifications in formal verification. The first, complementation, is required to check program adherence to a specification. The second, determination, is used in domains such as synthesis, probabilistic verification, and module checking. I present both empirical analysis of existing complementation constructions, and a new theoretical contribution that provides more deterministic complementation and a full determination construction.

Cette thèse traite de la theorie de la preuve pour les logiques a points fixes, telles que le μ-calcul, lalogique lineaire a points fixes, etc. ces logiques sont souvent munies de systèmes de preuves finitairesavec des règles d’induction à la Park. Il existe néanmoins d’autres sytèmes de preuves pour leslogiques à points fixes, qui reposent sur la notion de preuve infinitaire, mais qui sont beaucoupmoins developpés dans la litterature. L’objectif de cette thèse est de pallier à cette lacune dansl’état de l’art, en developpant la théorie de la preuve infnitaire pour les logiques a points fixes,avec deux domaines d’application en vue: les langages de programmation avec types de données(co)inductifs et la vérification des systèmes réactifs.Cette thèse contient trois partie. Dans la première, on rappelle les deux principales approchespour obtenir des systèmes de preuves pour les logiques à points fixes: les systèmes finitaires avecrègle explicite d’induction et les systèmes finitaires, puis on montre comment les deux approchesse relient. Dans la deuxième partie, on argumente que les preuves infinitaires ont effectivement unréel statut preuve-theorique, en montrant que la logique lineaire additive multiplicative avec pointsfixes admet les propriétés d’élimination des coupures et de focalisation. Dans la troisième partie,on utilise nos developpements sur les preuves infinitaires pour monter de manière constructive lacomplétude du μ-calcul lineaire relativement à l’axiomatisation de Kozen. / The subject of this thesis is the proof theory of logics with fixed points, such as the μ-calculus,linear-logic with fixed points, etc. These logics are usually equipped with finitary deductive systemsthat rely on Park’s rules for induction. other proof systems for these logics exist, which relyon infinitary proofs, but they are much less developped. This thesis contributes to reduce thisdeficiency by developing the infinitary proof-theory of logics with fixed points, with two domainsof application in mind: programming languages with (co)inductive data types and verification ofreactive systems.This thesis contains three parts. In the first part, we recall the two main approaches to theproof theory for logics with fixed points: the finitary and the infinitary one, then we show theirrelationships. In the second part, we argue that infinitary proofs have a true proof-theoreticalstatus by showing that the multiplicative additive linear-logic with fixed points admits focalizationand cut-elimination. In the third part, we apply our proof-theoretical investigations to obtain aconstructive proof of completeness for the linear-time μ-calculus w.r.t. Kozen’s axiomatization.

Recently, multi-priced timed automata have received much attention for real-time systems. These automata extend priced timed automata by featuring several price parameters. This permits to compute objectives like the optimal ratio between rewards and costs. Arising from the model of timed automata, the multi-weighted setting has also attracted much notice for classical nondeterministic automata. The present thesis develops multi-weighted MSO-logics on finite, infinite and timed words which are expressively equivalent to multi-weighted automata, and studies decision problems for them. In addition, a Nivat-like theorem for weighted timed automata is proved; this theorem establishes a connection between quantitative and qualitative behaviors of timed automata. Moreover, a logical characterization of timed pushdown automata is given.

Recently, multi-priced timed automata have received much attention for real-time systems. These automata extend priced timed automata by featuring several price parameters. This permits to compute objectives like the optimal ratio between rewards and costs. Arising from the model of timed automata, the multi-weighted setting has also attracted much notice for classical nondeterministic automata. The present thesis develops multi-weighted MSO-logics on finite, infinite and timed words which are expressively equivalent to multi-weighted automata, and studies decision problems for them. In addition, a Nivat-like theorem for weighted timed automata is proved; this theorem establishes a connection between quantitative and qualitative behaviors of timed automata. Moreover, a logical characterization of timed pushdown automata is given.