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.
CITATION STYLE
Melzer, S., & Esparza, J. (1996). Checking system properties via integer programming. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1058, pp. 250–264). Springer Verlag. https://doi.org/10.1007/3-540-61055-3_41
Mendeley helps you to discover research relevant for your work.