Linear-time temporal logics with Presburger constraints: an overview

We present an overview of linear-time temporal logics with Presburger constraints whose models are sequences of tuples of integers. Such formal specification languages are welldesigned to specify and verify systems that can be modelled with counter systems. The paper recalls the general framework of LTL over concrete domains and presents the main decidability and complexity results related to fragments of Presburger LTL. Related formalisms are also briefly presented. MOTS-CL

• Type: Journal
• Year: 2006
• Where: JANCL
• Authors: Stéphane Demri
• Keywords: JANCL 2006, Linear-time Temporal Logics, Presburger Constraints, Such Formal Specification