|
|||||
|
|
The power of the “always” operator in first-order temporal logic |
|
| Authors: | Michael Kaminski Chung Kei Wong |
| Affiliation: | 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. |
| Keywords: | |
| 本文献已被 ScienceDirect 等数据库收录！ | |