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
model checkingverification of infinite-state systemsabstractions of counter systemscomplexity and decidability issuestemporal logics with Presburger constraints
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
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
