Benutzer: Gast  Login
Wenn Sie Schwierigkeiten haben, das Dokument zu öffnen, versuchen Sie auch bitte diesen Link
Titel:

Model Checking LTL Using Net Unfoldings

Dokumenttyp:
Technical Report
Autor(en):
Frank Wallner
Abstract:
Net unfoldings are a well-studied partial order semantics for Petri nets. In this paper, we show that the finite prefix of an unfolding, introduced by McMillan, is suited for model checking linear-time temporal properties. The method is based on the so-called automata-theoretic approach to model checking. We propose a technique to treat this approach within the framework of safe Petri nets, and give an efficient algorithm for detecting the system runs violating a given specification.
Stichworte:
Model Checking; LTL; Net Unfoldings
Jahr:
1997
Jahr / Monat:
1997-12-01 00:00:00
Seiten/Umfang:
14
 BibTeX