Safety-Critical Autonomy and Verification for Space Missions

From Murray Wiki
Revision as of 02:34, 11 December 2022 by Murray (talk | contribs)
(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)
Jump to navigationJump to search

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:


  • Ali Agha (JPL)
  • Aaron Ames (MCE/CDS)



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.


  • Agency: JPL
  • Grant number:
  • Start date: 1 Oct 2017
  • End date: 31 May 2018
  • Support: 1 postdoc
  • Reporting: Annual reports