Flat model checking for counting LTL using quantifier-free Presburger arithmetic

DOI10.1007/978-3-030-11245-5_24MaRDI QIDQ2287113zbMATH OpenOpenAlexFDO

Authors Normann Decker, Anton Pirogov

Publication date 23 January 2020

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

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Model-Checking Counting Temporal Logics on Flat Structures
• Equivalence between model-checking flat counter systems and Presburger arithmetic
• On the Complexity of Verifying Regular Properties on Flat Counter Systems,
• Equivalence between model-checking flat counter systems and Presburger arithmetic
• Towards a Model-Checker for Counter Systems

Cited in

(5)

• Model-Checking Counting Temporal Logics on Flat Structures
• Model-checking \(\mathrm{CTL}^*\) over flat Presburger counter systems
• Equivalence between model-checking flat counter systems and Presburger arithmetic
• Towards a Model-Checker for Counter Systems
• Equivalence between model-checking flat counter systems and Presburger arithmetic

This page was built for publication: Flat model checking for counting LTL using quantifier-free Presburger arithmetic

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