Relevant timed schedules/clock vectors for constructing time Petri net reachability graphs

DOI10.1007/S10626-011-0100-4MaRDI QIDQ539486zbMATH OpenOpenAlexFDO

Authors H. Boucheneb, Kamel Barkaoui

Publication date 30 May 2011

Published in Discrete Event Dynamic Systems (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s10626-011-0100-4

zbMATH Keywords

Petri netsreachability graphsTPN model

Mathematics Subject Classification ID

Applications of graph theory (05C90) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Review text

The authors consider Petri nets (the TPN model). Their main result is the following: ``Only some timed schedules/clock vectors (one per enabled transition) of the clock/firing domains are relevant to construct reachability graphs for the TPN. Resulting graphs are smaller then reachability graphs proposed in literature before. The article contains some illustrative examples.

Recommendations

• Relevant Timed Schedules / Clock Valuations for Constructing Time Petri Net Reachability Graphs
• Verification of reachability properties for time Petri nets
• scientific article; zbMATH DE number 4209631
• State space computation and analysis of Time Petri Nets
• Symbolic Reachability Analysis of Integer Timed Petri Nets

Cites work

• A more efficient time Petri net state space abstraction useful to model checking timed linear properties
• Applications and Theory of Petri Nets 2004
• CTL* model checking for time Petri nets
• scientific article; zbMATH DE number 1337891 (Why is no real title available?)
• scientific article; zbMATH DE number 1956600 (Why is no real title available?)
• Model Checking Bounded Prioritized Time Petri Nets
• On-the-fly TCTL model checking for time Petri nets
• State space computation and analysis of Time Petri Nets
• TCTL model checking of time Petri nets

Cited in

(8)

• Temporal communication graphs: Lamport's process-time graphs augmented for the purpose of mapping and scheduling
• Time based deadlock prevention for Petri nets
• scientific article; zbMATH DE number 4209631 (Why is no real title available?)
• Relevant Timed Schedules / Clock Valuations for Constructing Time Petri Net Reachability Graphs
• A Clustering Approach to Approximate the Timed Reachability Graph for a Class of Time Petri Nets
• Verification of reachability properties for time Petri nets
• Timed aggregate graph: a finite graph preserving event- and state-based quantitative properties of time Petri nets
• An extremum timed extended reachability graph for temporal analysis of time Petri nets

This page was built for publication: Relevant timed schedules/clock vectors for constructing time Petri net reachability graphs

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q539486)