Reference:

S. Melzer and J. Esparza. Checking system properties via integer programming. In Proc. of ESOP'96, Lecture Notes in Computer Science. Springer-Verlag, 1996.

Abstract:

The marking equation is a well known verification method in the Petri net community. It has also be applied by Avrunin, Corbett et al. to automata models. It is a semidecision method, and it may fail to give an answer for some systems, in particular for those communicating by means of shared variables. In this paper, we complement the marking equation by a so called trap equation. We show that both together significantly extend the range of verifiable systems by conducting several case studies.

Suggested BibTeX entry:

@inproceedings{ME96,
    author = {S. Melzer and J. Esparza},
    booktitle = {Proc. of ESOP'96},
    publisher = {{Springer-Verlag}},
    series = {{Lecture Notes in Computer Science}},
    title = {Checking System Properties via Integer Programming},
    year = {1996}
}