Finite Bisimulations for Switched Linear Systems

Creative Commons License

AYDIN GÖL E., Ding X., Lazar M., Belta C.

IEEE TRANSACTIONS ON AUTOMATIC CONTROL, cilt.59, sa.12, ss.3122-3134, 2014 (SCI-Expanded) identifier identifier

  • Yayın Türü: Makale / Tam Makale
  • Cilt numarası: 59 Sayı: 12
  • Basım Tarihi: 2014
  • Doi Numarası: 10.1109/tac.2014.2351653
  • Dergi Adı: IEEE TRANSACTIONS ON AUTOMATIC CONTROL
  • Derginin Tarandığı İndeksler: Science Citation Index Expanded (SCI-EXPANDED), Scopus
  • Sayfa Sayıları: ss.3122-3134
  • Anahtar Kelimeler: Abstractions, formal methods, switched systems, DISCRETE-TIME-SYSTEMS, MODEL CHECKING, MOTION
  • Orta Doğu Teknik Üniversitesi Adresli: Evet

Özet

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.