WP 4: Implicit and explicit information-based reconfigurable discrete controller synthesis
WP Leader: KTH
The main objectives of this WP involve the controller synthesis in the discrete domain. Agent specifications are described by the rich framework of formal methods such as Linear Temporal Logic Formulas (LTL) and are enriched online through the updated implicit (sensor-based) and explicit (symbolic) information each agent receives. The particular issues that will be tackled are as follows:
- Controller synthesis for each agent from individual LTL specification.
- Specification adjustment due to updates based on impicit and explicit communication.
- Gradual verification at meeting events with other agents in the group.
- Reconfiguration strategies at the discrete level in the event that mutual satisfiability of agents plans are not possible.