\title{Generalised Unification of Temporal Logic Formulas}
       \author{Scott Hazelhurst}
       \affiliation{Department of Computer
       Science, University of the Witwatersrand, Johannesburg,\\ Private
       Bag 3, 2050 Wits, South Africa,\\ scott@cs.wits.ac.za}


       \begin{abstract}\noindent
         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 \implysynt 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 verification
         system. 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.
       \end{abstract}

       \keywords{unification, temporal logic, pattern matching}\\
       \CRCategories{F2.2, F4.1, F4.2, I2.4}