Zlepšení v model checkingu objektově-orientovaných Petriho sítí
Identifikátory výsledku
Kód výsledku v IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216305%3A26230%2F04%3APU49209" target="_blank" >RIV/00216305:26230/04:PU49209 - isvavai.cz</a>
Výsledek na webu
—
DOI - Digital Object Identifier
—
Alternativní jazyky
Jazyk výsledku
angličtina
Název v původním jazyce
Improvements in Model Checking for Object-Oriented Petri Nets
Popis výsledku v původním jazyce
Safety and liveness properties can be expressed by LTLX in model checking of a concurrent system. However, common logics, and LTLX 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.<br>Explicit-state model checking tools often incorporate partial-order reductions to reduce the number of explored states. In this paper, we presenta new version of partial order reduction algorithm for LTLX in the context of Object-Oriented Petri Nets.
Název v anglickém jazyce
Improvements in Model Checking for Object-Oriented Petri Nets
Popis výsledku anglicky
Safety and liveness properties can be expressed by LTLX in model checking of a concurrent system. However, common logics, and LTLX 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.<br>Explicit-state model checking tools often incorporate partial-order reductions to reduce the number of explored states. In this paper, we presenta new version of partial order reduction algorithm for LTLX in the context of Object-Oriented Petri Nets.
Klasifikace
Druh
D - Stať ve sborníku
CEP obor
JC - Počítačový hardware a software
OECD FORD obor
—
Návaznosti výsledku
Projekt
<a href="/cs/project/GA102%2F04%2F0780" target="_blank" >GA102/04/0780: Automatizované metody a nástroje pro vývoj spolehlivých paralelních a distribuovaných systémů</a><br>
Návaznosti
Z - Vyzkumny zamer (s odkazem do CEZ)
Ostatní
Rok uplatnění
2004
Kód důvěrnosti údajů
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Údaje specifické pro druh výsledku
Název statě ve sborníku
Proceedings of the ISAS CITSA 2004, Volume III, Communications, Information and Control Systems, Technologies and Applications
ISBN
980-6560-19-1
ISSN
—
e-ISSN
—
Počet stran výsledku
6
Strana od-do
269-274
Název nakladatele
The International Institute of Informatics and Systemics
Místo vydání
Orlando
Místo konání akce
Orlando, Florida
Datum konání akce
21. 7. 2004
Typ akce podle státní příslušnosti
WRD - Celosvětová akce
Kód UT WoS článku
—