11.2 Petri网形式化理论