a Department of Computer Science, Technion — Israel Institute of Technology, Technion City, Haifa 32000, Israel
b Computer Sciences Department, University of Texas, Austin, TX 78712, USA
Abstract:
It is shown that in first-order linear-time temporal logic, validity questions can be translated into validity questions of formulas not containing “next” or “until” operators. The translation can be performed in linear time.