Augmented finite transition systems as abstractions for control synthesis

作者：Nilsson Petter^*; Ozay Necmiye; Liu Jun

来源：Discrete Event Dynamic Systems, 2017, 27(2): 301-340.

DOI：10.1007/s10626-017-0243-z

• Correct-by-construction
• Control synthesis
• Abstraction refinement

This work is motivated by the problem of synthesizing switching protocols for continuous switched systems described by differential or difference equations, in a way that guarantees that the resulting closed-loop trajectories satisfy certain high-level specifications expressed in linear temporal logic. We introduce augmented finite transition systems as an abstract representation of the continuous dynamics; the augmentation consists in encodings of liveness properties that can be used to enforce progress in accordance with the underlying continuous dynamics. Abstraction and refinement relations that induce a preorder on this class of finite transition systems are established, and, by construction, this preorder respects the feasibility (i.e., realizability) of the synthesis problem. Hence, existence of a discrete strategy for one of these abstract finite transition systems guarantees the existence of a switching protocol for the continuous system that enforces the specification for all resulting trajectories. We show how abstractions and refinements can be computed for different classes of continuous systems through an incremental synthesis procedure that starts with a coarse abstraction and gradually refines it according to the established preorder relations. Finally, the incremental synthesis procedure is tailored to a class of temporal logic formulas by utilizing specific fixed point structures to enable localized updates in the refinement steps. The procedure is not guaranteed to terminate in general but we illustrate its practical applicability on numerical examples.

• 出版日期2017-6