Core Features of Petruchio

• π-Calculus editor with syntax highlighting where you specify your system
  

• Petri-Net editor with simulation capabilities

• Compiler from π-Calculus to Petri-Nets using structural or sequential semantics

• Trace editor 

• LTL editor

• MCKIT and INA integration

• Interactive counter-trace view as π-Calculus-Processes, Petri-Nets or process graphs