en
Scientific article
English

Toward efficient state space generation of algebraic Petri nets

Published inSMV technical report series, no. 206
Publication date2010
Abstract

Algebraic Petri Nets (APN: Petri Nets + Abstract Algebraic Data Types) are powerful tools to model concurrent systems. Because of their high expressive power, allowing end-user to model more complex systems, State Space Explo- sion is a big issue in APN. Symbolic Model Checking (SMC) and particularly Decision Diagrams (DD) based symbolic model checking is a proven technique to handle the State Space Explosion for simpler formalisms such as P/T Petri Nets. This paper discusses how to use Binary Decision Diagrams' (BDD) evo- lutions (Data Decision Diagrams, Set Decision Diagrams, Σ DD,... ) to tackle aforementioned problem in the APN world. The main contributions of this work are the encoding of any APN model using the DD framework and the notion of Algebraic Cluster that tackles the concurrency induced by the token multiplic- ity. The discussed algorithms have been implemented in a tool that is freely accessible on http://alpina.unige.ch.

Keywords
  • System design and verification
  • Higher-level Nets Models
  • Algebraic Petri Nets
  • State Space Generation
  • Decisions Diagrams
Citation (ISO format)
BUCHS, Didier, HOSTETTLER, Steve Patrick. Toward efficient state space generation of algebraic Petri nets. In: SMV technical report series, 2010, n° 206.
Main files (1)
Article (Submitted version)
accessLevelPublic
Identifiers
  • PID : unige:12332
757views
326downloads

Technical informations

Creation11/03/2010 4:53:00 PM
First validation11/03/2010 4:53:00 PM
Update time03/14/2023 4:08:23 PM
Status update03/14/2023 4:08:22 PM
Last indexation01/15/2024 9:46:57 PM
All rights reserved by Archive ouverte UNIGE and the University of GenevaunigeBlack