An automata-theoretic approach to constraint LTL
type: Item
instance of: scholarly article
title: An automata-theoretic approach to constraint LTL
zbMATH Open document ID: 1113.03015
author: Deepak D'Souza
author: Stéphane Demri
published in: Information and Computation
publication date: 2007-03-12T00:00:00Z
review text: Building on their earlier paper [``An automata-theoretic approach to constraint LTL'', Lect. Notes Comput. Sci. 2556, 121--132 (2002; Zbl 1027.03027)], the authors consider an extension of the linear-time temporal logic LTL with constraints interpreted over a concrete domain and, using a new automata-theoretic technique, they show PSPACE-decidability of the logics for the constraint systems \((\mathbb{Z},<,=)\) and \((\mathbb{N},<,=)\). Notably, unlike the propositional LTL, the formulae of these constraint logics do not preserve \(\omega\)-regularity of the sets of models. Nevertheless, the authors succeed to approximate from above the set of models of every such formula with an \(\omega\)-regular superset that contains the same ultimately periodic words, thus reducing the non-emptiness problem of the former to the non-emptiness problem of the latter, whence the decidability results follow. The second main contribution is the modularity of the automata-theoretic technique developed in the paper, in the sense that the automaton constructed to check satisfiability of a given formula is the interstection of two separate automata, one corresponding to the underlying logical language, and the other to the considered constraint system. The authors demonstrate the benefits from this modular approach, in particular by extending the decision procedure to handle past operators added to LTL, as well as to full Büchi MSO over \(\mathbb{N}\) over the considered systems of constraints. Finally, the authors extend the decidability and complexity results to constraint systems with constants, by reduction to the standard case, while they show that adding a `counting' mechanism to the constraint system leads to undecidability.
reviewed by: Valentin Goranko
Mathematics Subject Classification ID: 03B44
Mathematics Subject Classification ID: 03B70
Mathematics Subject Classification ID: 68Q60
Mathematics Subject Classification ID: 03D05
Mathematics Subject Classification ID: 03B25
zbMATH DE Number: 5133057
zbMATH Keywords: temporal logic
zbMATH Keywords: model-checking
zbMATH Keywords: automata
describes a project that uses: Truth/SLC
MaRDI profile type: Publication
full work available at URL: j.ic.2006.09.006
OpenAlex ID: W2019145653
cites work: Maintaining knowledge about temporal intervals
cites work: A theory of timed automata
cites work: Real-time logics: Complexity and expressiveness
cites work: A really temporal logic
cites work: Q4012242
cites work: Q4737132
cites work: Multi-dimensional modal logic as a framework for spatio-temporal reasoning
cites work: Untiming timed languages
cites work: Q5691140
cites work: Branching-Time Temporal Logic Extended with Qualitative Presburger Constraints
cites work: Q4418693
cites work: Q5525343
cites work: Deciding properties of integral relational automata
cites work: Q2753678
cites work: Presburger liveness verification of discrete timed automata.
cites work: From local to global consistency
cites work: Linear-time temporal logics with Presburger constraints: an overview ★
cites work: LTL over integer periodicity constraints
cites work: Q4415249
cites work: CONCUR 2005 – Concurrency Theory
cites work: The Effects of Bounding Syntactic Resources on Presburger LTL
cites work: LTL with the freeze quantifier and register automata
cites work: Q4415251
cites work: Q4322964
cites work: Many-dimensional modal logics: theory and applications
cites work: Q5715695
cites work: CONCUR 2003 - Concurrency Theory
cites work: Q4536378
cites work: PSpace Reasoning with the Description Logic ALCF(D)
cites work: Q5465445
cites work: NEXP TIME-complete description logics with concrete domains
cites work: Automated Reasoning with Analytic Tableaux and Related Methods
cites work: Introduction to constraint databases
cites work: The complexity of propositional linear temporal logics
cites work: Q4385530
cites work: Reasoning about infinite computations
cites work: Temporal logic can be more expressive
DOI: 10.1016/J.IC.2006.09.006
description: scientific article; zbMATH DE number 5133057