Model-checking CTL* over flat Presburger counter systems

DOI10.3166/jancl.20.313-344zbMath1242.68157OpenAlexW2073466252MaRDI QIDQ2901199

Stéphane P. Demri, Govert van Drimmelen, Alain Finkel, Valentin F. Goranko

Publication date: 17 July 2012

Published in: Journal of Applied Non-Classical Logics (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.3166/jancl.20.313-344

Mathematics Subject Classification ID

Automata and formal grammars in connection with logical questions (03D05) Specification and verification (program logics, model checking, etc.) (68Q60) First-order arithmetic and fragments (03F30)

Related Items (16)

Forward analysis and model checking for trace bounded WSTS ⋮ Equivalence Between Model-Checking Flat Counter Systems and Presburger Arithmetic ⋮ Regular Growth Automata: Properties of a Class of Finitely Induced Infinite Machines ⋮ Equivalence between model-checking flat counter systems and Presburger arithmetic ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Constraint LTL satisfiability checking without automata ⋮ Verification of Flat FIFO Systems ⋮ Unboundedness Problems for Languages of Vector Addition Systems. ⋮ Forward Analysis and Model Checking for Trace Bounded WSTS ⋮ Non axiomatisability of positive relation algebras with constants, via graph homomorphisms ⋮ Unnamed Item ⋮ BOUNDED PARIKH AUTOMATA ⋮ Model-Checking Counting Temporal Logics on Flat Structures ⋮ CTL* model checking for data-aware dynamic systems with arithmetic ⋮ Taming past LTL and flat counter systems

Cites Work

• Unnamed Item
• The theory of ends, pushdown automata, and second-order logic
• Finite presentations of infinite structures: Automata and interpretations
• On infinite transition graphs having a decidable monadic theory
• Specification in CTL + past for verification in CTL.
• Pushdown processes: Games and model-checking
• Presburger liveness verification of discrete timed automata.
• On iterating linear transformations over recognizable sets of integers
• Symbolic reachability analysis of FIFO-channel systems with nonregular sets of configurations
• LTL over integer periodicity constraints
• Semigroups, Presburger formulas, and languages
• Towards Model-Checking Programs with Lists
• The 3x + 1 Problem and Its Generalizations
• “Sometimes” and “not never” revisited
• More numerical evidence on the uniqueness of Markov Numbers
• Reversal-Bounded Multicounter Machines and Their Decision Problems
• A really temporal logic
• About the decision of reachability for register machines
• Programs with Lists Are Counter Automata

This page was built for publication: Model-checking CTL* over flat Presburger counter systems