Model checking memoryful linear-time logics over one-counter automata
From MaRDI portal
Publication:974117
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
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
