Lazic, Ranko (2011) Safety alternating automata on data words. ACM Transactions on Computational Logic (TOCL), Vol.12 (No.2). pp. 1-24. doi:10.1145/1877714.1877716 ISSN 1529-3785.

Research output not available from this repository.

Request-a-Copy directly from author or use local Library Get it For Me service.

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. Safety one-way alternating automata with one register on infinite data words are considered, their nonemptiness is shown to be EXPSPACE-complete, and their inclusion decidable but not primitive recursive. The same complexity bounds are obtained for satisfiability and refinement, respectively, for the safety fragment of linear temporal logic with freeze quantification. Dropping the safety restriction, adding past temporal operators, or adding one more register, each causes undecidability.

Item Type:	Journal Article
Divisions:	Faculty of Science, Engineering and Medicine > Science > Computer Science
Journal or Publication Title:	ACM Transactions on Computational Logic (TOCL)
Publisher:	Association for Computing Machinery, Inc.
ISSN:	1529-3785
Official Date:	2011
Dates:	Date Event 2011 Published
Volume:	Vol.12
Number:	No.2
Page Range:	pp. 1-24
DOI:	10.1145/1877714.1877716
Status:	Peer Reviewed
Publication Status:	Published
Access rights to Published version:	Restricted or Subscription Access
Funder:	Engineering and Physical Sciences Research Council (EPSRC) , Intel Corporation , ENS Cachan
Grant number:	GR/S52759/01 (EPSRC)

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