SE-LTL Model-checking on Timed GRAFCETS via ε-TPN

Médésu Sogbohossou; Rodrigue Yehouessi; Tahirou Djara; Theophile Aballo; Antoine Vianou

doi:10.9734/cjast/2019/v38i630433

Research Article Open access CC BY 4.0

SE-LTL Model-checking on Timed GRAFCETS via ε-TPN

Médésu Sogbohossou, Rodrigue Yehouessi, Tahirou Djara, Theophile Aballo, Antoine Vianou

Current Journal of Applied Science and Technology · pp. 1–12 · Published 26 Dec 2019

10.9734/cjast/2019/v38i630433

Abstract

The GRAFCET standard (IEC 60848) is one of the convenient formalisms used to specify the behaviour of the automated systems. Being just a semi-formal language, the usual practice is to go through an unambiguous formalism such as time Petri net (TPN) in order to validate a specification expressed by a GRAFCET model. In this paper, we propose how to perform model-checking on a GRAFCET model translated into a ε-TPN, specifically with State-Event Linear Temporal Logic (SE-LTL). Especially, we provide a way to take into account quantitative time constraints verification by integrating observers in the ε-TPN intermediate model, since TPN state-space abstractions do not allow directly such kind of model-checking.

GRAFCET (IEC 60848) Time Petri Net (TPN) model-checking SE-LTL observer.

Cited by 2

GRAFCET Reduction Techniques for Model Checking

Robin Mroß, Aron Schnakenbeck, Marcus Völker · 2023 IEEE 21st International Conference on Industrial Informatics (INDIN) · 2023

Transformation of GRAFCET Into GAL for Verification Purposes Based on a Detailed Meta-Model

Robin Mross, Aron Schnakenbeck, Marcus Völker · IEEE Access · 2022

Access this article

View at publisher

Cite this article

Médésu Sogbohossou, Rodrigue Yehouessi, Tahirou Djara, Theophile Aballo, Antoine Vianou (2019). SE-LTL Model-checking on Timed GRAFCETS via ε-TPN. Current Journal of Applied Science and Technology , 1–12. https://doi.org/10.9734/cjast/2019/v38i630433

Affiliations

Médésu Sogbohossou — Laboratoire d’Èlectrotechnique, de Télécommunications et d’Informatique Appliquée (LETIA), Ècole Polytechnique d’Abomey-Calavi (EPAC), UAC, 01 BP 2009 Cotonou, Benin.
Rodrigue Yehouessi — Laboratoire d’Èlectrotechnique, de Télécommunications et d’Informatique Appliquée (LETIA), Ècole Polytechnique d’Abomey-Calavi (EPAC), UAC, 01 BP 2009 Cotonou, Benin.
Tahirou Djara — Laboratoire d’Èlectrotechnique, de Télécommunications et d’Informatique Appliquée (LETIA), Ècole Polytechnique d’Abomey-Calavi (EPAC), UAC, 01 BP 2009 Cotonou, Benin.
Theophile Aballo — Laboratoire d’Èlectrotechnique, de Télécommunications et d’Informatique Appliquée (LETIA), Ècole Polytechnique d’Abomey-Calavi (EPAC), UAC, 01 BP 2009 Cotonou, Benin.
Antoine Vianou — Laboratoire d’Èlectrotechnique, de Télécommunications et d’Informatique Appliquée (LETIA), Ècole Polytechnique d’Abomey-Calavi (EPAC), UAC, 01 BP 2009 Cotonou, Benin.

Metrics

16
Views: 0
Downloads: 2
Citations: 1
Outbound

Full metrics

Article metrics

Real usage data collected on this platform.

16

Page views

0

PDF downloads

1

Outbound clicks

2

Citations

Views over time

Views by country

Approximate, from request IP at view time — not citizenship or institution. Countries with fewer than 5 views are grouped as "Other".

Traffic sources

Referring site, by host.

Views and downloads exclude known bots/crawlers. Citations combines this platform's own DOI-resolved index with each external source's own reported total — see Cited by above for individually listed citing works. Last refreshed 0 seconds ago.