id: 05265229
dt: a
an: 05265229
au: Lazić, Ranko
ti: Safely freezing LTL.
so: Arun-Kumar, S. (ed.) et al., FSTTCS 2006: Foundations of software
    technology and theoretical computer science. 26th international
    conference, Kolkata, India, December 13‒15, 2006. Proceedings.
    Berlin: Springer (ISBN 978-3-540-49994-7/pbk). Lecture Notes in
    Computer Science 4337, 381-392 (2006).
py: 2006
pu: Berlin: Springer
la: EN
cc: 
ut: 
ci: 
li: doi:10.1007/11944836_35
ab: Summary: 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.
rv: