Přístupnostní navigace
E-přihláška
Vyhledávání Vyhledat Zavřít
Detail publikace
HAŠA, L. ČEŠKA, M.
Originální název
Improvements in Model Checking for Object-Oriented Petri Nets
Typ
článek ve sborníku mimo WoS a Scopus
Jazyk
angličtina
Originální abstrakt
Safety and liveness properties can be expressed by LTL\X in model checking of a concurrent system. However, common logics, and LTL\X is ranked among them, do not provide tools for tracing particular instances along state space paths. For this reason, an indexed temporal logic (ICTL) has been introduced into Object-Object Petri Net model checking. Explicit-state model checking tools often incorporate partial-order reductions to reduce the number of explored states. In this paper, we present a new version of partial order reduction algorithm for LTL\X in the context of Object-Oriented Petri Nets.
Klíčová slova
LTL, ICTL, model checking, Object-Oriented Petri Nets, partial-order reduction, state space
Autoři
HAŠA, L.; ČEŠKA, M.
Rok RIV
2004
Vydáno
30. 8. 2004
Nakladatel
The International Institute of Informatics and Systemics
Místo
Orlando
ISBN
980-6560-19-1
Kniha
Proceedings of the ISAS CITSA 2004, Volume III, Communications, Information and Control Systems, Technologies and Applications
Strany od
269
Strany do
274
Strany počet
6
BibTex
@inproceedings{BUT17351, author="Luděk {Haša} and Milan {Češka}", title="Improvements in Model Checking for Object-Oriented Petri Nets", booktitle="Proceedings of the ISAS CITSA 2004, Volume III, Communications, Information and Control Systems, Technologies and Applications", year="2004", pages="269--274", publisher="The International Institute of Informatics and Systemics", address="Orlando", isbn="980-6560-19-1" }