Model checking Petri nets with MSVL

Ya Shi; Cong Tian; Zhenhua Duan; Mengchu Zhou

doi:10.1016/j.ins.2016.01.036

Back

Journal article

Peer reviewed

Model checking Petri nets with MSVL

Ya Shi, Cong Tian, Zhenhua Duan and Mengchu Zhou

Information sciences, Vol.363, pp.274-291

01/10/2016

DOI: https://doi.org/10.1016/j.ins.2016.01.036

Abstract

Model checking

MSVL

Petri nets

PPTL

Translation

This paper presents three translations from Petri nets to Modeling, Simulation and Verification Language (MSVL) programs. Each translation is directed by one of the three semantics of Petri nets, namely interleaving, concurrency and max-concurrency. Further, for each translation, an equivalence relation between Petri nets and generated MSVL programs is proved. As a result, the supporting tool MSV for MSVL can be used to verify the properties of Petri nets. Case studies are given to show how to do so with MSV under each semantics.

Metrics

1 Record Views

Details

Title: Model checking Petri nets with MSVL
Creators - without role: Ya Shi - Xidian University
Cong Tian - Xidian University
Zhenhua Duan - Xidian University
Mengchu Zhou - New Jersey Institute of Technology
Publication Details: Information sciences, Vol.363, pp.274-291
Publisher: Elsevier Inc
Grant note: 61133001; 61322202; 61420106004; 91418201; 61272117 / NSFC
Identifiers: 9938868208331
Academic Unit: King Abdulaziz University
Language: English
Resource Type: Journal article