Verification of qualitative \(\mathbb Z\) constraints
type: Item
instance of: scholarly article
title: Verification of qualitative \(\mathbb Z\) constraints
zbMATH Open document ID: 1157.68048
author: Régis Gascon
author: Stéphane Demri
published in: Theoretical Computer Science
publication date: 2008-12-12T00:00:00Z
Mathematics Subject Classification ID: 68Q60
Mathematics Subject Classification ID: 03B44
Mathematics Subject Classification ID: 68Q25
zbMATH DE Number: 5382281
zbMATH Keywords: temporal logic
zbMATH Keywords: arithmetical constraint
zbMATH Keywords: Büchi automaton
zbMATH Keywords: symbolic model
zbMATH Keywords: complexity
describes a project that uses: FAST
MaRDI profile type: Publication
full work available at URL: j.tcs.2008.07.023
OpenAlex ID: W2059905982
cites work: A theory of timed automata
cites work: A really temporal logic
cites work: Programs with Lists Are Counter Automata
cites work: Q4737132
cites work: Q4039803
cites work: Reachability analysis of pushdown automata: Application to model-checking
cites work: Untiming timed languages
cites work: Branching-Time Temporal Logic Extended with Qualitative Presburger Constraints
cites work: Q4012242
cites work: Flat Parametric Counter Automata
cites work: On infinite transition graphs having a decidable monadic theory
cites work: Q2753678
cites work: Deciding properties of integral relational automata
cites work: An automata-theoretic approach to constraint LTL
cites work: LTL over integer periodicity constraints
cites work: Towards a Model-Checker for Counter Systems
cites work: CONCUR 2005 – Concurrency Theory
cites work: THE EXISTENCE OF ω-CHAINS FOR TRANSITIVE MIXED LINEAR RELATIONS AND ITS APPLICATIONS
cites work: Presburger liveness verification of discrete timed automata.
cites work: Q4415251
cites work: Q4501546
cites work: CONCUR 2003 - Concurrency Theory
cites work: Q5715695
cites work: Q3999206
cites work: A classification of symbolic transition systems
cites work: Reversal-Bounded Multicounter Machines and Their Decision Problems
cites work: Q4474093
cites work: DP lower bounds for equivalence-checking and model-checking of one-counter automata
cites work: Q4778773
cites work: NEXP TIME-complete description logics with concrete domains
cites work: Q5590814
cites work: Programming Languages and Systems
cites work: The theory of ends, pushdown automata, and second-order logic
cites work: Automata for branching and layered temporal structures. An investigation into regularities of infinite transition systems
cites work: Introduction to constraint databases
cites work: The complexity of propositional linear temporal logics
cites work: Reasoning about infinite computations
cites work: Temporal logic can be more expressive
DOI: 10.1016/J.TCS.2008.07.023
description: scientific article; zbMATH DE number 5382281