ERATO Project Colloquium by Prof. Ichiro Hasuo will be held on Sep. 13th
On Tuesday September 13th, Prof. Ichiro Hasuo will give three talks for ERATO project colloquium at 16:30. Further details can be found below.
Widest Paths and Global Propagation in Bounded Value Iteration for Stochastic Games
(Replaying the talk at VeriProP 2022, based on [Phalakarn, Takisaka, Haas, Hasuo, CAV'20])
Solving stochastic games with the reachability objective is a fundamental problem, especially in quantitative verification and synthesis. For this purpose, bounded value iteration (BVI) attracts attention as an efficient iterative method. However, BVI's performance is often impeded by costly end component (EC) computation that is needed to ensure convergence.
Our contribution is a novel BVI algorithm that conducts, in addition to local propagation by the Bellman update that is typical of BVI, global propagation of upper bounds that is not hindered by ECs. To conduct global propagation in a computationally tractable manner, we construct a weighted graph and solve the widest path problem in it. Our experiments show the algorithm's performance advantage over the previous BVI algorithms that rely on EC computation.
Bisimulation Games Played in Fibered Categories
(Replaying the talk at VardiFest, based on [Komorida+, LICS'19 & '21]
and [Kori+, CAV'22])
I present our recent results [LICS'19,LICS'21] on capturing various bisimilarity notions--covering not only the conventional relational notion but also its quantitative extensions such as probabilistic bisimulation and bisimulation metric--in the language of category theory. The theory combines abstract category theory and concrete games--so-called codensity games which are played in categories--which I believe will be of interest of the audience.
Goal-Aware RSS for Complex Scenarios via Program Logic
(Replaying the talk at FoMLAS'22, based on [Hasuo, Eberhart, Haydon et al., IEEE Trans. Intell. Vehicles '22])
I present our work that establishes a formal logic foundation for RSS, a recent methodology for "theorem proving" safety of automated driving systems. RSS is proposed by researchers at Intel/Mobileye and is attracting a lot of interests from industry and academia alike, but its formal aspects have been underdeveloped (although RSS is really about theorem proving). In the paper, we introduce a logic dFHL--it can be seen as an adaptation of Platzer's differential dynamic logic--and a workflow for deriving formally verified safety rules. This extension of RSS allows one to prove the safety of much more complicated scenarios than RSS could previously handle. The workflow is experimentally evaluated, too.
Professor, National Institute of Informatics
16:30-18:00 / Tuesday, September 13th, 2022
If you would like to attend, please register through the following Google form:
A zoom link will be sent to you via e-mail. (using BCC).
For the latest information about ERATO colloquium / seminar, please visit the web.
Clovis Eberhart (ERATO MMSD Colloquium Organizer)
Email: eberhart [at] nii.ac.jp