Technical report
OA Policy
English

Properties specification language for algebraic Petri nets

Number of pages22
Publication date2010
Abstract

Model Checking consists in verifying if a model of a given system meets a set of requirements. The model and the properties can be specified with various formalisms. We chose Algebraic Petri Nets (APNs), a powerful formalism used to model concurrent systems, for the model specification. This report proposes a language for defining invariant properties on APNs. The expressiveness of the language proposed is similar to first order logic, with some extensions (deadlocks and cardinalities). These properties can be used to define the requirements for model checking. This language was created for the tool AlPiNA, an APN model checker developed at the University of Geneva.

Keywords
  • Model checking
  • Algebraic Petri Nets
  • Properties
  • Invariants
  • Specification language
  • First-order logic
  • AlPiNA
Citation (ISO format)
MARECHAL MARIN, Alexis Ayar, BUCHS, Didier. Properties specification language for algebraic Petri nets. 2010
Main files (1)
Report
accessLevelPublic
Identifiers
  • PID : unige:26582
539views
658downloads

Technical informations

Creation15/04/2011 16:03:00
First validation15/04/2011 16:03:00
Update time14/03/2023 20:04:01
Status update14/03/2023 20:04:01
Last indexation30/10/2024 08:54:44
All rights reserved by Archive ouverte UNIGE and the University of GenevaunigeBlack