# Reachability analysis of linear hybrid systems via block decomposition

## TL;DR

This paper introduces a novel approach for reachability analysis of linear hybrid systems that reduces computational complexity by performing most calculations in low-dimensional spaces through block decomposition and strategic operator enhancements.

## Contribution

The paper presents an improved method for reachability analysis that optimizes continuous and discrete post operators, enabling efficient analysis of high-dimensional linear hybrid systems.

## Key findings

- Enhanced continuous-post operator reduces computation in high-dimensional space.
- Discrete-post operator leverages system structure for low-dimensional computations.
- Demonstrated effectiveness on challenging benchmark systems.

## Abstract

Reachability analysis aims at identifying states reachable by a system within a given time horizon. This task is known to be computationally expensive for linear hybrid systems. Reachability analysis works by iteratively applying continuous and discrete post operators to compute states reachable according to continuous and discrete dynamics, respectively. In this paper, we enhance both of these operators and make sure that most of the involved computations are performed in low-dimensional state space. In particular, we improve the continuous-post operator by performing computations in high-dimensional state space only for time intervals relevant for the subsequent application of the discrete-post operator. Furthermore, the new discrete-post operator performs low-dimensional computations by leveraging the structure of the guard and assignment of a considered transition. We illustrate the potential of our approach on a number of challenging benchmarks.