Abstract
This paper presents a class of Petri nets, process nets with channels (PNCs) that can model some types of concurrent systems in two aspects: process and interaction. Its significance lies in offering efficient analysis and verification methods for these systems. PNCs belong to the class of extended free choice nets. This paper establishes the conditions to examine their liveness, reversibility, and reachability based on their structural characteristics. Siphons, traps, and a state equation are used to describe these conditions such that analysis techniques based on reachability graphs and siphon enumeration are avoided. A polynomial-time algorithm is presented for the liveness analysis, and an effective method is also given to decide the reachability. A real-world example is used to illustrate the application of PNCs.
| Original language | English (US) |
|---|---|
| Pages (from-to) | 213-225 |
| Number of pages | 13 |
| Journal | IEEE Transactions on Systems, Man, and Cybernetics Part A: Systems and Humans |
| Volume | 42 |
| Issue number | 1 |
| DOIs | |
| State | Published - Jan 1 2012 |
All Science Journal Classification (ASJC) codes
- Control and Systems Engineering
- Software
- Information Systems
- Human-Computer Interaction
- Computer Science Applications
- Electrical and Electronic Engineering
Keywords
- Discrete event systems
- Petri nets
- interaction
- liveness