Rt-Studio

Real Time Studio (RT-Studio) is a cutting-edge integrated environment designed for the seamless editing, simulation, and automated verification of real-time systems represented as networks of Interpreted Time Petri Nets (ITPNs). In its current iteration, this advanced tool offers a range of powerful abstractions for ITPNs, empowering users to effectively assess reachability, linear properties, and branching properties of their models.

RT-Studio goes beyond conventional functionalities by incorporating a classical CTL model-checker alongside an innovative TCTL model-checker that leverages a forward on-the-fly verification technique. To further enhance the tool's capabilities, a minimizer under bisimulation is integrated, ensuring optimized performance for verification processes.

Moreover, this versatile environment serves as a comprehensive simulation and verification solution for a wide array of Petri net extensions. For instance, it already enables the creation and simulation of Interpreted Hybrid Functional Petri Nets (IHFPNs) for in-depth analysis of Biopathways and continuous event system simulations. The ongoing development of RT-Studio is expected to introduce support for additional extensions, such as colored Petri nets and timed automata, further expanding its applicability and versatility.