Sequential and Parallel Algorithms for the State Space Exploration

Allal, Lamia; Belalem, Ghalem; Dhaussy, Philippe; Teodorov, Ciprian

doi:10.1515/cait-2016-0001

Abstract

In this article, we are interested in the exploration part of model checking which consists in traversing all the possible states of a system. We propose two approaches to exploration, parallel and sequential. We present a comparison between our parallel approach and the parallel algorithm proposed in SPIN.

References

1. Abed, N., S. Tripakis, J.-M. Vincent. Resource-Aware Verification Using Randomized Exploration of Large State Spaces. − In: Proc. of 15th International SPIN Workshop, Model Checking Software, Los Angeles, CA, USA, August 10-12 2008, pp. 214-231.10.1007/978-3-540-85114-1_16
Search in Google Scholar
2. Boukala, M. C., L. Petrucci. Towards Distributed Verification of Petri Nets Properties. – In: Proc. of First International Conference on Verification and Evaluation of Computer and Communication Systems, VECoS’07, May 2007, pp. 13-24.
Search in Google Scholar
3. Christensen, S., L. M. Kristensen, T. Mailund. A Sweep-Line Method for State Space Exploration. – In: Proc. of 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS’2001, April 2001, pp. 450-464.10.1007/3-540-45319-9_31
Search in Google Scholar
4. Clarke, E. M., W. Klieber, M. Nová£ek, P. Zuliani. Model Checking and the State Explosion Problem. – In: Proc. of 8th Laser Summer School on Software Engineering, Vol. 7682, September 2011, pp. 1-30.
Search in Google Scholar
5. Daugherty, J. Java Concurrency Framework. CSCI 5448, Spring 2011, May 2011.
Search in Google Scholar
6. Dhaussy, P., J. C. Roger, F. Boniol. Reducing State Explosion with Context Modeling for Model-Checking. – In: Proc. of 13th International Symposium on High Assurance Systems Engineering, HASE, November 2011, pp. 130-137.10.1109/HASE.2011.24
Search in Google Scholar
7. Ever, E., O. Gemikonakli, A. Koçyigit, E. Gemikonakli. A Hybrid Approach to Minimize State Space Explosion Problem for the Solution of Two Stage Tandem Queues. − J. Network and Computer Applications, Vol. 36, 2013, No 2, pp. 908-926.10.1016/j.jnca.2012.10.006
Search in Google Scholar
8. Guan, N., Z. Gu, W. Yi, G. Yu. Improving Scalability of Model-Checking for Minimizing Buffer Requirements of Synchronous Dataflow Graphs. – In: Proc. of 14th Asia and South Pacific Design Automation Conference, ASP-DAC’09, January 2009, pp. 715-720.
Search in Google Scholar
9. Holzmann, G. J. The Model Checker SPIN. − IEEE Transactions on Software Engineering, Vol. 23, May 1997, No 5, pp. 279-295.10.1109/32.588521
Search in Google Scholar
10. Holzmann, G. J. Parallelizing the Spin Model Checker. – In: Proc. of 19th International Conference on Model Checking Software, SPIN’12, Berlin, Heidelberg, 2012. Springer-Verlag, pp. 155-171.10.1007/978-3-642-31759-0_12
Search in Google Scholar
11. Inggs, C. P., H. Barringer. Effective State Exploration for Model Checking on a Shared Memory Architecture. − Electr. Notes Theor. Comput. Sci., Vol. 68, 2002, No 4, pp. 605-620.10.1016/S1571-0661(05)80395-0
Search in Google Scholar
12. Kamkin, A. S. Projecting Transition Systems: Overcoming State Explosion in Concurrent System Verification. − Program. Comput. Softw., Vol. 41, November 2015, No 6, pp. 311-324.10.1134/S0361768815060043
Search in Google Scholar
13. Koster, A. M.C.A., M. Tieves. Network Design with Compression: Complexity and Algorithms. – In: Proc. of INFORMS Computing Society Conference (INFORMS ICS), 2015.
Search in Google Scholar
14. Kwiatkowska, M., G. Norman, D. Parker. Prism: Probabilistic Model Checking for Performance and Reliability Analysis. – ACM SIGMETRICS Performance Evaluation Review, Vol. 36, 2009, No 4, pp. 40-45.10.1145/1530873.1530882
Search in Google Scholar
15. Leggetter, C. J., P. C. Woodland. Maximum Likelihood Linear Regression for Speaker Adaptation of Continuous Density Hidden Markov Models. – Computer Speech and Language, Vol. 9, 1995, No 1, pp. 171-185.10.1006/csla.1995.0010
Search in Google Scholar
16. Lerda, F., R. Sisto. Distributed-Memory Model-Checking with Spin. – In: Proc. of 5th and 6th International SPIN Workshops on Theoretical and Practical Aspects of SPIN Model Checking, Vol. 1680, July 1999, pp. 22-39.
Search in Google Scholar
17. Mukherjee, A., Z. Tari, P. Bertok. Memory Efficient State-Space Analysis in Software Model-Checking. – In: Proc. of Thirty-Third Australasian Conference on Computer Science ACSC‘10, Vol. 102, January 2010, pp. 23-32.
Search in Google Scholar
18. Pelánek, R. Fighting State Space Explosion: Review and Evaluation. – In: Proc. of 13th Conference on Formal Methods for Industrial Critical Systems FMICS’08, Vol. 5596, September 2008, pp. 37-52.
Search in Google Scholar
19. Saad, R. T., S. D. Zilio, B. Berthomieu. A General Lock Free Algorithm for Parallel State Space Construction. – In: Proc. of 9th International Workshop on Parallel and Distributed Methods in Verification, PDMC-HIBI’10, October 2010, pp. 8-16.10.1109/PDMC-HiBi.2010.10
Search in Google Scholar
20. Walters, E. J., C. H. Morrell, R. E. Auer. An Investigation of the Median-Median Method of Linear Regression. – Journal of Statistics Education, Vol. 14, 2006, No 2.10.1080/10691898.2006.11910582
Search in Google Scholar

Sequential and Parallel Algorithms for the State Space Exploration

Abstract

Paradigm

My account