Accession Number:

ADA371566

Title:

Efficient Symbolic State-Space Construction for Asynchronous Systems

Descriptive Note:

Corporate Author:

INSTITUTE FOR COMPUTER APPLICATIONS IN SCIENCE AND ENGINEERING HAMPTON VA

Report Date:

1999-12-01

Pagination or Media Count:

39.0

Abstract:

Many state of the art techniques for the verification of todays complex embedded systems rely on the analysis of their reachable state spaces. In this paper, we develop a new algorithm for the symbolic generation of the state space of asynchronous system models, such as Petri nets. The algorithm is based on previous work that employs Multi-valued Decision Diagrams MDDs for efficiently storing sets of reachable states. In contrast to related approaches, however, it fully exploits event locality which is a fundamental semantic property of asynchronous systems. Additionally, the algorithm supports intelligent cache management and achieves faster convergence via advanced iteration control. It is implemented in the tool SMART, and run time results for several examples taken from the Petri net literature show that the algorithm performs about one order of magnitude faster than the best existing state space generators.

Subject Categories:

  • Cybernetics

Distribution Statement:

APPROVED FOR PUBLIC RELEASE