The factored state representation and concurrency semantics of Petri nets are closely related to those of classical planning models, yet automated planning and Petri net analysis have developed independently, with minimal and mainly unconvincing attempts at crossfertilisation. This thesis exploits the relationship between the formal reachability problem, and the automated planning problem, via Petri net unfolding, which is an attractive reachability analysis method for highly concurrent systems as it facilitates reasoning about independent sub-problems. The first contribution of this thesis is the theory of directed unfolding: controlling the unfolding process with informative strategies, for the purpose of optimality and increased efficiency. The second contribution is the application of directed unfolding to automated planning. Inspired by well-known planning heuristics, this thesis shows how problem specific information can be employed to guide unfolding, in response to the formal problem of developing efficient, directed reachability analysis methods for concurrent systems. Complimenting this theoretical work, this thesis presents a new forward search method for partial order planning which can be exponentially more efficient than state space search. Our suite of planners based on directed unfolding can perform optimal and suboptimal classical planning subject to arbitrary action costs, optimal temporal planning with respect to arbitrary action durations, and address probabilistic planning via replanning for the most likely path. Empirical results reveal directed unfolding is competitive with current state of the art automated planning systems, and can solve Petri net reachability problems beyond the reach of the original “blind” unfolding technique. / Thesis (Ph.D.) -- University of Adelaide, School of Electrical and Electronic Engineering, 2008

L’objectif de cette thèse est la modélisation et l’étude de systèmes biologiques par l’intermédiaire de méthodes formelles. Les systèmes biologiques démontrent des comportements continus mais sont aussi susceptibles de montrer des changements abrupts dans leur dynamiques. Les équations différentielles ordinaires, ainsi que les systèmes dynamiques hybrides, sont deux formalismes mathématiques utilisés pour modéliser clairement de tels comportements. Un point critique de la modélisation de systèmes biologiques est la recherche des valeurs des paramètres du modèle afin de reproduire de manière précise un ensemble de données expérimentales. Si aucun jeu de paramètres valides n’est trouvé, il est nécessaire de réviser le modèle. Une possibilité est alors de remplacer un paramètre, ou un ensemble de paramètres, définissant un processus biologique par une fonctiondépendante du temps.Dans le cadre de cette thèse, nous exposons tout d’abord une méthode pour la révision de modèles hybrides. Pour cela, nous proposons une approche gloutonne appliquée à une méthode de contrôle optimal utilisant les mesures d’occupations etla relaxation convexe. Ensuite, nous étudions comment analyser les propriétés dynamiques d’un modèle à temps discret en utilisant la simulation ensembliste. Dans cet objectif, nous proposons deux méthodes basées sur deux outils mathématiques.La première méthode, qui se repose sur les polynômes de Bernstein, est une extension aux systèmes dynamiques hybrides, de l’outil de calcul ensembliste Sapo [1]. La seconde méthode utilise les représentations de Krivine-Stengle [2] pour permettre l’analyse d’atteignaiblité de systèmes dynamiques polynomiaux. Enfin, nous proposons aussi une méthodologie pour générer des systèmes dynamiques hybrides modélisant des protocoles biologiques expérimentaux. Les méthodes précédemment proposées sont appliquées sur divers études biologiques. Nous étudions tout d’abord un modèle de la production d’hémoglobinedurant la différentiation des érythrocytes dans la moelle [3]. Pour permettre la construction de ce modèle, nous avons dans un premier temps généré un ensemble de jeux de paramètres valides à l’aide d’une méthode de type Monte-Carlo. Dans un second temps, nous avons appliqué la méthode de révision de modèle afin de reproduire plus précisément les données expérimentales [4]. Nous proposons aussi un modèle préliminaire des effets à faibles doses du Cadmium sur la réponse du métabolisme à différentes étapes de la vie d’un rat. Enfin, nous appliquons les techniques d’analyse ensembliste pour la validation d’hypothèses sur un modèle d’homéostasie du fer [6] dans le cas où des paramètres varient dans de larges intervalles.Dans cette thèse, nous montrons aussi que le protocole associé à l’étude de la production d’hémoglobine, ainsi que le protocole étudiant l’intégration du Cadmium durant la vie d’un rat, peuvent être formalisés comme des systèmes dynamiques hybrides, et servent ainsi de preuves de concepts pour notre méthode de modélisation de protocoles expérimentaux / The purpose of this thesis is the modelling and analysis of biological systems with mechanistic models (in opposition with black-box models).In particular we use two mathematical formalisms for mechanism modelling: hybrid dynamical systems and polynomial Ordinary Differential Equations (ODEs).Biological systems modelling give rise to numerous problem and in this work we address three of them.First, the parameters in the differential equations are often uncertain or unknown.Consequently, we aim at generating a subset of valid parameter sets such that the models satisfy constraints deducted from some experimental data.This problem is addressed in the literature under the denomination of parameter synthesis, parameter estimation, parameter fitting, or parameter identification following the context.Then, if no valid parameter is found, one solution is to revise the model. This can be done by substituting a law in place of a constant parameter.In the literature, models with uncertain parts are known as grey models, and their studies can be found under the term of model identification.Finally, it may be necessary to ensure the correctness of the built models using validation, or verification, methods for a continuous over-approximation of the determined valid parameters.In this thesis we study the parameter synthesis problem, in the Haemoglobin production model case study, using an adaptation of the classical method based on Monte-Carlo sampling, and numerical simulations.To perform model revision of hybrid dynamical systems we propose an iterative scheme of an optimal control method based on occupation measures, and convex relaxations.Finally, we assess the quality of a model using set-based simulations, and reachability analysis.For this purpose, we propose two methods: the first one, which relies on Bernstein expansion, is an extension for hybrid dynamical systems of the reachability tool sapo , while the other uses Krivine-Stengle representations to perform the reachability analysis of polynomial ODEs.We also provide a methodology to generate hybrid dynamical systems modelling biological experimental protocols.All of these proposed methods were applied in different case studies.We first propose a model of haemoglobin production during the differentiation of an erythrocyte in the bone marrow.To develop this model we first applied the Monte-Carlo based parameters synthesis, followed by the model revision to correctly fit to the experimental data.We also propose a hybrid model of Cadmium flux in rats in the context of an experimental protocol, as well as a preliminary study of the effect of low dose Cadmium on a Glucose response.Finally, we apply the reachability analysis techniques for the validation on large parameters set of the iron homoeostasis model developed by Nicolas Mobilia during his Phd.We note the haemoglobin production model, as well as the glucose reponse model can be formalised, in their experimental context, as hybrid dynamical systems. Thus, they serve as proof of concept for the methodology of biological experimental protocols modelling.

Planejamento em inteligência artificial é a tarefa de determinar ações que satisfaçam um dado objetivo. Nos problemas de planejamento sob incerteza, as ações podem ter efeitos probabilísticos. Esses problemas são modelados como Processos de Decisão Markovianos (Markov Decision Processes - MDPs), modelos que permitem o cálculo de soluções ótimas considerando o valor esperado de cada ação em cada estado. Contudo, resolver problemas grandes de planejamento probabilístico, i.e., com um grande número de estados e ações, é um enorme desafio. MDPs grandes podem ser reduzidos através da computação de bissimulações estocásticas, i.e., relações de equivalência sobre o conjunto de estados do MDP original. A partir das bissimulações estocásticas, que podem ser exatas ou aproximadas, é possível obter um modelo abstrato reduzido que pode ser mais fácil de resolver do que o MDP original. No entanto, para problemas de alguns domínios, a computação da bissimulação estocástica sobre todo o espaço de estados é inviável. Os algoritmos propostos neste trabalho estendem os algoritmos usados para a computação de bissimulações estocásticas para MDPs de forma que elas sejam computadas sobre o conjunto de estados alcançáveis a partir de um dado estado inicial, que pode ser muito menor do que o conjunto de estados completo. Os resultados experimentais mostram que é possível resolver problemas grandes de planejamento probabilístico com desempenho superior às técnicas conhecidas de bissimulação estocástica. / Planning in artificial intelligence is the task of finding actions to reach a given goal. In planning under uncertainty, the actions can have probabilistic effects. This problems are modeled using Markov Decision Processes (MDPs), models that enable the computation of optimal solutions considering the expected value of each action when applied in each state. However, to solve big probabilistic planning problems, i.e., those with a large number of states and actions, is still a challenge. Large MDPs can be reduced by computing stochastic bisimulations, i.e., equivalence relations over the original MDP states. From the stochastic bisimulations, that can be exact or approximated, it is possible to get an abstract reduced model that can be easier to solve than the original MDP. But, for some problems, the stochastic bisimulation computation over the whole state space is unfeasible. The algorithms proposed in this work extend the algorithms that are used to compute stochastic bisimulations for MDPs in a way that they can be computed over the reachable set of states with a given initial state, which can be much smaller than the complete set of states. The empirical results show that it is possible to solve large probabilistic planning problems with better performance than the known techniques of stochastic bisimulation.

Machine learning (ML) has demonstrated great success in numerous complicated tasks. Fueled by these advances, many real-world systems like autonomous vehicles and aircraft are adopting ML techniques by adding learning-enabled components. Unfortunately, ML models widely used today, like neural networks, lack the necessary mathematical framework to provide formal guarantees on safety, causing growing concerns over these learning-enabled systems in safety-critical settings. In this dissertation, we tackle this problem by combining formal methods and machine learning to bring provable safety and robustness to learning-enabled systems. We first study the robustness verification problem of neural networks on classification tasks. We focus on providing provable safety guarantees on the absence of failures under arbitrarily strong adversaries. We propose an efficient neural network verifier LayR to compute a guaranteed and overapproximated range for the output of a neural network given an input set which contains all possible adversarially perturbed inputs. LayR relaxes nonlinear units in neural networks using linear bounds and refines such relaxations with mixed integer linear programming (MILP) to iteratively improve the approximation precision, which achieves tighter output range estimations compared to prior neural network verifiers. However, the neural network verifier focuses more on analyzing a trained neural network but less on learning provably safe neural networks. To tackle this problem, we study verifiable training that incorporates verification into training procedures to train provably safe neural networks and scale to larger models and datasets. We propose a novel framework, AdvIBP, for combining adversarial training and provable robustness verification. We show that the proposed framework can learn provable robust neural networks at a sublinear convergence rate. In the second part of the dissertation, we study the verification of system-level properties in neural-network controlled systems (NNCS). We focus on proving bounded-time safety properties by computing reachable sets. We first introduce two efficient NNCS verifiers ReachNN* and POLAR that construct polynomial-based overapproximations of neural-network controllers. We transfer NNCSs to tractable closed-loop systems with approximated polynomial controllers for computing reachable sets using existing reachability analysis tools of dynamical systems. The combination of polynomial overapproximations and reachability analysis tools opens promising directions for NNCS verification. We also include a survey and experimental study of existing NNCS verification methods, including combining state-of-the-art neural network verifiers with reachability analysis tools, to discuss what overapproximation is suitable for NNCS reachability analysis. While these verifiers enable proving safety properties of NNCS, the nonlinearity of neural-network controllers is the main bottleneck that limits their efficiency and scalability. We propose a novel framework of knowledge distillation to control “the degree of nonlinearity” of NN controllers to ease NNCS verification which improves provable safety of NNCSs especially when they are safe but cannot be verified due to their complexity. For the verification community, this opens up the possibility of reducing verification complexity by influencing how a system is trained. Though NNCS verification can prove safety when system models are known, modern deep learning, e.g., deep reinforcement learning (DRL), often targets tasks with unknown system models, also known as the model-free setting. To tackle this issue, we first focus on safe exploration of DRL and propose a novel Lyapunov-inspired method. Our method uses Gaussian Process models to provide probabilistic guarantees on the policies, and guide the exploration of the unknown environment in a safe fashion. Then, we study learning robust visual control policies in DRL to enhance the robustness against visual changes that were not seen during training. We propose a method DRIBO, which can learn robust state representations for RL via a novel contrastive version of the Multi-View Information Bottleneck (MIB). This approach enables us to train high-performance visual policies that are robust to visual distractions, and can generalize well to unseen environments.

The security of multi-robot systems is critical in various applications such as patrol, transportation, and search and rescue operations, where they face threats from adversaries attempting to gain control of the robots. These compromised robots are significant threats as they allow attackers to steer robots towards forbidden areas without being detected, potentially causing harm or compromising the mission. To address this problem, we propose a resilient planning, task assignment, and control framework. The proposed framework builds a multi-robot plan where robots are designed to get close enough to other robots according to a co-observation schedule, in order to mutually check for abnormal behaviors. For the first part of the thesis, we propose an optimal trajectory solver based on the alternating direction method of multipliers (ADMM) to generate multi-agent trajectories that satisfy spatio-temporal requirements introduced by the co-observation schedules. As part of the formulation, we provide a new reachability constraint to guarantee that, despite adversarial movement by the attacker, a compromised robot cannot reach forbidden areas between co-observations without being detected. In the second part of the thesis, to further enhance the system's performance, reliability, and robustness, we propose to deploy multiple robots on each route to form sub-teams. A new cross-trajectory co-observation scheme between sub-teams is introduced that preserves the optimal unsecured trajectories. The new planner ensures that at least one robot in each sub-team sticks to the planned trajectories, while sub-teams can constantly exchange robots during the task introducing additional co-observations that can secure originally unsecured routes. We show that the planning of cross-trajectory co-observations can be transformed into a network flow problem and solved using traditional linear program technique. In the final part of the thesis, we show that the introduction of sub-teams also improves the multi-robot system's robustness to unplanned situations, allowing servicing unplanned online events without breaking the security requirements. This is achieved by a distributed task assignment algorithm based on consensus ADMM which can handle tasks with different priorities. The assignment result and security requirements are formulated as spatio-temporal schedules and guaranteed through control barrier function (CBF) based controls.

Il s'agit d'une étude menée sur les systèmes cyber-physiques sur trois aspects principaux: la vérification de la stabilité, l'ordonnancement et la synthèse des paramètres. Les systèmes de contrôle embarqués (ECS) agissant dans le cadre de contrats temporels sont la classe considérée de systèmes cyber-physiques dans la thèse. ECS fait référence à des intégrations d'un dispositif informatique avec le système physique. En ce qui concerne les contrats temporels, ils sont des contraintes de temps sur les instants où se produisent certains événements tels que l'échantillonnage, l'actionnement et le calcul. Ces contrats sont utilisés pour modéliser les problèmes qui se posent dans les systèmes de contrôle modernes: incertitudes sur les retards d'actionnement, les périodes d'échantillonnage incertaines et l'interaction de plusieurs systèmes physiques avec des ressources informatiques partagées (CPUs). Maintenant, compte tenu d'un ECS et d'un contrat temporel, nous reformulons le système de manière impulsionnelle et vérifions la stabilité du système, sous toutes les incertitudes bornées et données par le contrat, en utilisant des techniques d'approximation convexe et de nouveaux résultats généralisés pour le problème sur une classe de systèmes modélisés dans le cadre des inclusions différentielles. Deuxièmement, compte tenu d'un ensemble de contrôleurs implémentés sur une plate-forme de calcul commune (CPUs), dont chacun est soumis à un contrat de synchronisation, et à son meilleur et son plus mauvais cas d'exécution dans chaque CPU, nous synthétisons une politique d’ordonnancement dynamique qui garantit que chaque contrat temporel est satisfait et que chacun des CPU partagés est attribué à au plus un contrôleur à tout moment. L'approche est basée sur une reformulation qui nous permet d'écrire le problème d’ordonnancement comme un jeu temporelle avec spécification de sureté. Ensuite, en utilisant l'outil UPPAAL-TIGA, une solution au jeu fournit une politique d’ordonnancement appropriée. En outre, nous fournissons une nouvelle condition nécessaire et suffisante pour l’ordonnancement des tâches de contrôle en fonction d’un jeu temporisé simplifiés. Enfin, nous résolvons un problème de synthèse de paramètres qui consiste à synthétiser une sous-approximation de l'ensemble des contrats de synchronisation qui garantissent en même temps l’ordonnancement et la stabilité des contrôleurs intégrés. La synthèse est basée sur un nouveau paramétrage du contrat temporel pour les rendre monotones, puis sur un échantillonnage à plusieurs reprises de l'espace des paramètres jusqu'à atteindre une précision d'approximation prédéfinie. / This is a study conducted on cyber-physical systems on three main aspects: stability verification, scheduling, and parameter synthesis. Embedded control systems (ECS) acting under timing contracts are the considered class of cyber-physical systems in the thesis. ECS refers to integrations of a computing device with the physical system. As for timing contracts they are time constraints on the instants where some events happen such as sampling, actuation, and computation. These contracts are used to model issues that arise in modern embedded control systems: uncertain sampling to actuation delays, uncertain sampling periods, and interaction of several physical systems with shared computational resources (CPUs). Now given an ECS and a timing contract we reformulate the system into an impulsive one and verifies stability of the system, under all possible bounded uncertainties given by the contract, using safe convex approximation techniques and new generalized results for the problem on a class of systems modeled in the framework of difference inclusions. Second given a set of controllers implemented on a common computational platform (CPUs), each of which is subject to a timing contract, and best and worst case execution times on each CPU, we synthesize a dynamic scheduling policy, which guarantees that each timing contract is satisfied and that each of the shared CPUs are allocated to at most one embedded controller at any time. The approach is based on a timed game formulation that allows us to write the scheduling problem as a timed safety game. Then using the tool UPPAAL-TIGA, a solution to the safety game provides a suitable scheduling policy. In addition, we provide a novel necessary and sufficient condition for schedulability of the control tasks based on a simplified timed game automaton. Last, we solve a parameter synthesis problem which consists of synthesizing an under-approximation of the set of timing contracts that guarantee at the same time the schedulability and stability of the embedded controllers. The synthesis is based on a re-parameterization of the timing contract to make them monotonic, and then on a repeatedly sampling of the parameter space until reaching a predefined precision of approximation.

In order to reach higher levels of autonomy in autonomous driving, it is important to consider potential occluded traffic participants. Current research has considered occlusion-aware autonomous driving in urban situations. However, no implementations have shown good performance in high velocity situations such as highway driving yet, since the current methods are too conservative in these situations and result in frequent excessive braking. In this work a method is proposed that tracks boundaries on the velocity states of potential hidden traffic using reachability analysis. It is proven that the method can guarantee collision-free trajectories for any, potentially hidden, traffic. The method is evaluated on cut-in scenarios retrieved from a dataset of recorded traffic. The results show that tracking the velocity bounds for potentially hidden traffic results in more efficient trajectories up to 18 km/h faster compared to existing occlusion-aware methods. While the method shows clear improvements, it does not always manage to establish a velocity bound and at times excessive braking still occurs. Further work is thus necessary to ensure consistently well-performing occlusion-aware highway driving. / För att nå högre nivåer av autonomi vid autonom körning är det viktigt att ta hänsyn till möjliga skymda trafikanter. Aktuell forskning har övervägt skymd-sikt-medveten autonom körning i urbana situationer. Emellertid har inga implementeringar visat bra prestanda i höghastighetssituationer såsom motorvägskörning ännu, eftersom de nuvarande metoderna är för konservativa i dessa situationer och resulterar i frekventa överdrivna inbromsningar. I detta arbete föreslås en metod som bestämmer gränser för hastighetstillstånden för möjlig skymd trafik med hjälp av nåbarhetsanalys. Det är bevisat att metoden kan garantera kollisionsfria banor för all möjlig skymd trafik. Metoden utvärderas på scenarier hämtade från ett dataset av registrerad trafik. Resultaten visar att bestämning av hastighetsgränserna för möjlig skymd trafik resulterar i effektivare banor upp till 18 km/h snabbare jämfört med befintliga skymd-sikt-medvetna-metoder. Även om metoden visar tydliga förbättringar, lyckas den inte alltid fastställa en hastighetsgräns och ibland förekommer fortfarande överdriven inbromsning. Ytterligare arbete är därför nödvändigt för att säkerställa konsekvent välpresterande motorvägskörning under skymd sikt.

Predicting the future state occupancies of pedestrians in urban scenarios is a challenging task, especially considering that conventional methods need an explicit model of the system, hence introducing data-driven reachability analysis. Data-driven reachability analysis uses data, inherently produced by an unknown system, to perform future state predictions using sets, generally represented by zonotopes. These predicted sets are generally more conservative than model-based reachable sets. Therefore, is it possible to cluster previously recorded trajectory data based on the expressed behavior and perform the predictions on each cluster to still be able to provide safety guarantees? The theory behind data-driven reachability analysis, which can handle input noise and model uncertainties and still provide safety guarantees, is quite recent. This means that previous implementations for predicting pedestrians are theoretically probabilistic and would not be appropriate to implement in actual systems. Thus, this thesis is not the first of its kind in predicting the future reachable sets for pedestrians using clustered behavioral data, but it is the first work that provides safety guarantees in the process. The method proposed in this thesis first labels the historically recorded trajectories into the behavior also referred to as mode, the pedestrian expressed, which is done by simple conditional statements. This is done offline. However, this implementation is designed to be modular enabling easier improvements to the labelling system. Then, the reachable sets are computed for each behavior separately, which enables a potential motion planner to decide on which modal sets are relevant for specific scenarios. Theoretically, this method provides safety guarantees. The outcomes of this method were more descriptive reachable sets, meaning that the predicted areas intersected areas that it reasonably should, and did not intersect areas it reasonably should not. Also, the volume of the zonotopes for the modal sets was observed to be smaller than the volume of the implemented baseline, indicating fewer over-approximations and less conservative predictions. These results enable more efficient path planning for Connected and Autonomous Vehicles (CAVs), thus reducing fuel consumption and brake wear. / Att predicera framtida tillstånd för fotgängare i urbana situationer är en utmaning, speciellt med tanke på att konventionella metoder behöver uttryckligen en modell av systemet, därav introduceringen av datadriven nåbarhetsanalys. Datadriven nåbarhetsanalys använder data, naturligt producerad av ett okänt system, för att genomföra framtida tillståndspredicering med hjälp av matematiska set, generellt representerade av zonotoper. Dessa predicerade sets är generellt sett mode konservativa än modellbaserade nåbara set. Därmed, är det möjligt att dela upp historiskt inspelade banor baserat på det uttryckta beteendet och genomföra prediceringar på varje kluster och bibehålla säkerhetsgarantier? Teorin bakom datadriven nåbarhetsanalys, som kan hantera brus i indatat och modellosäkerheter och bibehålla säkerhetsgarantier, är väldigt ny. Detta betyder att tidigare implementationer för att predicera fotgängare är, teoretiskt sett, probabilistiska och är inte lämpliga att implementera i riktiga system. Därmed, detta examensarbete är inte det första som predicerar framtida nåbara set för fotgängare genom att använda kluster för beteendedatat, men den är det första arbetet som bibehåller säkerhetsgarantier i processen. Den introducerade metoden i detta examensarbete rubricerar först de tidigare inspelade banorna baserat på beteendet, även kallat läget, som fotgängaren uttrycker, vilket är gjort genom simpla betingade påståenden. Detta görs offline. Dock, denna implementation är designad till att vara modulär vilket underlättar förbättringar till rubriceringssystemet. Fortsättningsvis, beräknas de nåbara seten för varje beteende separat, vilket möjliggör att en potentiell rörelseplanerare kan avgöra vilka beteendeset som är relevanta för specifika scenarion. Teoretiskt sett så ger denna metod säkerhetsgarantier. Resultaten från denna metod var först och främst mer beskrivande nåbara set, vilket betyder att de predicerade områdena korsar områden som de rimligtvis ska korsa, och inte korsar område som de rimligen inte ska korsa. Dessutom, volymen på zonotoperna for beteendeseten observerades att vara mindre än volymen för baslinjeseten, vilket indikerar lägre överskattningar och mindre konservativa prediceringar. Dessa resultat möjliggör mer effektiv rörelseplanering för uppkopplade och autonoma fordon, vilket reducerar bränsleförbrukningen och bromsslitage.

Les Systèmes à Evénements Discrets (SED) peuvent être définis comme des systèmes dans lesquels les variables d'état changent sous l'occurrence d'évènements au fil du temps. Les SED mettant en jeu des phénomènes de synchronisation peuvent être modélisés par des équations linéaires dans les algèbres de type (max,+). L'analyse d'atteignabilité est une problématique majeure pour les systèmes dynamiques. L'objectif est de calculer l'ensemble des états atteignables d'un système dynamique pour toutes les valeurs admissibles d'un ensemble d'états initiaux. Le problème de l'analyse d'atteignabilité pour les systèmes Max-Plus Linéaire (MPL) a été, proprement, résolu en décomposant le système MPL en une combinaison de systèmes affines par morceaux où les composantes affines du système sont représentées par des matrices de différences bornées (Difference Bound Matrix, DBM). La contribution principale de cette thèse est de présenter une procédure similaire pour résoudre le problème de l'atteignabilité pour des systèmes MPL incertains (uMPL), c'est-à-dire des systèmes MPL soumis à des bruits bornés, des perturbations et/ou des erreurs de modélisation. Tout d'abord, nous présentons une procédure permettant de partionner l'espace d'état d'un système uMPL en parties représentables par des DBM. Ensuite, nous étendons l'analyse d'atteignabilité des systèmes MPL aux systèmes uMPL. Enfin, les résultats sur l'analyse d'atteignabilité sont mis en oeuvre pour résoudre le problème d'atteignabilité conditionnelle, qui est étroitement lié au calcul du support de la densité de probabilité impliquée dans le problème de filtage stochastique / Discrete Event Dynamic Systems (DEDS) are discrete-state systems whose dynamics areentirely driven by the occurrence of asynchronous events over time. Linear equations in themax-plus algebra can be used to describe DEDS subjected to synchronization and time delayphenomena. The reachability analysis concerns the computation of all states that can bereached by a dynamical system from an initial set of states. The reachability analysis problemof Max Plus Linear (MPL) systems has been properly solved by characterizing the MPLsystems as a combination of Piece-Wise Affine (PWA) systems and then representing eachcomponent of the PWA system as Difference-Bound Matrices (DBM). The main contributionof this thesis is to present a similar procedure to solve the reachability analysis problemof MPL systems subjected to bounded noise, disturbances and/or modeling errors, calleduncertain MPL (uMPL) systems. First, we present a procedure to partition the state spaceof an uMPL system into components that can be completely represented by DBM. Then weextend the reachability analysis of MPL systems to uMPL systems. Moreover, the results onreachability analysis of uMPL systems are used to solve the conditional reachability problem,which is closely related to the support calculation of the probability density function involvedin the stochastic filtering problem. / Os Sistemas a Eventos Discretos (SEDs) constituem uma classe de sistemas caracterizada por apresentar espaço de estados discreto e dinâmica dirigida única e exclusivamente pela ocorrência de eventos. SEDs sujeitos aos problemas de sincronização e de temporização podem ser descritos em termos de equações lineares usando a álgebra max-plus. A análise de alcançabilidade visa o cálculo do conjunto de todos os estados que podem ser alcançados a partir de um conjunto de estados iniciais através do modelo do sistema. A análise de alcançabilidade de sistemas Max Plus Lineares (MPL) pode ser tratada por meio da decomposição do sistema MPL em sistemas PWA (Piece-Wise Affine) e de sua correspondente representação por DBM (Difference-Bound Matrices). A principal contribuição desta tese é a proposta de uma metodologia similar para resolver o problema de análise de alcançabilidade em sistemas MPL sujeitos a ruídos limitados, chamados de sistemas MPL incertos ou sistemas uMPL (uncertain Max Plus Linear Systems). Primeiramente, apresentamos uma metodologia para particionar o espaço de estados de um sistema uMPL em componentes que podem ser completamente representados por DBM. Em seguida, estendemos a análise de alcançabilidade de sistemas MPL para sistemas uMPL. Além disso, a metodologia desenvolvida é usada para resolver o problema de análise de alcançabilidade condicional, o qual esta estritamente relacionado ao cálculo do suporte da função de probabilidade de densidade envolvida o problema de filtragem estocástica.

Les travaux présentés dans ce manuscrit portent sur la conduite de systèmes complexes critiques. Ils s'inscrivent dans le cadre du projet CONNEXION (Investissements d'Avenir, BGLE2) qui réunit les principaux acteurs de la filière nucléaire française autour de la conception des systèmes de contrôle-commande des centrales et de leur exploitation. Dans le domaine de la conduite, les actions développées par le projet concernent la phase d'ingénierie avec pour objectif d'intégrer le point de vue de l'exploitant au plus tôt dans la validation des architectures de contrôle de commande, et la phase d'exploitation avec pour objectif de fournir une aide à la préparation et à l'exécution des procédures de conduite. Dans ce contexte, la contribution présentée dans ce mémoire porte sur la génération et la vérification de séquences d'actions de conduite répondant à un objectif donné et pouvant être opérées en toute sécurité sur le procédé. L'approche proposée repose la vérification d'une propriété d'atteignabilité sur un réseau d'automates temporisés modélisant le comportement des architectures. L'originalité réside dans la définition d’un cadre formel de modélisation sous la forme de patrons favorisant la réutilisabilité des modèles ainsi que dans la proposition d'algorithmes d'abstraction et de recherche d'atteignabilité itératifs exploitant la hiérarchisation intrinsèque des architectures afin de permettre le passage à l'échelle de l'approche proposée. La contribution a été éprouvée sur la plate-forme d'expérimentation CISPI du CRAN puis sur un cas d'étude à échelle industrielle proposé dans le cadre du projet CONNEXION / The works presented in this manuscript deals with critical complex systems operation. They are part of the CONNEXION project (Investissements d'Avenir, BGLE2), which involves the main actors in the French nuclear industry around the design of control systems for power plants and their operation. In the operation field, the actions developed by the project concern the engineering phase with the aim of integrating the operator's point of view as soon as possible in the validation of control architectures, and the operation phase with the aim of providing assistance in the preparation and execution of operation procedures. In this context, the contribution presented in this manuscript deals with the generation and verification of action sequences that meet a given objective and that can be safely operated on the process. The proposed approach relies on verifying a reachability property on a network of timed automata modelling the behavior of architectures. The originality is in the definition of a formal modelling framework using patterns promoting the reusability of models, as well as in the proposition of abstraction and reachability iterative analysis algorithms exploiting the intrinsic hierarchization of architectures in order to scale-up of the proposed approach. The contribution was evaluated on the CISPI experimental platform of the CRAN, and on an industrial scale case study proposed within the framework of the CONNEXION project