View source for Safety-Critical Autonomy and Verification for Space Missions

{{righttoc}} 
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. 

{| cellpadding=0 cellspacing=0 width=80%
|- valign=top
| 
Project participants:
{{project past participants}}
* Petter Nilsson (Postdoc, MCE)
|
Collaborators:
* Ali Agha (JPL)
* Aaron Ames (MCE/CDS)
|}

=== Objectives ===
[[Image:jpl-pdf17.png|right|400px]]
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 ===
{{project paper list}}

[[Category:Completed projects]]
{{Project
|Title=Safety-Critical Autonomy and Verification for Space Missions
|Agency=JPL
|Start date=1 Oct 2017
|End date=31 May 2018
|Support summary=1 postdoc
|Reporting requirements=Annual reports
|Project ID=JPL PDF17
}}