Model checking Petri nets with MSVL

Ya Shi; Cong Tian; Zhenhua Duan; Mengchu Zhou

doi:10.1016/j.ins.2016.01.036

Model checking Petri nets with MSVL

Ya Shi, Cong Tian, Zhenhua Duan, Mengchu Zhou

Electrical and Computer Engineering

Research output: Contribution to journal › Article › peer-review

9 Scopus citations

Abstract

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.

Original language	English (US)
Pages (from-to)	274-291
Number of pages	18
Journal	Information sciences
Volume	363
DOIs	https://doi.org/10.1016/j.ins.2016.01.036
State	Published - Oct 1 2016

All Science Journal Classification (ASJC) codes

Software
Control and Systems Engineering
Theoretical Computer Science
Computer Science Applications
Information Systems and Management
Artificial Intelligence

Keywords

MSVL
Model checking
PPTL
Petri nets
Translation

Access to Document

10.1016/j.ins.2016.01.036

Cite this

@article{dd22e4f0e27242c883a07d21747d1a60,

title = "Model checking Petri nets with MSVL",

abstract = "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.",

keywords = "MSVL, Model checking, PPTL, Petri nets, Translation",

author = "Ya Shi and Cong Tian and Zhenhua Duan and Mengchu Zhou",

note = "Publisher Copyright: {\textcopyright} 2016 Elsevier Inc.",

year = "2016",

month = oct,

day = "1",

doi = "10.1016/j.ins.2016.01.036",

language = "English (US)",

volume = "363",

pages = "274--291",

journal = "Information sciences",

issn = "0020-0255",

publisher = "Elsevier Inc.",

}

TY - JOUR

T1 - Model checking Petri nets with MSVL

AU - Shi, Ya

AU - Tian, Cong

AU - Duan, Zhenhua

AU - Zhou, Mengchu

PY - 2016/10/1

Y1 - 2016/10/1

N2 - 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.

AB - 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.

KW - MSVL

KW - Model checking

KW - PPTL

KW - Petri nets

KW - Translation

UR - http://www.scopus.com/inward/record.url?scp=84956635581&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84956635581&partnerID=8YFLogxK

U2 - 10.1016/j.ins.2016.01.036

DO - 10.1016/j.ins.2016.01.036

M3 - Article

AN - SCOPUS:84956635581

SN - 0020-0255

VL - 363

SP - 274

EP - 291

JO - Information sciences

JF - Information sciences

ER -

Model checking Petri nets with MSVL

Abstract

All Science Journal Classification (ASJC) codes

Keywords

Access to Document

Other files and links

Fingerprint

Cite this