Verification of qualitative \(\mathbb Z\) constraints
From MaRDI portal
Publication:959820
DOI10.1016/j.tcs.2008.07.023zbMath1157.68048OpenAlexW2059905982MaRDI QIDQ959820
Régis Gascon, Stéphane P. Demri
Publication date: 12 December 2008
Published in: Theoretical Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.tcs.2008.07.023
Analysis of algorithms and problem complexity (68Q25) Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44)
Related Items
Satisfiability of \(\operatorname{ECTL}^\ast\) with constraints ⋮ Verification of Gap-Order Constraint Abstractions of Counter Systems ⋮ Satisfiability of ECTL* with Tree Constraints ⋮ Satisfiability of \(\mathrm{ECTL}^*\) with local tree constraints ⋮ Verification of gap-order constraint abstractions of counter systems ⋮ CTL* model checking for data-aware dynamic systems with arithmetic
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Untiming timed languages
- Automata for branching and layered temporal structures. An investigation into regularities of infinite transition systems
- An automata-theoretic approach to constraint LTL
- The theory of ends, pushdown automata, and second-order logic
- A theory of timed automata
- Reasoning about infinite computations
- On infinite transition graphs having a decidable monadic theory
- Presburger liveness verification of discrete timed automata.
- DP lower bounds for equivalence-checking and model-checking of one-counter automata
- LTL over integer periodicity constraints
- THE EXISTENCE OF ω-CHAINS FOR TRANSITIVE MIXED LINEAR RELATIONS AND ITS APPLICATIONS
- Temporal logic can be more expressive
- Towards a Model-Checker for Counter Systems
- The complexity of propositional linear temporal logics
- Reversal-Bounded Multicounter Machines and Their Decision Problems
- A really temporal logic
- Deciding properties of integral relational automata
- NEXP TIME-complete description logics with concrete domains
- A classification of symbolic transition systems
- Programming Languages and Systems
- Branching-Time Temporal Logic Extended with Qualitative Presburger Constraints
- Programs with Lists Are Counter Automata
- CONCUR 2005 – Concurrency Theory
- CONCUR 2003 - Concurrency Theory
- Flat Parametric Counter Automata
- Introduction to constraint databases
- Reachability analysis of pushdown automata: Application to model-checking
