Systems and methods for timed plan verification and strategy synthesis for multi-robot coordination

A method implemented by a node for temporal plan verification and timed game automata, TIGA, controller strategy synthesis for coordination of a plurality of agents, the method comprising:

• determining a first model of a plurality of temporal plans for timed operations of the plurality of agents violates at least one predefined safety rule;
• generating the TIGA controller strategy for controlling the timed operations of at least a subset of the plurality of agents, the TIGA controller strategy meeting the at least one predefined safety rule and being based on the first model;
• and
• causing transmission of the TIGA controller strategy to a dispatch device for translating the TIGA controller strategy to instructions for the plurality of agents.

A dispatcher device for implementing a timed game automata, TIGA, controller strategy for coordination of a plurality of agents, comprising:

• processing circuitry configured to:
• receive the TIGA controller strategy for the plurality of agents;
• transform the TIGA controller strategy to first instructions for the plurality of agents, the first instructions being configured to modify at least one of a plurality of temporal plans for timed operations of the plurality of agents in order to satisfy at least one safety rule;
• and
• cause signaling of the first instructions to the plurality of agents.

A method implemented by a dispatcher device for implementing a timed game automata, TIGA, controller strategy for coordination of a plurality of agents, the method comprising:

• receiving the TIGA controller strategy for the plurality of agents;
• transforming the TIGA controller strategy to first instructions for the plurality of agents, the first instructions being configured to modify at least one of a plurality of temporal plans for timed operations of the plurality of agents in order to satisfy at least one safety rule;
• and
• causing signaling of the first instructions to the plurality of agents.