State space computation and analysis of Time Petri Nets

DOI10.1017/S147106840600264XMaRDI QIDQ5476391zbMATH OpenOpenAlexFDO

Authors Guillaume Gardey, Olivier H. Roux, Olivier Roux

Publication date 14 July 2006

Published in Theory and Practice of Logic Programming (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1017/s147106840600264x

zbMATH Keywords

bisimulationreachability analysistime Petri netstimed automatazones

Mathematics Subject Classification ID

Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• Formal Modeling and Analysis of Timed Systems
• Model checking of time Petri nets using the state class timed automaton
• TCTL model checking of time Petri nets
• Structural translation from time Petri nets to timed automata
• scientific article; zbMATH DE number 5152608

Cited in

(29)

• Post and pre-initialized stopwatch Petri nets: formal semantics and state space computation
• Backward symbolic optimal reachability in weighted timed automata
• A state class construction for computing the intersection of time Petri nets languages
• Symbolic unfolding of parametric stopwatch Petri nets
• State space analysis of Petri nets with relation-algebraic methods
• scientific article; zbMATH DE number 5152608 (Why is no real title available?)
• Symbolic State Space of Stopwatch Petri Nets with Discrete-Time Semantics (Theory Paper)
• Relevant Timed Schedules / Clock Valuations for Constructing Time Petri Net Reachability Graphs
• Time Recursive Petri Nets
• Towards building the state class graph of the TSPN model
• A more efficient time Petri net state space abstraction useful to model checking timed linear properties
• TCTL model checking of time Petri nets
• scientific article; zbMATH DE number 1956600 (Why is no real title available?)
• scientific article; zbMATH DE number 1755141 (Why is no real title available?)
• A concurrency-preserving translation from time Petri nets to networks of timed automata
• Reduced state space representation for unbounded vector state spaces
• Region-based analysis of hybrid Petri nets with a single general one-shot transition
• The tool TINA – Construction of abstract state spaces for petri nets and time petri nets
• scientific article; zbMATH DE number 744061 (Why is no real title available?)
• Improving the construction of the DBM over-approximation of the state space of real-time preemptive systems
• Relevant timed schedules/clock vectors for constructing time Petri net reachability graphs
• The on-line diagnosis of time Petri nets
• Applications and Theory of Petri Nets 2004
• Computer Aided Verification
• Formal Modeling and Analysis of Timed Systems
• A state class based controller synthesis approach for time Petri nets
• Weakly strong semantics of time Petri nets and its algebraic description
• Formal verification of real-time systems with preemptive scheduling
• Model checking of time Petri nets using the state class timed automaton

Describes a project that uses

Uses Software

• Kronos
• Uppaal

This page was built for publication: State space computation and analysis of Time Petri Nets

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