Formal verification is becoming more prevalent, especially in the development of safety-critical systems where mathematically precise proofs are required to ensure suitability and faultlessness. The major drawback of formal methods is their computation intensive nature. This also holds for one of the most important formal verification technique, the reachability analysis: even a relatively small model can have a large or infinite state space. In order to overcome this problem, new and efficient algorithms are required, since the complexity of the models also tend to increase. One of these algorithms is the so called counterexample guided abstraction refinement (CEGAR) method. The CEGAR approach works on an abstraction of the original model and refines the abstraction using the information from the explored part of the state space. The abstract model usually has a less detailed state space representation. Therefore, the reachability analysis on the abstract model is easier.
In my work I examine a recently published algorithm, which applies the CEGAR approach on the reachability analysis of Petri nets. I show that the algorithm can give an incorrect answer in some special cases and I also present counterexamples of the completeness of the algorithm. I suggest new improvements to ensure correctness and to extend the set of decidable problems. I also implemented the algorithm with the new contributions and I analyze its performance by measurements.