  This work targets the development of an efficient abstraction method for
formal analysis and control synthesis of discrete-time stochastic hybrid
systems (SHS) with linear dynamics. The focus is on temporal logic
specifications, both over finite and infinite time horizons. The framework
constructs a finite abstraction as a class of uncertain Markov models known as
interval Markov decision process (IMDP). Then, a strategy that maximizes the
satisfaction probability of the given specification is synthesized over the
IMDP and mapped to the underlying SHS. In contrast to existing formal
approaches, which are by and large limited to finite-time properties and rely
on conservative over-approximations, we show that the exact abstraction error
can be computed as a solution of convex optimization problems and can be
embedded into the IMDP abstraction. This is later used in the synthesis step
over both finite- and infinite-horizon specifications, mitigating the known
state-space explosion problem. Our experimental validation of the new approach
compared to existing abstraction-based approaches shows: (i) significant
(orders of magnitude) reduction of the abstraction error; (ii) marked
speed-ups; and (iii) boosted scalability, allowing in particular to verify
models with more than 10 continuous variables.
