Sciweavers

Share
CONCUR
2001
Springer

Bounded Reachability Checking with Process Semantics

9 years 11 months ago
Bounded Reachability Checking with Process Semantics
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.
Keijo Heljanko
Added 28 Jul 2010
Updated 28 Jul 2010
Type Conference
Year 2001
Where CONCUR
Authors Keijo Heljanko
Comments (0)
books