The explicit conflict check algorithm implemented in the Waters library
Malik, R. (2018). The explicit conflict check algorithm implemented in the Waters library (Working paper series. University of Waikato, Department of Computer Science. No. 01/2018). Hamilton, New Zealand: University of Waikato.
Permanent Research Commons link: https://hdl.handle.net/10289/12069
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.
Department of Computer Science, The University of Waikato
© 2018 The Authors