-
Computational Complexity of Standpoint LTL
Authors:
Stéphane Demri,
Przemysław Andrzej Wałęga
Abstract:
Standpoint linear temporal logic SLTL is a recent formalism able to model possibly conflicting commitments made by distinct agents, taking into account aspects of temporal reasoning. In this paper, we analyse the computational properties of SLTL. First, we establish logarithmic-space reductions between the satisfiability problems for the multi-dimensional modal logic PTLxS5 and SLTL. This leads to…
▽ More
Standpoint linear temporal logic SLTL is a recent formalism able to model possibly conflicting commitments made by distinct agents, taking into account aspects of temporal reasoning. In this paper, we analyse the computational properties of SLTL. First, we establish logarithmic-space reductions between the satisfiability problems for the multi-dimensional modal logic PTLxS5 and SLTL. This leads to the EXPSPACE-completeness of the satisfiability problem in SLTL, which is a surprising result in view of previous investigations. Next, we present a method of restricting SLTL so that the obtained fragment is a strict extension of both the (non-temporal) standpoint logic and linear-time temporal logic LTL, but the satisfiability problem is PSPACE-complete in this fragment. Thus, we show how to combine standpoint logic with LTL so that the worst-case complexity of the obtained combination is not higher than of pure LTL.
△ Less
Submitted 16 August, 2024;
originally announced August 2024.
-
Constraint Automata on Infinite Data Trees: From CTL(Z)/CTL*(Z) To Decision Procedures
Authors:
Stephane Demri,
Karin Quaas
Abstract:
We introduce the class of tree constraint automata with data values in Z (equipped with the less than relation and equality predicates to constants) and we show that the nonemptiness problem is ExpTime-complete. Using an automata-based approach, we establish that the satisfiability problem for CTL(Z) (CTL with constraints in Z) is ExpTime-complete and the satisfiability problem for CTL*(Z) is 2Exp…
▽ More
We introduce the class of tree constraint automata with data values in Z (equipped with the less than relation and equality predicates to constants) and we show that the nonemptiness problem is ExpTime-complete. Using an automata-based approach, we establish that the satisfiability problem for CTL(Z) (CTL with constraints in Z) is ExpTime-complete and the satisfiability problem for CTL*(Z) is 2ExpTime-complete solving a longstanding open problem (only decidability was known so far). By-product results with other concrete domains and other logics, such as description logics with concrete domains, are also briefly presented.
△ Less
Submitted 18 June, 2025; v1 submitted 10 February, 2023;
originally announced February 2023.
-
Why Does Propositional Quantification Make Modal and Temporal Logics on Trees Robustly Hard?
Authors:
Bartosz Bednarczyk,
Stéphane Demri
Abstract:
Adding propositional quantification to the modal logics K, T or S4 is known to lead to undecidability but CTL with propositional quantification under the tree semantics (tQCTL) admits a non-elementary Tower-complete satisfiability problem. We investigate the complexity of strict fragments of tQCTL as well as of the modal logic K with propositional quantification under the tree semantics. More spec…
▽ More
Adding propositional quantification to the modal logics K, T or S4 is known to lead to undecidability but CTL with propositional quantification under the tree semantics (tQCTL) admits a non-elementary Tower-complete satisfiability problem. We investigate the complexity of strict fragments of tQCTL as well as of the modal logic K with propositional quantification under the tree semantics. More specifically, we show that tQCTL restricted to the temporal operator EX is already Tower-hard, which is unexpected as EX can only enforce local properties. When tQCTL restricted to EX is interpreted on N-bounded trees for some N >= 2, we prove that the satisfiability problem is AExpPol-complete; AExpPol-hardness is established by reduction from a recently introduced tiling problem, instrumental for studying the model-checking problem for interval temporal logics. As consequences of our proof method, we prove Tower-hardness of tQCTL restricted to EF or to EXEF and of the well-known modal logics such as K, KD, GL, K4 and S4 with propositional quantification under a semantics based on classes of trees.
△ Less
Submitted 4 August, 2022; v1 submitted 27 April, 2021;
originally announced April 2021.
-
Modal Logics with Composition on Finite Forests: Expressivity and Complexity (Extra Material)
Authors:
Bartosz Bednarczyk,
Stéphane Demri,
Raul Fervari,
Alessio Mansutti
Abstract:
We investigate the expressivity and computational complexity of two modal logics on finite forests equipped with operators to reason on submodels. The logic ML(|) extends the basic modal logic ML with the composition operator | from static ambient logic, whereas ML(*) contains the separating conjunction * from separation logic. Though both operators are second-order in nature, we show that ML(|) i…
▽ More
We investigate the expressivity and computational complexity of two modal logics on finite forests equipped with operators to reason on submodels. The logic ML(|) extends the basic modal logic ML with the composition operator | from static ambient logic, whereas ML(*) contains the separating conjunction * from separation logic. Though both operators are second-order in nature, we show that ML(|) is as expressive as the graded modal logic GML (on finite trees) whereas ML(*) lies strictly between ML and GML. Moreover, we establish that the satisfiability problem for ML(*) is Tower-complete, whereas for ML(|) is (only) AExpPol-complete. As a by-product, we solve several open problems related to sister logics, such as static ambient logic, modal separation logic, and second-order modal logic on finite trees.
△ Less
Submitted 16 July, 2020;
originally announced July 2020.
-
A Complete Axiomatisation for Quantifier-Free Separation Logic
Authors:
Stéphane Demri,
Étienne Lozes,
Alessio Mansutti
Abstract:
We present the first complete axiomatisation for quantifier-free separation logic. The logic is equipped with the standard concrete heaplet semantics and the proof system has no external feature such as nominals/labels. It is not possible to rely completely on proof systems for Boolean BI as the concrete semantics needs to be taken into account. Therefore, we present the first internal Hilbert-sty…
▽ More
We present the first complete axiomatisation for quantifier-free separation logic. The logic is equipped with the standard concrete heaplet semantics and the proof system has no external feature such as nominals/labels. It is not possible to rely completely on proof systems for Boolean BI as the concrete semantics needs to be taken into account. Therefore, we present the first internal Hilbert-style axiomatisation for quantifier-free separation logic. The calculus is divided in three parts: the axiomatisation of core formulae where Boolean combinations of core formulae capture the expressivity of the whole logic, axioms and inference rules to simulate a bottom-up elimination of separating connectives, and finally structural axioms and inference rules from propositional calculus and Boolean BI with the magic wand.
△ Less
Submitted 9 August, 2021; v1 submitted 9 June, 2020;
originally announced June 2020.
-
Internal Calculi for Separation Logics
Authors:
Stéphane Demri,
Etienne Lozes,
Alessio Mansutti
Abstract:
We present a general approach to axiomatise separation logics with heaplet semantics with no external features such as nominals/labels. To start with, we design the first (internal) Hilbert-style axiomatisation for the quantifier-free separation logic. We instantiate the method by introducing a new separation logic with essential features: it is equipped with the separating conjunction, the predic…
▽ More
We present a general approach to axiomatise separation logics with heaplet semantics with no external features such as nominals/labels. To start with, we design the first (internal) Hilbert-style axiomatisation for the quantifier-free separation logic. We instantiate the method by introducing a new separation logic with essential features: it is equipped with the separating conjunction, the predicate ls, and a natural guarded form of first-order quantification. We apply our approach for its axiomatisation. As a by-product of our method, we also establish the exact expressive power of this new logic and we show PSpace-completeness of its satisfiability problem.
△ Less
Submitted 11 October, 2019;
originally announced October 2019.
-
The Effects of Adding Reachability Predicates in Quantifier-Free Separation Logic
Authors:
Stéphane Demri,
Etienne Lozes,
Alessio Mansutti
Abstract:
The list segment predicate ls used in separation logic for verifying programs with pointers is well-suited to express properties on singly-linked lists. We study the effects of adding ls to the full quantifier-free separation logic with the separating conjunction and implication, which is motivated by the recent design of new fragments in which all these ingredients are used indifferently and veri…
▽ More
The list segment predicate ls used in separation logic for verifying programs with pointers is well-suited to express properties on singly-linked lists. We study the effects of adding ls to the full quantifier-free separation logic with the separating conjunction and implication, which is motivated by the recent design of new fragments in which all these ingredients are used indifferently and verification tools start to handle the magic wand connective. This is a very natural extension that has not been studied so far. We show that the restriction without the separating implication can be solved in polynomial space by using an appropriate abstraction for memory states whereas the full extension is shown undecidable by reduction from first-order separation logic. Many variants of the logic and fragments are also investigated from the computational point of view when ls is added, providing numerous results about adding reachability predicates to quantifier-free separation logic.
△ Less
Submitted 28 February, 2021; v1 submitted 12 October, 2018;
originally announced October 2018.
-
Reasoning about Data Repetitions with Counter Systems
Authors:
Stephane Demri,
Diego Figueira,
M Praveen
Abstract:
We study linear-time temporal logics interpreted over data words with multiple attributes. We restrict the atomic formulas to equalities of attribute values in successive positions and to repetitions of attribute values in the future or past. We demonstrate correspondences between satisfiability problems for logics and reachability-like decision problems for counter systems. We show that allowing/…
▽ More
We study linear-time temporal logics interpreted over data words with multiple attributes. We restrict the atomic formulas to equalities of attribute values in successive positions and to repetitions of attribute values in the future or past. We demonstrate correspondences between satisfiability problems for logics and reachability-like decision problems for counter systems. We show that allowing/disallowing atomic formulas expressing repetitions of values in the past corresponds to the reachability/coverability problem in Petri nets. This gives us 2EXPSPACE upper bounds for several satisfiability problems. We prove matching lower bounds by reduction from a reachability problem for a newly introduced class of counter systems. This new class is a succinct version of vector addition systems with states in which counters are accessed via pointers, a potentially useful feature in other contexts. We strengthen further the correspondences between data logics and counter systems by characterizing the complexity of fragments, extensions and variants of the logic. For instance, we precisely characterize the relationship between the number of attributes allowed in the logic and the number of counters needed in the counter system.
△ Less
Submitted 29 July, 2016; v1 submitted 11 April, 2016;
originally announced April 2016.
-
On the Complexity of Verifying Regular Properties on Flat Counter Systems
Authors:
Stéphane Demri,
Amit Kumar Dhar,
Arnaud Sangnier
Abstract:
Among the approximation methods for the verification of counter systems, one of them consists in model-checking their flat unfoldings. Unfortunately, the complexity characterization of model-checking problems for such operational models is not always well studied except for reachability queries or for Past LTL. In this paper, we characterize the complexity of model-checking problems on flat counte…
▽ More
Among the approximation methods for the verification of counter systems, one of them consists in model-checking their flat unfoldings. Unfortunately, the complexity characterization of model-checking problems for such operational models is not always well studied except for reachability queries or for Past LTL. In this paper, we characterize the complexity of model-checking problems on flat counter systems for the specification languages including first-order logic, linear mu-calculus, infinite automata, and related formalisms. Our results span different complexity classes (mainly from PTime to PSpace) and they apply to languages in which arithmetical constraints on counter values are systematically allowed. As far as the proof techniques are concerned, we provide a uniform approach that focuses on the main issues.
△ Less
Submitted 23 April, 2013;
originally announced April 2013.
-
A Note on the Complexity of Model-Checking Bounded Multi-Pushdown Systems
Authors:
Kshitij Bansal,
Stéphane Demri
Abstract:
In this note, we provide complexity characterizations of model checking multi-pushdown systems. Multi-pushdown systems model recursive concurrent programs in which any sequential process has a finite control. We consider three standard notions for boundedness: context boundedness, phase boundedness and stack ordering. The logical formalism is a linear-time temporal logic extending well-known logic…
▽ More
In this note, we provide complexity characterizations of model checking multi-pushdown systems. Multi-pushdown systems model recursive concurrent programs in which any sequential process has a finite control. We consider three standard notions for boundedness: context boundedness, phase boundedness and stack ordering. The logical formalism is a linear-time temporal logic extending well-known logic CaRet but dedicated to multi-pushdown systems in which abstract operators (related to calls and returns) such as those for next-time and until are parameterized by stacks. We show that the problem is EXPTIME-complete for context-bounded runs and unary encoding of the number of context switches; we also prove that the problem is 2EXPTIME-complete for phase-bounded runs and unary encoding of the number of phase switches. In both cases, the value k is given as an input (whence it is not a constant of the model-checking problem), which makes a substantial difference in the complexity. In certain cases, our results improve previous complexity results.
△ Less
Submitted 6 December, 2012;
originally announced December 2012.
-
Petri Net Reachability Graphs: Decidability Status of First Order Properties
Authors:
Philippe Darondeau,
Stephane Demri,
Roland Meyer,
Christophe Morvan
Abstract:
We investigate the decidability and complexity status of model-checking problems on unlabelled reachability graphs of Petri nets by considering first-order and modal languages without labels on transitions or atomic propositions on markings. We consider several parameters to separate decidable problems from undecidable ones. Not only are we able to provide precise borders and a systematic analysis…
▽ More
We investigate the decidability and complexity status of model-checking problems on unlabelled reachability graphs of Petri nets by considering first-order and modal languages without labels on transitions or atomic propositions on markings. We consider several parameters to separate decidable problems from undecidable ones. Not only are we able to provide precise borders and a systematic analysis, but we also demonstrate the robustness of our proof techniques.
△ Less
Submitted 19 October, 2012; v1 submitted 10 October, 2012;
originally announced October 2012.
-
Taming Past LTL and Flat Counter Systems
Authors:
Stéphane Demri,
Amit Kumar Dhar,
Arnaud sangnier
Abstract:
Reachability and LTL model-checking problems for flat counter systems are known to be decidable but whereas the reachability problem can be shown in NP, the best known complexity upper bound for the latter problem is made of a tower of several exponentials. Herein, we show that the problem is only NP-complete even if LTL admits past-time operators and arithmetical constraints on counters. Actually…
▽ More
Reachability and LTL model-checking problems for flat counter systems are known to be decidable but whereas the reachability problem can be shown in NP, the best known complexity upper bound for the latter problem is made of a tower of several exponentials. Herein, we show that the problem is only NP-complete even if LTL admits past-time operators and arithmetical constraints on counters. Actually, the NP upper bound is shown by adequately combining a new stuttering theorem for Past LTL and the property of small integer solutions for quantifier-free Presburger formulae. Other complexity results are proved, for instance for restricted classes of flat counter systems.
△ Less
Submitted 8 February, 2013; v1 submitted 30 May, 2012;
originally announced May 2012.
-
On Selective Unboundedness of VASS
Authors:
Stéphane Demri
Abstract:
Numerous properties of vector addition systems with states amount to checking the (un)boundedness of some selective feature (e.g., number of reversals, run length). Some of these features can be checked in exponential space by using Rackoff's proof or its variants, combined with Savitch's theorem. However, the question is still open for many others, e.g., reversal-boundedness. In the paper, we int…
▽ More
Numerous properties of vector addition systems with states amount to checking the (un)boundedness of some selective feature (e.g., number of reversals, run length). Some of these features can be checked in exponential space by using Rackoff's proof or its variants, combined with Savitch's theorem. However, the question is still open for many others, e.g., reversal-boundedness. In the paper, we introduce the class of generalized unboundedness properties that can be verified in exponential space by extending Rackoff's technique, sometimes in an unorthodox way. We obtain new optimal upper bounds, for example for place-boundedness problem, reversal-boundedness detection (several variants exist), strong promptness detection problem and regularity detection. Our analysis is sufficiently refined so as we also obtain a polynomial-space bound when the dimension is fixed.
△ Less
Submitted 31 October, 2010;
originally announced November 2010.
-
The complexity of linear-time temporal logic over the class of ordinals
Authors:
Stephane Demri,
Alexander Rabinovich
Abstract:
We consider the temporal logic with since and until modalities. This temporal logic is expressively equivalent over the class of ordinals to first-order logic by Kamp's theorem. We show that it has a PSPACE-complete satisfiability problem over the class of ordinals. Among the consequences of our proof, we show that given the code of some countable ordinal alpha and a formula, we can decide in PSP…
▽ More
We consider the temporal logic with since and until modalities. This temporal logic is expressively equivalent over the class of ordinals to first-order logic by Kamp's theorem. We show that it has a PSPACE-complete satisfiability problem over the class of ordinals. Among the consequences of our proof, we show that given the code of some countable ordinal alpha and a formula, we can decide in PSPACE whether the formula has a model over alpha. In order to show these results, we introduce a class of simple ordinal automata, as expressive as Büchi ordinal automata. The PSPACE upper bound for the satisfiability problem of the temporal logic is obtained through a reduction to the nonemptiness problem for the simple ordinal automata.
△ Less
Submitted 21 December, 2010; v1 submitted 27 September, 2010;
originally announced September 2010.
-
Model checking memoryful linear-time logics over one-counter automata
Authors:
Stephane Demri,
Ranko Lazic,
Arnaud Sangnier
Abstract:
We study complexity of the model-checking problems for LTL with registers (also known as freeze LTL) and for first-order logic with data equality tests over one-counter automata. We consider several classes of one-counter automata (mainly deterministic vs. nondeterministic) and several logical fragments (restriction on the number of registers or variables and on the use of propositional variable…
▽ More
We study complexity of the model-checking problems for LTL with registers (also known as freeze LTL) and for first-order logic with data equality tests over one-counter automata. We consider several classes of one-counter automata (mainly deterministic vs. nondeterministic) and several logical fragments (restriction on the number of registers or variables and on the use of propositional variables for control locations). The logics have the ability to store a counter value and to test it later against the current counter value. We show that model checking over deterministic one-counter automata is PSPACE-complete with infinite and finite accepting runs. By constrast, we prove that model checking freeze LTL in which the until operator is restricted to the eventually operator over nondeterministic one-counter automata is undecidable even if only one register is used and with no propositional variable. As a corollary of our proof, this also holds for first-order logic with data equality tests restricted to two variables. This makes a difference with the facts that several verification problems for one-counter automata are known to be decidable with relatively low complexity, and that finitary satisfiability for the two logics are decidable. Our results pave the way for model-checking memoryful (linear-time) logics over other classes of operational models, such as reversal-bounded counter machines.
△ Less
Submitted 18 January, 2010; v1 submitted 30 October, 2008;
originally announced October 2008.
-
LTL with the Freeze Quantifier and Register Automata
Authors:
Stephane Demri,
Ranko Lazic
Abstract:
A data word is a sequence of pairs of a letter from a finite alphabet and an element from an infinite set, where the latter can only be compared for equality. To reason about data words, linear temporal logic is extended by the freeze quantifier, which stores the element at the current word position into a register, for equality comparisons deeper in the formula. By translations from the logic t…
▽ More
A data word is a sequence of pairs of a letter from a finite alphabet and an element from an infinite set, where the latter can only be compared for equality. To reason about data words, linear temporal logic is extended by the freeze quantifier, which stores the element at the current word position into a register, for equality comparisons deeper in the formula. By translations from the logic to alternating automata with registers and then to faulty counter automata whose counters may erroneously increase at any time, and from faulty and error-free counter automata to the logic, we obtain a complete complexity table for logical fragments defined by varying the set of temporal operators and the number of registers. In particular, the logic with future-time operators and 1 register is decidable but not primitive recursive over finite data words. Adding past-time operators or 1 more register, or switching to infinite data words, cause undecidability.
△ Less
Submitted 3 April, 2008; v1 submitted 5 October, 2006;
originally announced October 2006.
-
On the freeze quantifier in Constraint LTL: decidability and complexity
Authors:
Stéphane Demri,
Ranko Lazic,
David Nowak
Abstract:
Constraint LTL, a generalisation of LTL over Presburger constraints, is often used as a formal language to specify the behavior of operational models with constraints. The freeze quantifier can be part of the language, as in some real-time logics, but this variable-binding mechanism is quite general and ubiquitous in many logical languages (first-order temporal logics, hybrid logics, logics for…
▽ More
Constraint LTL, a generalisation of LTL over Presburger constraints, is often used as a formal language to specify the behavior of operational models with constraints. The freeze quantifier can be part of the language, as in some real-time logics, but this variable-binding mechanism is quite general and ubiquitous in many logical languages (first-order temporal logics, hybrid logics, logics for sequence diagrams, navigation logics, logics with lambda-abstraction etc.). We show that Constraint LTL over the simple domain (N,=) augmented with the freeze quantifier is undecidable which is a surprising result in view of the poor language for constraints (only equality tests). Many versions of freeze-free Constraint LTL are decidable over domains with qualitative predicates and our undecidability result actually establishes Sigma_1^1-completeness. On the positive side, we provide complexity results when the domain is finite (EXPSPACE-completeness) or when the formulae are flat in a sense introduced in the paper. Our undecidability results are sharp (i.e. with restrictions on the number of variables) and all our complexity characterisations ensure completeness with respect to some complexity class (mainly PSPACE and EXPSPACE).
△ Less
Submitted 29 September, 2006; v1 submitted 4 September, 2006;
originally announced September 2006.
-
Reasoning about transfinite sequences
Authors:
Stéphane Demri,
David Nowak
Abstract:
We introduce a family of temporal logics to specify the behavior of systems with Zeno behaviors. We extend linear-time temporal logic LTL to authorize models admitting Zeno sequences of actions and quantitative temporal operators indexed by ordinals replace the standard next-time and until future-time operators. Our aim is to control such systems by designing controllers that safely work on $ω$-…
▽ More
We introduce a family of temporal logics to specify the behavior of systems with Zeno behaviors. We extend linear-time temporal logic LTL to authorize models admitting Zeno sequences of actions and quantitative temporal operators indexed by ordinals replace the standard next-time and until future-time operators. Our aim is to control such systems by designing controllers that safely work on $ω$-sequences but interact synchronously with the system in order to restrict their behaviors. We show that the satisfiability problem for the logics working on $ω^k$-sequences is EXPSPACE-complete when the integers are represented in binary, and PSPACE-complete with a unary representation. To do so, we substantially extend standard results about LTL by introducing a new class of succinct ordinal automata that can encode the interaction between the different quantitative temporal operators.
△ Less
Submitted 16 August, 2006; v1 submitted 26 May, 2005;
originally announced May 2005.
-
Deciding regular grammar logics with converse through first-order logic
Authors:
Stephane Demri,
Hans de Nivelle
Abstract:
We provide a simple translation of the satisfiability problem for regular grammar logics with converse into GF2, which is the intersection of the guarded fragment and the 2-variable fragment of first-order logic. This translation is theoretically interesting because it translates modal logics with certain frame conditions into first-order logic, without explicitly expressing the frame conditions…
▽ More
We provide a simple translation of the satisfiability problem for regular grammar logics with converse into GF2, which is the intersection of the guarded fragment and the 2-variable fragment of first-order logic. This translation is theoretically interesting because it translates modal logics with certain frame conditions into first-order logic, without explicitly expressing the frame conditions.
A consequence of the translation is that the general satisfiability problem for regular grammar logics with converse is in EXPTIME. This extends a previous result of the first author for grammar logics without converse. Using the same method, we show how some other modal logics can be naturally translated into GF2, including nominal tense logics and intuitionistic logic.
In our view, the results in this paper show that the natural first-order fragment corresponding to regular grammar logics is simply GF2 without extra machinery such as fixed point-operators.
△ Less
Submitted 16 February, 2004; v1 submitted 20 June, 2003;
originally announced June 2003.
