In: Farn Wang (Ed.): Lecture Notes in Computer Science, Vol. 3299: Automated Technology for Verification and Analysis: Second International Conference, ATVA 2004, Taipei, Taiwan, ROC, October 31-November 3, 2004, pages 93-107. Springer-Verlag, 2004.
Abstract: We apply linear algebra techniques to over-approximate the reachability relation of a numerical system (Petri nets, counters automata, timed automata and so on) by a transitive and reflexive finite union of affine spaces. Thanks to this kind of approximation, we naturally define the notion of disjunctive place invariants. All the results presented in this paper have been implemented as a plug-in for our symbolic model-checker Fast and applied to the 40 systems available on the Fast-homepage. Research funded by the Faculté des arts et des sciences of the Université de Montréal and by the Natural Sciences and Engineering Research Council of Canada through a discovery grant held by Pierre McKenzie.