Model-Checking Counting Temporal Logics on Flat Structures

DOI10.4230/LIPICS.CONCUR.2017.29zbMATH Open1442.68105arXiv1706.08608OpenAlexW2963079949MaRDI QIDQ5111643FDOQ5111643

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

Publication date: 27 May 2020

Abstract: We study several extensions of linear-time and computation-tree temporal logics with quantifiers that allow for counting how often certain properties hold. For most of these extensions, the model-checking problem is undecidable, but we show that decidability can be recovered by considering flat Kripke structures where each state belongs to at most one simple loop. Most decision procedures are based on results on (flat) counter systems where counters are used to implement the evaluation of counting operators.

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

Recommendations

• Counting Models of Linear-Time Temporal Logic
• Flat model checking for counting LTL using quantifier-free Presburger arithmetic
• The complexity of counting models of linear-time temporal logic
• The complexity of counting models of linear-time temporal logic
• scientific article; zbMATH DE number 2196601
• Model-checking timed temporal logics
• A counting logic for structure transition systems
• Deciding continuous-time metric temporal logic with counting modalities
• Complexity of metric temporal logics with counting and the Pnueli modalities
• Complexity of Metric Temporal Logics with Counting and the Pnueli Modalities

zbMATH Keywords

model checkingcounting temporal logicflat Kripke structure

Mathematics Subject Classification ID

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

Cites Work

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

Cited In (9)

• Verification of Flat FIFO Systems
• Counting Models of Linear-Time Temporal Logic
• The complexity of counting models of linear-time temporal logic
• ``Most of leads to undecidability: failure of adding frequencies to LTL
• Title not available (Why is that?)
• Model Checking Metric Temporal Logic over Automata with One Counter
• On the Complexity of Verifying Regular Properties on Flat Counter Systems,
• Title not available (Why is that?)
• Model-Checking Counting Temporal Logics on Flat Structures

This page was built for publication: Model-Checking Counting Temporal Logics on Flat Structures

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5111643)