PV3 ⊧ TAPAALperforms queries on Petri nets

Tool that supports modelling, simulation and verification (model checking) for extended timed-arc Petri nets

Application domain/field

• Timed-Arc Petri Nets (TAPNs)
• Simulation
• Model checking

Type of tool

Framework/model checking for timed-arc petri nets

Expected input

• Model
• Query (it supports the operators EF, EG, AF and AG)

Format:

• Model: to be constructed in the TAPAAL GUI
• Query: input in the TAPAAL GUI

Internals

Uses verifydtapn

Comments

TAPAAL models can be automatically translated into UPPAAL models. So the user can choose to translate a TAPAAL model and use UPPAAL as a verification engine instead of TAPAAL.