Oxford logo
[CLL+19] Nathalie Cauchi, Luca Laurenti, Morteza Lahijanian, Alessandro Abate, Marta Kwiatkowska and Luca Cardelli. Efficiency through Uncertainty: Scalable Formal Synthesis for Stochastic Hybrid Systems. In Proc. 22nd ACM International Conference on Hybrid Systems: Computation and Control (HSCC'19), ACM. 2019. [pdf] [bib]
Downloads:  pdf pdf (589 KB)  bib bib
Abstract. 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 speci fications, both over fi nite and in finite 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 speci fication is synthesized over the IMDP and mapped to the underlying SHS. In contrast to existing formal approaches, which are by and large limited to fi nite-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 fi nite- and in finite-horizon speci fications, mitigating the known state-space explosion problem. Our experimental validation of the new approach compared to existing abstraction-based approaches shows: (i) signi ficant (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.