Verification of Timed-Arc {P}etri Nets

D 2011

Verification of Timed-Arc {P}etri Nets

JACOBSEN, Lasse; Morten JACOBSEN; H. Mikael MOLLER a Jiří SRBA

Základní údaje

Originální název

Verification of Timed-Arc {P}etri Nets

Název česky

Verifikace Casovych Petriho Siti

Autoři

JACOBSEN, Lasse; Morten JACOBSEN; H. Mikael MOLLER a Jiří SRBA

Vydání

Neuveden, Proceedings of the 37th International Conference on Current Trends in Theory and Practice of Computer Science ({SOFSEM}'11), od s. 46-72, 26 s. 2011

Nakladatel

Springer-Verlag

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Nizozemské království

Utajení

není předmětem státního či obchodního tajemství

Forma vydání

tištěná verze "print"

Odkazy

URL

Impakt faktor

Impact factor: 0.402 v roce 2005

Označené pro přenos do RIV

Ano

Kód RIV

RIV/00216224:14330/11:00067340

Organizační jednotka

Fakulta informatiky

ISBN

978-3-642-18380-5

ISSN

DOI

https://doi.org/10.1007/978-3-642-18381-2_4

UT WoS

000296264200004

Klíčová slova česky

verifikace; Petriho site; nastroje; rozhodnutelnost

Klíčová slova anglicky

verification; Petri net; tool; decidability

Změněno: 30. 4. 2014 04:17, RNDr. Pavel Šmerk, Ph.D.

Anotace

ORIG CZ

V originále

Timed-Arc Petri Nets (TAPN) are an extension of the classical P/T nets with continuous time. Tokens in TAPN carry an age and arcs between places and transitions are labelled with time intervals restricting the age of tokens available for transition firing. The TAPN model posses a number of interesting theoretical properties distinguishing them from other time extensions of Petri nets. We shall give an overview of the recent theory developed in the verification of TAPN extended with features like read/transport arcs, timed inhibitor arcs and age invariants. We will examine in detail the boundaries of automatic verification and the connections between TAPN and the model of timed automata. Finally, we will mention the tool TAPAAL that supports modelling, simulation and verification of TAPN and discuss a small case study of alternating bit protocol.

Česky

Časované Petriho sítě Arc (TAPN) je rozšíření klasické P / T sítí se spojitým časem. Tokeny TAPN nesou věku a oblouky mezi místy a přechody jsou označeny časových intervalech omezení věku známek pro přechod palbu.TAPN modelu vlastnit několik zajímavých teoretických vlastností odlišuje od ostatních doby rozšíření Petriho sítí. Měli bychom dát přehled o posledních teorie byla vyvinuta při ověřování TAPN rozšířena o funkce, jako je čtení / doprava oblouky, časované inhibitor oblouky a věku invarianty. Se budeme podrobně prozkoumat hranice automatické verifikace a spojení mezi TAPN a model automatu časově. Nakonec se zmíníme o nástroj, který podporuje TAPAAL modelování, simulaci a ověření TAPN a diskutovat o malou případovou studii střídání bit protokolu.

Návaznosti

MSM0021622419, záměr

Název: Vysoce paralelní a distribuované výpočetní systémy

Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Vysoce paralelní a distribuované výpočetní systémy

Citovat

JACOBSEN, Lasse; Morten JACOBSEN; H. Mikael MOLLER a Jiří SRBA. Verification of Timed-Arc {P}etri Nets. In Cerná, Ivana, Gyimóthy, Tibor, Hromkovic, Juraj, Jefferey, Keith, Královic, Rastislav, Vukolic, Marko, Wolf, Stefan. Proceedings of the 37th International Conference on Current Trends in Theory and Practice of Computer Science ({SOFSEM}'11). Neuveden: Springer-Verlag, 2011, s. 46-72, 26 s. ISBN 978-3-642-18380-5. Dostupné z: https://doi.org/10.1007/978-3-642-18381-2_4.

@inproceedings{963625,
   author = {Jacobsen, Lasse and Jacobsen, Morten and Moller, H. Mikael and Srba, Jiří},
   address = {Neuveden},
   booktitle = {Proceedings of the 37th International Conference on Current Trends in Theory and Practice of Computer Science ({SOFSEM}'11)},
   doi = {https://doi.org/10.1007/978-3-642-18381-2_4},
   editor = {Cerná, Ivana, Gyimóthy, Tibor, Hromkovic, Juraj, Jefferey, Keith, Královic, Rastislav, Vukolic, Marko, Wolf, Stefan},
   keywords = {verification; Petri net; tool; decidability},
   howpublished = {tištěná verze "print"},
   language = {eng},
   location = {Neuveden},
   isbn = {978-3-642-18380-5},
   pages = {46-72},
   publisher = {Springer-Verlag},
   title = {Verification of Timed-Arc {P}etri Nets},
   url = {http://www.springerlink.com/content/ek83j00501734324/},
   year = {2011}
}

TY  - CONF
ID  - 963625
AU  - Jacobsen, Lasse - Jacobsen, Morten - Moller, H. Mikael - Srba, Jiří
PY  - 2011
TI  - Verification of Timed-Arc {P}etri Nets
PB  - Springer-Verlag
CY  - Neuveden
SN  - 9783642183805
KW  - verification
KW  - Petri net
KW  - tool
KW  - decidability
UR  - http://www.springerlink.com/content/ek83j00501734324/
N2  - Timed-Arc Petri Nets (TAPN) are an extension of the classical P/T nets with continuous time. Tokens in TAPN carry an age and arcs between places and transitions are labelled with time intervals restricting the age of tokens available for transition firing. The TAPN model posses a number of interesting theoretical properties distinguishing them from other time extensions of Petri nets. We shall give an overview of the recent theory developed in the verification of TAPN extended with features like read/transport arcs, timed inhibitor arcs and age invariants. We will examine in detail the boundaries of automatic verification and the connections between TAPN and the model of timed automata. Finally, we will mention the tool TAPAAL that supports modelling, simulation and verification of TAPN and discuss a small case study of alternating bit protocol.
ER  -

JACOBSEN, Lasse; Morten JACOBSEN; H. Mikael MOLLER a Jiří SRBA. Verification of Timed-Arc $\{$P$\}$etri Nets. In Cerná, Ivana, Gyimóthy, Tibor, Hromkovic, Juraj, Jefferey, Keith, Královic, Rastislav, Vukolic, Marko, Wolf, Stefan. \textit{Proceedings of the 37th International Conference on Current Trends in Theory and Practice of Computer Science ($\{$SOFSEM$\}$'11)}. Neuveden: Springer-Verlag, 2011, s.~46-72, 26 s. ISBN~978-3-642-18380-5. Dostupné z: https://doi.org/10.1007/978-3-642-18381-2\_{}4.

Přehled o publikaci