The tool TINA – Construction of abstract state spaces for petri nets and time petri nets
From MaRDI portal
Publication:4671274
DOI10.1080/00207540412331312688zbMath1060.68695OpenAlexW2070996046MaRDI QIDQ4671274
Pierre-Olivier Ribet, Bernard Berthomieu, François Vernadat
Publication date: 26 April 2005
Published in: International Journal of Production Research (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1080/00207540412331312688
Symbolic computation and algebraic computation (68W30) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)
Related Items
Petri Net Reductions for Counting Markings ⋮ Interpreted synchronous extension of time Petri nets. Definition, semantics and formal analysis ⋮ Accelerating the computation of dead and concurrent places using reductions ⋮ State observer for DES under partial observation with time Petri nets ⋮ Universal Sleptsov net ⋮ Towards a formal semantics for UML/MARTE state machines based on hierarchical timed automata ⋮ Petri nets semantics of reaction rules (RR). A language for ecosystems modelling ⋮ Design of Optimal Petri Net Supervisors for Flexible Manufacturing Systems via Weighted Inhibitor Arcs ⋮ Reachability problems and abstract state spaces for time Petri nets with stopwatches ⋮ Universality in Infinite Petri Nets ⋮ A CTL* Model Checker for Petri Nets ⋮ Methods for Efficient Unfolding of Colored Petri Nets ⋮ Nested-unit Petri nets ⋮ Sleptsov nets are Turing-complete ⋮ Reo + \(\mathrm{mCRL2}\): a framework for model-checking dataflow in service compositions ⋮ Model Checking Bounded Prioritized Time Petri Nets ⋮ Assessment of initial-state-opacity in live and bounded labeled Petri net systems via optimization techniques ⋮ Improvements in unfolding of colored Petri nets ⋮ Model checking time-dependent system specifications using time stream Petri nets and \texttt{UPPAAL} ⋮ Verification of hypercube communication structures via parametric Petri nets ⋮ On the composition of time Petri nets ⋮ A concurrency-preserving translation from time Petri nets to networks of timed automata ⋮ Comparing the Expressiveness of Timed Automata and Timed Extensions of Petri Nets ⋮ TCTL-preserving translations from timed-arc Petri nets to networks of timed automata ⋮ Diagnosability analysis of patterns on bounded labeled prioritized Petri nets ⋮ Covering Steps Graphs of Time Petri Nets ⋮ Adaptation of Open Component-Based Systems ⋮ Dynamical modeling and analysis of large cellular regulatory networks ⋮ Model checking Petri nets with MSVL ⋮ Sequential composition of linear systems' clans ⋮ Parallel Processes with Real-Time and Data: The ATLANTIF Intermediate Format ⋮ Effective Representation of RT-LOTOS Terms by Finite Time Petri Nets ⋮ Verification of Timed-Arc Petri Nets ⋮ Investigating the usability of real-time scheduling theory with the Cheddar project ⋮ Dynamic Exploration of Multi-agent Systems with Periodic Timed Tasks ⋮ Diagnosability verification using LTL model checking
Uses Software
Cites Work
