In the paper we present a bounded model checking for 1-safe Petri nets and properties expressed in LTL and the universal fragment of CTL, based on binary decision diagrams. The presented experimental results show that we have obtained a technique which performs better in some of the considered cases, in comparison with the existing SAT-based implementation. The results are also compared with standard BDD-based symbolic method.
JavaScript jest wyłączony w Twojej przeglądarce internetowej. Włącz go, a następnie odśwież stronę, aby móc w pełni z niej korzystać.