Generalised unification of finite temporal logic formulas

Abstract

Given two temporal logic formulas, g and h, we wish to know whether there is a modification, m, we can make to h so that g ==> m( h). This problem has important applications in hardware verification, where finding such modifications efficiently is important for an inferencing system. The temporal logic used, TL, is a relatively simple logic which is interpreted over finite state machine models. The modifications allowed are 'time-shifting' (nesting under the next-time temporal operator) and substitution of expressions for variables. An algorithm has been developed and implemented in the Voss verfication system for the finite fragment of TL. The basis of the algorithm is to use a relatively compact, normalised representation of the formulas, which converts the problem into a generalised string matching problem. Some experimental results have been obtained from the use of the algorithm in practice.