No description available.

This thesis is a continuation of last year's work and it builds on earlier construction of a rover that will deploy an interferometer on the far side of the moon. The project is done in collaboration with (JPL) Jet Propulsion Laboratoryin Pasadena, California. Given the size of the mission, accuracy and time limit project has been split into several smaller projects. The areas that are the focus of this project are the suspension and the transition system. The transition system that is originated from the stage when the rover transforms from the transit mode to ready mode, and the suspension system, are in this thesis work presented by detailed conceptual design. The next step, not mentioned this thesis work, will be to perform aprimary structure design on the details. The project owner’s ultimate goal is to create a better understanding about the origins of the universe and its continual changing. This would give scientists an opportunity to study some of the most fundamental questions that are still are waiting for answers. Together with a group of energy engineers, Gustav Andersson and Emil Ericsson, we were caught by the very attractive project assignment, well aware that not many people get the chance or the opportunity to be involved or work with projects like this.

Yes / In advanced manufacturing systems, the production of complex and highly customisable products requires the preparation of many different product specifications and associated manufacturing process plans. The creation of these plans involves the search for the production resources (e.g. robots, machine tools, inspection devices) that are needed to implement the product specifications and how to orchestrate them. We present a model-based approach to the automatic generation of manufacturing process plans from the models of the target products and available resources. The modelling language is based on labelled transition systems, which are useful to represent sequences of operations that can be executed in parallel by multiple production resources. Some preliminary experimental results demonstrate the feasibility of the presented approach. / This conference paper will be released for public view at the end of the publisher embargo on 19 May 2025.

An architecture for norm-regulated multi-agent systems based on an algebraic approach to normative systems is instrumentalized and further developed. The core of the instrumentalization is a Prolog module, which together with a Java library can be used for creating client/server-based runtime systems. Norms are represented as conditional sentences, whose normative consequences are formulated by applying normative operators to descriptive conditions. From such general normative conditions follow normative sentences regarding specific states of affairs. These in turn result in permission or prohibition of individual actions in specific situations. Furthermore, an approach to turning runtime systems into instruments for problem-solving by using evolutionary mechanisms for evolving normative systems, is presented. The construction of norm-creating operators on conditions, which forms the basis for the representation of normative systems, is approached from two angles. (i) A logical analysis based on the Kanger-Lindahl theory of normative positions is conducted. This results in two extended sets of types of normative positions, and based on an algebraic version of one of these extended systems, a set of operators for creating agent-specific norms is constructed. (ii) An alternative analysis, which takes as its starting point a systematic exploration of types of state transitions, yields a set of norm-creating operators based on prohibition of transition types. It is furthermore argued that in the context of a class of transition systems, in which transitions are deterministic and associated with a single agent performing an act, operators based on (ii) specify a meaningful semantics of operators based on (i). Theoretical results together with shared code and example applications contribute to make possible theoretically sound, transparently described, and efficiently implemented norm-regulated autonomous agent systems. / En arkitektur för normreglerade multiagentsystem baserad på en algebraisk representation av normativa system instrumentaliseras och vidareutvecklas. Kärnan i instrumentaliseringen utgörs av en Prolog-modul som tillsammans med ett Java-bibliotek kan användas för att skapa client/server-baserad körbar kod. Normer representeras som ordnade par av grundvillkor och följdvillkor. De senare konstrueras genom att normativa operatorer appliceras på deskriptiva villkor. Från sådana generella normativa villkor följer normativa satser om specifika sakförhållanden, vilka i sin tur ger upphov till förbud mot eller tillåtelse att utföra enskilda handlingar i olika situationer. Vidare skisseras en metod för att göra körbara multiagentsystem till verktyg för problemlösning genom att använda evolutionära mekanismer för att odla fram normativa system. Konstruktionen av normskapande operatorer på villkor, vilka ligger till grund för representationen av normativa system, betraktas ur två olika synvinklar. (i) En logisk analys, baserad på Kanger-Lindahls teori om normativa positioner. Denna resulterar i två utökade uppsättningar av typer av normativa positioner och utgående från en algebraisk version av ett av dessa utökade system konstrueras sedan en uppsättning operatorer för att skapa agentspecifika normer. (ii) En alternativ analys, som tar sin utgångspunkt i en systematisk undersökning av olika typer av tillståndsövergångar. Denna ger upphov till en uppsättning av normskapande operatorer som är baserade på förbud mot olika typer av övergångar. Argument presenteras vidare för att inom ramen för en klass av övergångssystem, där övergångar är deterministiska och associerade med en agent som utför en handling, så specificerar operatorer baserade på (ii) en meningsfull semantik för operatorer baserade på (i). Teoretiska resultat tillsammans med tillgängliggjord programkod och exempel på tillämpningar bidrar till att underlätta skapandet av teoretiskt sunda, transparent beskrivna och effektivt implementerade normreglerade system av autonoma agenter. / <p>At the time of the doctoral defense, the following papers were unpublished and had a status as follows: Paper 4: Submitted. Paper 5: Forthcoming.</p>

With the development and integration of cyber-physical and safety-critical systems, control systems are expected to achieve tasks that include logic rules, receptive decision-making, safety constraints, and so forth. For example, in a persistent surveillance application, an unmanned aerial vehicle might be required to "take photos of areas A and B infinitely often, always avoid unsafe region C, and return to the charging point when the battery level goes low." One possible design approach to achieve such complex specifications is automata-based planning using formal verification algorithms. Central to the existing formal verification of continuous-time systems is the notion of abstraction, which consists of partitioning the state space into cells, and then formulating a certain control problem on each cell. The control problem is characterized as finding a state feedback to make all the closed-loop trajectories starting from one cell reach and enter a consecutive cell in finite time without intruding any other cells. This essentially abstracts the continuous system into a finite-state transition graph. The complex specifications can thus be checked against the simple transition model using formal verification tools, which yields a sequence of cells to visit consecutively. While control algorithms have been developed in the literature for linear systems associated with a polytopic partitioning of the state space, the partitioning and control problem for systems on a curved space is a relatively unexplored research area. In this thesis, we consider $ SO (3) $ and $ \ mathbb {S} ^ 2 $, the two most commonly encountered manifolds in mechanical systems, and propose several approaches to address the partitioning and control problem that in principle could be generalized to other manifolds. Chapter 2 proposes a discretization scheme that consists of sampling point generation and cell construction. Each cell is constructed as a ball region around a sampling point with an identical radius. Uniformity measures for the sampling points are proposed. As a result, the $SO(3)$ manifold is discretized into interconnected cells whose union covers the whole space. A graph model is naturally built up based on the cell adjacency relations. This discretization method, in general, can be extended to any Riemannian manifold. To enable the cell transitions, two reference trajectories are constructed corresponding to the cell-level plan. We demonstrate the results by solving a constrained attitude maneuvering problem with arbitrary obstacle shapes. It is shown that the algorithm finds a feasible trajectory as long as it exists at that discretization level. In Chapter 3, the 2-sphere manifold is considered and discretized into spherical polytopes, an analog of convex polytopes in the Euclidean space. Moreover, with the gnomonic projection, we show that the spherical polytopes can be naturally mapped into Euclidean polytopes and the dynamics on the manifold locally transform to a simple linear system via feedback linearization. Based on this transformation, the control problems then can be solved in the Euclidean space, where many control schemes exist with safe cell transition guarantee. This method serves as a special case that solves the partition-and-control problem by transforming the states and dynamics on manifold to Euclidean space in local charts. In Chapter 4, we propose a notion of high-order barrier functions for general control affine systems to guarantee set forward invariance by checking their higher order derivatives. This notion provides a unified framework to constrain the transient behavior of the closed-loop trajectories, which is essential in the cell-transition control design. The asymptotic stability of the forward invariant set is also proved, which is highly favorable for robustness with respect to model perturbations. We revisit the cell transition problem in Chapter 2 and show that even with a simple stabilizing nominal controller, the proposed high-order barrier function framework provides satisfactory transient performance. / <p>QC 20201012</p>

Message Sequence Charts are a visual representation of the system specification which shows how all the participating processes are interacting with each other. Message Sequence Graphs provide modularity by easily allowing combination of more than one Message Sequence Charts to show more complicated system behavior. Requirements modeled as Message Sequence Graphs give a global view of the system as interaction across all the participating processes can be viewed. Thus systems modeled as Message Sequence Graphs are like sequential composition of parallel process. This makes it very attractive during the requirements gathering and review phases as it needs inter-working between different stakeholders with varied domain knowledge and expertise – requirements engineers, system designers, end customers, test professionals etc. In this thesis we give a detailed construction of a finite-state transition system for a com-connected Message Sequence Graph. Though this result is fairly well-known in the literature there has been no precise description of such a transition system. Several analysis and verification problems concerning MSG specifications can be solved using this transition system. The transition system can be used to construct correct tools for problems like model-checking and detecting implied scenarios in MSG specifications. There are several contributions of this thesis. Firstly, we have provided a detailed construction of a transition system exactly implementing the message sequence graph. We have provided the detailed correctness arguments for this construction. Secondly, this construction works for general Message Sequence Graphs and not limited to com-connected graphs alone, although, we show that a finite model can be ensured only if the original graph is com-connected. Also, we show that the construction works for both synchronous and asynchronous messaging systems. Thirdly, we show how to find implied scenarios using the transition model we have generated. We also discuss some of the flaws in the existing approaches. Fourthly we provide a proof of undecidability argument for non com-connected MSG with synchronous messaging.

201 pages / Ensuring algorithms work accurately is crucial, especially when they drive safety critical systems like self-driving cars. We formally model a published distributed algorithm for autonomous vehicles to collaborate and pass thorough an intersection. Models are built and validated using the “Labelled Transition System Analyser” (LTSA). Our models reveal situations leading to deadlocks and crashes in the algorithm. We demonstrate two approaches to gain insight about a large and complex system without modeling the entire system: Modeling a sub system - If the sub system has issues, the super system too. Modeling a fast-forwarded state - Reveals problems that can arise later in a process. Some productivity tools developed for distributed system development are also presented. Manulator, our distributed system simulator, enables quick prototyping and debugging on a single workstation. LTSA-O, extension to LTSA, listens to messages exchanged in an execution of a distributed system and validates it against a model.

In this work, we propose a specialization of the inductive incremental coverability algorithm that solves alternating finite automata emptiness problem. We experiment with various design decisions, analyze them and prove their correctness. Even though the problem itself is PSpace-complete, we are focusing on making the decision of emptiness computationally feasible for some practical classes of applications. We have obtained interesting comparative results against state-of-the-art algorithms, especially in comparison with antichain-based algorithms.

Linear Temporal Logic (LTL), as one of the temporal logic, can generate a fully automated correct-by-design controller synthesis approach for single or multiple autonomous vehicles, under much more complex missions than the traditional point-to-point navigation.In this master thesis, a framework which combines model- checking-based robot motion planning with action planning is proposed based on LTL for-mulas. The specifications implicitly require both sequential regions for multi-agent to visit and the desired actions to perform at these regions while avoid-ing collision with each other and fixed obstacles. The high level motion and task planning and low level navigation function based collision avoidance controller are verified by nontrivial simulation and implementation on real quadcopter in Smart Mobility Lab.

A Cyber-physical System (CPS) can be described as a network of interlinked, concurrent computational components that interact with the physical world. Such a system is usually of reactive nature and must satisfy strict timing requirements to guarantee a correct behaviour. The components can be of mixed-criticality which implies different progress models and communication models, depending whether the focus of a component lies on predictability or resource efficiency. In this dissertation I present a novel approach that bridges the gap between stream processing models and Labelled Transition Systems (LTSs). The former offer powerful tools to describe concurrent systems of, usually simple, components while the latter allow to describe complex, reactive, components and their mutual interaction. In order to achieve the bridge between the two domains I introduce the novel LTS Synchronous Interface Automaton (SIA) that allows to model the interaction protocol of a process via its interface and to incrementally compose simple processes into more complex ones while preserving the system properties. Exploiting these properties I introduce an analysis to identify permanent blocking situations in a network of composed processes. SIAs are wrapped by the novel component-based coordination model Process Network with Synchronous Communication (PNSC) that allows to describe a network of concurrent processes where multiple communication models and the co-existence and interaction of heterogeneous processes is supported due to well defined interfaces. The work presented in this dissertation follows a holistic approach which spans from the theory of the underlying model to an instantiation of the model as a novel coordination language, called Streamix. The language uses network operators to compose networks of concurrent processes in a structured and hierarchical way. The work is validated by a prototype implementation of a compiler and a Run-time System (RTS) that allows to compile a Streamix program and execute it on a platform with support for ISO C, POSIX threads, and a Linux operating system.