Overview
LTLMoP is a modular toolkit for high-level, provably-correct robot control.
This page presents an overview of the system, with links to subcomponents for further detail.
In general, workflow within LTLMoP is as follows:
- The user writes a [task specification](Task Specifications) over an [abstraction of the problem](Task Specifications#abstraction) (using SpecEditor)
- This specification, combined with a workspace map (created using RegionEditor1), is transformed by a parser into an LTL specification
- A synthesis tool attempts to create a discrete control strategy that satisfies the LTL specification.
- If a strategy exists (i.e. the specification is synthesizable):
- The Executor composes the discrete strategy with continuous control handlers to create a hybrid controller
- The way in which the strategy is composed with handlers is determined by an execution configuration (created with ConfigEditor1)
- This hybrid controller is then used to control a [real or simulated robot](Supported Robots), with real-time execution status displayed in the [Execution Status Monitor](Execution Status Monitor)
- If a strategy does not exist (i.e. the specification is unsynthesizable):
- Analysis tools help the user to determine the cause of unsynthesizability.
- Some feedback is shown directly in SpecEditor, but in more complex cases the interactive [Counter-strategy Visualizer](Counterstrategy Visualization Tool) can provide further insight.
1. In most cases, there is no need to manually start any application other than SpecEditor. They are all accessible from the SpecEditor GUI.