The Library
Safely freezing LTL
Tools
Lazic, Ranko (2006) Safely freezing LTL. In: 26th International Conference on Foundations of Software Technology and Theoretical Computer Science, Calcutta, India, 13-15 Dec 2006, Volume 4337 pp. 381-392. ISBN 9783540499947. ISSN 0302-9743.
PDF
freezltl.pdf - Published Version Embargoed item. Restricted access to Repository staff only - Requires a PDF viewer. Download (238Kb) |
Official URL: http://dx.doi.org/10.1007/11944836_35
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 (Paper) | ||||
---|---|---|---|---|---|
Subjects: | Q Science > QA Mathematics > QA76 Electronic computers. Computer science. Computer software | ||||
Divisions: | Faculty of Science, Engineering and Medicine > Science > Computer Science | ||||
Series Name: | Lecture Notes in Computer Science | ||||
Publisher: | Springer Berlin Heidelberg | ||||
ISBN: | 9783540499947 | ||||
ISSN: | 0302-9743 | ||||
Book Title: | FSTTCS 2006 : Foundations of Software Technology and Theoretical Computer Science | ||||
Editor: | ArunKumar, S. and Garg, N. | ||||
Official Date: | 2006 | ||||
Dates: |
|
||||
Volume: | Volume 4337 | ||||
Number of Pages: | 12 | ||||
Page Range: | pp. 381-392 | ||||
Status: | Peer Reviewed | ||||
Publication Status: | Published | ||||
Access rights to Published version: | Restricted or Subscription Access | ||||
Date of first compliant deposit: | 28 July 2016 | ||||
Conference Paper Type: | Paper | ||||
Title of Event: | 26th International Conference on Foundations of Software Technology and Theoretical Computer Science | ||||
Type of Event: | Conference | ||||
Location of Event: | Calcutta, India | ||||
Date(s) of Event: | 13-15 Dec 2006 |
Data sourced from Thomson Reuters' Web of Knowledge
Request changes or add full text files to a record
Repository staff actions (login required)
View Item |