Finite Bisimulations for Switched Linear Systems

TL;DR

This paper presents an algorithm to construct finite bisimulation quotients for discrete-time switched linear systems within bounded state spaces, enabling system verification and control synthesis using polyhedral Lyapunov functions.

Contribution

The paper introduces a novel algorithm that efficiently constructs finite bisimulation quotients for switched linear systems using sublevel sets of polyhedral Lyapunov functions.

Findings

Algorithm terminates in finite steps

Bisimulation quotients facilitate system verification

Applicable to systems with stable subsystems

Abstract

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 any larger sublevel set. The bisimulation quotient can then be further used for synthesis of the switching law and system verification with respect to specifications given as syntactically co-safe Linear Temporal Logic formulas over the observed polytopic subsets.