Local entailment test in the reachability problem for well structured transition systems

D. L. Chubarov

Computing Centre of Siberian Branch of Russian Academy of Sciences, Novosibirsk

Abstract: We describe the symbolic backward reachability procedure for infinite state systems and show that the variant of the procedure with the local entailment test still decides coverability properties of well structured systems.

UDC: 004.021

Received: 01.06.2006