Formal approaches to security-aware robotic motion planning using hyperproperties
Loading...
Authors
Meeting name
Sponsors
Date
Journal Title
Format
Thesis
Subject
Abstract
Motion planning and control of complex systems have in recent times gained a lot of attention in fields such as robotics. Usually, such problems are formulated as temporal logic specifications over a discrete representation of the given system. Despite the expressivity of conventional logic such as Linear Temporal Logic (LTL), Metric Temporal Logic (MTL), Signal Temporal logic (STL), etc., they cannot be used to formalize complex requirements such as side-channel timing, opacity, service-level agreements, etc., which are examples of hyperproperties. Hyperproperties generalize trace properties to enable reasoning about multiple computation traces that conventional logic cannot. In this dissertation, we introduce a new formalism, HyperTWTL, which extends the compact semantics of Time Window Temporal Logic (TWTL), a domain-specific formal specification language for robotics, by allowing explicit and simultaneous quantification over multiple execution traces. This work also proposes and evaluates methods and algorithms for synthesizing and verifying complex control policies formalized using HyperTWTL. The first part of this dissertation investigates a novel domain-specific formal specification language for specifying important timed hyperproperties such as information flow security policies, service level agreements, etc. Specifically, a new formal security specification language for robotic motion planning, HyperTWTL, will be introduced for TWTL (HyperTWTL) by extending the classical time window temporal logic (TWTL). The drawbacks of already existing hyper-temporal logic, specifically HyperLTL, HyperSTL, and HyperMTL, will be analyzed to enhance the feasibility and practicality of HyperTWTL. We will subsequently demonstrate the application of HyperTWTL to express timed hyperproperties in robotic applications. The second part of the dissertation discusses the proposal of efficient techniques for verification, specifically using automata-based and satisfiability modulo theory (SMT)-based model checking methods under HyperTWTL specifications. This is because most existing model-checking verification techniques based on both automata and SMT are limited to the analysis of individual trace executions and, as such, may not be applicable for the same purpose when using HyperTWTL. Recent works show the effectiveness and prospect of Hyperproperties, specifically Hyperproperties for Linear Temporal Logic (HyperLTL), in optimality-, robustness-, and privacy-aware robotic motion planning. However, despite their rich expressiveness, HyperLTL cannot express tasks with time constraints. In the third part of this dissertation, we demonstrate that HyperTWTL can be used to formalize complex robotic planning objectives. Given HyperTWTL specifications, we also propose a symbolic approach for synthesizing optimality-, robustness-, and privacy-aware strategies by reducing the planning problem to a first-order logic satisfiability problem. The planning problem was then solved using two industrial-strength SMT solvers. The feasibility of HyperTWTL and the efficiency and scalability of the proposed strategy synthesis approach are demonstrated by formalizing important motion planning objectives of a surveillance mission case study and synthesizing the respective strategies using Z3 and CVC4 SMT solvers. Traditionally, most temporal logic specifications have been verified using an automata-based model checking framework. Model checking is indeed an unavoidable part of designing safety-critical systems. However, verification of important properties of a given system using model checking does not guarantee that the system will behave as expected during the runtime operation, which falls under the scope of runtime verification (RV). The fourth part of this dissertation investigates efficient algorithms for runtime monitoring of HyperTWTL specifications. Reinforcement learning (RL) is a sequential decision-making process in which an agent continuously interacts with and learns from an unknown environment. This approach has been used with various temporal logics to solve motion planning problems. In the fifth part of this dissertation, we study the problem of learning to satisfy complex tasks assigned to robotic agents in environments that may exhibit probabilistic behavior. We investigate a Reinforcement Learning (RL) approach to maximizing the expected sum of rewards subject to constraints formalized as HyperTWTL during learning optimal policies for autonomous systems in unknown environments. The final part of the dissertation concludes this work and discusses future works.
Table of Contents
DOI
PubMed ID
Degree
Ph. D.