Multi-core model checking algorithms for LTL verification with fairness assumptions

Publication Type

Conference Proceeding Article

Publication Date

5-2013

Abstract

The main challenge in model checking is the state space explosion. With developments in hardware today, most processors have many cores inside. To leverage on the advances in hardware, we can increase the performance of verifying large models by designing parallel algorithms to run efficiently on multi-core architecture. This work focuses on this problem in the context of Linear Temporal Logic (LTL) model checking, which can be seen as finding accepting cycles in a graph. Recently, there are some parallel algorithms based on Nested Depth First Search (NDFS). In this work, we propose two new parallel algorithms based on strongly connected component (SCC) searching algorithm (i.e., Tarjan's algorithm). By finding all the SCCs in the graph, our approaches can not only check LTL properties, but also handle fairness assumptions all together. The experiments show that our new algorithms are comparable or faster than the state-of-the-art multi-core algorithms.

Discipline

Software Engineering

Research Areas

Software and Cyber-Physical Systems

Publication

Proceedings of the 2013 20th Asia-Pacific Software Engineering Conference (APSEC), Bangkok, Thailand, December 2-5

First Page

547

Last Page

552

ISBN

9781479921447

Identifier

10.1109/APSEC.2013.79

Publisher

IEEE

City or Country

Thailand

Additional URL

https://doi.org/10.1109/APSEC.2013.79

This document is currently not available here.

Share

COinS