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

Zuohua Ding, Yuan Zhou, Mingyue Jiang, Mengchu Zhou

Research output: Contribution to journalArticlepeer-review

18 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 languageEnglish (US)
Article number6995961
Pages (from-to)1087-1100
Number of pages14
JournalIEEE Transactions on Systems, Man, and Cybernetics: Systems
Volume45
Issue number7
DOIs
StatePublished - 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)

Fingerprint Dive into the research topics of 'A new class of Petri nets for modeling and property verification of switched stochastic systems'. Together they form a unique fingerprint.

Cite this