Formula-free finite abstractions for linear temporal verification of Stochastic Hybrid Systems

Abstract:

Results on approximate model-checking of Stochastic Hybrid Systems (SHS) against general temporal specifications lead to abstractions that structurally depend on the given specification or with a state cardinality that crucially depends on the size of the specification. In order to cope with the associated issues of generality and scalability, we propose a specification-free abstraction approach that is general, namely it allows constructing a single abstraction to be then used for a whole cohort of problems. It furthermore computationally outperforms specification-dependent abstractions over linear temporal properties, such as bounded LTL (BLTL). The proposed approach unifies techniques for the approximate abstraction of SHS over different classes of properties by explicitly relating the error introduced by the approximation to the distance between transition kernels of abstract and concrete models, and by propagating the error in time over the horizon of the specification.