40th Logic Seminar
Ichiro Hasuo

Dept. Computer Science, Univ. Tokyo
http://www-mmm.is.s.u-tokyo.ac.jp/~ichiro/

2013-2-21, 15:10-16:40

Seminar room of the RCIS, 3. floor

Hybrid systems are those which exhibit both discrete "jump" and continuous "flow" dynamics. Their importance---as components of cyber-physical systems---is paramount now that more and more physical systems (cars, airplanes, etc.) are controlled with computers.

There are naturally two directions towards the study of hybrid systems: control theory (typically continuous) and formal verification (typically discrete). For us from the formal verification community, therefore, the big challenge is how to incorporate continuous "flow" dynamics. Many existing techniques---such as hybrid automaton or Platzer’s differential dynamic logic---include differential equations explicitly. This incurs a difficult (and very interesting) question of how to handle differential equations.

In our project we take a different path of turning flow into jump---more precisely into infinitely many jumps each of which is infinitesimal (i.e. infinitely small). This makes everything discrete jump dynamics, to which all the discrete techniques accumulated in the community of formal verification readily apply. This venture is mathematically supported by nonstandard analysis, where we can rigorously speak about infinites and infinitesimals.

In the talk I will lay out: 1) our framework of a while-language and a Hoare-style program logic, augmented with an infinitesimal constant, for modeling and verification of hybrid systems; 2) how discrete verification techniques can be *transferred*, as they are, to hybrid applications, via the celebrated *transfer principle* in nonstandard analysis; and 3) the overview of our prototype automatic prover.

The talk is based on the joint work with Kohei Suenaga, Kyoto University, and Hiroyoshi Sekine, Univ. Tokyo.

References:
[1] Kohei Suenaga and Ichiro Hasuo. Programming with Infinitesimals: A While-Language for Hybrid System Modeling. Proc. ICALP 2011, Track B. LNCS 6756, p. 392-403. Springer-Verlag.

[2] Ichiro Hasuo and Kohei Suenaga. Exercises in Nonstandard Static Analysis of Hybrid Systems. Proc. CAV 2012. LNCS 7358, p. 462-478. Springer-Verlag.

[3] Kohei Suenaga, Hiroyoshi Sekine and Ichiro Hasuo. Hyperstream Processing Systems: Nonstandard Modeling of Continuous-Time Signals. Proc. POPL 2013, p. 417-430. ACM.

Contact Person Hiroakira Ono