Author name cluster

Stéphane Demri

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

34 papers

2 author rows

CSL Conference 2026 Conference Paper

Robustness of Constraint Automata for Description Logics with Concrete Domains

Stéphane Demri
Tianwen Gu

Decidability or complexity issues about the consistency problem for description logics with concrete domains have already been analysed with tableaux-based or type elimination methods. Concrete domains in ontologies are essential to consider concrete objects and predefined relations. In this work, we expose an automata-based approach leading to the optimal upper bound ExpTime, that is designed by enriching the transitions with symbolic constraints. We show that the nonemptiness problem for such automata belongs to ExpTime if the concrete domains satisfy a few simple properties. Then, we provide a reduction from the consistency problem for ontologies, yielding ExpTime-membership. Thanks to the expressivity of constraint automata, the results are extended to additional ingredients such as inverse roles, functional role names and constraint assertions, while maintaining ExpTime-membership, which illustrates the robustness of the approach.

KR Conference 2025 Conference Paper

On the Effects of Adding Assignments in Linear-Time Temporal Logics Modulo Theories

Stéphane Demri
Raul Fervari

We introduce linear-time temporal logics with past operators featuring a simple assignment modality that performs local changes on the models. Such structures are infinite sequences of valuations interpreting variables by elements from a possibly infinite data domain. We study several fragments as well as the case with the Boolean domain, for which we establish that it is actually as expressive as first-order logic over infinite sequences of propositional valuations. For the logics over concrete domains N, Z and Q equipped with the respective linear ordering and equality tests, we show the satisfiability problem is decidable, and that the logics are as expressive as the version without the assignment operator. Interestingly, this entails such assignments provide a huge concise ness, which is then helpful for succinct specifications.

PDF Details DOI

ECAI Conference 2024 Conference Paper

Computational Complexity of Standpoint LTL

Stéphane Demri
Przemyslaw Andrzej Walega

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 PTL×S5 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.

JELIA Conference 2023 Conference Paper

First Steps Towards Taming Description Logics with Strings

Stéphane Demri
Karin Quaas

Abstract We consider the description logic \(\mathcal {A}\mathcal {L}\mathcal {C}\mathcal {F}^{\mathcal {P}}(\mathcal {D}_{\varSigma })\) over the concrete domain \(\mathcal {D}_{\varSigma } = (\varSigma ^*, \prec, =, (=_{\mathfrak {w}})_{\mathfrak {w}\in \varSigma ^*})\), where \(\prec \) is the strict prefix order over finite strings in \(\varSigma ^*\). Using an automata-based approach, we show that the concept satisfiability problem w. r. t. general TBoxes for \(\mathcal {A}\mathcal {L}\mathcal {C}\mathcal {F}^{\mathcal {P}}(\mathcal {D}_{\varSigma })\) is ExpTime -complete for all finite alphabets \(\varSigma \). As far as we know, this is the first complexity result for an expressive description logic with a nontrivial concrete domain on strings.

KR Conference 2023 Conference Paper

How to Manage a Budget with ATL+

Stéphane Demri
Raine Rönnholm

We study the alternating-time temporal logic ATL+ enriched with one resource (written ATL+(1)) extending ATL+ with the possibility to manage a budget. We propose a game-theoretic semantics via the introduction of two evaluation games so that the compositional semantics is captured by strategies in the games. We show that the model-checking problem for ATL+(1) is in PSpace and we identify several non-trivial fragments that can be solved in PTime. By-products of our investigations include also a simplified Pspace decision procedure for resource-free ATL+, an effective way to synthesize constraints in a version of ATL+(1) with parameters and a PSpace bound to solve an energy game with one counter whose objectives are LTL formulae of temporal depth one.

PDF Details DOI

AAAI Conference 2023 Conference Paper

Model-Checking for Ability-Based Logics with Constrained Plans

Stéphane Demri
Raul Fervari

We investigate the complexity of the model-checking problem for a family of modal logics capturing the notion of “knowing how”. We consider the most standard ability-based knowing how logic, for which we show that model-checking is PSpace-complete. By contrast, a multi-agent variant based on an uncertainty relation between plans in which uncertainty is encoded by a regular language, is shown to admit a PTime model-checking problem. We extend with budgets the above-mentioned ability-logics, as done for ATL-like logics. We show that for the former logic enriched with budgets, the complexity increases to at least ExpSpace-hardness, whereas for the latter, the PTime bound is preserved. Other variant logics are discussed along the paper.

PDF Details DOI

AIJ Journal 2021 Journal Article

Strategic reasoning with a bounded number of resources: The quest for tractability

Francesco Belardinelli
Stéphane Demri

The resource-bounded alternating-time temporal logic RB±ATL combines strategic reasoning with reasoning about resources. Its model-checking problem is known to be 2exptime-complete (the same as its proper extension RB±ATL ⁎) and fragments have been identified to lower the complexity. In this work, we consider the variant RB±ATL + that allows for Boolean combinations of path formulae starting with single temporal operators, but restricted to a single resource, providing an interesting trade-off between temporal expressivity and resource analysis. We show that the model-checking problem for RB±ATL + restricted to a single agent and a single resource is Δ 2 P -complete, hence the same as for the standard branching-time temporal logic CTL +. In this case reasoning about resources comes at no extra computational cost. When a fixed finite set of linear-time temporal operators is considered, the model-checking problem drops to ptime, which includes the special case of RB±ATL restricted to a single agent and a single resource. Furthermore, we show that, with an arbitrary number of agents and a fixed number of resources, the model-checking problem for RB±ATL + can be solved in exptime using a sophisticated Turing reduction to the parity game problem for alternating vector addition systems with states (AVASS).

CSL Conference 2020 Conference Paper

Internal Calculi for Separation Logics

Stéphane Demri
Étienne Lozes
Alessio Mansutti

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 SL(∗, -*). 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.

Highlights Conference 2020 Conference Abstract

Modal Logics for Updating, Sharing or Composing

Stéphane Demri

Non-classical logics having a syntactical mechanism to update models are ubiquitous and include dynamic logics, separation logics or ambient logics to quote a few of them. More specifically, modal logics for updating models have been quite studied, see e. g. second-order modal logics, and more recently logics of public announcements, sabotage modal logics and modal separation logics. In this talk, recent developments on modal logics with built-in update mechanisms based on composition are presented as well as their relationships with other logical formalisms. Recent results about decidability status, computational complexity and expressive power are presented. Part of the talk is based on joint works with B. Bednarczyk, M. Deters, R. Fervari and A. Mansutti.

AAAI Conference 2020 Conference Paper

Parameterised Resource-Bounded ATL

Natasha Alechina
Stéphane Demri
Brian Logan

It is often advantageous to be able to extract resource requirements in resource logics of strategic ability, rather than to verify whether a ﬁxed resource requirement is sufﬁcient for achieving a goal. We study Parameterised Resource-Bounded Alternating Time Temporal Logic where parameter extraction is possible. We give a parameter extraction algorithm and prove that the model-checking problem is 2EXPTIMEcomplete.

ECAI Conference 2020 Conference Paper

Reasoning with a Bounded Number of Resources in ATL+

Francesco Belardinelli
Stéphane Demri

The resource-bounded alternating-time temporal logic RB±ATL combines strategic reasoning with reasoning about resources. Its model-checking problem is known to be 2EXPTIME-complete (the same as its proper extension RB±ATL*). Several fragments have been identified to lower the complexity. In this work, we consider the variant RB±ATL + which permits Boolean combinations of path formulae starting with single temporal operators, but restricted to a single resource, providing an interesting trade-off between temporal expressivity and resource analysis. We show that the model-checking problem for RB±ATL + restricted to a single agent and a single resource is Δ p 2 -complete, hence the same as for CTL +. In this case reasoning about resources comes at no extra computational cost. Furthermore, we show that, with an arbitrary number of agents and a fixed number of resources, the problem can be solved in EXPTIME using a Turing reduction to the parity game problem for alternating vector addition systems with states.

JELIA Conference 2019 Conference Paper

Axiomatising Logics with Separating Conjunction and Modalities

Stéphane Demri
Raul Fervari
Alessio Mansutti

Abstract Modal separation logics are formalisms that combine modal operators to reason locally, with separating connectives that allow to perform global updates on the models. In this work, we design Hilbert-style proof systems for the modal separation logics \(\text {MSL} ^{}(*, \langle \ne \rangle )\) and \(\text {MSL} ^{}(*, \Diamond )\), where \(*\) is the separating conjunction, \(\Diamond \) is the standard modal operator and \(\langle \ne \rangle \) is the difference modality. The calculi only use the logical languages at hand (no external features such as labels) and take advantage of new normal forms and of their axiomatisation.

AAMAS Conference 2019 Conference Paper

Resource-bounded ATL: the Quest for Tractable Fragments

Francesco Belardinelli
Stéphane Demri

Resource-aware logics to represent strategic abilities in multi-agent systems are notoriously hard to handle as they combine strategic reasoning with reasoning about resources. In this work, we begin by providing a general overview of the model-checking results currently available for the Resource-bounded Alternating-time Temporal Logic RB±ATL. This allows us to identify several open problems in the literature, as well as to establish relationships with RBTL-like logics, when RB±ATL is restricted to a single agent. Then, we tackle one such open problem that we deem highly significant: we show that model checking RB±ATL is ptime-complete when restricted to a single agent and a single resource. To do so, we make a valuable detour on vector addition systems with states, by proving new complexity results for their state-reachability and nontermination problems, when restricted to a single counter. Thus, reasoning about resources comes at no computational extra cost in the single-resource, single-agent case.

TCS Journal 2018 Journal Article

Equivalence between model-checking flat counter systems and Presburger arithmetic

Stéphane Demri
Amit Kumar Dhar
Arnaud Sangnier

We show that model-checking flat counter systems with the branching-time temporal logic CTL* extended with arithmetical constraints on counter values has the same worst-case complexity as the satisfiability problem for Presburger arithmetic. The lower bound already holds with strong restrictions: the logical language uses only the temporal operator EF and no arithmetical constraints, and the guards on the transitions are made of linear constraints. This work complements our understanding of model-checking flat counter systems with linear-time temporal logics, such as LTL, for which the problem is already known to be (only) NP-complete with guards restricted to the linear fragment.

TIME Conference 2018 Conference Paper

On Temporal and Separation Logics (Invited Paper)

Stéphane Demri

There exist many success stories about the introduction of logics designed for the formal verification of computer systems. Obviously, the introduction of temporal logics to computer science has been a major step in the development of model-checking techniques. More recently, separation logics extend Hoare logic for reasoning about programs with dynamic data structures, leading to many contributions on theory, tools and applications. In this talk, we illustrate how several features of separation logics, for instance the key concept of separation, are related to similar notions in temporal logics. We provide formal correspondences (when possible) and present an overview of related works from the literature. This is also the opportunity to present bridges between well-known temporal logics and more recent separation logics.

I&C Journal 2015 Journal Article

Taming past LTL and flat counter systems

Stéphane Demri
Amit Kumar Dhar
Arnaud Sangnier

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 this problem is only NP-complete even if LTL admits past-time operators and arithmetical constraints on counters. As far as past-time operators are concerned, their addition to LTL immediately leads to complications and hence an NP upper bound cannot be deduced by translating formulae into LTL and studying the problem only for this latter logic. We also provide other complexity results obtained by restricting further the class of flat counter systems.

Highlights Conference 2013 Conference Abstract

Reasoning about data repetitions with counter systems

Stéphane Demri
Diego Figueira
M. Praveen

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 poten- tially 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.

I&C Journal 2012 Journal Article

On the almighty wand

Rémi Brochenin
Stéphane Demri
Etienne Lozes

We investigate decidability, complexity and expressive power issues for (first-order) separation logic with one record field (herein called SL) and its fragments. SL can specify properties about the memory heap of programs with singly-linked lists. Separation logic with two record fields is known to be undecidable by reduction of finite satisfiability for classical predicate logic with one binary relation. Surprisingly, we show that second-order logic is as expressive as SL and as a by-product we get undecidability of SL. This is refined by showing that SL without the separating conjunction is as expressive as SL, whence undecidable too. As a consequence, in SL the separating implication (also known as the magic wand) can simulate the separating conjunction. By contrast, we establish that SL without the magic wand is decidable, and we prove a non-elementary complexity by reduction from satisfiability for the first-order theory over finite words. This result is extended with a bounded use of the magic wand that appears in Hoare-style rules. As a generalization, it is shown that k SL, the separation logic over heaps with k ⩾ 1 record fields, is equivalent to k SO, the second-order logic over heaps with k record fields.

LOPSTR Conference 2011 Conference Paper

Automata-Based Computation of Temporal Equilibrium Models

Pedro Cabalar
Stéphane Demri

Abstract Temporal Equilibrium Logic (TEL) is a formalism for temporal logic programming that generalizes the paradigm of Answer Set Programming (ASP) introducing modal temporal operators from standard Linear-time Temporal Logic (LTL). In this paper we solve some problems that remained open for TEL like decidability, bounds for computational complexity as well as computation of temporal equilibrium models for arbitrary theories. We propose a method for the latter that consists in building a Büchi automaton that accepts exactly the temporal equilibrium models of a given theory, providing an automata-based decision procedure and illustrating the ω -regularity of such sets. We show that TEL satisfiability can be solved in exponential space and it is hard for polynomial space. Finally, given two theories, we provide a decision procedure to check if they have the same temporal equilibrium models.

JELIA Conference 2010 Invited Paper

Counter Systems for Data Logics

Stéphane Demri

Abstract Data logics are logical formalisms that are used to specify properties on structures equipped with data (data words, data trees, runs from counter systems, timed words, etc.). In this survey talk, we shall see how satisfiability problems for such data logics are related to reachability problems for counter systems (including counter automata with errors, vector addition systems with states, etc.). This is the opportunity to provide an overview about the relationships between data logics and verification problems for counter systems.

TCS Journal 2010 Journal Article

Model checking memoryful linear-time logics over one-counter automata

Stéphane Demri
Ranko Lazić
Arnaud Sangnier

We study complexity of the model-checking problems for LTL with registers (also known as freeze LTL and written LTL ↓ ) and for first-order logic with data equality tests (written FO ( ∼, <, + 1 ) ) 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 states). 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 LTL ↓ and FO ( ∼, <, + 1 ) over deterministic one-counter automata is PSpace-complete with infinite and finite accepting runs. By contrast, we prove that model checking LTL ↓ in which the until operator U is restricted to the eventually F over nondeterministic one-counter automata is Σ 1 1 -complete [resp. Σ 1 0 -complete] in the infinitary [resp. finitary] case even if only one register is used and with no propositional variable. As a corollary of our proof, this also holds for FO ( ∼, <, + 1 ) restricted to two variables (written FO 2 ( ∼, <, + 1 ) ). This makes a difference with respect to the facts that several verification problems for one-counter automata are known to be decidable with relatively low complexity, and that finitary satisfiability problems for LTL ↓ and FO 2 ( ∼, <, + 1 ) 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.

CSL Conference 2008 Conference Paper

On the Almighty Wand

Rémi Brochenin
Stéphane Demri
Étienne Lozes

Abstract We investigate decidability, complexity and expressive power issues for (first-order) separation logic with one record field (herein called SL ) and its fragments. SL can specify properties about the memory heap of programs with singly-linked lists. Separation logic with two record fields is known to be undecidable by reduction of finite satisfiability for classical predicate logic with one binary relation. Surprisingly, we show that second-order logic is as expressive as SL and as a by-product we get undecidability of SL. This is refined by showing that SL without the separating conjunction is as expressive as SL, whence undecidable too. As a consequence of this deep result, in SL the magic wand can simulate the separating conjunction. By contrast, we establish that SL without the magic wand is decidable with non-elementary complexity by reduction from satisfiability for the first-order theory over finite words. Equivalence between second-order logic and separation logic extends to the case with more than one selector.

TCS Journal 2008 Journal Article

Verification of qualitative Z constraints

Stéphane Demri
Régis Gascon

We introduce an LTL-like logic with atomic formulae built over a constraint language interpreting variables in Z. The constraint language includes periodicity constraints and comparison constraints of the form x = y and x < y; it is closed under Boolean operations and admits a restricted form of existential quantification. Such constraints are used, for instance, in calendar formalisms or abstractions of counter automata by using congruences modulo some power of two. Indeed, various programming languages perform arithmetic operators modulo some integer. We show that the satisfiability and model-checking problems (with respect to an appropriate class of constraint automata) for this logic are decidable in polynomial space improving significantly known results about its strict fragments. This is the largest set of qualitative constraints over Z known so far, shown to admit a decidable LTL extension.

I&C Journal 2007 Journal Article

An automata-theoretic approach to constraint LTL

Stéphane Demri
Deepak D’Souza

We consider an extension of linear-time temporal logic (LTL) with constraints interpreted over a concrete domain. We use a new automata-theoretic technique to show PSPACE decidability of the logic for the constraint systems ( Z, <, = ) and ( N, <, = ). Along the way, we give an automata-theoretic proof of a result of Balbiani and Condotta when the constraint system satisfies the completion property. Our decision procedures extend easily to handle extensions of the logic with past-time operators and constants, as well as an extension of the temporal language itself to monadic second order logic. Finally we show that the logic becomes undecidable when one considers constraint systems that allow a counting mechanism.

I&C Journal 2007 Journal Article

On the freeze quantifier in Constraint LTL: Decidability and complexity

Stéphane Demri
Ranko Lazić
David Nowak

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 λ-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 Σ 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).

LPAR Conference 2007 Conference Paper

The Complexity of Temporal Logic with Until and Since over Ordinals

Stéphane 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 thanks to 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 ordinal α and a formula, we can decide in pspace whether the formula has a model over ordinal α. 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.

TIME Conference 2007 Conference Paper

The Effects of Bounding Syntactic Resources on Presburger LTL

Stéphane Demri
Régis Gascon

We study decidability and complexity issues for fragments of LTL with Presburger constraints by restricting the syntactic resources of the formulae (the class of constraints, the number of variables and the distance between two states for which counters can be compared) while preserving the strength of the logical operators. We provide a complete picture refining known results from the literature, in some cases pushing forward the known decidability limits. By way of example, we show that model-checking formulae from LTL with quantifier-free Presburger arithmetic over one-counter automata is only PSPACE-complete. In order to establish the PSPACE upper bound, we show that the nonemptiness problem for Buchi one-counter automata taking values in Z and allowing zero tests and sign tests, is only NLOGSPACE-complete.

TCS Journal 2006 Journal Article

LTL over integer periodicity constraints

Stéphane Demri

Periodicity constraints are used in many logical formalisms, in fragments of Presburger LTL, in calendar logics, and in logics for access control, to quote a few examples. In the paper, we introduce the logic PLTL mod, an extension of Linear-Time Temporal Logic LTL with past-time operators whose atomic formulae are defined from a first-order constraint language dealing with periodicity. Although the underlying constraint language is a fragment of Presburger arithmetic shown to admit a PSPACE-complete satisfiability problem, we establish that PLTL mod model-checking and satisfiability problems remain in PSPACE as plain LTL (full Presburger LTL is known to be highly undecidable). This is particularly interesting for dealing with periodicity constraints since the language of PLTL mod has a language more concise than existing languages and the temporalization of our first-order language of periodicity constraints has the same worst case complexity as the underlying constraint language. Finally, we show examples of introduction the quantification in the logical language that provide to PLTL mod, EXPSPACE-complete problems. As another application, we establish that the equivalence problem for extended single-string automata, known to express the equality of time granularities, is PSPACE-complete by designing a reduction from QBF and by using our results for PLTL mod.

TIME Conference 2005 Conference Paper

On the Freeze Quantifier in Constraint LTL: Decidability and Complexity

Stéphane Demri
Ranko Lazic 0001
David Nowak

Constraint LTL, a generalization 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, etc.). We show that Constraint LTL over the simple domain augmented with the freeze operator is undecidable which is a surprising result regarding 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 /spl Sigma//sub 1//sup 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.

TCS Journal 2003 Journal Article

A polynomial space construction of tree-like models for logics with local chains of modal connectives

Stéphane Demri

The LA-logics (“logics with Local Agreement”) are polymodal logics defined semantically such that at any world of a model, the sets of successors for the different accessibility relations can be linearly ordered and the accessibility relations are equivalence relations. In a previous work, we have shown that every LA-logic defined with a finite set of modal indices has an NP-complete satisfiability problem. In this paper, we introduce a class of LA-logics with a countably infinite set of modal indices and we show that the satisfiability problem is PSPACE-complete for every logic of such a class. The upper bound is shown by exhibiting a tree structure of the models. This allows us to establish a surprising correspondence between the modal depth of formulae and the number of occurrences of distinct modal connectives. More importantly, as a consequence, we can show the PSPACE-completeness of Gargov's logic DALLA and Nakamura's logic LGM restricted to modal indices that are rational numbers, for which the computational complexity characterization has been open until now. These logics are known to belong to the class of information logics and fuzzy modal logics, respectively.

I&C Journal 2002 Journal Article

The Complexity of Propositional Linear Temporal Logics in Simple Cases

Stéphane Demri
Philippe Schnoebelen

It is well known that model checking and satisfiability for PLTL are PSPACE-complete. By contrast, very little is known about whether there exist some interesting fragments of PLTL with a lower worst-case complexity. Such results would help understand why PLTL model checkers are successfully used in practice. In this article we investigate this issue and consider model checking and satisfiability for all fragments of PLTL obtainable by restricting (1) the temporal connectives allowed, (2) the number of atomic propositions, and (3) the temporal height.

TCS Journal 1998 Journal Article

A class of decidable information logics

Stéphane Demri

For a class of propositional information logics defined from Pawlak's information systems, the validity problem is proved to be decidable using a significant variant of the standard filtration technique. Decidability is proved by showing that each logic has the strong finite model property and by bounding the size of the models. The logics in the scope of this paper are characterized by classes of Kripke-style structures with interdependent relations pairwise satisfying the Gargov's local agreement condition and closed under the so-called restriction operation. They include Gargov's data analysis logic with local agreement and Nakamura's logic of graded modalities. The last part of the paper is devoted to the definition of complete Hubert-style axiomatizations for subclasses of the introduced logics, thus providing evidence that such logics are subframe logics in Wolter's sense.

MFCS Conference 1996 Conference Paper

A Class of Information Logics with a Decidable Validity Problem

Stéphane Demri

Abstract For a class of prepositional information logics defined from Pawlak's information systems, the validity problem is proved to be decidable using a significant variant of the standard filtration technique. Actually the decidability is proved by showing that each logic has the strong finite model property and by bounding the size of the models. The logics in the scope of this paper are characterized by classes of Kripkestyle structures with interdependent equivalence relations and closed by the so-called restriction operation. They include Gargov's data analysis logic with local agreement and Nakamura's logic of graded modalities.

TCS Journal 1996 Journal Article

Logical analysis of demonic nondeterministic programs

Stéphane Demri
Ewa Orłowska

A logical framework is presented for representing and reasoning about nondeterministic programs that may not terminate. We propose a logic PDL(; ;, |, d(∗)) which is an extension of dynamic logic such that the program constructors related to demonic operations are introduced in its language. A complete and sound Hilbert-style proof system is given and it is shown that PDL(; ;, |, d(∗)) is decidable. In the second part of this paper, a translation is defined between PDL(; ;, |, d(∗)) and a relational logic. A sound and complete Rasiowa-Sikorski-style proof system for the relational logic is given. It provides a natural deduction-style method of reasoning for PDL(; ;, |, d(∗)).