Reachability Analysis of P-time Petri Nets with Parametric Markings

This paper deals with the verification of P-Time Petri nets with parametric markings. It investigates the verification of reach ability properties in the case of an upward-closed set of initial markings. We propose an efficient state space abstraction which preserves markings and firing sequences. I...

Full description

Saved in:
Bibliographic Details
Main Authors: Boucheneb, H., Barkaoui, K.
Format: Conference Proceeding
Language:English
Subjects:
Abstracts
Availability
Clocks
over-approximation
P-time Petri nets
parametric markings
Petri nets
Reachability analysis
Semantics
Time domain analysis
Online Access:Request full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:This paper deals with the verification of P-Time Petri nets with parametric markings. It investigates the verification of reach ability properties in the case of an upward-closed set of initial markings. We propose an efficient state space abstraction which preserves markings and firing sequences. In such an abstraction, sets of states reached by the same firing sequence are over-approximated and represented concisely by their minimal marking and the union of their time domains (abstract states). We show that even if abstract states may contain some extra states, we can retrieve the exact reachable states and then verify reach ability properties.
ISSN:1550-4808
2374-8567
DOI:10.1109/ACSD.2012.23