Verification of gap-order constraint abstractions of counter systems

DOI10.1016/j.tcs.2013.12.002zbMath1358.68182OpenAlexW2014528727MaRDI QIDQ2435309

Sophie Pinchinat, Laura Bozzelli

Publication date: 4 February 2014

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.tcs.2013.12.002

zbMATH Keywords

model checkingverification of infinite-state systemsabstractions of counter systemscomplexity and decidability issuestemporal logics with Presburger constraints

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60) Decidability of theories and sets of sentences (03B25) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Temporal logic (03B44)

Related Items

Verification of Gap-Order Constraint Abstractions of Counter Systems ⋮ Satisfiability of ECTL* with Tree Constraints ⋮ Satisfiability of \(\mathrm{ECTL}^*\) with local tree constraints ⋮ Interprocedural Reachability for Flat Integer Programs ⋮ CTL* model checking for data-aware dynamic systems with arithmetic

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A closed-form evaluation for Datalog queries with integer (gap)-order constraints
• An automata-theoretic approach to constraint LTL
• Verification of qualitative \(\mathbb Z\) constraints
• Approximated parameterized verification of infinite-state processes with global conditions
• Reasoning about infinite computations
• Monotonicity Constraints for Termination in the Integer Domain
• Automatic Inference of Upper Bounds for Recurrence Relations in Cost Analysis
• Towards a Model-Checker for Counter Systems
• Iterating Octagons
• “Sometimes” and “not never” revisited
• Reversal-Bounded Multicounter Machines and Their Decision Problems
• The benefits of relaxing punctuality
• Deciding properties of integral relational automata
• Branching-Time Temporal Logic Extended with Qualitative Presburger Constraints
• Programs with Lists Are Counter Automata
• Size-Change Termination, Monotonicity Constraints and Ranking Functions