A Design of GPU-Based Quantitative Model Checking
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  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:15|
|A Synchronous Effects Logic for Temporal Verification of Pure Esterel|
|17:15 - 17:30|
|A Design of GPU-Based Quantitative Model Checking|