Safety-Critical Autonomy and Verification for Space Missions: Difference between revisions
(Created page with "{{subst:project boilerplate}} The main objective of this proposal is to develop a mathematical language to principally bridge the gap between high-level mission specificati...") |
No edit summary |
||
| (10 intermediate revisions by the same user not shown) | |||
| Line 1: | Line 1: | ||
{{righttoc}} | {{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% | {| cellpadding=0 cellspacing=0 width=80% | ||
|- valign=top | |- valign=top | ||
| | | | ||
Project participants: | |||
{{project | {{project past participants}} | ||
* Petter Nilsson (Postdoc, MCE) | |||
| | | | ||
Collaborators: | Collaborators: | ||
* Ali Agha (JPL) | |||
* Aaron Ames (MCE/CDS) | |||
|} | |} | ||
=== Objectives === | === Objectives === | ||
[[Image: | [[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 === | === References === | ||
{{project paper list}} | {{project paper list}} | ||
[[Category: | [[Category:Completed projects]] | ||
{{Project | {{Project | ||
|Title=Safety-Critical Autonomy and Verification for Space Missions | |Title=Safety-Critical Autonomy and Verification for Space Missions | ||
|Agency=JPL | |Agency=JPL | ||
|Start date=1 | |Start date=1 Oct 2017 | ||
|End date= | |End date=31 May 2018 | ||
|Support summary=1 postdoc | |Support summary=1 postdoc | ||
|Reporting requirements=Annual reports | |Reporting requirements=Annual reports | ||
|Project ID=JPL PDF17 | |||
}} | }} | ||
Latest revision as of 02:34, 11 December 2022
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..
|
|
|
