Substructure Temporal Logic

In formal verification and design, reasoning about substructures is a crucial aspect for several fundamental problems, whose solution often requires to select a portion of the model of interest on which to verify a specific property. In this paper, we present a new branching-time temporal logic, called Substructure Temporal Logic (STL*, for short), whose distinctive feature is to allow for quantifying over the possible substructure of a given structure. This logic is obtained by adding two new operators to CTL*, whose interpretation is given relative to the partial order induced by a suitable substructure relation. STL* turns out to be very expressive and allows to capture in a very natural way many well known problems, such as module checking, reactive synthesis and reasoning about games. A formal account of the model theoretic properties of the new logic and results about (un)decidability and complexity of related decision problems are also provided.