GRAFCET Reduction Techniques for Model Checking

Abstract

Model checking of GRAFCET, an IEC standardized specification language, is typically performed by a translation of GRAFCET into a different (target) formalism. However, analyzing instances of considerable sizes quickly becomes unfeasible due to the state space explosion problem. We propose three techniques to reduce a GRAFCET instance depending on the property to be evaluated, resulting in a smaller state space. These techniques can be employed, even in combination, before transformation into a formalism suitable for model checking.

Authors 5

1. Robin Mroß Aachen Lehrstuhl Informatik 11

   RWTH Aachen University

   Affiliation as printed

   RWTH Aachen University,Lehrstuhl Informatik 11,Aachen,Germany,52074

2. Aron Schnakenbeck

   Helmut Schmidt University

   Affiliation as printed

   Institut für Automatisierungstechnik Helmut-Schmidt-Universität,Hamburg,Germany,22043

3. Marcus Völker Aachen Lehrstuhl Informatik 11

   RWTH Aachen University

   Affiliation as printed

   RWTH Aachen University,Lehrstuhl Informatik 11,Aachen,Germany,52074

4. Alexander Fay

   Helmut Schmidt University

   Affiliation as printed

   Institut für Automatisierungstechnik Helmut-Schmidt-Universität,Hamburg,Germany,22043

5. Stefan Kowalewski Aachen Lehrstuhl Informatik 11

   RWTH Aachen University

   Affiliation as printed

   RWTH Aachen University,Lehrstuhl Informatik 11,Aachen,Germany,52074