The explicit conflict check algorithm implemented in the Waters library
Citation
Export citationMalik, R. (2018). The explicit conflict check algorithm implemented in the Waters library (Working paper No. 01/2018). Hamilton, New Zealand: University of Waikato, Department of Computer Science.
Permanent Research Commons link: https://hdl.handle.net/10289/12069
Abstract
This working paper describes the implementation of explicit model checking algorithms to verify the nonblocking or nonconflicting property of discrete event systems. Explicit algorithms enumerate and store all reachable states of a synchronous composition. Three alternatives optimised for memory consumption or runtime are described and compared. The algorithms have been implemented in C++ in the discrete event systems library Waters, and experimental results show that they can explore more than 100 million states on standard computers.
Date
2018Type
Report No.
01/2018
Publisher
Department of Computer Science, The University of Waikato
Rights
© 2018 The Authors