Reasoning About Substructures and Games

Many decision problems in formal verification and design can be suitably formulated in game-theoretic terms. This is the case for the model checking of open and closed systems and both controller and reactive synthesis. Interpreted in this context, these problems require one to find a strategy (i.e., a plan) to force the system to fulfill some desired goal, no matter what the opponent (e.g., the environment) does. A strategy essentially constrains the possible behaviors of the system to those that are compatible with the decisions dictated by the plan itself. Therefore, finding a strategy to meet some goal basically reduces to identifying a portion of the model of interest (i.e., one of its substructures) that satisfies that goal. In this view, the ability to reason about substructures becomes a crucial aspect for several fundamental problems. In this article, we present and study a new branching-time temporal logic, called Substructure Temporal Logic (STL star for short), whose distinctive feature is to allow for quantifying over the possible substructure of a given structure. The logic is obtained by adding four new temporal-like operators to CTL star, whose interpretation is given relative to the partial order induced by a suitable substructure relation. STL star turns out to be very expressive and allows one to capture in a very natural way many well-known problems, such as module checking, reactive synthesis, and reasoning about games in a wide sense. 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.