Time-annotated game graphs for synthesis from abstracted systems
- Creators
- Livingston, Scott C.
Abstract
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.
Additional Information
© 2015 IEEE. The author thanks Richard M. Murray for motivating discussions. This work was partially supported by United Technologies Corporation and IBM, through the industrial cyber-physical systems (iCyPhy) consortium.Additional details
- Eprint ID
- 66081
- DOI
- 10.1109/CDC.2015.7403290
- Resolver ID
- CaltechAUTHORS:20160412-100408277
- United Technologies Corporation
- IBM
- Created
-
2016-04-12Created from EPrint's datestamp field
- Updated
-
2021-11-10Created from EPrint's last_modified field