Demri, Stéphane P., Lazic, Ranko and Sangnier, Arnaud (2010) Model checking memoryful linear-time logics over one-counter automata. Theoretical Computer Science, Vol.411 (No.22-24). pp. 2298-2316. doi:10.1016/j.tcs.2010.02.021 ISSN 0304-3975.

PDF test1.pdf - Published Version Embargoed item. Restricted access to Repository staff only - Requires a PDF viewer. Download (374Kb)

Request Changes to record.

Abstract

We study complexity of the model-checking problems for LTL with registers (also known as freeze LTL and written LTL down arrow) and for first-order logic with data equality tests (written FO (similar to, <, +1)) over one-counter automata. We consider several classes of one-counter automata (mainly deterministic vs. nondeterministic) and several logical fragments (restriction on the number of registers or variables and on the use of propositional variables for control states). The logics have the ability to store a counter value and to test it later against the current counter value. We show that model checking LTL down arrow and FO(similar to, <, +1) over deterministic one-counter automata is PSPACE-complete with infinite and finite accepting runs. By contrast, we prove that model checking LTL down arrow in which the until operator U is restricted to the eventually F over nondeterministic one-counter automata is Sigma(1)(1)-complete [resp. Sigma(0)(1)-completel in the infinitary [resp. finitary] case even if only one register is used and with no propositional variable. As a corollary of our proof, this also holds for FO(similar to, <, +1) restricted to two variables (written FO2(similar to, <, +1)). This makes a difference with respect to the facts that several verification problems for one-counter automata are known to be decidable with relatively low complexity, and that finitary satisfiability problems for LTL down arrow and FO2(similar to, <, +1) are decidable. Our results pave the way for model checking memoryful (linear-time) logics over other classes of operational models, such as reversal-bounded counter machines. (C) 2010 Elsevier B.V. All rights reserved.

Item Type:	Journal Article
Subjects:	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):	Computational complexity, First-order logic
Journal or Publication Title:	Theoretical Computer Science
Publisher:	Elsevier Science BV
ISSN:	0304-3975
Official Date:	17 May 2010
Dates:	Date Event 17 May 2010 Published
Volume:	Vol.411
Number:	No.22-24
Number of Pages:	19
Page Range:	pp. 2298-2316
DOI:	10.1016/j.tcs.2010.02.021
Status:	Peer Reviewed
Publication Status:	Published
Access rights to Published version:	Restricted or Subscription Access
Date of first compliant deposit:	3 December 2015
Funder:	France. Agence nationale de la recherche (ANR)
Grant number:	ANR-06-SETIN-001 (ANR)
Open Access Version:	ArXiv

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