MATISSE is a free MATLAB toolbox for safety verification and reachable set computation of large dimensional, constrained linear systems. Matisse is based on the framework of abstracting linear systems using approximate bisimulation relations [1,2,3,4]. Contrary to the usual notions of system equivalence and refinement based on language inclusion or exact bisimulation relations, approximate bisimulation relations do not require the behavior of a system and its abstraction to be exactly the same. Approximate bisimulation relations aim in capturing the most significant characteristics of a system dynamics and neglect less important ones. The degree of approximation is given by the precision of the approximate bisimulation. This precision notably provides a bound of the distance between the trajectories of a system and of its abstraction. Approximate bisimulation based abstraction is particularly useful for the safety verification problem which consists in checking whether the intersection of the reachable set of the system with an unsafe set is empty or not. If we can check that the distance of the unsafe set to the reachable set of the abstraction of the system is greater than the precision of the approximate bisimulation then it follows that the original system is safe. The more robustly safe a system, the more approximations are possible which confirms the intuitive fact that the verification of robustly safe systems should be easier.

References in zbMATH (referenced in 25 articles , 1 standard article )

Showing results 1 to 20 of 25.
Sorted by year (citations)

1 2 next

  1. Gosea, Ion Victor; Petreczky, Mihaly; Antoulas, Athanasios C.; Fiter, Christophe: Balanced truncation for linear switched systems (2018)
  2. Han, Xiao-Guang; Chen, Zeng-Qiang: A matrix-based approach to verifying stability and synthesizing optimal stabilizing controllers for finite-state automata (2018)
  3. Hoeher, P. A.: OFDM data detection and channel estimation (2017)
  4. Murthy, Abhishek; Islam, Md. Ariful; Smolka, Scott A.; Grosu, Radu: Computing compositional proofs of input-to-output stability using SOS optimization and (\delta)-decidability (2017)
  5. Tran, Hoang-Dung; Nguyen, Luan Viet; Xiang, Weiming; Johnson, Taylor T.: Order-reduction abstractions for safety verification of high-dimensional linear systems (2017)
  6. Yang, Kaihong; Ji, Haibo: Hierarchical analysis of large-scale control systems via vector simulation function (2017)
  7. Kaihong, Yang; Haibo, Ji: Hierarchical control of linear systems from the abstraction feedback gain (2016)
  8. Papadopoulos, Alessandro Vittorio; Prandini, Maria: Model reduction of switched affine systems (2016)
  9. Islam, Md. Ariful; Murthy, Abhishek; Bartocci, Ezio; Cherry, Elizabeth M.; Fenton, Flavio H.; Glimm, James; Smolka, Scott A.; Grosu, Radu: Model-order reduction of ion channel dynamics using approximate bisimulation (2015)
  10. Julius, A. Agung: Trajectory-based theory for hybrid systems (2015)
  11. Kobayashi, Koichi; Imura, Jun-Ichi; Matsushima, Hiromichi: Model predictive control of directed-graph constrained systems (2015)
  12. Munteanu, Laura; Grasse, Kevin A.: Constructing simulation relations for IDO systems affine in inputs and disturbances (2015)
  13. Tanner, Herbert G.; Fu, Jie; Rawal, Chetan; Piovesan, Jorge L.; Abdallah, Chaouki T.: Finite abstractions for hybrid systems with stable continuous dynamics (2012)
  14. Braman, Julia M. B.; Murray, Richard M.: Bisimulation conversion and verification procedure for goal-based control systems (2011)
  15. Chatterjee, Krishnendu; Majumdar, Rupak: Minimum attention controller synthesis for omega-regular objectives (2011)
  16. Girard, Antoine; Pappas, George J.: Approximate bisimulation: a bridge between computer science and control theory (2011)
  17. Kobayashi, Koichi; Imura, Jun-ichi; Hiraishi, Kunihiko: Stabilization of finite automata with application to hybrid systems control (2011)
  18. Quesel, Jan-David; Fränzle, Martin; Damm, Werner: Crossing the bridge between similar games (2011)
  19. Casagrande, Alberto; Piazza, Carla; Policriti, Alberto: Discrete semantics for hybrid automata. Avoiding misleading assumptions in systems biology (2009)
  20. Girard, Antoine; Pappas, George J.: Hierarchical control system design using approximate simulation (2009)

1 2 next