GRAFCET reduction techniques for model checking

Mroß, Robin; Schnakenbeck, Aron; Völker, Marcus; Fay, Alexander; Kowalewski, Stefan

doi:10.1109/indin51400.2023.10218247

GRAFCET reduction techniques for model checking

Publication date

2023-08-22

Document type

Konferenzbeitrag

Author

Mroß, Robin

Schnakenbeck, Aron

Völker, Marcus

Fay, Alexander

Kowalewski, Stefan

Organisational unit

Automatisierungstechnik

DOI

10.1109/indin51400.2023.10218247

URI

https://openhsu.ub.hsu-hh.de/handle/10.24405/22622

Conference

21st International Conference on Industrial Informatics (INDIN 2023) ; Lemgo, Germany ; July 18–20, 2023

Publisher

IEEE

Book title

2023 IEEE 21st International Conference on Industrial Informatics (INDIN)

ISBN

978-1-6654-9313-0

Part of the university bibliography

✅

Language

English

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.

Version

Published version

Access right on openHSU

Metadata only access