Abstract
High-level Petri nets make models more concise and readable
as compared to low-level Petri nets. However, usual verification
techniques such as state space analysis remain an open challenge for
both because of state space explosion. The contribution of this paper is
to propose an approach for property based reduction of the state space
of Algebraic Petri nets (a variant of high-level Petri nets). To achieve
the objective, we propose a slicing algorithm for Algebraic Petri nets
(APNSlicing). The proposed algorithm can alleviate state space even for
certain strongly connected nets and is proved not to increase the state
space. We exemplify our technique through the running case study of car
crash management system.
as compared to low-level Petri nets. However, usual verification
techniques such as state space analysis remain an open challenge for
both because of state space explosion. The contribution of this paper is
to propose an approach for property based reduction of the state space
of Algebraic Petri nets (a variant of high-level Petri nets). To achieve
the objective, we propose a slicing algorithm for Algebraic Petri nets
(APNSlicing). The proposed algorithm can alleviate state space even for
certain strongly connected nets and is proved not to increase the state
space. We exemplify our technique through the running case study of car
crash management system.
Original language | English |
---|---|
Pages | 275 |
Publication status | Published - 2013 |
Event | International Workshop on Modeling and Business Environments ModBE'13 - Milano, Italy Duration: 24 Jun 2013 → 25 Jun 2013 |
Conference
Conference | International Workshop on Modeling and Business Environments ModBE'13 |
---|---|
Abbreviated title | ModBE'13 |
Country/Territory | Italy |
City | Milano |
Period | 24/06/13 → 25/06/13 |
Keywords
- High-level Petri nets
- Model checking
- Slicing