Automatic Discovery of Fair Paths in Infinite-State Transition Systems

Proving existential properties of infinite-state systems (e.g. software non-termination, model checking of hybrid automata) comes with a key challenge: differently from the finite-state case, witnesses may not be in form of lasso-shaped fair paths. In this paper we propose an approach to automatically prove existential properties for infinite state transition systems, presenting witnesses in an indirect way. The approach is based on the notion of well-founded funnel, where a ranking function guarantees that the states in the source set are guaranteed to inevitably reach the destination set. We show that, under suitable conditions, a sequence of funnels ensures the existence of a fair path. We propose an algorithm that, working in an abstract space induced by a set of predicates, identifies candidate funnels, proves their well-foundedness, and searches for a sequencing order. An experimental evaluation shows that the approach is effective in proving existential properties on a wide range of examples taken from both software and LTL model checking, and outperforms various competitor tools.