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
524views
653downloads

Technical informations

Creation04/15/2011 4:03:00 PM
First validation04/15/2011 4:03:00 PM
Update time03/14/2023 8:04:01 PM
Status update03/14/2023 8:04:01 PM
Last indexation10/30/2024 8:54:44 AM
All rights reserved by Archive ouverte UNIGE and the University of GenevaunigeBlack