Write a Blog >>
POPL 2021
Sun 17 - Fri 22 January 2021 Online
Tue 19 Jan 2021 17:15 - 17:30 at VMCAI - Applications Chair(s): Rayna Dimitrova

In this paper, we implement a GPU-based quantitative model checker and compare its performance with a CPU-based one. Linear Temporal Logic for Control (LTLC) is a quantitative variation of LTL to describe properties of a linear system and LTLC-Checker [1] is an implementation of its model checking algorithm. In practice, its long and unpredictable execution time has been a concern in applying the technique to real-time applications such as automatic control systems. In this paper, we design an LTLC model checker using a GPGPU programming technique. The resulting model checker is not only faster than the CPU-based one especially when the problem is not simple, but it has less variation in the execution time as well. Furthermore, multiple counterexamples can be found together when the CPU-based checker can find only one.

Tue 19 Jan
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

17:00 - 17:30: ApplicationsVMCAI at VMCAI
Chair(s): Rayna DimitrovaCISPA Helmholtz Center for Information Security
17:00 - 17:15
A Synchronous Effects Logic for Temporal Verification of Pure Esterel
Yahui SongNational University of Singapore, Wei-Ngan ChinNational University of Singapore
Media Attached
17:15 - 17:30
A Design of GPU-Based Quantitative Model Checking
YoungMin KwonSUNY Korea, Eunhee Kim2e Consulting Corp.
Media Attached