Estimating reachable states of hybrid systems via l-complete approximations

This contribution treats the estimation of reachable states for timeinvariant hybrid systems. Using the framework provided by Willems behavioural systems theory, we suggest a method based on l-complete approximations, which can be realized by finite statemachines. The approximating behaviour is a superset of the original behaviour. Hence, the estimate of reachable states based on an l-complete approximation can be shown to be conservative, i.e. the exact set of reachable states is guaranteed to be contained in the estimate. Because of this property our method is adequate for verification tasks where the state variable has to remain within a certain specification