Model checking memoryful linear-time logics over one-counter automata
type: Item
instance of: scholarly article
title: Model checking memoryful linear-time logics over one-counter automata
zbMATH Open document ID: 1334.68131
author: Ranko Lazić
author: Arnaud Sangnier
author: Stéphane Demri
published in: Theoretical Computer Science
publication date: 2010-05-27T00:00:00Z
Mathematics Subject Classification ID: 68Q60
Mathematics Subject Classification ID: 03B44
Mathematics Subject Classification ID: 68Q45
zbMATH DE Number: 5712827
zbMATH Keywords: one-counter automaton
zbMATH Keywords: temporal logic
zbMATH Keywords: first-order logic
zbMATH Keywords: computational complexity
MaRDI profile type: Publication
full work available at URL: j.tcs.2010.02.021
OpenAlex ID: W2036684363
cites work: Q5590814
cites work: A theory of timed automata
cites work: Shuffle Expressions and Words with Nested Data
cites work: Two-variable logic on data trees and XML reasoning
cites work: Bounded Depth Data Trees
cites work: LTL with the freeze quantifier and register automata
cites work: On the freeze quantifier in Constraint LTL: Decidability and complexity
cites work: Safely Freezing LTL
cites work: Foundations of Software Science and Computation Structures
cites work: On the decidability and complexity of Metric Temporal Logic over finite words
cites work: An algebraic approach to data languages and timed languages
cites work: Finite state machines for strings over infinite alphabets
cites work: Automata and Logics for Words and Trees over an Infinite Alphabet
cites work: On Notions of Regularity for Data Languages
cites work: Hierarchies of modal and temporal logics with reference pointers
cites work: Bounded-Variable Fragments of Hybrid Logics
cites work: Model checking hybrid logics (with an application to semistructured data)
cites work: Computer Science Logic
cites work: CONCUR 2003 - Concurrency Theory
cites work: DP lower bounds for equivalence-checking and model-checking of one-counter automata
cites work: Model Checking Freeze LTL over One-Counter Automata
cites work: Q3674621
cites work: Reversal-Bounded Multicounter Machines and Their Decision Problems
cites work: When Model-Checking Freeze LTL over Counter Machines Becomes Decidable
DOI: 10.1016/J.TCS.2010.02.021
description: scientific article; zbMATH DE number 5712827