Petruchio: From Dynamic Networks to Nets

We introduce Petruchio, a tool for computing Petri net translations of dynamic networks. To cater for unbounded architectures beyond the capabilities of existing implementations, the principle fixedpoint engine runs interleaved with coverability queries. We discuss algorithmic enhancements and provide experimental evidence that Petruchio copes with models of reasonable size.

• Type: Conference
• Year: 2010
• Where: CAV
• Authors: Roland Meyer, Tim Strazny
• Keywords: CAV 2010, Hardware, Petri Net Translations, Petruchio Copes, Principle fixedpoint Engine