Safely freezing LTL
Lazic, Ranko (2006) Safely freezing LTL. In: 26th International Conference on Foundations of Software Technology and Theoretical Computer Science, Calcutta, INDIA, DEC 13-15, 2006. Published in: FSTTCS 2006: Foundations of Software Technology and Theoretical Computer Science, Proceedings, 4337 pp. 381-392.Full text not available from this repository.
We consider the safety fragment of linear temporal logic with the freeze quantifier. The freeze quantifier is used to store a value from an infinite domain in a register for later comparison with other such values. We show that, for one register, satisfiability, refinement and model checking problems are decidable. The main result in the paper is that satisfiability is EXPSPACE-complete. The proof of EXPSPACE-membership involves a translation to a new class of faulty counter automata. We also show that refinement and model checking are not primitive recursive, and that dropping the safety restriction, adding past-time temporal operators, or adding one more register, each cause undecidability of all three decision problems.
|Item Type:||Conference Item (UNSPECIFIED)|
|Subjects:||Q Science > QA Mathematics > QA76 Electronic computers. Computer science. Computer software|
|Series Name:||LECTURE NOTES IN COMPUTER SCIENCE|
|Journal or Publication Title:||FSTTCS 2006: Foundations of Software Technology and Theoretical Computer Science, Proceedings|
|Editor:||ArunKumar, S and Garg, N|
|Number of Pages:||12|
|Page Range:||pp. 381-392|
|Title of Event:||26th International Conference on Foundations of Software Technology and Theoretical Computer Science|
|Location of Event:||Calcutta, INDIA|
|Date(s) of Event:||DEC 13-15, 2006|
Actions (login required)