Reactive systems are computer systems that maintain continuous interaction with the environment in which they operate. Such systems are nowadays part of our daily life: think about common yet critical applications like engine control units in automotive, aircraft autopilots, medical aided- devices, or micro-controllers in mass production. Clearly, any flaw in such critical systems can have catastrophic consequences. However, they exhibit several characteristics, like resource limitation constraints, real-time responsiveness, concurrency that make them difficult to implement correctly. To ensure the design of reactive systems that are dependable, safe, and efficient, researchers and industrials have advocated the use of so-called formal methods, that rely on mathematical models to express precisely and analyze the behaviors of these systems.Automata theory provides a fundamental notion such as languages of program executions for which membership, emptiness, inclusion, and equivalence problems allow us to specify and verify properties of reactive systems. However, these Boolean notions yield the correctness of the system against a given property that sometimes, falls short of being satisfactory answers when the performances are prone to errors. As a consequence, a common engineering approach is not just to verify that a system satisfies a property, but whether it does so within a degree of quality and robustness.This thesis investigates the expressibility, recognition, and robustness of quantitative properties for program executions.• Firstly, we provide a survey on languages definable by regular automata with Presburger definable constraints on letter occurrences for which we provide descriptive complexity. Inspired by this model, we introduce an expression formalism that mixes formula and automata to define quantitative languages \ie function from words to integers. These expressions use Presburger arithmetic to combine values given by regular automata weighted by integers. We show that quantitative versions of the classical decision problems such as emptiness, universality, inclusion, and equivalence are computable. Then we investigate the extension of our expressions with a ''Kleene star'' style operator. This allows us to iterate an expression over smaller fragments of the input word, and to combine the results by taking their iterated sum. The decision problems quickly turn out to be not computable, but we introduce a new subclass based on a structural restriction for which algorithmic procedures exist.• Secondly, we consider a notion of robustness that places a distance on words, thus defining neighborhoods of program executions. A language is said to be robust if the membership satisfiability cannot differ for two ''close'' words, and that leads to robust versions of all the classical decision problems. Our contribution is to study robustness verification problems in the context of weighted transducers with different measures (sum, mean-payoff, and discounted sum). Here, the value associated by the transducer to rewrite a word into another denotes the cost of the noise that this rewriting induce. For each measure, we provide algorithms that determine whether a language is robust up to a given threshold of error and we solve the synthesis of the robust kernel for the sum measure. Furthermore, we provide case studies including modeling human control failures and approximate recognition of type-1 diabetes using robust detection of blood sugar level swings.• Finally, we observe that algorithms for structural patterns recognition of automata often share similar techniques. So, we introduce a generic logic to express structural properties of automata with outputs in some monoid, in particular, the set of predicates talking about the output values is parametric. Then, we consider three particular automata models (regular automata, transducers, and automata weighted by integers) and instantiate the generic logic for each of them. We give tight complexity results for the three logics with respect to the pattern recognition problem. We study the expressiveness of our logics by expressing classical structural patterns characterizing for instance unambiguity and polynomial ambiguity in the case of regular automata, determinizability, and finite-valuedness in the case of transducers and automata weighted by integers. As a consequence of our complexity results, we directly obtain that these classical properties can be decided in logarithmic space. / Doctorat en Sciences / info:eu-repo/semantics/nonPublished