Time-annotated game graphs for synthesis from abstracted systems

The construction of discrete abstractions is a crucial part of many methods for control synthesis of hybrid systems subject to formal specifications. In general, the product of discrete abstractions may not be a discrete abstraction for the product of the underlying continuously-valued systems. Addressing this, we present a control synthesis method for transition systems that are built from components with uncertain timing characteristics. The new device, called here time-annotated game graphs, is demonstrated in a variety of examples. While it is applicable generally to parity games, we consider it in the context of control subject to GR(1) specifications. We show how a nominal strategy obtained without time knowledge can be modified to recover correctness when time information becomes available. The methods are applied to a brief case study of an aircraft electric power system.