Model checking memoryful linear-time logics over one-counter automata

DOI10.1016/J.TCS.2010.02.021zbMath1334.68131OpenAlexW2036684363MaRDI QIDQ974117

Arnaud Sangnier, Ranko Lazić, Stéphane P. Demri

Publication date: 27 May 2010

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.tcs.2010.02.021

zbMATH Keywords

computational complexityfirst-order logictemporal logicone-counter automaton

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44)

Related Items (5)

Path Checking for MTL and TPTL over Data Words ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ The Complexity of Flat Freeze LTL

Cites Work

• Unnamed Item
• Unnamed Item
• On the freeze quantifier in Constraint LTL: Decidability and complexity
• A theory of timed automata
• An algebraic approach to data languages and timed languages
• DP lower bounds for equivalence-checking and model-checking of one-counter automata
• Hierarchies of modal and temporal logics with reference pointers
• Model checking hybrid logics (with an application to semistructured data)
• LTL with the freeze quantifier and register automata
• Two-variable logic on data trees and XML reasoning
• Shuffle Expressions and Words with Nested Data
• When Model-Checking Freeze LTL over Counter Machines Becomes Decidable
• Bounded-Variable Fragments of Hybrid Logics
• Automata and Logics for Words and Trees over an Infinite Alphabet
• Reversal-Bounded Multicounter Machines and Their Decision Problems
• Finite state machines for strings over infinite alphabets
• On the decidability and complexity of Metric Temporal Logic over finite words
• Safely Freezing LTL
• Computer Science Logic
• Bounded Depth Data Trees
• On Notions of Regularity for Data Languages
• Model Checking Freeze LTL over One-Counter Automata
• Foundations of Software Science and Computation Structures
• Foundations of Software Science and Computation Structures
• CONCUR 2003 - Concurrency Theory

This page was built for publication: Model checking memoryful linear-time logics over one-counter automata