Verification of Liveness Properties on Closed Timed-Arc Petri Nets

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F13%3A00067580" target="_blank" >RIV/00216224:14330/13:00067580 - isvavai.cz</a>

Výsledek na webu

<a href="http://dx.doi.org/10.1007/978-3-642-36046-6_8" target="_blank" >http://dx.doi.org/10.1007/978-3-642-36046-6_8</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1007/978-3-642-36046-6_8" target="_blank" >10.1007/978-3-642-36046-6_8</a>

Jazyk výsledku

angličtina

Název v původním jazyce

Verification of Liveness Properties on Closed Timed-Arc Petri Nets

Popis výsledku v původním jazyce

Verification of closed timed models by explicit state-space exploration methods is an alternative to the wide-spread symbolic techniques based on difference bound matrices (DBMs). A few experiments found in the literature confirm that for the reachability analysis of timed automata explicit techniques can compete with DBM-based algorithms, at least for situations where the constants used in the models are relatively small. To the best of our knowledge, the explicit methods have not yet been employed inthe verification of liveness properties in Petri net models extended with time. We present an algorithm for liveness analysis of closed Timed-Arc Petri Nets (TAPN) extended with weights, transport arcs, inhibitor arcs and age invariants and prove its correctness. The algorithm computes optimized maximum constants for each place in the net that bound the size of the reachable state-space.

Název v anglickém jazyce

Verification of Liveness Properties on Closed Timed-Arc Petri Nets

Popis výsledku anglicky

Verification of closed timed models by explicit state-space exploration methods is an alternative to the wide-spread symbolic techniques based on difference bound matrices (DBMs). A few experiments found in the literature confirm that for the reachability analysis of timed automata explicit techniques can compete with DBM-based algorithms, at least for situations where the constants used in the models are relatively small. To the best of our knowledge, the explicit methods have not yet been employed inthe verification of liveness properties in Petri net models extended with time. We present an algorithm for liveness analysis of closed Timed-Arc Petri Nets (TAPN) extended with weights, transport arcs, inhibitor arcs and age invariants and prove its correctness. The algorithm computes optimized maximum constants for each place in the net that bound the size of the reachable state-space.

Druh

D - Stať ve sborníku

CEP obor

IN - Informatika

OECD FORD obor

—

Projekt

<a href="/cs/project/LG13010" target="_blank" >LG13010: Zastoupení ČR v European Research Consortium for Informatics and Mathematics</a><br>

Návaznosti

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)<br>I - Institucionalni podpora na dlouhodoby koncepcni rozvoj vyzkumne organizace

Rok uplatnění

2013

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ů

Název statě ve sborníku

Proceedings of Mathematical and Engineering Methods in Computer Science (MEMICS'12)

ISBN

9783642360442

ISSN

0302-9743

e-ISSN

—

Počet stran výsledku

13

Strana od-do

69-81

Název nakladatele

Springer

Místo vydání

Netherlands

Místo konání akce

Znojmo

Datum konání akce

1. 1. 2012

Typ akce podle státní příslušnosti

EUR - Evropská akce

Kód UT WoS článku

—