Model-Checking Counting Temporal Logics on Flat Structures

DOI10.4230/LIPIcs.CONCUR.2017.29zbMath1442.68105arXiv1706.08608OpenAlexW2963079949MaRDI QIDQ5111643

Arnaud Sangnier, Daniel Thoma, Martin Leucker, Normann Decker, Peter Habermehl

Publication date: 27 May 2020

Full work available at URL: https://arxiv.org/abs/1706.08608

zbMATH Keywords

model checkingcounting temporal logicflat Kripke structure

Mathematics Subject Classification ID

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

Related Items

Verification of Flat FIFO Systems ⋮ ``Most of leads to undecidability: failure of adding frequencies to LTL ⋮ Unnamed Item ⋮ Model-Checking Counting Temporal Logics on Flat Structures

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• The complexity of logical theories
• Taming past LTL and flat counter systems
• Model-checking CTL* over flat Presburger counter systems
• LTL with the freeze quantifier and register automata
• Weak Kripke Structures and LTL
• Equivalence Between Model-Checking Flat Counter Systems and Presburger Arithmetic
• Counting CTL
• Kleene, Rabin, and Scott Are Available
• Model-Checking Counting Temporal Logics on Flat Structures
• Arithmetic, first-order logic, and counting quantifiers
• Automated Technology for Verification and Analysis
• Axiomatische Untersuchungen über Einige mit der Presburgerschen Arithmetik Verwandte Systeme
• Reachability analysis of pushdown automata: Application to model-checking