Sciweavers

Free Online Productivity Tools i2Speak i2Symbol i2OCR iTex2Img iWeb2Print iWeb2Shot i2Type iPdf2Split iPdf2Merge i2Bopomofo i2Arabic i2Style i2Image i2PDF iLatex2Rtf Sci2ools

12

CONCUR
2001
Springer

favoriteEmaildiscussreport

112views Distributed And Parallel Com...» more CONCUR 2001»

Bounded Reachability Checking with Process Semantics

13 years 9 months ago

Bounded Reachability Checking with Process Semantics

Download lib.tkk.fi

Bounded model checking has been recently introduced as an eﬃcient veriﬁcation method for reactive systems. In this work we apply bounded model checking to asynchronous systems. More speciﬁcally, we translate the bounded reachability problem for 1-safe Petri nets into constrained Boolean circuit satisﬁability. 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

Real-time Traffic

CONCUR 2001 | Constrained Boolean Circuit | Distributed And Parallel Computing | Model Checking | Reachability |

claim paper

Related Content

» Proving Reachability Using FShell Competition Contribution

» Bounded LTL Model Checking with Stable Models

» Advances in Probabilistic Model Checking

» Bounded Model Checking for Region Automata

» A Portable CompilerIntegrated Approach to Permanent Checking

» Best Probabilistic Transformers

» Interpolant Learning and Reuse in SATBased Model Checking

» Partial Order Reduction for Model Checking of Timed Automata

» A Decidable Fragment of Separation Logic

Post Info
More Details (n/a)

Added	28 Jul 2010
Updated	28 Jul 2010
Type	Conference
Year	2001
Where	CONCUR
Authors	Keijo Heljanko

Comments (0)