Combining structural and symbolic methods for the verification of concurrent systems
Document typeConference report
PublisherInstitute of Electrical and Electronics Engineers (IEEE)
Rights accessOpen Access
The contributions during the last few years on the structural theory of Petri nets can now be applied to formal verification. The structural theory provides methods to find efficient encoding schemes for symbolic representations of the reachable markings. It also provides approximations of the state space that allow one to alleviate many bottlenecks in the calculation of the reachability set by breadth or depth first search algorithms. The paper reviews some of the results on the structural theory and explains how they can be incorporated in a model checking verification framework for concurrent systems.
CitationCortadella, J. Combining structural and symbolic methods for the verification of concurrent systems. A: International Conference on Application of Concurrency to System Design. "1998 International Conference on Application of Concurrency to System Design: March 23-26, 1998, Fukushima, Japan: proceedings". Institute of Electrical and Electronics Engineers (IEEE), 1998, p. 2-7.