No description available.

No description available.

No description available.

No description available.

Motion-planning is an essential component of autonomous aerial and terrestrial vehicles. The canonical Motion-planning problem, which is widely studied in the literature, is of planning point-to-point motion while avoiding obstacles. However, the desired degree of vehicular autonomy has steadily risen, and has consequently led to motion-planning problems where a vehicle is required to accomplish a high-level intelligent task, rather than simply move between two points. One way of specifying such intelligent tasks is via linear temporal logic (LTL) formulae. LTL is a formal logic system that includes temporal operators such as always, eventually, and until besides the usual logical operators. For autonomous vehicles, LTL formulae can concisely express tasks such as persistent surveillance, safety requirements, and temporal orders of visits to multiple locations. Recent control theoretic literature has discussed the generation of reference trajectories and/or the synthesis of feedback control laws to enable a vehicle to move in manners that satisfy LTL specifications. A crucial step in such synthesis is the generation of a so-called discrete abstraction of a vehicle kinematic/dynamic model. Typical techniques of generating a discrete abstraction require strong assumptions on controllability and/or linearity. This dissertation discusses fast motion-planning and control techniques to satisfy LTL specifications for vehicle models with nonholonomic kinematic constraints, which do not satisfy the aforesaid assumptions. The main contributions of this dissertation are as follows. First, we present a new technique for constructing discrete abstractions of a Dubins vehicle model (namely, a vehicle that moves forward at a constant speed with a minimum turning radius). This technique relies on the so-called method of lifted graphs and precomputed reachable set calculations. Using this technique, we provide an algorithm to generate vehicle reference trajectories satisfying LTL specifications without requiring complete controllability in the presence of workspace constraints, and without requiring linearity or linearization of the vehicle model. Second, we present a technique for centralized motion-planning for a team of vehicles to collaboratively satisfy a common LTL specification. This technique is also based on the method of lifted graphs. Third, we present an incremental version of the proposed motion-planning techniques, which has an “anytime" property. This property means that a feasible solution is computed quickly, and the iterative updates are made to this solution with a guarantee of convergence to an optimal solution. This version is suited for real-time implementation, where a hard bound on the computation time is imposed. Finally, we present a randomized sampling-based technique for generating reference trajectories that satisfy given LTL specifications. This technique is an alternative to the aforesaid technique based on lifted graphs. We illustrate the proposed techniques using numerical simulation examples. We demonstrate the superiority of the proposed techniques in comparison to the existing literature in terms of computational time and memory requirements.

The reason for data mining is to generate rules that can be used as the basis for making decisions. One such area is sequence mining which, in terms of transactional datasets, can be stated as the discovery of inter-transaction associations or associations between different transactions. The data used for sequence mining is not limited to data stored in overtly temporal or longitudinally maintained datasets and in such domains data can be viewed as a series of events, or episodes, occurring at specific times. The problem thus becomes a search for collections of events that occur frequently together. While the mining of frequent episodes is an important capability, the manner in which such episodes interact can provide further useful knowledge in the search for a description of the behaviour of a phenomenon but as yet has received little investigation. Moreover, while many sequences are associated with absolute time values, most sequence mining routines treat time in a relative sense, returning only patterns that can be described in terms of Allen-style relationships (or simpler), ie. nothing about the relative pace of occurrence. They thus produce rules with a more limited expressive power. Up to this point in time temporal interval patterns have been based on the endpoints of the intervals, however in many cases the ‘natural’ point of reference is the midpoint of an interval and it is therefore appropriate to develop a mechanism for reasoning between intervals when midpoint information is known. This thesis presents a method for discovering interacting episodes from temporal sequences and the analysis of them using temporal patterns. The mining can be conducted both with and without the mechanism for handling the pace of events and the analysis is conducted using both the traditional interval algebras and a midpoint algebra presented in this thesis. The visualisation of rules in data mining is a large and dynamic field in its own right and although there has been a great deal of research in the visualisation of associations, there has been little in the area of sequence or episodic mining. Add to this the emerging field of mining stream data and there is a need to pursue methods and structures for such visualisations, and as such this thesis also contributes toward research in this important area of visualisation.

Model checking is an automated technique for deciding whether a computer program satisfies a temporal property. Abstraction is the key to scaling model checking to industrial-sized problems, which approximates a large (or infinite) program by a smaller abstract model and lifts the model checking result over the abstract model back to the original program. In this thesis, we study abstraction in model checking based on \emph{exact-approximation}, which allows for verification and refutation of temporal properties within the same abstraction framework. Our work in this thesis is driven by problems from both practical and theoretical aspects of exact-approximation. We first address challenges of effectively applying symmetry reduction to \emph{virtually} symmetric programs. Symmetry reduction can be seen as a \emph{strong} exact-approximation technique, where a property holds on the original program if and only if it holds on the abstract model. In this thesis, we develop an efficient procedure for identifying virtual symmetry in programs. We also explore techniques for combining virtual symmetry with symbolic model checking. Our second study investigates model checking of \emph{recursive} programs. Previously, we have developed a software model checker for non-recursive programs based on exact-approximating predicate abstraction. In this thesis, we extend it to reachability and non-termination analysis of recursive programs. We propose a new program semantics that effectively removes call stacks while preserving reachability and non-termination. By doing this, we reduce recursive analysis to non-recursive one, which allows us to reuse existing abstract analysis in our software model checker to handle recursive programs. A variety of \emph{partial} transition systems have been proposed for construction of abstract models in exact-approximation. Our third study conducts a systematic analysis of them from both semantic and logical points of view. We analyze the connection between semantic and logical consistency of partial transition systems, compare the expressive power of different families of these formalisms, and discuss the precision of model checking over them. Abstraction based on exact-approximation uses a uniform framework to prove correctness and detect errors of computer programs. Our results in this thesis provide better understanding of this approach and extend its applicability in practice.

Model checking is an automated technique for deciding whether a computer program satisfies a temporal property. Abstraction is the key to scaling model checking to industrial-sized problems, which approximates a large (or infinite) program by a smaller abstract model and lifts the model checking result over the abstract model back to the original program. In this thesis, we study abstraction in model checking based on \emph{exact-approximation}, which allows for verification and refutation of temporal properties within the same abstraction framework. Our work in this thesis is driven by problems from both practical and theoretical aspects of exact-approximation. We first address challenges of effectively applying symmetry reduction to \emph{virtually} symmetric programs. Symmetry reduction can be seen as a \emph{strong} exact-approximation technique, where a property holds on the original program if and only if it holds on the abstract model. In this thesis, we develop an efficient procedure for identifying virtual symmetry in programs. We also explore techniques for combining virtual symmetry with symbolic model checking. Our second study investigates model checking of \emph{recursive} programs. Previously, we have developed a software model checker for non-recursive programs based on exact-approximating predicate abstraction. In this thesis, we extend it to reachability and non-termination analysis of recursive programs. We propose a new program semantics that effectively removes call stacks while preserving reachability and non-termination. By doing this, we reduce recursive analysis to non-recursive one, which allows us to reuse existing abstract analysis in our software model checker to handle recursive programs. A variety of \emph{partial} transition systems have been proposed for construction of abstract models in exact-approximation. Our third study conducts a systematic analysis of them from both semantic and logical points of view. We analyze the connection between semantic and logical consistency of partial transition systems, compare the expressive power of different families of these formalisms, and discuss the precision of model checking over them. Abstraction based on exact-approximation uses a uniform framework to prove correctness and detect errors of computer programs. Our results in this thesis provide better understanding of this approach and extend its applicability in practice.

Highly dynamic and complex computing systems are increasingly needed and are relied upon in daily life. One such system is the dynamic network, particularly in communication, in which it has widespread applications, such as: Internet, peer-to-peer networks, mobile networks and wireless networks. Dynamic networks consist of nodes and edges whose operating status may change over time; the edges may be unreliable and operate intermittently. Message-passing in such networks is inherently difficult and reasoning about the behaviour of message-passing algorithms is also difficult and hard to analyse. Their behaviour and correctness are hard to formulate and establish. To undertake formal reasoning about such systems, abstract models are essential in order to separate the general reasoning about message routing and the updating of routing tables from the details of how these are implemented in particular networks. This thesis proposes a new approach to modelling and reasoning about dynamic networks as follows. It develops a series of abstract models which makes it possible to focus on the correctness of routing methods. It models the dynamic network as a “demonic” process which runs concurrently with routing updates and message-passing, to express dynamic networks as concurrent systems. This allows the use of temporal logic and fairness constraints to reason about dynamic networks. To do so, it introduces a modal logic and formulates concepts of fairness which capture network properties. The correctness of dynamic networks means that under certain conditions, all messages will eventually be delivered. Formulating networks as concurrent systems means can establish the correctness for networks that never cease to change. Modelling at that one level of abstraction means being able to prove the properties of networks independently of the mechanisms in actual networks. Therefore, it provides “a factorisation” of proofs of correctness for actual dynamic networks. The models are implemented as multi-threaded programs, and then adopted an experimental runtime verification tool called RULER to test whether model instances satisfy the modal correctness for message delivery.

Autonomous robots like household service robots, self-driving cars and dronesare emerging as important parts of our daily lives in the near future. They need tocomprehend and fulfill complex tasks specified by the users with minimal humanintervention. Also they should be able to handle un-modeled changes and contingentevents in the workspace. More importantly, they shall communicate and collaboratewith each other in an efficient and correct manner. In this thesis, we address theseissues by focusing on the distributed and hybrid control of multi-robot systemsunder complex individual tasks. We start from the nominal case where a single dynamical robot is deployed in astatic and fully-known workspace. Its local tasks are specified as Linear TemporalLogic (LTL) formulas containing the desired motion. We provide an automatedframework as the nominal solution to construct the hybrid controller that drives therobot such that its resulting trajectory satisfies the given task. Then we expand theproblem by considering a team of networked dynamical robots, where each robot hasa locally-specified individual task also as LTL formulas. In particular, we analyzefour different aspects as described below. When the workspace is only partially known to each robot, the nominal solutionmight be inadequate. Thus we first propose an algorithm for initial plan synthesis tohandle partially infeasible tasks that contain hard and soft constraints. We designan on-line scheme for each robot to verify and improve its local plan during runtime, utilizing its sensory measurements and communications with other robots. Itis ensured that the hard constraints for safety are always fulfilled while the softconstraints for performance are improved gradually. Secondly, we introduce a new approach to construct a full model of both robotmotion and actions. Based on this model, we can specify much broader robotic tasksand it is used to model inter-robot collaborative actions, which are essential for manymulti-robot applications to improve system capability, efficiency and robustness.Accordingly, we devise a distributed strategy where the robots coordinate theirmotion and action plans to fulfill the desired collaboration by their local tasks. Thirdly, continuous relative-motion constraints among the robots, such as collision avoidance and connectivity maintenance, are closely related to the stability,safety and integrity of multi-robot systems. We propose two different hybrid controlapproaches to guarantee the satisfaction of all local tasks and the relative-motionconstraints at all time: the first one is based on potential fields and nonlinear controltechnique; the second uses Embedded Graph Grammars (EGGs) as the main tool. At last, we take into account two common cooperative robotic tasks, namelyservice and formation tasks. These tasks are requested and exchanged among therobots during run time. The proposed hybrid control scheme ensures that the real-time plan execution incorporates not only local tasks of each robot but also thecontingent service and formation tasks it receives. Some of the theoretical results of the thesis have been implemented and demonstrated on various robotic platforms. / Denna avhandling fokuserar på distribuerad och hybridstyrning av multi-robot-system för komplexa, lokala och tidsberoende uppgifter. Dessa uppgifter specificerasav logiska formler rörande robotens rörelser och andra ageranden. Avhandlingenbehandlar ett tvärvetenskapligt område som integrerar reglering av nätverkaderobotsystem och planering baserad på formella metoder. Ett ramverk för hybridstyrning av flera dynamiska robotar med lokalt specificerade uppgifter presenteras.Fyra huvudscenarier betraktas: (1) robot-planering med motstridiga arbetsuppgifterinom ett delvis okänt arbetsområde; (2) beroende uppgifter för en grupp heterogenaoch samverkande robotar; (3) relativa rörelsebegränsningar hos varje robot; samt(4) robotar med uppgifter som begärs och bekräftas under körning. Numeriskasimuleringar och experiment visas för att validera de teoretiska resultaten. / <p>QC 20151204</p> / EU STREP RECONFIG: FP7-ICT-2011-9-600825 / Swedish Research Council (VR)