Reference:

J. Esparza and S. Melzer. Verification of safety properties using integer programming: Beyond the state equation. Formal Methods in System Design, 16:159–189, 2000.

Abstract:

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 a safety property P, the state equation is used to derive a necessary condition for P to hold which can be mechanically checked. The necessary conditions derived from the state equation are known to be of little use for systems communicating by means of shared variables, in the sense that many of these systems satisfying the property but not the conditions. In this paper, we use traps, a well-known notion of net theory, to obtain stronger conditions that can still be efficiently checked. We show that the new conditions significantly extend the range of verifiable systems.

Suggested BibTeX entry:

@article{EM00,
    author = {J. Esparza and S. Melzer},
    journal = {Formal Methods in System Design},
    pages = {159--189},
    title = {Verification of Safety Properties Using Integer Programming: Beyond the State Equation},
    volume = {16},
    year = {2000}
}