Predicate Detection on Infinite Computations

Earlier work on predicate detection has assumed that the given computation is finite. Detecting violation of a liveness predicate requires that the predicate be evaluated on an infinite computation. In this work we develop theory and associated algorithms for predicate detection in infinite runs. We introduce the concept of d-diagram which is a finite representation of infinite directed graphs. We extend the techniques of computation slicing to ddiagrams which allows us to efficiently detect predicates in a subclass of CTL, called RCTL. RCTL is sufficient to represent properties such as violation of liveness.