Extensions to the CEGAR approach on Petri nets
Formal verification is becoming more prevalent and often compulsory in the safety-critical system and software development processes. Reachability analysis can provide information about safety and invariant properties of the developed system. However, checking the reachability is a computationally h...
Elmentve itt :
| Szerzők: | |
|---|---|
| Testületi szerző: | |
| Dokumentumtípus: | Cikk |
| Megjelent: |
2014
|
| Sorozat: | Acta cybernetica
21 No. 3 |
| Kulcsszavak: | Számítástechnika |
| Tárgyszavak: | |
| doi: | 10.14232/actacyb.21.3.2014.8 |
| Online Access: | http://acta.bibl.u-szeged.hu/34476 |
| LEADER | 01790nab a2200277 i 4500 | ||
|---|---|---|---|
| 001 | acta34476 | ||
| 005 | 20220620084037.0 | ||
| 008 | 161017s2014 hu o 0|| eng d | ||
| 022 | |a 0324-721X | ||
| 024 | 7 | |a 10.14232/actacyb.21.3.2014.8 |2 doi | |
| 040 | |a SZTE Egyetemi Kiadványok Repozitórium |b hun | ||
| 041 | |a eng | ||
| 100 | 1 | |a Hajdu Ákos | |
| 245 | 1 | 0 | |a Extensions to the CEGAR approach on Petri nets |h [elektronikus dokumentum] / |c Hajdu Ákos |
| 260 | |c 2014 | ||
| 300 | |a 401-417 | ||
| 490 | 0 | |a Acta cybernetica |v 21 No. 3 | |
| 520 | 3 | |a Formal verification is becoming more prevalent and often compulsory in the safety-critical system and software development processes. Reachability analysis can provide information about safety and invariant properties of the developed system. However, checking the reachability is a computationally hard problem, especially in the case of asynchronous or infinite state systems. Petri nets are widely used for the modeling and verification of such systems. In this paper we examine a recently published approach for the reachability checking of Petri net markings. We give proofs concerning the completeness and the correctness properties of the algorithm, and we introduce algorithmic improvements. We also extend the algorithm to handle new classes of problems: submarking coverability and reachability of Petri nets with inhibitor arcs. | |
| 650 | 4 | |a Természettudományok | |
| 650 | 4 | |a Számítás- és információtudomány | |
| 695 | |a Számítástechnika | ||
| 700 | 0 | 1 | |a Vörös András |e aut |
| 700 | 0 | 1 | |a Bartha Tamás |e aut |
| 700 | 0 | 1 | |a Mártonka Zoltán |e aut |
| 710 | |a Symposium on Programming Languages and Software Tools (2013) (Szeged) | ||
| 856 | 4 | 0 | |u http://acta.bibl.u-szeged.hu/34476/1/actacyb_21_3_2014_8.pdf |z Dokumentum-elérés |