Abstract
Model checking is a promising automated verification technique. The state space explosion is the major difficulty of model checking. To deal with this problem, researchers present a new model checking algorithm for the temporal logic CTL based on MapReduce framework. And the algorithm’s data structure is defined for the Kripke structure. This MapReduce algorithm outputs the set of states of the model that satisfies the formula by giving a model and a CTL formula. Researchers justify its correctness by an example with the EU formula. Finally, an example illustrates the validity of this algorithm, and the result shows this method is feasible.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsReferences
Apache.: Welcome to Apache Hadoop[EB/OL]. http://hadoop.apache.org/ (2012)
Baier, C., Katoen, J.P.: Principles of Model Checking (Vol. 26202649). MIT Press, New York (2008)
Bourahla, M.: Distributed CTL model checking. Software, IEEE Proceedings-IET. 152(6):297–308 (2005)
Clarke, E.M., Grumberg, O., Peled, D A.: Model Checking. MIT press, Cambridge (2000)
Huth, M., Ryan, M.: Logic in Computer Science: Modelling and Reasoning About Systems, 2nd edn. Cambridge University Press, Cambridge (2004)
Kripke Structure (model checking)-Wikipedia, the Free Encyclopedia [EB/OL]. http://en.wikipedia.org/wiki/Kripke_structure_(model_checking) (2012)
Lam, C.: Hadoop in Action. Manning Publications Co, Greenwich (2010)
White, T.: Hadoop: The definitive guide. O’Reilly Media, Sebastopol (2012)
Acknowledgments
This work was supported by the National Natural Science Foundation of China (No.61070030, No.61111130121); Funding Project for Academic Human Resources Development in Institutions of Higher Learning Under the Jurisdiction of Beijing Municipality numbered PHR201107107; Plan of Beijing College Students’ research and entrepreneurial action.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer Science+Business Media New York
About this paper
Cite this paper
Guo, F., Wei, G., Deng, M., Shi, W. (2013). CTL Model Checking Algorithm Using MapReduce . In: Wong, W.E., Ma, T. (eds) Emerging Technologies for Information Systems, Computing, and Management. Lecture Notes in Electrical Engineering, vol 236. Springer, New York, NY. https://doi.org/10.1007/978-1-4614-7010-6_39
Download citation
DOI: https://doi.org/10.1007/978-1-4614-7010-6_39
Publisher Name: Springer, New York, NY
Print ISBN: 978-1-4614-7009-0
Online ISBN: 978-1-4614-7010-6
eBook Packages: EngineeringEngineering (R0)