Title
A HOL Conversion for Translating Linear Time Temporal Logic to omega-Automata
Abstract
We present an embedding of linear time temporal logic LTL in HOL together with an elegant translation of LTL formulas into equivalent ω-automata. The translation is completely implemented by HOL rules and is therefore safe. Its implementation is mainly based on preproven theorems such that the conversion works very efficiently. In particular, it runs in linear time in terms of the given formula. The main application of this conversion is the sound integration of symbolic model checkers as (unsafe) decision procedures in the HOL theorem prover. On the other hand, the conversion also enables HOL users to directly verify temporal properties by means of HOL's induction rules.
Year
DOI
Venue
1999
10.1007/3-540-48256-3_17
TPHOLs
Keywords
Field
DocType
elegant translation,induction rule,decision procedure,hol theorem prover,hol rule,translating linear time temporal,temporal property,hol user,temporal logic ltl,linear time,ltl formula,hol conversion
HOL,Kripke structure,Discrete mathematics,Model checking,Computer science,Automated theorem proving,Algorithm,Linear temporal logic,Temporal logic,Linear logic,Formal verification
Conference
Volume
ISSN
ISBN
1690
0302-9743
3-540-66463-7
Citations 
PageRank 
References 
20
1.21
26
Authors
2
Name
Order
Citations
PageRank
Klaus Schneider114218.72
Dirk W. Hoffmann2272.15