CTL Model Checking based on Giraph

DOI

10.2991/icamcs-16.2016.133How to use a DOI?

Keywords

CTL, Kripke, Model checking, Giraph, Hadoop

Abstract

Model checking is a popular model based formal automated verification technology. Computation tree logic is a prominent branching temporal logic for specifying system properties. In order to dispose of the state space explosion problem, we proposed a novel method based on BSP model employing Giraph which is an iterative graph processing system with high scalability. The result of the experiments shows that our method is much more efficient than current methods based on Map-Reduce model.

Copyright

© 2016, the Authors. Published by Atlantis Press.

Open Access

This is an open access article distributed under the CC BY-NC license (http://creativecommons.org/licenses/by-nc/4.0/).

Download article (PDF)

TY  - CONF
AU  - Tingyin Duan
AU  - Qinglei Zhou
AU  - Shan Pan
AU  - Weijun Zhu
PY  - 2016/06
DA  - 2016/06
TI  - CTL Model Checking based on Giraph
BT  - Proceedings of the 2016 5th International Conference on Advanced Materials and Computer Science
PB  - Atlantis Press
SP  - 652
EP  - 657
SN  - 2352-5401
UR  - https://doi.org/10.2991/icamcs-16.2016.133
DO  - 10.2991/icamcs-16.2016.133
ID  - Duan2016/06
ER  -