Safety-Critical Autonomy and Verification for Space Missions
The goal of this project is to develop a mathematical language to bridge the gap between high-level mission specifications and low-level control algorithms under partial and uncertain real-world environment representation. One of the important gaps between theory and real-world applications is that high level language that expresses mission in terms of temporal specifications, assumes the low level temporal properties are deterministic. This assumption is very unrealistic in real-world systems (in particular, for space applications) where the environment representation, and hence safety properties, are created based on imperfect and noisy sensor measurements.
|
Project participants:
|
Collaborators:
|
Objectives
Design belief space variants of probabilistic signal temporal logic to enable automatic synthesis of the mission plan under uncertainty. This language can exploit the rich information provided by the belief space controllers (i.e., time-varying probabilistic safety-level, cost, and time). As a result of this continuous probing, the mission logic can autonomously adapt to changes in system’s belief and environment state. The encoded logic is a hybrid system in the form of a directed graph: Each vertex is a domain for the continuous dynamics. Edges transition between domains based upon events such as sensor information, health information, external events.
References
- Temporal Logic Control of POMDPs via Label-based Stochastic Simulation Relations. S. Haesaert, P. Nilsson, C. I. Vasile, R. Thakker, A. Agha-mohammadi, A. D. Ames and R. M. Murray. To appear in IFAC Conference on Analysis and Design of Hybrid Systems (ADHS), 2018.
- Toward Specification-Guided Active Mars Exploration for Cooperative Robot Teams. P. Nilsson, S. Haesaert, C. Vasile, R. Thakker, A. Agha-mohammadi. R. M. Murray and A. D. Ames. To appear in Robotics: Science and Systems (RSS), 2018..
|
|
|
