A Usable Reachability Analyser
Victor Khomenko · 2009
Abstract—Reachability analysis consists in checking if a state satisfying some property is reachable. In this paper a solution to the problem of generating formulae expressing reachability properties for concrete models is suggested. The traditional methods either require the user to input the formula manually, which can be very tedious and error-prone, or automatically generate formulae for some fixed set of common properties, which does not allow one to check custom properties. The proposed approach allows the user to write a concise abstract specification of the property in a specially developed language REACH, which is then automatically expanded into a formula for a concrete model. Its usefulness is demonstrated on several case studies. Index Terms—Reachability analysis, model checking, Petri nets, STG.