For the most recent entries see the Petri Nets Newsletter.

Bounded Reachability Checking with Process Semantics.

Heljanko, Keijo

In: LNCS 2154: CONCUR 2001 - Concurrency Theory, pages 218-pp. 12th International Conference, Aalborg, Denmark, August 20-25, 2001, Proceedings / K. G. Larsen, M. Nielsen (Eds.) --- Springer Verlag, 2001.

Abstract: Bounded model checking has been recently introduced as an efficient verification method for reactive systems. In this work we apply bounded model checking to asynchronous systems. More specifically, we translate the bounded reachability problem for 1-safe Petri nets into constrained Boolean circuit satisfiability. We consider three semantics: process, step, and interleaving semantics. We show that process semantics has often the best performance for bounded reachability checking.

Do you need a refined search? Try our search engine which allows complex field-based queries.

Back to the Petri Nets Bibliography