Detail publikace

Improvements in Model Checking for Object-Oriented Petri Nets

ČEŠKA Milan a HAŠA Luděk. Improvements in Model Checking for Object-Oriented Petri Nets. In: Proceedings of the ISAS CITSA 2004, Volume III, Communications, Information and Control Systems, Technologies and Applications. Orlando: The International Institute of Informatics and Systemics, 2004, s. 269-274. ISBN 980-6560-19-1.
Název česky
Zlepšení v model checkingu objektově-orientovaných Petriho sítí
Typ
článek ve sborníku konference
Jazyk
angličtina
Autoři
Klíčová slova

LTL, ICTL, model checking, objektově orientované Petriho sítě, redukce stavového prostoru

Abstrakt

Pro popis bezpečnosti a živosti ve verifikaci paralelních systémů se často používá lineární temporální logika (LTL\X). Temporální logika však neumožňuje sledovat jednotlivé instance objektů podél cest stavového prosotru. Proto do verifikace objektově-orintovaných Petriho sítí byla zavedena indexovaná temporální logika (indexed temporal logic (ICTL)).
Verifikační nástroje se snaží redukovat počet navštívených stavů stavového prostoru. Pro model checking objektově-orientovaných Petriho sítí tento článek prezentuje novou verzi algoritmu redukce stavového prostoru pomocí částečného uspořání.

Rok
2004
Strany
269-274
Sborník
Proceedings of the ISAS CITSA 2004, Volume III, Communications, Information and Control Systems, Technologies and Applications
Konference
International Conference on Cybernetics and Information Technologies, Systems and Applications: CITSA 2004, Orlando, Florida, US
ISBN
980-6560-19-1
Vydavatel
The International Institute of Informatics and Systemics
Místo
Orlando, US
BibTeX
@INPROCEEDINGS{FITPUB7548,
   author = "Milan \v{C}e\v{s}ka and Lud\v{e}k Ha\v{s}a",
   title = "Improvements in Model Checking for Object-Oriented Petri Nets",
   pages = "269--274",
   booktitle = "Proceedings of the ISAS CITSA 2004, Volume III, Communications, Information and Control Systems, Technologies and Applications",
   year = 2004,
   location = "Orlando, US",
   publisher = "The International Institute of Informatics and Systemics",
   ISBN = "980-6560-19-1",
   language = "english",
   url = "https://www.fit.vut.cz/research/publication/7548"
}
Nahoru