Bounded epsilon-Reach Set Computation of a Class of Deterministic and Transversal Linear Hybrid Automata

TL;DR

This paper introduces a method to approximate the reach sets of a specific class of hybrid automata, called DTLHA, over finite time intervals with arbitrary precision using sampling and polyhedral over-approximation.

Contribution

It defines DTLHA, a new class of hybrid automata, and develops an algorithm to compute bounded epsilon-reach sets with arbitrary accuracy.

Findings

The approach can approximate reach sets arbitrarily closely.

The method is based on sampling and polyhedral over-approximation.

An algorithm and architecture for the computation process are proposed.

Abstract

We define a special class of hybrid automata, called Deterministic and Transversal Linear Hybrid Automata (DTLHA), whose continuous dynamics in each location are linear time-invariant (LTI) with a constant input, and for which every discrete transition up to a given bounded time is deterministic and, importantly, transversal. For such a DTLHA starting from an initial state, we show that it is possible to compute an approximation of the reach set of a DTLHA over a finite time interval that is arbitrarily close to the exact reach set, called a bounded epsilon-reach set, through sampling and polyhedral over-approximation of sampled states. We propose an algorithm and an attendant architecture for the overall bounded epsilon-reach set computation process.