Skip to content Skip to navigation
University of Warwick
  • Study
  • |
  • Research
  • |
  • Business
  • |
  • Alumni
  • |
  • News
  • |
  • About

University of Warwick
Publications service & WRAP

Highlight your research

  • WRAP
    • Home
    • Search WRAP
    • Browse by Warwick Author
    • Browse WRAP by Year
    • Browse WRAP by Subject
    • Browse WRAP by Department
    • Browse WRAP by Funder
    • Browse Theses by Department
  • Publications Service
    • Home
    • Search Publications Service
    • Browse by Warwick Author
    • Browse Publications service by Year
    • Browse Publications service by Subject
    • Browse Publications service by Department
    • Browse Publications service by Funder
  • Help & Advice
University of Warwick

The Library

  • Login
  • Admin

LTL with the freeze quantifier and register automata

Tools
- Tools
+ Tools

Demri, Stéphane P. and Lazic, Ranko (2009) LTL with the freeze quantifier and register automata. ACM Transactions on Computational Logic (TOCL), Vol.10 (No.3). p. 16. doi:10.1145/1507244.1507246 ISSN 1529-3785.

[img] PDF
acmtrans.pdf - Published Version
Embargoed item. Restricted access to Repository staff only - Requires a PDF viewer.

Download (517Kb)
Official URL: http://dx.doi.org/10.1145/1507244.1507246

Request Changes to record.

Abstract

A data word is a sequence of pairs of a letter from a finite alphabet and an element from an infinite set, where the latter can only be compared for equality. To reason about data words, linear temporal logic is extended by the freeze quantifier, which stores the element at the current word position into a register, for equality comparisons deeper in the formula. By translations from the logic to alternating automata with registers and then to faulty counter automata whose counters may erroneously increase at any time, and from faulty and error-free counter automata to the logic, we obtain a complete complexity table for logical fragments defined by varying the set of temporal operators and the number of registers. In particular, the logic with future-time operators and 1 register is decidable but not primitive recursive over finite data words. Adding past-time operators or 1 more register, or switching to infinite data words, causes undecidability.

Item Type: Journal Article
Subjects: Q Science > QA Mathematics
Q Science > QA Mathematics > QA76 Electronic computers. Computer science. Computer software
Divisions: Faculty of Science, Engineering and Medicine > Science > Computer Science
Library of Congress Subject Headings (LCSH): Computer programs -- Verification , Computational complexity, Algorithms, Formal languages, Machine theory
Journal or Publication Title: ACM Transactions on Computational Logic (TOCL)
Publisher: Association for Computing Machinery, Inc.
ISSN: 1529-3785
Official Date: April 2009
Dates:
DateEvent
April 2009Published
Volume: Vol.10
Number: No.3
Number of Pages: 30
Page Range: p. 16
DOI: 10.1145/1507244.1507246
Status: Peer Reviewed
Publication Status: Published
Access rights to Published version: Restricted or Subscription Access
Date of first compliant deposit: 13 December 2015
Funder: ACI Sécurité et informatique (ACI), Engineering and Physical Sciences Research Council (EPSRC), Intel Corporation, École normale supérieure (Cachan, France) (ENS)
Grant number: GR/S52759/01 (EPSRC)
Version or Related Resource: This article is a revised and extended version of: Demri, S. and Lazic, R. (2006). LTL with the freeze quantifier and register automata. Proceedings of the 21st IEEE Symposium on Logic in Computer Science (LICS), pp. 17–26.

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 View Item
twitter

Email us: wrap@warwick.ac.uk
Contact Details
About Us