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.

Abstract

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
Publisher:	SPRINGER-VERLAG BERLIN
ISBN:	978-3-540-49994-7
ISSN:	0302-9743
Editor:	ArunKumar, S and Garg, N
Date:	2006
Volume:	4337
Number of Pages:	12
Page Range:	pp. 381-392
Publication Status:	Published
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
URI:	http://wrap.warwick.ac.uk/id/eprint/30973

Data sourced from Thomson Reuters' Web of Knowledge

Request changes to a record

Actions (login required)

View Item