Lightweight temporal ontology languages have become a very active field of research in recent years. Many real-world applications, like processing electronic health records (EHRs), inherently contain a temporal dimension, and require efficient reasoning algorithms. Moreover, since medical data is not recorded on a regular basis, reasoners must deal with sparse data with potentially large temporal gaps. In this paper, we introduce a temporal extension of the tractable language ELH⊥, which features a new class of convex diamond operators that can be used to bridge temporal gaps. We develop a completion algorithm for our logic, which shows that entailment remains tractable. Based on this, we develop a minimal-world semantics for answering metric temporal conjunctive queries with negation. We show that query answering is combined first-order rewritable, and hence in polynomial time in data complexity.

Metamodellierung im Sinne der Meta Object Facility (MOF) stellt eine Methode für die strukturelle Definition der abstrakten Syntax von Modellierungssprachen und Modellen im Softwareentwicklungsprozess dar. Um Modellsimulation und dynamische Analysen für metamodellbasierte Sprachen zu unterstützen, fehlt es an einem Kalkül zur operationalen Semantik. In dieser Arbeit wird ausgehend von MOF die Aktionssemantik MActions entwickelt, die die Definition von operationaler Semantik als Verhalten in Metamodellen ermöglicht. Diese Erweiterung geht einher mit der Beschreibung von Laufzeitmodellen sowie Zuständen und Parallelitätseigenschaften, so dass eine Verifikation von dynamischen Eigenschaften möglich wird. Zu diesem Zweck wird mit der Linear Temporal Object Constraint Language (LT-OCL) exemplarisch eine prädikatenlogische Temporallogik entwickelt, die eine metamodellunabhängige Analyse für ausführbare Modelle erlaubt. Dabei ist die Semantik von temporalen Ausdrücken über Zuständsänderungen von (aufgezeichneten) Ausführungsläufen beschrieben, wobei eine Linearisierung parallele Änderungen zusammenführt. Als weiteren Anwendungsfall der dynamischen Analyse untersuchen wir die Relation zum Verhaltensvergleich im Sinne der Bisimulationstheorie. Metamodelle, Aktionssemantik und Temporallogik werden mittels einer erweiterten Abstract State Machine (ASM) formal beschrieben und kommen in zwei Fallstudien zur Anwendung (Timed Automata und C#). / Object-oriented metamodelling as defined by the Meta Object Facility (MOF) provide a means to describe the structure of models and the abstract syntax of modelling languages at various stages in a software development process. However, MOF lacks concepts for the definition of operational semantics and there is no support for dynamic model analysis based on the semantics and abstract states of a language definition. This thesis investigates on extending the metamodelling framework with an action semantics - the MActions - to support the definition of operational semantics in metamodels and enable simulation as well as verification of dynamic properties. For this purpose, runtime models are incorporated with semantics for states, time, and properties of parallelism that allow a generic analysis solely bound to a certain metamodel definition. Furthermore, we develop the Linear Temporal Object Constraint Language (LT-OCL) to perform a dynamic analysis of execution runs based on the executable models. The semantics of this temporal predicate logic is bound to state changes of (recorded) execution traces that are linearizations of parallel changes of the runtimes model. This establishes the link to the theory of bisimulation as a second application case of dynamic analysis. Abstract State Machines (ASM) have been used to formally define the action language in conjunction with metamodels and the temporal logic. As proof of concept of the whole approach, the framework has been implemented and applied to two languages as case studies (namely Timed Automata and C#).

Cette thèse porte sur le monitorage des simulations de circuits en signaux mixtes. Dans le domaine de la vérification de matériel, l'utilisation de formalismes déclaratifs pour la specification, dans le cadre de la validation par simulation, s'est installée dans la pratique courante. Cependant, le manque de fonctionnalités visant à spécifier les comportements asynchrones, ou l'intégration insuffisante des résultats de la vérification, rend les language d'assertions et de mesures inopérants pour la vérification de comportements en signaux mixtes. Nous proposons des outils théoriques et pratiques pour la description et le monitorage de ces comportements, qui comportent des aspects à la fois discrets et continus. Pour cela, nous nous appuyons sur des travaux antérieurs portant sur les extensions temps-réel de la logique temporelle et des expressions régulières. Nous décrivons de nouveaux algorithmes pour calculer la distance entre une trace de simulation et une propriété en logique temporelle données. Une nouvelle procédure de diagnostic est conçue pour déboguer efficacement de telles traces. Le monitorage des comportements continus est ensuite étendu à d'autres formes d'assertions basées sur des expressions régulières. Ces expressions constituent la base de notre language de description de mesures, qui permet de définir conjointement la mesure et les intervals temporels sur lesquels cette mesure doit être prise. Nous montrons comment d'autres mesures, déjà mises en œuvre dans les simulateurs analogiques peuvent être importées dans les descriptions digitales. Ceci permet d'étendre vers le domaine en signaux mixtes les approches hiérarchiques utilisées en vérification de circuits digitaux. / This thesis is concerned with the monitoring of mixed-signal circuit simulations. In the field of hardware verification, the use of declarative property languages in combination with simulation is now standard practice. However the lack of features to specify asynchronous behaviors, or the insufficient integration of verification results, makes existing assertion and measurement languages unable to enforce mixed-signal requirements. We propose several theoretical and practical tools for the description and automatic monitoring of such behaviors, that feature both discrete and continuous aspects. For this we build on previous work on real-time extensions of temporal logic and regular expressions. We describe new algorithms to compute the distance from some simulation trace to temporal logic specifications, whose complexity is not higher than traditional monitoring. A novel diagnostic procedure is provided in order to efficiently debug such traces. The monitoring of continuous behaviors is then extended to other forms of assertions based on regular expressions. These expressions form the basis of our measurement language, that describes conjointly a measure and the patterns over which that measure should be taken. We show how other measurements implemented in analog circuits simulators can be ported to digital descriptions, this way extending structured verification approaches used for digital designs toward mixed-signal.

Le raisonnement spatial et temporel qualitatif est un domaine principal d’études de l’intelligence artificielle et, en particulier, du domaine de la représentation des connaissances, qui traite des concepts cognitifs fondamentaux de l’espace et du temps de manière abstraite. Dans notre thèse, nous nous focalisons sur les formalismes du domaine du raisonnement spatial et temporel qualitatif représentant les informations par des contraintes et apportons des contributions sur plusieurs aspects. En particulier, étant donnée des bases de connaissances d’informations qualitatives sur l’espace ou le temps, nous définissons des nouvelles conditions de consistance locale et des techniques associées afin de résoudre efficacement les problèmes fondamentaux se posant. Nous traitons notamment du problème de la satisfiabilité qui est le problème de décider s’il existe une interprétation quantitative de toutes les entités satisfaisant l’ensemble des contraintes qualitatives. Nous considérons également le problème de l’étiquetage minimal qui consiste à déterminer pour toutes les contraintes qualitatives les relations de base participant à au moins une solution ainsi que le problème de redondance consistant à déterminer les contraintes qualitatives non redondantes. En outre, nous enrichissons le domaine des formalismes spatio-temporels par des contributions concernant une logique spatio-temporelle combinant la logique temporelle propositionnelle (PTL) avec un langage de contraintes qualitatives spatiales et une étude de la problématique consistant à gérer une séquence temporelle de configurations spatiales qualitatives devant satisfaire des contraintes de transition. / Qualitative Spatial and Temporal Reasoning is a major field of study in Artificial Intelligence and, particularly, in Knowledge Representation, which deals with the fundamental cognitive concepts of space and time in an abstract manner. In our thesis, we focus on qualitative constraint-based spatial and temporal formalisms and make contributions to several aspects. In particular, given a knowledge base of qualitative spatial or temporal information, we define novel local consistency conditions and related techniques to efficiently solve the fundamental reasoning problems that are associated with such knowledge bases. These reasoning problems consist of the satisfiability problem, which is the problem of deciding whether there exists a quantitative interpretation of all the entities of a knowledge base such that all of its qualitative relations are satisfied by that interpretation, the minimal labeling problem, which is the problem of determining all the atoms for each of the qualitative relations of a knowledge base that participate in at least one of its solutions, and the redundancy problem, which is the problem of obtaining all the non-redundant qualitative relations of a knowledge base. Further, we enrich the field of spatio-temporal formalisms that combine space and time in an interrelated manner by making contributions with respect to a qualitative spatio-temporal logic that results by combining the propositional temporal logic (PTL) with a qualitative spatial constraint language, and by investigating the task of ordering a temporal sequence of qualitative spatial configurations to meet certain transition constraints.

This work studies new algorithms and data structures that are useful in the context of program verification. As computers have become more and more ubiquitous in our modern societies, an increasingly large number of computer-based systems are considered safety-critical. Such systems are characterized by the fact that a failure or a bug (computer error in the computing jargon) could potentially cause large damage, whether in loss of life, environmental damage, or economic damage. For safety-critical systems, the industrial software engineering community increasingly calls for using techniques which provide some formal assurance that a certain piece of software is correct.<p>One of the most successful program verification techniques is model checking, in which programs are typically abstracted by a finite-state machine. After this abstraction step, properties (typically in the form of some temporal logic formula) can be checked against the finite-state abstraction, with the help of automated tools. Alternating automata play an important role in this context, since many temporal logics on words and trees can be efficiently translated into those automata. This property allows for the reduction of model checking to automata-theoretic questions and is called the automata-theoretic approach to model checking. In this work, we provide three novel approaches for the analysis (emptiness checking) of alternating automata over finite and infinite words. First, we build on the successful framework of antichains to devise new algorithms for LTL satisfiability and model checking, using alternating automata. These algorithms combine antichains with reduced ordered binary decision diagrams in order to handle the exponentially large alphabets of the automata generated by the LTL translation. Second, we develop new abstraction and refinement algorithms for alternating automata, which combine the use of antichains with abstract interpretation, in order to handle ever larger instances of alternating automata. Finally, we define a new symbolic data structure, coined lattice-valued binary decision diagrams that is particularly well-suited for the encoding of transition functions of alternating automata over symbolic alphabets. All of these works are supported with empirical evaluations that confirm the practical usefulness of our approaches. / Ce travail traite de l'étude de nouveaux algorithmes et structures de données dont l'usage est destiné à la vérification de programmes. Les ordinateurs sont de plus en plus présents dans notre vie quotidienne et, de plus en plus souvent, ils se voient confiés des tâches de nature critique pour la sécurité. Ces systèmes sont caractérisés par le fait qu'une panne ou un bug (erreur en jargon informatique) peut avoir des effets potentiellement désastreux, que ce soit en pertes humaines, dégâts environnementaux, ou économiques. Pour ces systèmes critiques, les concepteurs de systèmes industriels prônent de plus en plus l'usage de techniques permettant d'obtenir une assurance formelle de correction.<p><p>Une des techniques de vérification de programmes les plus utilisées est le model checking, avec laquelle les programmes sont typiquement abstraits par une machine a états finis. Après cette phase d'abstraction, des propriétés (typiquement sous la forme d'une formule de logique temporelle) peuvent êtres vérifiées sur l'abstraction à espace d'états fini, à l'aide d'outils de vérification automatisés. Les automates alternants jouent un rôle important dans ce contexte, principalement parce que plusieurs logiques temporelle peuvent êtres traduites efficacement vers ces automates. Cette caractéristique des automates alternants permet de réduire le model checking des logiques temporelles à des questions sur les automates, ce qui est appelé l'approche par automates du model checking. Dans ce travail, nous étudions trois nouvelles approches pour l'analyse (le test du vide) desautomates alternants sur mots finis et infinis. Premièrement, nous appliquons l'approche par antichaînes (utilisée précédemment avec succès pour l'analyse d'automates) pour obtenir de nouveaux algorithmes pour les problèmes de satisfaisabilité et du model checking de la logique temporelle linéaire, via les automates alternants.Ces algorithmes combinent l'approche par antichaînes avec l'usage des ROBDD, dans le but de gérer efficacement la combinatoire induite par la taille exponentielle des alphabets d'automates générés à partir de LTL. Deuxièmement, nous développons de nouveaux algorithmes d'abstraction et raffinement pour les automates alternants, combinant l'usage des antichaînes et de l'interprétation abstraite, dans le but de pouvoir traiter efficacement des automates de grande taille. Enfin, nous définissons une nouvelle structure de données, appelée LVBDD (Lattice-Valued Binary Decision Diagrams), qui permet un encodage efficace des fonctions de transition des automates alternants sur alphabets symboliques. Tous ces travaux ont fait l'objet d'implémentations et ont été validés expérimentalement. / Doctorat en Sciences / info:eu-repo/semantics/nonPublished

Les méthodes d’ingénierie dirigée par modèle des systèmes, telles que la simulation, l’analyse formelle et l’émulation ont été intensivement utilisées ces dernières années pour étudier et prévoir les propriétés et les comportements des systèmes complexes. Les résultats de ces analyses révèlent des connaissances qui peuvent améliorer la compréhension d’un système existant ou soutenir un processus de conception de manière à éviter des erreurs couteuses (et catastrophiques) qui pourraient se produire dans le système. Les réponses à certaines questions que l’on se pose sur un système sont généralement obtenues en utilisant des méthodes d’analyse spécifiques ; par exemple les performances et les comportements d’un système peuvent être étudiés de façon efficace dans certains cadres expérimentaux, en utilisant une méthode appropriée de simulation. De façon similaire, la vérification de propriétés telles que la vivacité, la sécurité et l’équité sont mieux étudiées en utilisant des méthodes formelles appropriées tandis que les méthodologies d’émulation peuvent être utilisées pour vérifier des hypothèses temporelles et des activités et comportements impliquant des interactions humaines. Donc, une étude exhaustive d’un système complexe (ou même d’apparence simple) nécessite souvent l’utilisation de plusieurs méthodes d’analyse pour produire des réponses complémentaires aux probables questions. Nul doute que la combinaison de multiples méthodes d’analyse offre plus de possibilités et de rigueur pour analyser un système que ne peut le faire chacune des méthodes prise individuellement. Si cet exercice (de combinaison) permet d’aller vers une connaissance (presque) complète des systèmes complexes, son adoption pratique ne va pas de pair avec les avancées théoriques en matière de formalismes et d’algorithmes évolués, qui résultent de décennies de recherche par les praticiens des différentes méthodes. Ce déficit peut s’expliquer parles compétences mathématiques requises pour utiliser ces formalismes, en combinaison avec la faible portabilité des modèles entre les outils des différentes méthodes. Cette dernière exigence rend nécessaire la tâche herculéenne de créer et de gérer plusieurs modèles du même système dans différents formalismes et pour différents types d’analyse. Un autre facteur bloquant est que la plupart des environnements d’analyse sont dédiés à une méthode d’analyse spécifique (i.e., simulation, ou analyse formelle, ou émulation) et sont généralement difficiles à étendre pour réaliser d’autres types d’analyse. Ainsi, une vaste connaissance de formalismes supportant la multitude de méthodes d’analyse est requise, pour pouvoir créer les différents modèles nécessaires, mais surtout un problème de cohérence se pose lorsqu’il faudra mettre à jour séparément ces modèles lorsque certaines parties du système changent. La contribution de cette thèse est d’alléger les charges d’un utilisateur de méthodes d'analyse multiples, dans sa quête d’exhaustivité dans l’étude des systèmes complexes, grâce à un cadre qui utilise les technologies d’Ingénierie Dirigée par les Modèles (IDM) pour fédérer la simulation, l’analyse formelle et l’émulation. Ceci est rendu possible grâce à la définition d’un langage de spécification unifié de haut niveau, supporté par des capacités de synthèse automatiques d’artéfacts requis par les différentes méthodes d’analyse. (...) / Model-based systems engineering methodologies such as Simulation, Formal Methods (FM) and Enactment have been used extensively in recent decades to study, analyze, and forecast the properties and behaviors of complex systems. The results of these analyses often reveal subtle knowledge that could enhance deeper understanding of an existing system or provide timely feedbacks into a design process to avert costly (and catastrophic) errors that may arise in the system. Questions about different aspects of a system are usually best answered using some specific analysis methodologies; for instance, system's performance and behavior in some specified experimental frames can be efficiently studied using appropriate simulation methodologies. Similarly, verification of properties such as, liveness, safeness and fairness are better studied with appropriate formal methods while enactment methodologies may be used to verify assumptions about some time-based and human-in-the-loop activities and behaviors. Therefore, an exhaustive study of a complex (or even seemingly simple) system often requires the use of different analysis methodologies to produce complementary answers to likely questions. There is no gainsaying that a combination of multiple analysis methodologies offers more powerful capabilities and rigor to test system designs than can be accomplished with any of the methodologies applied alone. While this exercise will provide (near) complete knowledge of complex systems and helps analysts to make reliable assumptions and forecasts about their properties, its practical adoption is not commensurate with the theoretical advancements, and evolving formalisms and algorithms, resulting from decades of research by practitioners of the different methodologies. This shortfall has been linked to the prerequisite mathematical skills for dealing with most formalisms, which is compounded by little portability of models between tools of different methodologies that makes it mostly necessary to bear the herculean task of creating and managing several models of same system in different formalisms. Another contributing factor is that most of existing computational analysis environments are dedicated to specific analysis methodologies (i.e., simulation or FM or enactment) and are usually difficult to extend to accommodate other approaches. Thus, one must learn all the formalisms underlining the various methods to create models and go round to update all of them whenever certain system variables change. The contribution of this thesis to alleviating the burdens on users of multiple analysis methodologies for exhaustive study of complex systems can be described as a framework that uses Model-Driven Engineering (MDE) technologies to federate simulation, FM and enactment analysis methodologies behind a unified high-level specification language with support for automated synthesis of artifacts required by the disparate methodologies. This framework envelops four pieces of contributions: i) a methodology that emulates the Model- Driven Architecture (MDA) to propose an independent formalism to integrate the different analysis methodologies. ii) Integration of concepts from the three methodologies to provide a common metamodel to unite some selected formalisms for simulation, FM and enactment. Iii) Mapping rules for automated synthesis of artifacts for simulation, FM and enactment from a common reference model of a system and its requirements. iv) A framework for the enactment of idiscrete event systems. We use the beverage vending system as a running example throughout the thesis. (...)

In this thesis we focus on new methods for probabilistic model checking (PMC) with linear temporal logic (LTL). The standard approach translates an LTL formula into a deterministic ω-automaton with a double-exponential blow up. There are approaches for Markov chain analysis against LTL with exponential runtime, which motivates the search for non-deterministic automata with restricted forms of non-determinism that make them suitable for PMC. For MDPs, the approach via deterministic automata matches the double-exponential lower bound, but a practical application might benefit from approaches via non-deterministic automata. We first investigate good-for-games (GFG) automata. In GFG automata one can resolve the non-determinism for a finite prefix without knowing the infinite suffix and still obtain an accepting run for an accepted word. We explain that GFG automata are well-suited for MDP analysis on a theoretic level, but our experiments show that GFG automata cannot compete with deterministic automata. We have also researched another form of pseudo-determinism, namely unambiguity, where for every accepted word there is exactly one accepting run. We present a polynomial-time approach for PMC of Markov chains against specifications given by an unambiguous Büchi automaton (UBA). Its two key elements are the identification whether the induced probability is positive, and if so, the identification of a state set inducing probability 1. Additionally, we examine the new symbolic Muller acceptance described in the Hanoi Omega Automata Format, which we call Emerson-Lei acceptance. It is a positive Boolean formula over unconditional fairness constraints. We present a construction of small deterministic automata using Emerson-Lei acceptance. Deciding, whether an MDP has a positive maximal probability to satisfy an Emerson-Lei acceptance, is NP-complete. This fact has triggered a DPLL-based algorithm for deciding positiveness.

Cette étude s’inscrit dans le domaine de l’intelligence artificielle, plus précisément au croisement des deux domaines que sont la planification autonome en environnement probabiliste et la vérification formelle probabiliste. Dans ce contexte, elle pose la question de la maîtrise de la complexité face à l’intégration de nouvelles technologies dans les systèmes critiques : comment garantir que l’ajout d’une intelligence à un système, sous la forme d’une autonomie, ne se fasse pas au détriment de la sécurité ? Pour répondre à cette problématique, cette étude a pour enjeu de développer un processus outillé, permettant de concevoir des systèmes auto-adaptatifs critiques, ce qui met en œuvre à la fois des méthodes de modélisation formelle des connaissances d’ingénierie, ainsi que des algorithmes de planification sûre et optimale des décisions du système. / This study takes place in the broad field of Artificial Intelligence, specifically at the intersection of two domains : Automated Planning and Formal Verification in probabilistic environment. In this context, it raises the question of the integration of new technologies in critical systems, and the complexity it entails : How to ensure that adding intelligence to a system, in the form of autonomy, is not done at the expense of safety ? To address this issue, this study aims to develop a tool-supported process for designing critical, self-adaptive systems. Throughout this document, innovations are therefore proposed in methods of formal modeling and in algorithms for safe and optimal planning.

Learning-based testing is a testing paradigm that combines model-based testing with machine learning algorithms to automate the modeling of the SUT, test case generation, test case execution and verdict construction. A tool that implements LBT been developed at the CSC school at KTH called LBTest. LBTest utilizes machine learning algorithms with off-the-shelf equivalence- and model-checkers, and the modeling of user requirements by propositional linear temporal logic. In this study, it is be investigated whether LBT may be suitable for testing a micro bus architecture within an embedded telecommunication device. Furthermore ideas to further automate the testing process by designing a data model to automate user requirement generation are explored. / Inlärningsbaserad testning är en testningsparadigm som kombinerar model-baserad testning med maskininlärningsalgoritmer för att automatisera systemmodellering, testfallsgenering, exekvering av tester och utfallsbedömning. Ett verktyg som är byggt på LBT är LBTest, utvecklat på CSC skolan på KTH. LBTest nyttjar maskininlärningsalgoritmer med färdiga ekvivalent- och model-checkers, och modellerar användarkrav med linjär temporal logik. I denna studie undersöks det om det är lämpat att använda LBT för att testa en mikrobus arkitektur inom inbyggda telekommunikationsenheter. Utöver det undersöks även hur testprocessen skulle kunna ytterligare automatiseras med hjälp av en data modell för att automatisera generering av användarkrav.

Recent urbanization and industrialization have brought tremendous pressure and challenges to modern autonomous systems. When considering multiple complex tasks, cooperation and coordination between multiple agents can improve efficiency in a system. In real-world applications, multi-agent systems (MAS) are widely used in various fields, such as robotics, unmanned aerial systems, autonomous vehicles, distributed sensor networks, etc. Unlike traditional MAS systems based on pre-defined algorithms and rules, a special human-in-loop (HIL) based MAS involves human interactions to enhance the system’s adaptability for special scenarios, as well as apply human preferences for robot control. However, existing HIL strategies are primarily based on human involvement at a low level, such as mixed-initiative control and mixed-agent scenarios with both human-driven and intelligent robots. There are fewer investigations on applying HIL in high-level coordination. In particular, designing a coordination strategy for multi-task multi-agent scenarios, which can also deal with real-time human commands, will be one of the key topics of this Master’s thesis project. In this thesis work, different kinds of tasks described by signal temporal logic (STL) are created for agents, which can be enforced by control barrier function (CBF) constraints. Both centralized and distributed frameworks are designed for agent coordination. In detail, the centralized strategy is developed for machine-to-infrastructure (M2I) communication, by using the nonlinear model predictive control (NMPC) method to obtain collision-free trajectories. The distributed strategy utilizing graph theory is proposed for machine-to-machine (M2M), in order to reduce computation time by offloading. Most importantly, a HIL model is generated for both frameworks to apply online human commands to the coordination, with a novel task allocation protocol. Simulations and experiments are carried out on both Matlab and Python-based ROS simulators, to show that proposed frameworks can achieve obvious performance advantages in safety, smoothness, and stability for task completion. Numerical results are provided to validate the feasibility and applicability of our algorithms. / Den senaste urbaniseringen och industrialiseringen har medfört enormt tryck och utmaningar för moderna autonoma system. Vid beaktande av flera komplexa uppgifter kan samarbete och samordning mellan flera agenter förbättra effektiviteten i ett system. I verkliga tillämpningar används multiagent-system (MAS) i stor utsträckning inom olika områden, såsom robotik, obemannade luftfarkoster, autonoma fordon, distribuerade sensorsystem etc. Till skillnad från traditionella MAS-system baserade på fördefinierade algoritmer och regler, innebär ett särskilt människa-i-loop (HIL)-baserat MAS mänsklig interaktion för att förbättra systemets anpassningsförmåga till speciella scenarier samt anpassa mänskliga preferenser för robotstyrning. Emellertid är befintliga HIL-strategier främst baserade på mänsklig inblandning på en låg nivå, såsom mixad-initiativkontroll och mixade agentscenarier med både människa-drivna och intelligenta robotar. Det finns färre undersökningar om att tillämpa HIL på högnivåkoordination. Särskilt att utforma en koordineringsstrategi för fleruppgiftsfleragent-scenarier, som också kan hantera mänskliga kommandon i realtid, kommer att vara ett av huvudämnena för detta masterprojekt. I detta examensarbete skapas olika typer av uppgifter beskrivna av signaltemporallogik (STL) för agenter, som kan upprätthållas genom styrbarriärfunktions (CBF) -begränsningar. Både centraliserade och distribuerade ramverk utformas för agentkoordination. Mer specifikt utvecklas den centraliserade strategin för maskin-till-infrastruktur (M2I)-kommunikation genom att använda icke-linjär modellprediktiv reglering (NMPC) för att erhålla kollisionsfria trajektorier. Den distribuerade strategin med användning av grafteori föreslås för maskin-till-maskin (M2M) för att minska beräkningstiden genom avlastning. Viktigast av allt genereras en HIL-modell för båda ramverken för att tillämpa online-mänskliga kommandon på koordinationen med en ny protokoll för uppgiftstilldelning. Simuleringar och experiment utförs på både Matlab och Python-baserade ROS-simulatorer för att visa att de föreslagna ramverken kan uppnå tydliga prestandafördelar när det gäller säkerhet, smidighet och stabilitet för uppgiftsslutförande. Numeriska resultat presenteras för att validera genomförbarheten och tillämpligheten hos våra algoritmer.