Verification of Safety Properties Using IntegerProgramming: Beyond the State Equation

摘要: The state equation is a verification technique that has been applied—not always under this name—to numerous systems modelled as Petri nets or communicating automata. Given safety property P, the used to derive necessary condition for P hold which can be mechanically checked. conditions derived from are known of little use by means shared variables, in sense many these satisfy but not conditions. In paper, we traps, well-known notion net theory, obtain stronger still efficiently We show new significantly extend range verifiable systems.