Model-Checking Counting Temporal Logics on Flat Structures

DOI10.4230/LIPICS.CONCUR.2017.29MaRDI QIDQ5111643zbMATH OpenOpenAlexFDO

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

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)

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.

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

Cites work

• scientific article; zbMATH DE number 3870578 (Why is no real title available?)
• scientific article; zbMATH DE number 1954380 (Why is no real title available?)
• scientific article; zbMATH DE number 5585443 (Why is no real title available?)
• scientific article; zbMATH DE number 3310089 (Why is no real title available?)
• Arithmetic, first-order logic, and counting quantifiers
• Automated Technology for Verification and Analysis
• Axiomatische Untersuchungen über Einige mit der Presburgerschen Arithmetik Verwandte Systeme
• Counting CTL
• Equivalence between model-checking flat counter systems and Presburger arithmetic
• Kleene, Rabin, and Scott Are Available
• LTL with the freeze quantifier and register automata
• Model-Checking Counting Temporal Logics on Flat Structures
• Model-checking \(\mathrm{CTL}^*\) over flat Presburger counter systems
• Reachability analysis of pushdown automata: Application to model-checking
• Taming past LTL and flat counter systems
• The complexity of logical theories
• Weak Kripke structures and LTL
• What's decidable about availability languages?

Cited in

(13)

• ``Most of leads to undecidability: failure of adding frequencies to LTL
• Model Checking Metric Temporal Logic over Automata with One Counter
• Model-Checking Counting Temporal Logics on Flat Structures
• Verification of flat FIFO systems
• Model-checking \(\mathrm{CTL}^*\) over flat Presburger counter systems
• On the Complexity of Verifying Regular Properties on Flat Counter Systems,
• scientific article; zbMATH DE number 1670482 (Why is no real title available?)
• Verification of Flat FIFO Systems
• Counting Models of Linear-Time Temporal Logic
• The complexity of counting models of linear-time temporal logic
• The complexity of counting models of linear-time temporal logic
• A counting logic for structure transition systems
• Flat model checking for counting LTL using quantifier-free Presburger arithmetic

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)