GSTE is partitioned model checking |
| |
Authors: | Roberto Sebastiani Eli Singerman Stefano Tonetta Moshe Y Vardi |
| |
Affiliation: | (1) Dipartimento di Informatica e Telecomunicazioni, Università di Trento, Trento, Italy;(2) Intel Israel Design Center, Haifa, Israel;(3) Faculty of Informatics, University of Lugano, Lugano, Switzerland;(4) Department of Computer Science, Rice University, Houston, USA |
| |
Abstract: | Verifying whether an ω-regular property is satisfied by a finite-state system is a core problem in model checking. Standard techniques build an
automaton with the complementary language, compute its product with the system, and then check for emptiness. Generalized
symbolic trajectory evaluation (GSTE) has been recently proposed as an alternative approach, extending the computationally
efficient symbolic trajectory evaluation (STE) to general ω-regular properties. In this paper, we show that the GSTE algorithms are essentially a partitioned version of standard symbolic
model-checking (SMC) algorithms, where the partitioning is driven by the property under verification. We export this technique
of property-driven partitioning to SMC and show that it typically does speed up SMC algorithms.
A shorter version of this paper has been presented at CAV’04 (R. Sebastiani et al., Lecture Notes in Comput. Sci., vol. 3114,
pp. 143–160, 2004).
R. Sebastiani supported in part by the CALCULEMUS! IHP-RTN EC project, code HPRN-CT-2000-00102, by a MIUR COFIN02 project, code 2002097822_003, and by a grant from the Intel Corporation.
M.Y. Vardi supported in part by NSF grants CCR-9988322, CCR-0124077, CCR-0311326, IIS-9908435, IIS-9978135, EIA-0086264, and
ANI-0216467 by BSF grant 9800096, and by a grant from the Intel Corporation. |
| |
Keywords: | Symbolic model checking GSTE Property-driven partitioning |
本文献已被 SpringerLink 等数据库收录! |
|