Generalised unification of finite temporal logic formulas
Loading...
Authors
Hazelhurst, S
Issue Date
1999
Type
Article
Language
en
Keywords
Unification , Temporal logic , Pattern matching
Alternative Title
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.
Description
Citation
Hazelhurst S (1999) Generalised unification of finite temporal logic formulas. South African Computer Journal, Number 24, 1999
Publisher
South African Computer Society (SAICSIT)
License
Journal
Volume
Issue
PubMed ID
DOI
ISSN
2313-7835