Strategy-Driven Partitioning into Switching Modes for Piecewise-Affine Systems with Continuous Environments
Ioannis Filippidis and Richard M. Murray
Submitted, 2014 Conference on Decision and Control (CDC)
We propose a methodology for abstracting discrete-time piecewise-affine systems influenced by additive continuous environment variables, to synthesize correct-by-construction controllers from linear temporal logic specifications. The proposed algorithm partitions the environment domain into polytopes, considered as modes controlled by the environment. In each mode the environment variable is treated as a bounded disturbance for the system. Mode polytopes are iteratively enlarged while a strategy isomorphism between successive system partitions can be constructed. Isomorphisms are obtained by solving the stable marriage problem after proving that our case admits a unique solution. This leads to mapping high-level symbolic variables to equivalence classes of polytopes, instead of single polytopes as in other works. We thus avoid the need to merge partitions, which can create sliver polytopes, causing numerical problems during reachability computations. The approach enables using the same strategy over partitions that have an isomorphic subgraph relevant to the strategy. Reachability checks between neighboring partitions are used to reduce non-determinism introduced by switching and allow continuous restoration of discrete state. If bifurca- tions occur that prevent strategy reuse, then switched system game synthesis is performed, and a logic modeling formalism proposed that avoids trivial cyclic counterexamples.
- Conference Paper: http://www.cds.caltech.edu/~murray/preprints/fm14-cdc s.pdf
- Project(s):
