Penrose: Putting Compositionality to Work for Petri Net Reachability

摘要

Recent work by the authors introduced a technique for reachability checking in Petri Nets, exploiting compositionality to increase performance for some well-known examples. We introduce a tool that uses this technique, Penrose, discuss some design details in its implementation, and identify potential future improvements.