FBSLS

FBSLS

Description: The Finite Bisimulations For Switched Linear Systems tool is designed to generate finite bisimulations for switched linear systems. Given a set of observations over polytopic subsets of the state space and a switched linear system with stable subsystems, the tool 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 tool iteratively constructs the bisimulation quotient for any larger sublevel set. The tool also implements synthesis of the switching law and system verification with respect to specifications given as syntactically co-safe Linear Temporal Logic (scLTL) formulas over the observed polytopic subsets.

The main entry of the tool is the MATLAB script named “BISIMULATION_SW.m”.
The extension to piecewise linear systems with piecewise polyhedral Lyapunov functions is also implemented. See `”BISIMULATION_SW.m” for details.

The tool is implemented in MATLAB. The tool takes as input:

• System dynamics
• A polyhedral Lyapunov function
• Working set, target set (sublevel sets of the Lyapunov function)
• Set of observations
• An automata file (see sccsyn for details of construction of the automata file from an scLTL formula)

VO Integration: No

Active: Yes

Available Benchmarks: No

Website: http://sites.bu.edu/hyness/switchedpolybis/

Download: Link

Documentation: None, other than the link above explianing how to construct an automata file.

Contact: BU Robotics Lab, contact form

Excerpt from: http://sites.bu.edu/hyness/switchedpolybis/