Finite Bisimulations for Switched Linear Systems
From MaRDI portal
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.
Cited in
(6)- Augmented finite transition systems as abstractions for control synthesis
- Decentralized abstractions for multi-agent systems under coupled constraints
- Refinements of behavioural abstractions for the supervisory control of hybrid systems
- Reachability and observability reduction for linear switched systems with constrained switching
- Abstractions of varying decentralization degree for reachability of coupled multiagent systems
- Temporal logic control for stochastic linear systems using abstraction refinement of probabilistic games
This page was built for publication: Finite Bisimulations for Switched Linear Systems
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2982914)