Finite Bisimulations for Switched Linear Systems

Date

2014-12-01

Author

Aydın Göl, Ebru
Ding, Xuchu
Lazar, Mircea
Belta, Calin

Metadata

Show full item record

This work is licensed under a Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International License.

Item Usage Stats

26
views

24
downloads

Cite This

In this paper, we consider the problem of constructing a finite bisimulation quotient for a discrete-time switched linear system in a bounded subset of its state space. Given a set of observations over polytopic subsets of the state space and a switched linear system with stable subsystems, the proposed algorithm generates the bisimulation quotient in a finite number of steps with the aid of sublevel sets of a polyhedral Lyapunov function. Starting from a sublevel set that includes the origin in its interior, the proposed algorithm iteratively constructs the bisimulation quotient for the region bounded by any larger sublevel set. We show how this bisimulation quotient can be used for synthesis of switching laws and verification with respect to specifications given as syntactically co-safe Linear Temporal Logic formulae over the observed polytopic subsets.

Subject Keywords

Abstractions, Formal methods, Switched systems

URI

https://hdl.handle.net/11511/46021

Collections

Department of Computer Engineering, Article