Les systèmes digitaux jouent un rôle croissant dans le bon fonctionnement de notre société.Au delà de la grande diversité de leur domaines d'utilisations, on confie aujourd'hui destâches importantes à des algorithmes. Déjà largement utilisés dans des domaines aussi délicatque le transport, la chirurgie ou l'économie, il est aujourd'hui de plus en plus question defaire de la place aux systèmes digitaux dans les domaines sociaux et politiques :vote électronique, algorithmes de sélection, profilage électoraldotsPour les tâches confiées à des algorithmes, la responsabilité est déplacées de l'exécutantvers les concepteurs, développeurs et testeurs de ces algorithmes. Il incombe aussi auxchercheurs qui étudient ces algorithmes de proposer des techniques de vérifications fiablequi pourront être utilisées à tous les niveaux : conception, développement et test.Les méthodes de vérifications formelles donnent des outils mathématiques pourprévenir des erreurs à chaque niveaux. Parmi elle, le diagnostic d'erreur consiste en lacréation d'un diagnostiqueur basé sur un modèle formel du système à vérifier.Le diagnostiqueur est exécuté en parallèle du système qu'il doit surveiller et prévientun contrôleur si il détecte un comportement dangereux du système.Pour les systèmes modélisés par des automates temporisés, il n'est pas toujours possiblede construire un diagnostiqueur sous la forme d'un autre automate temporisé. En effetles automates temporisés, introduits par cite{AD94} dans les années 90 et largementétudiés et utilisés depuis pour modéliser des systèmes avec contraintes temporelles,ne sont pas déterminisable. Une machine plus puissante qu'un automate temporisé peutcependant être utilisée pour construire le diagnostiqueur d'un automate temporisé commele montre cite{Tripakis02}. L'aboutissement de ce travail de thèse est la constructionautomatique d'un diagnostiqueur pour les automates temporisés à une horloge.Ce diagnostiqueur, dans le même esprit que celui de cite{Tripakis02}, est une machineplus puissante qu'un automate temporisé. La partie~I du manuscrit introduit un cadreformel pour ce type de machine et plus généralement pour la modélisation et ladéterminisation de systèmes quantitatifs. Y est introduit le modèle des automates surstructures temporisés, qui apporte un nouveau point de vue sur la manière de modéliserles systèmes avec variables quantitatives. La partie~II étudie le problème de ladéterminisation des automates sur structures temporises, et plus spécifiquement celuides automates temporisés qui peuvent se traduire dans ce cadre nouveau cadre formel.La partie~III montre comment utiliser les automates sur structure temporisés pourconstruire de manière générique un diagnostiqueur pour les automate temporisés à unehorloge. Cette technique est implémentée dans un outils, DOTA , et comparée à lamachine construite par cite{Tripakis02}. / Digital system are now part of our society. They are used in a wide range of domainsand in particular they have to handle delicate tasks. Already used in domainssuch as transportation, surgery or economy, we speak now of using digital systemsfor social or political matters : electronic vote, selection algorithms, electoralprofilingdots For task handled by algorithm, the responsibility is moved from theexecutioner to the designer, developer and tester of those algorithms. It is alsothe responsibility of computer scientists who study those algorithms to proposereliable techniques of verification which will be applicable in the design, thedevelopment or the testing phase. Formal verification methods provide mathematicaltools to prevent executions error in all phases. Among them, fault-diagnosis consiston the construction of a diagnoser based on a formal model of the system we aim tocheck. The diagnoser runs in parallel with the real system and emit a warning anytime it detect a dangerous behavior. For systems modeled by timed automata, it isnot always possible to construct a timed automaton to diagnose it. Indeed timed automata,introduce in the nineties by cite{AD94} and widely studied and used since to modeltimed systems, are not determinizable. A machine, more powerful than a timed automaton,can still be used to construct the diagnoser of a timed automaton as it is done incite{Tripakis02}. This thesis work aim at constructing a diagnoser for any one-clocktimed automata. This diagnoser is constructed with the help of a machine more powerfulthan timed automata, following the idea of cite{Tripakis02}. Part~I of this thesisintroduce a formal framework for the modeling of quantitative systems and the study oftheir determinization. In this framework we introduce automata on timed structures,the model used to construct the diagnoser. Part~II study the determinization problemof automata on timed structures, and particularly the one of timed automatadeterminization in this framework. Part~III illustrate how automata on timed structurescan be used to construct in a generic way a diagnoser for one clock timed automata.This technique is implemented in a tool, DOTA , and is compared to the technique usedin cite{Tripakis02}.

We show that the termination of Mohri's algorithm is decidable for polynomially ambiguous weighted finite automata over the tropical semiring which gives a partial answer to a question by Mohri [29]. The proof relies on an improvement of the notion of the twins property and a Burnside type characterization for the finiteness of the set of states produced by Mohri's algorithm.

Cette thèse porte sur la vérification des automates temporisés, un modèle bien établi pour les systèmes temps-réels. La thèse est constituée de trois parties. La première est dédiée à la déterminisation des automates temporisés, problème qui n'a pas de solution en général. Nous proposons une méthode approchée (sur-approximation, sous-approximation, mélange des deux) fondée sur la construction d'un jeu de sûreté. Cette méthode améliore les approches existantes en combinant leurs avantages respectifs. Nous appliquons ensuite cette méthode de déterminisation à la génération automatique de tests de conformité. Dans la seconde partie, nous prenons en compte des aspects quantitatifs des systèmes temps-réel grâce à une notion de fréquence des états acceptants dans une exécution d'un automate temporisé. Plus précisément, la fréquence d'une exécution est la proportion de temps passée dans les états acceptants. Nous intéressons alors à l'ensemble des fréquences des exécutions d'un automate temporisé pour étudier, par exemple, le vide de langages seuils. Nous montrons ainsi que les bornes de l'ensemble des fréquences sont calculables pour deux classes d'automates temporisés. D'une part, les bornes peuvent être calculées en espace logarithmique par une procédure non-déterministe dans les automates temporisés à une horloge. D'autre part, elles peuvent être calculées en espace polynomial dans les automates temporisés à plusieurs horloges ne contenant pas de cycles forçant la convergence d'horloges. Finalement, nous étudions le problème de l'accessibilité des états acceptants dans des réseaux d'automates temporisés qui communiquent via des files FIFO. Nous considérons tout d'abord des automates temporisés à temps discret, et caractérisons les topologies de réseaux pour lesquelles l'accessibilité est décidable. Cette caractérisation est ensuite étendue aux automates temporisés à temps continu. / This thesis is about verification of timed automata, a well-established model for real time systems. The document is structured in three parts. The first part is dedicated to the determinization of timed automata, a problem which has no solution in general. We propose an approximate (over-approximation/under-approximation/mix) method based on the construction of a safety game. This method improves both existing approaches by combining their respective advantages. Then, we apply this determinization approach to the generation of conformance tests. In the second part, we take into account quantitative aspects of real time systems thanks to a notion of frequency of accepting states along executions of timed automata. More precisely, the frequency of a run is the proportion of time elapsed in accepting states. Then, we study the set of frequencies of runs of a timed automaton in order to decide, for example, the emptiness of threshold languages. We thus prove that the bounds of the set of frequencies are computable for two classes of timed automata. On the one hand, we prove that bounds are computable in logarithmic space by a non-deterministic procedure in one-clock timed automata. On the other hand, they can be computed in polynomial space in timed automata with several clocks, but having no cycle that forces the convergence between clocks. Finally, we study the reachability problem in networks of timed automata communicating through FIFO channels. We first consider dicrete timed automata, and characterize topologies of networks for which reachability is decidable. Then, this characterization is extended to dense-time automata.

Given a formal model of the behavior of a system, an objective and some notion of control the goal of controller synthesis is to construct a (finite-state) controller that ensures that the system always satisfies the objective. Often, the controller can base its decisions only on limited observations of the system. This notion of limited observability induces a partial-information game between the controller and the uncontrollable part of the system. A successful controller then realizes an observation-based strategy that enforces the objective. In this thesis we consider the controller synthesis problem in the linear-time setting where the behavior of the system is given as a nondeterministic, labeled transitions system A, where the controller can only partially observe and control the behavior of A. The goal of the thesis is to develop a compositional approach for constructing controllers, suitable to treat conjunctive cascades of linear-time objectives P_1, P_2, ..., P_k in an online manner. We iteratively construct a controller C_1 for system A enforcing P_1, then a controller C_2 enforcing P_2 for the parallel composition of the first controller with the system, and so on. It is crucial for this approach that each controller C_i enforces P_i in a most general manner, being as permissive as possible. Otherwise, behavior that is needed to enforce subsequent objectives could be prematurely removed. Standard notions of strategies and controllers only allow the most general treatment for the limited class of safety objectives. We introduce a novel concept of most general strategies and controllers suited for the compositional treatment of objectives beyond safety. We demonstrate the existence of most general controllers for all enforceable, observation-based omega-regular objectives and provide algorithms for the construction of such most general controllers, with specialized variants for the subclass of safety and co-safety objectives. We furthermore adapt and apply our general framework for the compositional synthesis of most general controllers to the setting of exogenous coordination in the context of the channel-based coordination language Reo and the constraint automata framework and report on our implementation in the verification toolset Vereofy. The construction of most general controllers in Vereofy for omega-regular objectives relies on our tool ltl2dstar for generating deterministic omega-automata from Linear Temporal Logic (LTL) formulas. We introduce a generic improvement for exploiting insensitiveness to stuttering during the determinization construction and evaluate its effectiveness in practice. We further investigate the performance of recently proposed variants of Safra\'s determinization construction in practice.

Given a formal model of the behavior of a system, an objective and some notion of control the goal of controller synthesis is to construct a (finite-state) controller that ensures that the system always satisfies the objective. Often, the controller can base its decisions only on limited observations of the system. This notion of limited observability induces a partial-information game between the controller and the uncontrollable part of the system. A successful controller then realizes an observation-based strategy that enforces the objective. In this thesis we consider the controller synthesis problem in the linear-time setting where the behavior of the system is given as a nondeterministic, labeled transitions system A, where the controller can only partially observe and control the behavior of A. The goal of the thesis is to develop a compositional approach for constructing controllers, suitable to treat conjunctive cascades of linear-time objectives P_1, P_2, ..., P_k in an online manner. We iteratively construct a controller C_1 for system A enforcing P_1, then a controller C_2 enforcing P_2 for the parallel composition of the first controller with the system, and so on. It is crucial for this approach that each controller C_i enforces P_i in a most general manner, being as permissive as possible. Otherwise, behavior that is needed to enforce subsequent objectives could be prematurely removed. Standard notions of strategies and controllers only allow the most general treatment for the limited class of safety objectives. We introduce a novel concept of most general strategies and controllers suited for the compositional treatment of objectives beyond safety. We demonstrate the existence of most general controllers for all enforceable, observation-based omega-regular objectives and provide algorithms for the construction of such most general controllers, with specialized variants for the subclass of safety and co-safety objectives. We furthermore adapt and apply our general framework for the compositional synthesis of most general controllers to the setting of exogenous coordination in the context of the channel-based coordination language Reo and the constraint automata framework and report on our implementation in the verification toolset Vereofy. The construction of most general controllers in Vereofy for omega-regular objectives relies on our tool ltl2dstar for generating deterministic omega-automata from Linear Temporal Logic (LTL) formulas. We introduce a generic improvement for exploiting insensitiveness to stuttering during the determinization construction and evaluate its effectiveness in practice. We further investigate the performance of recently proposed variants of Safra\'s determinization construction in practice.

In this thesis, we investigate different theoretical questions concerning weighted automata models over tree-like input structures. First, we study exact and approximated determinisation and then, we turn to Kleene-like and Büchi-like characterisations. We consider multiple weighted automata models, including weighted tree automata over semirings (Chapters 3 and 4), weighted forest automata over M-monoids (Chapter 5), and rational weighted tree languages with storage (Chapter 6). For an explanation as to why the last class can be considered as a weighted automaton model, we refer to page 188 of the thesis. We will now summarise the main contributions of the thesis. In Chapter 3, we focus on the determinisation of weighted tree automata and present our determinisation framework, called M-sequentialisation, which can model different notions of determinisation from the existing literature. Then, we provide a positive M-sequentialisation result for the case of additively idempotent semirings or finitely M-ambiguous weighted tree automata. Another important contribution of Chapter 3 is Theorem 77, where we provide a blueprint theorem that can be used to find determini- sation results for more classes of semirings and weighted tree automata easily. In fact, instead of repeating an entire determinisation construction, Theorem 77 allows us to prove a determinisation result by finding certain finite equivalence relations. This is a very potent tool for future research in the area of determinisation. In Chapter 4, we move from exact determinisation towards approximate determini- sation. We lift the formalisms and the main results from one approach from the literature from the word case to the tree case. This successfully results in an approximated determinisation construction for weighted tree automata over the tropical semiring. We provide a formal mathematical description of the approximated determinisation construction, rather than an algorithmic description as found in the related approach from the literature. In Chapter 5, we turn away from determinisation and instead consider Kleene-like and Büchi-like characterisations of weighted recognisability. We introduce weighted forest automata over M-monoids, which are a generalisation of weighted tree automata over M-monoids and weighted forest automata over semirings. Then, we prove that our recognisable weighted forest languages can be decomposed into a finite product of recognisable weighted tree languages. We also prove that the initial algebra semantic and the run semantic for weighted forest automata are equivalent under certain conditions. Lastly, we define rational forest expressions and forest M-expressions and and prove that the classes of languages generated by these formalisms coincide with recognisable weighted forest languages under certain conditions. In Chapter 6, we consider rational weighted tree languages with storage, where the storage is introduced by composing rational weighted tree languages without storage with a storage map. It has been proven in the literature that rational weighted tree languages with storage are closed under the rational operations. In Chapter 6, we provide alternative proofs of these closure properties. In fact, we prove that our way of introducing storage to rational weighted tree languages preserves the closure properties from rational weighted tree languages without storage.:1 Introduction 2 Preliminaries 2.1 Languages 2.2 WeightedLanguages 2.3 Weighted Tree Automata 3 A Unifying Framework for the Determinisation of Weighted Tree Automata 3.1 Introduction 3.2 Preliminaries 3.3 Factorisation in Monoids 3.3.1 Ordering Multisets over Monoids 3.3.2 Cayley Graph and Cayley Distance 3.3.3 Divisors and Rests 3.3.4 Factorisation Properties 3.4 Weighted Tree Automata over M_fin(M) and the Twinning Property 3.4.1 Weighted Tree Automata over M_fin(M) 3.4.2 The Twinning Property 3.5 Sequentialisation of Weighted Tree Automata over M_fin(M) 3.5.1 The Sequentialisation Construction 3.5.2 The Finitely R-Ambiguous Case 3.6 Relating WTA over M_fin(M) and WTA over S 3.7 M-Sequentialisation of Weighted Tree Automata 3.7.1 Accumulation of D_B 3.7.2 M-Sequentialisation Results 3.8 Comparison of our Results to the Literature 3.8.1 Determinisation of Unweighted Tree Automata 3.8.2 The Free Monoid Case 3.8.3 The Group Case 3.8.4 The Extremal Case 3.9 Conclusion 4 Approximated Determinisation of Weighted Tree Automata 125 4.1 Introduction 4.2 Preliminaries 4.3 Approximated Determinisation 4.3.1 The Approximated Determinisation Construction 4.3.2 Correctness of the Construction 4.4 The Approximated Twinning Property 4.4.1 Implications for Approximated Determinisability 4.4.2 Decidability of the Twinning Property 4.5 Conclusion 5 Kleene and Büchi Theorems for Weighted Forest Languages over M-Monoids 5.1 Introduction 5.2 Preliminaries 5.3 WeightedForestAutomata 5.3.1 Forests 5.3.2 WeightedForestAutomata 5.3.3 Rectangularity 5.3.4 I-recognisable is R-recognisable 5.4 Kleene’s Theorem 5.4.1 Kleene’s Theorem for Trees 5.4.2 Kleene’s Theorem for Forests 5.4.3 An Inductive Approach 5.5 Büchi’s Theorem 5.5.1 Büchi’s Theorem for Trees 5.5.2 Büchi’s Theorem for Forests 5.6 Conclusion 6 Rational Weighted Tree Languages with Storage 6.1 Introduction 6.2 Preliminaries 6.3 Rational Weighted Tree Languages with Storage 6.4 The Kleene-Goldstine Theorem 6.5 Closure of Rat(S¢,Σ,S) under Rational Operations 6.5.1 Top-Concatenation, Scalar Multiplication, and Sum 6.5.2 α-Concatenation 6.5.3 α-Kleene Star 6.6 Conclusion 7 Outlook References

The topic of this paper is the determinization problem of ω-automata under the transition-based Emerson-Lei acceptance (called TELA), which generalizes all standard acceptance conditions and is defined using positive Boolean formulas. Such automata can be determinized by first constructing an equivalent generalized Büchi automaton (GBA), which is later determinized. The problem of constructing an equivalent GBA is considered in detail, and three new approaches of solving it are proposed. Furthermore, a new determinization construction is introduced which determinizes several GBA separately and combines them using a product construction. An experimental evaluation shows that the product approach is competitive when compared with state-of-the-art determinization procedures. The second part of the paper studies limit-determinization of TELA and we show that this can be done with a single-exponential blow-up, in contrast to the known double-exponential lower-bound for determinization. Finally, one version of the limit-determinization procedure yields good-for-MDP automata which can be used for quantitative probabilistic model checking.