Computing Reviews
Today's Issue Hot Topics Search Browse Recommended My Account Log In
Review Help
Search
Differential hybrid games
Platzer A. ACM Transactions on Computational Logic18 (3):1-44,2017.Type:Article
Date Reviewed: Mar 22 2018

As software becomes ever more pervasive in safety-critical devices--from pacemakers to cars, from robots to airplanes--it is important that we have means of insuring their safety. For some of the more advanced applications, namely those that involve control systems that evolve simultaneously in discrete and continuous time, with both discrete and continuous inputs and outputs, we do not have any reasonable theory of how to do this. At best, we have simulation methods, and these are not known to be correct. This safety problem is, of course, extremely difficult.

The author of this paper has been forging ahead, at quite a breakneck pace, creating elegant, natural new theory to tackle just this problem. Step by step, more features of genuine interest get integrated into new frameworks. Differential hybrid games represent yet another significant step in creating a broad theory applicable to many systems of interest. Platzer is almost alone in forging this new path. Why? The following sentence from the end of the introduction of this paper greatly helps explain it: “These proofs draw from many areas, including logic, proof theory, Carathéodory solutions, viscosity solutions of PDEs, real algebraic geometry, and real analysis.” There are very few people who are both in the computing field and possess a mathematical background rich enough to encompass all of these domains. In fact, there are few mathematicians who do, never mind people with a software engineering bent, whose end goal is not elegant theory but rather effective tools to prove that safety-critical software is indeed safe.

The heavy mathematics is interspersed with clear illustrative examples and, just as important, remarks on subtle issues. For example, the quantifier on ζ in rule (1) on page 10 is explicated with an insightful example on the bottom of page 10 and the start of page 11. Even during the technically challenging section 5, where the principal results are proved, the author continues to carefully point out subtleties. The principal results here are that some well-justified proof rules are indeed sound. This culminates in the next section in a “surprising” result about expressivity, which goes in the opposite direction of results in the hybrid system case.

It is quite rare to find an author who can deftly leverage powerful mathematics from a wide variety of domains with such seeming ease, apply them to the solution of practical problems arising in concrete contexts, and write about it lucidly, taking great care in conveying intuition while not shying away from technical correctness. Anyone with an interest in formal methods applied to hybrid systems (and cyber-physical systems in general) should read this paper. If they want to know what’s next, they just have to dip into Platzer’s preprints on arXiv!

Reviewer:  Jacques Carette Review #: CR145926 (1806-0324)
Bookmark and Share
  Editor Recommended
Featured Reviewer
 
 
Semantics Of Programming Languages (F.3.2 )
 
 
Modal Logic (F.4.1 ... )
 
 
Performance of Systems (C.4 )
 
 
Special-Purpose And Application-Based Systems (C.3 )
 
Would you recommend this review?
yes
no
Other reviews under "Semantics Of Programming Languages": Date
Contractions in comparing concurrency semantics
Kok J. (ed), Rutten J. Theoretical Computer Science 76(2-3): 179-222, 2001. Type: Article
Aug 1 1991
Abstract language design
Bradley L. Theoretical Computer Science 77(1-2): 5-26, 1990. Type: Article
Nov 1 1991
Determinism → (event structure isomorphism = step sequence equivalence)
Vaandrager F. Theoretical Computer Science 79(2): 275-294, 1991. Type: Article
Dec 1 1991
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