The implementation of Mazurkiewicz traces in POEM. (English) Zbl 1161.68579

Graf, Susanne (ed.) et al., Automated technology for verification and analysis. 4th international symposium, ATVA 2006, Beijing, China, October 23–26, 2006. Proceedings. Berlin: Springer (ISBN 978-3-540-47237-7/pbk). Lecture Notes in Computer Science 4218, 508-522 (2006).
Summary: We present the implementation of trace theory in a new model checking tool framework, POEM, that has a strong emphasis on Partial Order Methods. A tree structure is used to store trace systems, which allows sharing common prefixes among traces and therefore reduces memory cost. This structure is easy to extend to incorporate additional features. Two applications are shown in the paper: An extended structure to support a new adequate order for Local First Search, and an acceleration of event zone based state space search for timed automata.
For the entire collection see [Zbl 1137.68008].


68Q60 Specification and verification (program logics, model checking, etc.)
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)


IF-2.0; POEM
Full Text: DOI