Bounded Satisfiability Checking of Metric Temporal Logic Specifications

We introduce Bounded Satisfiability Checking, a verification technique that extends Bounded Model Checking by allowing also the analysis of a descriptive model, consisting of temporal logic formulae, instead of the more customary operational model, consisting of a state-transition system. We define techniques for encoding temporal logic formulae into Boolean logic that support the use of bi-infinite time domain and of metric time operators. In the framework of Bounded Satisfiability Checking, we show how a descriptive model can be refined into an operational one, and how the correctness of such a refinement can be verified for the bounded case, setting the stage for a stepwise system development method based on a bounded model refinement. Finally, we show how the adoption of a modular approach can make the bounded refinement process more manageable and efficient. All introduced concepts are extensively applied to a set of case studies, and thoroughly experimented through Zot, our SAT solver-based verification toolset.