Demri, Stéphane P., 1967-, 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. ISSN 0304-3975

Full text not available from this repository.

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 > 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
Date:	17 May 2010
Volume:	Vol.411
Number:	No.22-24
Number of Pages:	19
Page Range:	pp. 2298-2316
Identification Number:	10.1016/j.tcs.2010.02.021
Status:	Peer Reviewed
Publication Status:	Published
Access rights to Published version:	Restricted or Subscription Access
Funder:	France. Agence nationale de la recherche (ANR)
Grant number:	ANR-06-SETIN-001 (ANR)
URI:	http://wrap.warwick.ac.uk/id/eprint/5741

Data sourced from Thomson Reuters' Web of Knowledge

Request changes to a record

Actions (login required)

View Item