Computing Reviews
Today's Issue Hot Topics Search Browse Recommended My Account Log In
Review Help
Search
Efficiency through uncertainty: scalable formal synthesis for stochastic hybrid systems
Cauchi N., Laurenti L., Lahijanian M., Abate A., Kwiatkowska M., Cardelli L.  HSCC 2019 (Proceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control, Montreal, Canada, Apr 16-18, 2019)240-251.2019.Type:Proceedings
Date Reviewed: Jul 12 2019

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.

Reviewer:  George Hacken Review #: CR146620 (1909-0342)
1) Hespanha, J. Logic-based switching algorithms in control, PhD thesis. Yale University, 1998. https://www.ece.ucsb.edu/~hespanha/published/phd.pdf.
2) Hespanha, J. Stochastic hybrid modeling of on-off TCP flows. In: Stochastic hybrid systems: recent developments and research trends. 160-173, CRC Press, 2001.
3) Hu, J.; Lygeros, J.; Sastry, S. Towards a theory of stochastic hybrid systems. In Hybrid systems: computation and control (LNCS 1790) Springer, 2000, 160–173.
4) Huth, M.; Ryan, M. Logic in computer science (2nd ed.). Cambridge University Press, Cambridge, UK, 2004.
Bookmark and Share
  Featured Reviewer  
 
Formal Methods (D.2.4 ... )
 
 
Temporal Logic (F.4.1 ... )
 
Would you recommend this review?
yes
no
Other reviews under "Formal Methods": Date
On a method of multiprogramming
Feijen W., van Gasteren A., Springer-Verlag New York, Inc., New York, NY, 1999. Type: Book (9780387988702)
May 1 2000
Computer-Aided reasoning: ACL2 case studies
Kaufmann M. (ed), Manolios P. (ed), Moore J. Kluwer Academic Publishers, Norwell, MA,2000. Type: Divisible Book
Jul 2 2002
Architecting families of software systems with process algebras
Bernardo M., Ciancarini P., Donatiello L. ACM Transactions on Software Engineering and Methodology 11(4): 386-426, 2002. Type: Article
Mar 10 2003
more...

E-Mail This Printer-Friendly
Send Your Comments
Contact Us
Reproduction in whole or in part without permission is prohibited.   Copyright 1999-2024 ThinkLoud®
Terms of Use
| Privacy Policy