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

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