Resynthesis - VerifiableRobotics/LTLMoP GitHub Wiki

Applications

Unknown-Region Exploration

  • Trigger: handler (upon detection of a new region that would affect the strategy)
  • Changes: map, specification (group update)

Dialogue-based Control

  • Trigger: UI (upon "go" command)
  • Changes: specification

Runtime Verification/Robustness

  • Trigger: violation of environment assumptions
  • Changes: The env safety and/or liveness assumptions of the specification

Online Trajectory Optimization (?)

  • Trigger: a) Current environment input changes to one that has not been seen before (simple) or b) Current goal order changed from previous ones (advance)
  • Changes: Spec (LTL file)

Approach

  1. pause execution
  2. modify existing specification as appropriate for specific application
  3. send through parser
  4. remove all initial conditions, replace with current execution state (NOTE: region needs to be specified in terms of new map, and internal propositions need to be limited to only those present in the updated specification)
  5. call synthesis (TODO: incremental/patching? what to do if unreal?)
  6. load in new strategy
  7. alert handlers that project has changed
  8. resume execution