Model-checking CTL^* over flat Presburger counter systems
From MaRDI portal
Publication:2901199
Recommendations
- Towards a Model-Checker for Counter Systems
- Equivalence between model-checking flat counter systems and Presburger arithmetic
- Equivalence between model-checking flat counter systems and Presburger arithmetic
- Flat model checking for counting LTL using quantifier-free Presburger arithmetic
- Model-Checking Counting Temporal Logics on Flat Structures
Cites work
- A really temporal logic
- About the decision of reachability for register machines
- Finite presentations of infinite structures: Automata and interpretations
- scientific article; zbMATH DE number 3310089 (Why is no real title available?)
- LTL over integer periodicity constraints
- More numerical evidence on the uniqueness of Markov Numbers
- On infinite transition graphs having a decidable monadic theory
- On iterating linear transformations over recognizable sets of integers
- Presburger liveness verification of discrete timed automata.
- Programs with Lists Are Counter Automata
- Pushdown processes: Games and model-checking
- Reversal-Bounded Multicounter Machines and Their Decision Problems
- Semigroups, Presburger formulas, and languages
- Specification in CTL + past for verification in CTL.
- Symbolic reachability analysis of FIFO-channel systems with nonregular sets of configurations
- The 3x + 1 Problem and Its Generalizations
- The theory of ends, pushdown automata, and second-order logic
- Towards Model-Checking Programs with Lists
- “Sometimes” and “not never” revisited
Cited in
(24)- Model checking CTL over restricted classes of automatic structures
- CTL* model checking for data-aware dynamic systems with arithmetic
- Taming past LTL and flat counter systems
- Equivalence between model-checking flat counter systems and Presburger arithmetic
- Bounded Parikh automata
- Forward analysis and model checking for trace bounded WSTS
- Forward analysis and model checking for trace bounded WSTS
- Regular Growth Automata: Properties of a Class of Finitely Induced Infinite Machines
- The complexity of reversal-bounded model-checking
- Equivalence between model-checking flat counter systems and Presburger arithmetic
- Towards a Model-Checker for Counter Systems
- Computable CTL * for Discrete-Time and Continuous-Space Dynamic Systems
- Efficient CTL model-checking for pushdown systems
- Constraint LTL satisfiability checking without automata
- Analyzing automata with Presburger arithmetic and uninterpreted function symbols
- Unboundedness problems for languages of vector addition systems
- Efficient CTL verification via Horn constraints solving
- scientific article; zbMATH DE number 7471708 (Why is no real title available?)
- Non axiomatisability of positive relation algebras with constants, via graph homomorphisms
- Model-Checking Counting Temporal Logics on Flat Structures
- Verification of flat FIFO systems
- Model Checking Software
- Verification of Flat FIFO Systems
- Synchronized CTL over one-counter automata
This page was built for publication: Model-checking \(\mathrm{CTL}^*\) over flat Presburger counter systems
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2901199)
