Hybrid systems are those “with both continuous dynamics and discrete logic” [1]. The discrete logic serves to label or parametrize (my terms) states; state-specific continuous dynamics, modeled largely if not exclusively by differential equations, operate within each discrete state [2]. A particularly good example is an array of proportional-integral-derivative (PID) controllers--labeled discretely as, say, 1, ..., N--whose set points are periodically adjusted by a human(-in-the-loop) operator [1]. If, furthermore, transitions among a hybrid system’s states are modeled as probabilistic rather than deterministic, then that system is a stochastic hybrid system (SHS), the general subject of this paper [2,3]. (The more specific subject is discrete-time SHSs.)
Given the basic context just set, it is appropriate to mention here that this excellent paper is clearly aimed at experts, though mindful reading by nonspecialists will serve quite well as serviceable orientation. The ideal level of desired expertise extends to formal methods. Markov processes already go with the stochastic territory; here, however, continuous-space stochastic models are “abstracted” to discrete-space Markov models. The reader should, in this regard, also be comfortable with the notion of convex optimization. The introduction states that formal methods “can provide formal guarantees [of] the probabilistic satisfaction of quantitative specifications, such as those expressed in linear temporal logic (LTL)” [4]. This “theoretical and computational” framework is “both formal and scalable.” Scalability is here an amelioration, if not elimination, of the plague of state-space explosion.
Seven mathematically/logically rigorous theoretical sections are followed by section 8, “Experimental Results,” which includes three case studies of interval Markov decision processes (IMDP) as mapped by the authors to SHSs. The sections include explication of SHSs, temporal logic specifications, Markov models, post images of polytopes (convex optimization), SHS abstractions as IMDPs, IMDP computation and space discretization, bounds of transition probabilities, strategy synthesis, and computed satisfaction probability correctness.
The relegation of proofs to an appendix contributes to this paper’s smooth flow, thus ameliorating the reader’s assimilation of its subject matter. Section 8’s table 1 and figures 1 and 2 substantiate the computational performance improvement that the authors have achieved.
I am very glad to have read--and happy to recommend--this paper.