LTL falsification in infinite-state systems

In infinite-state systems not all false LTL properties admit lasso-shaped witnesses. In this work, we propose an automatic approach that presents potentially non-lasso witnesses in an indirect way. The approach is based on two key insights. First, we define the notion of well-founded funnel to describe a source set of states that inevitably reach a destination set. We show that, under suitable conditions, a sequence of funnels ensures the existence of a fair path. Second, we adopt a compositional approach to partition the original system into projections and employ them together with funnels to build the indirect witness. Then, we propose an algorithm that identifies candidate funnels, proves their well-foundedness, and searches for a sequencing order. We experimentally evaluate the approach on examples taken from software, timed and hybrid systems, showing its wide applicability and expressiveness, with an implementation that outperforms various competitor tools.