publication . Conference object . 2016

Bandwidth and Wavefront Reduction for Static Variable Ordering in Symbolic Reachability Analysis

Meijer, Jeroen; van de Pol, Jan Cornelis; Rayadurgam, Sanjai; Tkachuk, Oksana;
Open Access English
  • Published: 07 Jun 2016
  • Publisher: Springer
Abstract
We investigate the use of bandwidth and wavefront reduction algorithms to determine a static BDD variable ordering. The aim is to reduce the size of BDDs arising in symbolic reachability. Previous work showed that minimizing the (weighted) event span of the variable dependency graph yields small BDDs. The bandwidth and wavefront of symmetric matrices are well studied metrics, used in sparse matrix solvers, and many bandwidth and wavefront reduction algorithms are readily available in libraries like Boost and ViennaCL. In this paper, we transform the dependency matrix to a symmetric matrix and apply various bandwidth and wavefront reduction algorithms, measuring ...
Subjects
free text keywords: IR-100721, Event span, Bandwidth, Profile, Sparse matrix, EWI-27067, Event locality, Petri net, METIS-318457, Wavefront, Decision diagram, Symbolic reachability
Related Organizations
Download from
Universiteit Twente Repository
Conference object . 2016
Provider: NARCIS
30 references, page 1 of 2

1. Aloul, F.A., Markov, I.L., Sakallah, K.A.: FORCE: a fast and easy-to-implement variableordering heuristic. In: 13th ACM, VLSI. pp. 116-119. ACM (2003)

2. Blom, S., van de Pol, J.: Symbolic Reachability for Process Algebras with Recursive Data Types. In: ICTAC 2008. LNCS, vol. 5160, pp. 81-95. Springer (2008)

3. Bollig, B., Wegener, I.: Improving the Variable Ordering of OBDDs Is NP-Complete. IEEE Trans. Comput. 45(9), 993-1002 (Sep 1996)

4. Bryant, R.E.: Graph-Based Algorithms for Boolean Function Manipulation. IEEE Trans. Computers 35(8), 677-691 (1986)

5. Burch, J.R., Clarke, E.M., Long, D.E.: Symbolic model checking with partitioned transition relations. In: VLSI 1991 (1991)

6. Ciardo, G., Marmorstein, R.M., Siminiceanu, R.: The saturation algorithm for symbolic state-space exploration. STTT 8(1), 4-25 (2006)

7. Ciardo, G., Miner, A.S., Wan, M.: Advanced features in SMART: the stochastic model checking analyzer for reliability and timing. SIGMETRICS PER 36(4), 58-63 (2009)

8. Cimatti, A., et al.: NuSMV Version 2: An OpenSource Tool for Symbolic Model Checking. In: CAV 2002. LNCS, vol. 2404. Springer (2002)

9. Cranen, S., et al.: An Overview of the mCRL2 Toolset and Its Recent Advances. In: TACAS 2013. LNCS, vol. 7795, pp. 199-213. Springer (2013) [OpenAIRE]

10. Cuthill, E., McKee, J.: Reducing the Bandwidth of Sparse Symmetric Matrices. In: Proceedings 24th National Conference. pp. 157-172. ACM (1969)

11. Gibbs, N.E., Poole, Jr, W.G., Stockmeyer, P.K.: An algorithm for reducing the bandwidth and profile of a sparse matrix. SIAM Journal on Numerical Analysis 13(2), 236-250 (1976)

12. Grumberg, O., Livne, S., Markovitch, S.: Learning to Order BDD Variables in Verification. JAIR 18, 83-116 (2003)

13. Heiner, M., Rohr, C., Schwarick, M.: MARCIE - Model checking And Reachability analysis done effiCIEntly. In: PETRI NETS 2013. LNCS, vol. 7927, pp. 389-399. Springer (2013)

14. Kant, G., et al.: LTSmin: High-Performance Language-Independent Model Checking. In: TACAS 2015. LNCS, vol. 9035, pp. 692-707. Springer (2015)

15. Karantasis, K.I., et al.: Parallelization of Reordering Algorithms for Bandwidth and Wavefront Reduction. In: ICHPC 2014. pp. 921-932. IEEE (2014)

30 references, page 1 of 2
Related research
Abstract
We investigate the use of bandwidth and wavefront reduction algorithms to determine a static BDD variable ordering. The aim is to reduce the size of BDDs arising in symbolic reachability. Previous work showed that minimizing the (weighted) event span of the variable dependency graph yields small BDDs. The bandwidth and wavefront of symmetric matrices are well studied metrics, used in sparse matrix solvers, and many bandwidth and wavefront reduction algorithms are readily available in libraries like Boost and ViennaCL. In this paper, we transform the dependency matrix to a symmetric matrix and apply various bandwidth and wavefront reduction algorithms, measuring ...
Subjects
free text keywords: IR-100721, Event span, Bandwidth, Profile, Sparse matrix, EWI-27067, Event locality, Petri net, METIS-318457, Wavefront, Decision diagram, Symbolic reachability
Related Organizations
Download from
Universiteit Twente Repository
Conference object . 2016
Provider: NARCIS
30 references, page 1 of 2

1. Aloul, F.A., Markov, I.L., Sakallah, K.A.: FORCE: a fast and easy-to-implement variableordering heuristic. In: 13th ACM, VLSI. pp. 116-119. ACM (2003)

2. Blom, S., van de Pol, J.: Symbolic Reachability for Process Algebras with Recursive Data Types. In: ICTAC 2008. LNCS, vol. 5160, pp. 81-95. Springer (2008)

3. Bollig, B., Wegener, I.: Improving the Variable Ordering of OBDDs Is NP-Complete. IEEE Trans. Comput. 45(9), 993-1002 (Sep 1996)

4. Bryant, R.E.: Graph-Based Algorithms for Boolean Function Manipulation. IEEE Trans. Computers 35(8), 677-691 (1986)

5. Burch, J.R., Clarke, E.M., Long, D.E.: Symbolic model checking with partitioned transition relations. In: VLSI 1991 (1991)

6. Ciardo, G., Marmorstein, R.M., Siminiceanu, R.: The saturation algorithm for symbolic state-space exploration. STTT 8(1), 4-25 (2006)

7. Ciardo, G., Miner, A.S., Wan, M.: Advanced features in SMART: the stochastic model checking analyzer for reliability and timing. SIGMETRICS PER 36(4), 58-63 (2009)

8. Cimatti, A., et al.: NuSMV Version 2: An OpenSource Tool for Symbolic Model Checking. In: CAV 2002. LNCS, vol. 2404. Springer (2002)

9. Cranen, S., et al.: An Overview of the mCRL2 Toolset and Its Recent Advances. In: TACAS 2013. LNCS, vol. 7795, pp. 199-213. Springer (2013) [OpenAIRE]

10. Cuthill, E., McKee, J.: Reducing the Bandwidth of Sparse Symmetric Matrices. In: Proceedings 24th National Conference. pp. 157-172. ACM (1969)

11. Gibbs, N.E., Poole, Jr, W.G., Stockmeyer, P.K.: An algorithm for reducing the bandwidth and profile of a sparse matrix. SIAM Journal on Numerical Analysis 13(2), 236-250 (1976)

12. Grumberg, O., Livne, S., Markovitch, S.: Learning to Order BDD Variables in Verification. JAIR 18, 83-116 (2003)

13. Heiner, M., Rohr, C., Schwarick, M.: MARCIE - Model checking And Reachability analysis done effiCIEntly. In: PETRI NETS 2013. LNCS, vol. 7927, pp. 389-399. Springer (2013)

14. Kant, G., et al.: LTSmin: High-Performance Language-Independent Model Checking. In: TACAS 2015. LNCS, vol. 9035, pp. 692-707. Springer (2015)

15. Karantasis, K.I., et al.: Parallelization of Reordering Algorithms for Bandwidth and Wavefront Reduction. In: ICHPC 2014. pp. 921-932. IEEE (2014)

30 references, page 1 of 2
Related research
Powered by OpenAIRE Open Research Graph
Any information missing or wrong?Report an Issue