Cette thèse a pour objectif la génération de séquences de franchissement dans les Réseaux de Petri Temporisés (RdPT) en utilisant une approche incrémentale. Le verrou principal auquel est confronté ce travail est l’explosion combinatoire qui résulte de la construction classique du graphe d’accessibilité du RdPT. Nous proposons d’utiliser la notion de séquence de steps temporisés, afin d’exprimer progressivement l’ensemble des séquences de franchissements permettant de passer d’un état courant à un état cible. La notion de step temporisé correspond à une abstraction logique du comportement du système considéré. Le caractère incrémental de l’approche a pour objectif de gagner en efficacité. En effet, il consiste à exprimer tout nouvel état de la résolution par rapport à une profondeur K+1, en fonction d’un état atteint à la profondeur K. Ainsi, nous proposons plusieurs algorithmes de recherche incrémentale permettant d'améliorer l'efficacité de la résolution des problèmes d'accessibilité. Nous utilisons ensuite la programmation par contraintes pour modéliser le problème de recherche d’accessibilité dans un RdPT et mettre en œuvre notre approche incrémentale. Notre approche permet également d’ajouter des contraintes spécifiques à un contexte de résolution. Nous avons notamment utilisé cette possibilité pour proposer des techniques d'identification des jetons dans un RdPT borné, dans le cadre de la reconfiguration des systèmes manufacturiers. Nous concluons par l’évaluation de différentes applications constituant des « benchmarks » permettant d’illustrer l'efficacité des approches proposées / This PhD thesis is dedicated to the generation of firing sequences in Timed Petri Net (TPN) using an incremental approach. To reduce the influence of the well-known combinatorial explosion issue, a unique sequence of timed steps is introduced to represent implicitly the underlying reachability graph of the TPN, without needing its whole construction. This sequence of timed steps is developed based on the logical abstraction technique. The advantage of the incremental approach is that it can express any state just from the last step information, instead of representing all states before.Several incremental search algorithms are introduced to improve the efficiency of our methodology. Constraint programming techniques are used to model and solve our incremental model, in which search strategies are developed that can search for solutions more efficiently. Our methodology can be used to add specific constraints to model realistic systems. Token identification techniques are developed to handle token confusion issues that appear when addressing the reconfiguration of manufacturing systems. Experimental benchmarks illustrate the effectiveness of approaches proposed in this thesis

Computer systems are used in almost all aspects of our lives and our dependency on them keeps on increasing. When computer systems are used to handle critical tasks, any software failure can cause severe human and/or material losses. Therefore, for such applications, it is important to detect software errors at an early stage of software development. Furthermore, the growing use of concurrent and distributed programs exponentially increases the complexity of computer systems, making the problem of detecting software errors even harder (if not impossible). This calls for defining systematic and efficient techniques to evaluate the safety and the correctness of programs. The aim of Model-Checking is to analyze automatically whether a given program satisfies its specification. Early applications of Model-Checking were restricted to systems whose behaviors can be captured by finite graphs, so called finite-state systems. Since many computer systems cannot be modeled as finite-state machines, there has been a growing interest in extending the applicability of Model-Checking to infinite-state systems. The goal of this thesis is to extend the applicability of Model Checking for three instances of infinite-state systems: Ad-Hoc Networks, Dynamic Register Automata and Multi Pushdown Systems. Each one of these instances models challenging types of networks of communicating processes. In both Ad-Hoc Networks and Dynamic Register Automata, communication is carried through message passing. In each type of network, a graph topology models the communication links between processes in the network. The graph topology is static in the case of Ad-Hoc Networks while it is dynamic in the case of Dynamic Register Automata. The number of processes in both types of networks is unbounded. Finally, we consider Multi Pushdown Systems, a model used to study the behaviors of concurrent programs composed of sequential recursive sequential programs communicating through a shared memory.

The ability to provide succinct information about why a property does, or does not, hold in a given system is a key feature in the context of formal verification and model checking. It can be used both to explain the behavior of the system to a user of verification software, and as a tool to aid automated abstraction and synthesis procedures. Counterexample traces, which are executions of the system that do not satisfy the desired specification, are a classical example. Specifications of systems with probabilistic behavior usually require that an event happens with sufficiently high (or low) probability. In general, single executions of the system are not enough to demonstrate that such a specification holds. Rather, standard witnesses in this setting are sets of executions which in sum exceed the required probability bound. In this thesis we consider methods to certify and witness that probabilistic reachability constraints hold in Markov decision processes (MDPs) and probabilistic timed automata (PTA). Probabilistic reachability constraints are threshold conditions on the maximal or minimal probability of reaching a set of target-states in the system. The threshold condition may represent an upper or lower bound and be strict or non-strict. We show that the model-checking problem for each type of constraint can be formulated as a satisfiability problem of a system of linear inequalities. These inequalities correspond closely to the probabilistic transition matrix of the MDP. Solutions of the inequalities are called Farkas certificates for the corresponding property, as they can indeed be used to easily validate that the property holds. By themselves, Farkas certificates do not explain why the corresponding probabilistic reachability constraint holds in the considered MDP. To demonstrate that the maximal reachability probability in an MDP is above a certain threshold, a commonly used notion are witnessing subsystems. A subsystem is a witness if the MDP satisfies the lower bound on the optimal reachability probability even if all states not included in the subsystem are made rejecting trap states. Hence, a subsystem is a part of the MDP which by itself satisfies the lower-bounded threshold constraint on the optimal probability of reaching the target-states. We consider witnessing subsystems for lower bounds on both the maximal and minimal reachability probabilities, and show that Farkas certificates and witnessing subsystems are related. More precisely, the support (i.e., the indices with a non-zero entry) of a Farkas certificate induces the state-space of a witnessing subsystem for the corresponding property. Vice versa, given a witnessing subsystem one can compute a Farkas certificate whose support corresponds to the state-space of the witness. This insight yields novel algorithms and heuristics to compute small and minimal witnessing subsystems. To compute minimal witnesses, we propose mixed-integer linear programming formulations whose solutions are Farkas certificates with minimal support. We show that the corresponding decision problem is NP-complete even for acyclic Markov chains, which supports the use of integer programs to solve it. As this approach does not scale well to large instances, we introduce the quotient-sum heuristic, which is based on iteratively solving a sequence of linear programs. The solutions of these linear programs are also Farkas certificates. In an experimental evaluation we show that the quotient-sum heuristic is competitive with state-of-the-art methods. A large part of the algorithms proposed in this thesis are implemented in the tool SWITSS. We study the complexity of computing minimal witnessing subsystems for probabilistic systems that are similar to trees or paths. Formally, this is captured by the notions of tree width and path width. Our main result here is that the problem of computing minimal witnessing subsystems remains NP-complete even for Markov chains with bounded path width. The hardness proof identifies a new source of combinatorial hardness in the corresponding decision problem. Probabilistic timed automata generalize MDPs by including a set of clocks whose values determine which transitions are enabled. They are widely used to model and verify real-time systems. Due to the continuously-valued clocks, their underlying state-space is inherently uncountable. Hence, the methods that we describe for finite-state MDPs do not carry over directly to PTA. Furthermore, a good notion of witness for PTA should also take into account timing aspects. We define two kinds of subsystems for PTA, one for maximal and one for minimal reachability probabilities, respectively. As for MDPs, a subsystem of a PTA is called a witness for a lower-bounded constraint on the (maximal or minimal) reachability probability, if it itself satisfies this constraint. Then, we show that witnessing subsystems of PTA induce Farkas certificates in certain finite-state quotients of the PTA. Vice versa, Farkas certificates of such a quotient induce witnesses of the PTA. Again, the support of the Farkas certificates corresponds to the states included in the subsystem. These insights are used to describe algorithms for the computation of minimal witnessing subsystems for PTA, with respect to three different notions of size. One of them counts the number of locations in the subsystem, while the other two take into account the possible clock valuations in the subsystem.:1 Introduction 2 Preliminaries 3 Farkas certificates 4 New techniques for witnessing subsystems 5 Probabilistic systems with low tree width 6 Explications for probabilistic timed automata 7 Conclusion

Yes / The broadcast nature of wireless local area networks has made them prone to several types of wireless injection attacks, such as Man-in-the-Middle (MitM) at the physical layer, deauthentication, and rogue access point attacks. The implementation of novel intrusion detection systems (IDSs) is fundamental to provide stronger protection against these wireless injection attacks. Since most attacks manifest themselves through different metrics, current IDSs should leverage a cross-layer approach to help toward improving the detection accuracy. The data fusion technique based on the Dempster–Shafer (D-S) theory has been proven to be an efficient technique to implement the cross-layer metric approach. However, the dynamic generation of the basic probability assignment (BPA) values used by D-S is still an open research problem. In this paper, we propose a novel unsupervised methodology to dynamically generate the BPA values, based on both the Gaussian and exponential probability density functions, the categorical probability mass function, and the local reachability density. Then, D-S is used to fuse the BPA values to classify whether the Wi-Fi frame is normal (i.e., non-malicious) or malicious. The proposed methodology provides 100% true positive rate (TPR) and 4.23% false positive rate (FPR) for the MitM attack and 100% TPR and 2.44% FPR for the deauthentication attack, which confirm the efficiency of the dynamic BPA generation methodology. / Gulf Science, Innovation and Knowledge Economy Programme of the U.K. Government under UK-Gulf Institutional Link Grant IL 279339985 and in part by the Engineering and Physical Sciences Research Council (EPSRC), U.K., under Grant EP/R006385/1.

In this thesis, we first use the reachability theory to develop algorithms for state predictionunder delayed state or output measurements. We next develop control strategies forcollision avoidance and trajectory tracking of UAVs based on the devised algorithms andthe model predictive control theory. Finally, simulations results for collision avoidanceand trajectory tracking problems are presented, for different communication delays,using a UAV model with 6 degrees of freedom. / I denna avhandling använder vi först tillgänglighetsteorin för att utveckla algoritmerför tillståndsförutsägelse under fördröjda tillstånds- eller utgångsmätningar. Därefterutvecklar kontrollstrategier för undvikande av kollision och spårning av UAV: er baseradepå de planerade algoritmerna och modellen förutsägbar kontrollteori. Slutligenpresenteras simuleringsresultat för att undvika kollision och problem med spårningav banan, för olika kommunikationsförseningar, med en UAV-modell med 6 frihetsgrader.

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.

No description available.

<p>This thesis considers the problems of modelling and control of batch processes, a class of finite duration chemical processes characterized by their absence of equilibrium conditions and nonlinear, time-varying dynamics over a wide range of operating conditions. In contrast to continuous processes, the control objective in batch processes is to achieve a non-equilibrium desired end-point or product quality by the batch termination time. However, the distinguishing features of batch processes complicate their control problem and call for dedicated modelling and control tools. In the initial phase of this research, a predictive controller based on the novel concept of reverse-time reachability regions (RTRRs) is developed. Defined as the set of states from where the process can be steered inside a desired end-point neighbourhood by batch termination subject to input constraints and model uncertainties, an algorithm is developed to characterize these sets at each sampling instance offline; these characterizations subsequently play an integral role in the control design. A key feature of the resultant controller is that it requires the online computation of only the immediate control action while guaranteeing reachability to the desired end-point neighbourhood, rendering the control problem efficiently solvable even when using the nonlinear process model. Moreover, the use of RTRRs and one-step ahead type control policy embeds important fault-tolerant characteristics into the controller. Next, we address the problem of the unavailability of reliable and computationally manageable first-principles-based process models by developing a new data-based modelling approach. In this approach, local linear models (identified via latent variable regression techniques) are combined with weights (arising from fuzzy c-means clustering) to describe global nonlinear process dynamics. Nonlinearities are captured through the appropriate combination of the different models while the linearity of the individual models prevents against a computationally expensive predictive controller. This modelling approach is also generalized to account for time-varying dynamics by incorporating online learning ability into the model, making it adaptive. This is accomplished by developing a probabilistic recursive least squares (PRLS) algorithm for updating a subset of the model parameters. The data-based modelling approach is first used to generate data-based reverse-time reachability regions (RTRRs), which are subsequently incorporated in a new predictive controller. Next, the modelling approach is applied on a complex nylon-6,6 batch polymerization process in order to design a trajectory tracking predictive controller for the key process outputs. Through simulations, the modelling approach is shown to capture the major process nonlinearities and closed-loop results demonstrate the advantages of the proposed controller over existing options. Through further simulation studies, model adaptation (via the PRLS algorithm) is shown to be crucial for achieving acceptable control performance when encountering large disturbances in the initial conditions. Finally, we consider the problem of direct quality control even when there are limited quality-related measurements available from the process; this situation typically calls for indirectly pursuing the control objective through trajectory tracking control. To address the problem of unavailability of online quality measurements, an inferential quality model, which relates the process conditions over the entire batch duration to the final quality, is required. The accuracy of this type of quality model, however, is sensitive to the prediction of the future batch behaviour until batch termination. This "missing data" problem is handled by integrating the previously developed data-based modelling approach with the inferential model in a predictive control framework. The key feature of this approach is that the causality and nonlinear relationships between the future inputs and outputs are accounted for in predicting the final quality and computing the manipulated input trajectory. The efficacy of the proposed predictive control design is illustrated via simulations of the nylon-6,6 batch polymerization process with a different control objective than considered previously.</p> / Doctor of Philosophy (PhD)

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.

<p dir="ltr">In the context of a Human-in-the-Loop (HITL) system, the accuracy of reachability analysis plays a significant role in ensuring the safety and reliability of HITL systems. In addition, one can avoid unnecessary conservativeness by explicitly considering human control behavior compared to those methods that rely on the system dynamics alone. One possible approach is to use a Gaussian Mixture Model (GMM) to encode human control behavior using the Expectation-Maximization (EM) algorithm. However, relatively few works consider the admissible control input ranges due to physical limitations when modeling human control behavior. This could make the following reachability analysis overestimate the system's capability, thereby affecting the performance of the HITL system. To address this issue, this work presents a constrained stochastic reachability analysis algorithm that can explicitly account for the admissible control input ranges. By confining the ellipsoidal confidence region of each Gaussian component using Sequential Quadratic Programming (SQP), we probabilistically constrain the GMM as well as the corresponding stochastic reachable sets. A comprehensive mathematical analysis of how the constrained GMM can affect the stochastic reachable sets is provided in this work. Finally, the proposed stochastic reachability analysis algorithm is validated via an illustrative numerical example.</p>