Affiliations: Faculty of Mathematics and Computer Science, University of Łódź, Banacha 22, 90-238 Łódź, Poland. {polrola,cybula}@math.uni.lodz.pl | Faculty of Mathematics and Computer Science, University of Łódź, Banacha 22, 90-238 Łódź, Poland | Institute of Computer Science, PAS, Warsaw, Poland. [email protected]
Note: [] Address for correspondence: Faculty of Mathematics and Computer Science, University of Łódź, Banacha 22, 90-238 Łódź, Poland
Abstract: Time Petri nets by Merlin and Farber are a powerful modelling formalism. However, symbolic model checking methods for them consider in most cases the nets which are 1-safe, i.e., allow the places to contain at most one token. In our paper we present an approach which applies symbolic verification to testing reachability for time Petri nets without this restriction. We deal with the class of bounded nets restricted to disallow multiple enabledness of transitions, and present the method of reachability testing based on a translation into a satisfiability modulo theory (SMT).
