A new class of Petri nets for modeling and property verification of switched stochastic systems

Zuohua Ding; Yuan Zhou; Mingyue Jiang; Mengchu Zhou

doi:10.1109/TSMC.2014.2379654

A new class of Petri nets for modeling and property verification of switched stochastic systems

Zuohua Ding, Yuan Zhou, Mingyue Jiang, Mengchu Zhou

Electrical and Computer Engineering

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

22 Scopus citations

Abstract

Switched stochastic systems (SSS) can be used to describe hybrid systems with randomness. However, the languages to describe their discrete switching logic and stochastic dynamic processes are different, and this difference makes their design and analysis hard. This paper proposes a new Petri net model, namely stochastic-differential Petri net (S-DPN), to describe both discrete switching logic, represented by a Markov chain, and stochastic dynamic processes, represented by a set of stochastic differential equations. We then apply a model checking technique to S-DPN to check the correctness of the requirements of SSS. A temperature control system is used to demonstrate the effectiveness of our method.

Original language	English (US)
Article number	6995961
Pages (from-to)	1087-1100
Number of pages	14
Journal	IEEE Transactions on Systems, Man, and Cybernetics: Systems
Volume	45
Issue number	7
DOIs	https://doi.org/10.1109/TSMC.2014.2379654
State	Published - Jul 1 2015

All Science Journal Classification (ASJC) codes

Software
Control and Systems Engineering
Human-Computer Interaction
Computer Science Applications
Electrical and Electronic Engineering

Keywords

Markovian jump
model verification
stochastic-differential Petri net (S-DPN)
switched stochastic system (SSS)

Access to Document

10.1109/TSMC.2014.2379654

Cite this

@article{02224abcb41c415992eda2fda34366b5,

title = "A new class of Petri nets for modeling and property verification of switched stochastic systems",

abstract = "Switched stochastic systems (SSS) can be used to describe hybrid systems with randomness. However, the languages to describe their discrete switching logic and stochastic dynamic processes are different, and this difference makes their design and analysis hard. This paper proposes a new Petri net model, namely stochastic-differential Petri net (S-DPN), to describe both discrete switching logic, represented by a Markov chain, and stochastic dynamic processes, represented by a set of stochastic differential equations. We then apply a model checking technique to S-DPN to check the correctness of the requirements of SSS. A temperature control system is used to demonstrate the effectiveness of our method.",

keywords = "Markovian jump, model verification, stochastic-differential Petri net (S-DPN), switched stochastic system (SSS)",

author = "Zuohua Ding and Yuan Zhou and Mingyue Jiang and Mengchu Zhou",

note = "Publisher Copyright: {\textcopyright} 2014 IEEE.",

year = "2015",

month = jul,

day = "1",

doi = "10.1109/TSMC.2014.2379654",

language = "English (US)",

volume = "45",

pages = "1087--1100",

journal = "IEEE Transactions on Systems, Man, and Cybernetics: Systems",

issn = "2168-2216",

publisher = "IEEE Advancing Technology for Humanity",

number = "7",

}

TY - JOUR

T1 - A new class of Petri nets for modeling and property verification of switched stochastic systems

AU - Ding, Zuohua

AU - Zhou, Yuan

AU - Jiang, Mingyue

AU - Zhou, Mengchu

PY - 2015/7/1

Y1 - 2015/7/1

N2 - Switched stochastic systems (SSS) can be used to describe hybrid systems with randomness. However, the languages to describe their discrete switching logic and stochastic dynamic processes are different, and this difference makes their design and analysis hard. This paper proposes a new Petri net model, namely stochastic-differential Petri net (S-DPN), to describe both discrete switching logic, represented by a Markov chain, and stochastic dynamic processes, represented by a set of stochastic differential equations. We then apply a model checking technique to S-DPN to check the correctness of the requirements of SSS. A temperature control system is used to demonstrate the effectiveness of our method.

AB - Switched stochastic systems (SSS) can be used to describe hybrid systems with randomness. However, the languages to describe their discrete switching logic and stochastic dynamic processes are different, and this difference makes their design and analysis hard. This paper proposes a new Petri net model, namely stochastic-differential Petri net (S-DPN), to describe both discrete switching logic, represented by a Markov chain, and stochastic dynamic processes, represented by a set of stochastic differential equations. We then apply a model checking technique to S-DPN to check the correctness of the requirements of SSS. A temperature control system is used to demonstrate the effectiveness of our method.

KW - Markovian jump

KW - model verification

KW - stochastic-differential Petri net (S-DPN)

KW - switched stochastic system (SSS)

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

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

U2 - 10.1109/TSMC.2014.2379654

DO - 10.1109/TSMC.2014.2379654

M3 - Article

AN - SCOPUS:84932644412

SN - 2168-2216

VL - 45

SP - 1087

EP - 1100

JO - IEEE Transactions on Systems, Man, and Cybernetics: Systems

JF - IEEE Transactions on Systems, Man, and Cybernetics: Systems

IS - 7

M1 - 6995961

ER -

A new class of Petri nets for modeling and property verification of switched stochastic systems

Abstract

All Science Journal Classification (ASJC) codes

Keywords

Access to Document

Other files and links

Fingerprint

Cite this