A Sweep-Line Method for Büchi Automata-based Model Checking

• Autorzy: Evangelista S. , Kristensen L.M.

Identyfikatory

DOI

10.3233/FI-2014-1003

• Języki publikacji: EN

Abstrakty

EN

The sweep-line method allows explicit state model checkers to delete states from memory on-the-fly during state space exploration, thereby lowering the memory demands of the verification procedure. The sweep-line method is based on a least-progress-first search order that prohibits the immediate use of standard on-the-fly Büchi automata-based model checking algorithms that rely on a depth-first search order in the search for an acceptance cycle. This paper proposes and experimentally evaluates an algorithm for Büchi automata-based model checking compatible with the search order and deletion of states prescribed by the sweep-line method.

Słowa kluczowe

EN

machine theory; computer storage devices; computer systems; computer algorithms; search engines

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2014
• Tom: Vol. 131, nr 1
• Strony: 27--53
• Opis fizyczny: Bibliogr. 35 poz., rys., tab.

Twórcy

autor

Evangelista S.

• Université Paris 13, Sorbonne Paris Cité, LIPN, CNRS, UMR 7030, F-93430, Villetaneuse, France

autor

Kristensen L.M.

• Department of Computing, Mathematics, and Physics, Bergen University College, Norway

Bibliografia

• [1] J. Barnat, L. Brim, P. Simecek, and M. Weber. Revisiting Resistance Speeds Up I/O Efficient LTL Model Checking. In Proc. of TACAS’08, volume 4963 of LNCS, pages 48–62. Springer, 2008.
• [2] G. Behrmann, A. David, K.G. Larsen, J. Hakansson, P. Petterson, W. Yi, and M. Hendriks. Uppaal 4.0. In Proc. of 3rd International Conference on the Quantitative Evaluation of Systems, pages 125–126. IEEE Computer Society, 2006.
• [3] G. Behrmann, K.G. Larsen, and R. Pelánek. To Store or Not to Store. In Proc. of CAV’03, volume 2725 of LNCS, pages 433–445. Springer, 2003.
• [4] J. Billington, G. Gallasch, L.M. Kristensen, and T. Mailund. Exploiting Equivalence Reduction and the Sweep-Line Method for Detecting Terminal States. IEEE Transactions on SMC - Part A, 34(1):23–38, 2004.
• [5] Dragan Bosnacki, Stefan Leue, and Alberto Lluch-Lafuente. Partial-Order Reduction for General State Exploring Algorithms. In Prof. of SPIN’06, volume 3925 of LNCS, pages 271–287. Springer, 2006.
• [6] L. Brim, I. Cern´a, P. Moravec, and J. Simsa. Accepting Predecessors Are Better than Back Edges in Distributed LTL Model-Checking. In Proc. of FMCAD’2004, volume 3312 of LNCS, pages 352–366. Springer, 2004.
• [7] L. Brim, I. Cerná, P. Moravec, and J. Simsa. How to Order Vertices for Distributed LTL Model-Checking Based on Accepting Predecessors. ENTCS, 135(2):3–18, 2006.
• [8] S. Christensen, L.M. Kristensen, and T. Mailund. A Sweep-Line Method for State Space Exploration. In Proc. of TACAS’01, volume 2031 of LNCS, pages 450–464. Springer, 2001.
• [9] E.M. Clarke, O. Grumberg, M. Minea, and D. Peled. State Space Reduction Using Partial Order Techniques. Int. Journal on Software Tools for Technology Transfer, 2(3):279–287, 1999.
• [10] E.M. Clarke, O. Grumberg, and D. Peled. Model Checking. The MIT Press, 1999.
• [11] C. Courcoubetis, M.Y. Vardi, P. Wolper, and M. Yannakakis. Memory Efficient Algorithms for the Verification of Temporal Properties. In Proc. of CAV’90, volume 531 of LNCS, pages 233–242. Springer, 1990.
• [12] J.-M. Couvreur. On-the-Fly Verification of Linear Temporal Logic. In Proc. of FM’1999, volume 1708 of LNCS, pages 253–271. Springer, 1999.
• [13] Quick Guide: The DVE Specification Language. http://divine.fi.muni.cz/language.html, 2010.
• [14] S. Evangelista and L. M. Kristensen. Search-Order Independent State Caching. Transactions on Petri Nets and Other Models of Concurrency IV, LNCS Vol. 6550:21–41, 2010.
• [15] S. Evangelista and L. M. Kristensen. Hybrid On-the-Fly Model Checking with the Sweep-line Method. In Proc. of ICATPN’12, volume 7347 of LNCS, pages 248–267. Springer, 2012.
• [16] G. E. Gallasch, J. Billington, S. Vanit-Anunchai, and L.M. Kristensen. Checking Safety Properties On-the-fly with the Sweep-Line Method. Int. Journal on Software Tools for Technology Transfer, 9(3-4):371–392, 2007.
• [17] G.E. Gallasch, B. Han, and J. Billington. Sweep-Line Analysis of TCP Connection Management. In Proc. of ICFEM’05, volume 3785 of LNCS, pages 156–172. Springer, 2005.
• [18] G.E. Gallasch, C. Ouyang, J. Billington, and L.M. Kristensen. Experimenting with Progress Mappings for the Sweep-Line Analysis of the Internet Open Trading Protocol. In Proc. of 5th CPN Workshop and Tutorial, pages 19–38, 2004.
• [19] J. Geldenhuys and A. Valmari. More efficient on-the-fly ltl verification with tarjan’s algorithm. Theoretical Computer Science, 345(1):60–85, 2005.
• [20] P. Godefroid. Partial-Order Methods for the Verification of Concurrent Systems, volume 1032 of LNCS. Springer, 1996.
• [21] P. Godefroid, G.J. Holzmann, and D. Pirottin. State-Space Caching Revisited. In Proc. of CAV’92, volume 663 of LNCS, pages 178–191. Springer, 1992.
• [22] S. Gordon, L.M. Kristensen, and J. Billington. Verification of a Revised WAP Wireless Transaction Protocol. In Proc. of ICATPN’02, volume 2360 of LNCS, pages 182–202. Springer, 2002.
• [23] G.J. Holzmann. Tracing Protocols. AT&T Technical J., 64(10):2413–2434, 1985.
• [24] L.M. Kristensen and T. Mailund. A Compositional Sweep-Line State Space Exploration Method. In Proc. Of FORTE’02, volume 2529 of LNCS, pages 327–343. Springer, 2002.
• [25] L.M. Kristensen and T. Mailund. A Generalised Sweep-Line Method for Safety Properties. In Proc. Of FME’02, volume 2391 of LNCS, pages 549–567. Springer, 2002.
• [26] L.M. Kristensen and T. Mailund. Efficient Path Finding with the Sweep-Line Method using External Storage. In Proc. of ICFEM’03, volume 2885 of LNCS, pages 319–337. Springer, 2003.
• [27] A. Lehmann, N. Lohmann, and K. Wolf. Stubborn Sets for Simple Linear Time Properties. In Proc. Of ICATPN’12, volume 7347 of LNCS, pages 228–247. Springer, 2012.
• [28] T. Mailund and M.Westergaard. Obtaining Memory-Efficient Reachability Graph Representations Using the Sweep-Line Method. In Proc. of TACAS’04, volume 2988 of LNCS, pages 177–191. Springer, 2004.
• [29] A. Miller, A. Donaldson, and M. Calder. Symmetry in Temporal Logic Model Checking. ACM Computing Surveys, 38(3):8, 2006.
• [30] R. Pelánek. BEEM: Benchmarks for Explicit Model Checkers. In Proc. of SPIN’07, volume 4595 of LNCS, pages 263–267. Springer, 2007.
• [31] D. Peled. All from One, One for All: on Model Checking Using Representatives. In Proc. of CAV’93, volume 697 of LNCS, pages 409–423. Springer, 1993.
• [32] K. Schmidt. LoLA: A Low Level Analyser. In Proc. of ICATPN’00, volume 1825 of LNCS, pages 465–474. Springer, 2000.
• [33] S. Vanit-Anunchai, J. Billington, and G. E. Gallasch. Analysis of the Datagram Congestion Control Protocols Connection Management Procedures using the Sweep-line Method. Int. Journal on Software Tools for Technology Transfer, 10(1):29–56, 2008.
• [34] M.Y. Vardi and P. Wolper. An Automata-Theoretic Approach to Automatic Program Verification. In Proc. Of LICS’86, pages 332–344. IEEE Computer Society, 1986.
• [35] M. Westergaard, S. Evangelista, and L.M. Kristensen. ASAP: An Extensible Platform for State Space Analysis. In Proc. of ICATPN’09, volume 5606 of LNCS, pages 303–312. Springer, 2009.