Extensions to the CEGAR approach on Petri nets

Hajdu Ákos and Vörös András and Bartha Tamás and Mártonka Zoltán: Extensions to the CEGAR approach on Petri nets. In: Acta cybernetica, (21) 3. pp. 401-417. (2014)

[thumbnail of actacyb_21_3_2014_8.pdf]
Cikk, tanulmány, mű

Download (349kB) | Preview


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.

Item Type: Article
Journal or Publication Title: Acta cybernetica
Date: 2014
Volume: 21
Number: 3
ISSN: 0324-721X
Page Range: pp. 401-417
Language: English
Place of Publication: Szeged
Event Title: Symposium on Programming Languages and Software Tools (2013) (Szeged)
Related URLs: http://acta.bibl.u-szeged.hu/38537/
DOI: 10.14232/actacyb.21.3.2014.8
Uncontrolled Keywords: Számítástechnika
Additional Information: Bibliogr.: 417. p. és a lábjegyzetekben ; összefoglalás angol nyelven
Subjects: 01. Natural sciences
01. Natural sciences > 01.02. Computer and information sciences
Date Deposited: 2016. Oct. 17. 10:37
Last Modified: 2022. Jun. 20. 08:40
URI: http://acta.bibl.u-szeged.hu/id/eprint/34476

Actions (login required)

View Item View Item