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.

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.

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.

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.

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.

We introduce the class of tree constraint automata with data values in ℤ (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(ℤ) (CTL with constraints in ℤ) is EXPTIME-complete, and the satisfiability problem for CTL^*(ℤ) is 2ExpTime-complete (only decidability was known so far). By-product results with other concrete domains and other logics, are also briefly discussed.

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.

We study the expressivity and complexity of two modal logics interpreted on finite forests and equipped with standard modalities to reason on submodels. The logic \(\mathsf {ML} ({\color{black}{{\vert\!\!\vert\!\vert}}})\) extends the modal logic K with the composition operator \({\color{black}{{\vert\!\!\vert\!\vert}}}\) from ambient logic whereas \(\mathsf {ML} (\mathbin {\ast })\) features the separating conjunction \(\mathbin {\ast }\) from separation logic. Both operators are second-order in nature. We show that \(\mathsf {ML} ({\color{black}{{\vert\!\!\vert\!\vert}}})\) is as expressive as the graded modal logic \(\mathsf {GML}\) (on trees) whereas \(\mathsf {ML} (\mathbin {\ast })\) is strictly less expressive than \(\mathsf {GML}\) . Moreover, we establish that the satisfiability problem is Tower -complete for \(\mathsf {ML} (\mathbin {\ast })\) , whereas it is (only) AExp Pol -complete for \(\mathsf {ML} ({\color{black}{{\vert\!\!\vert\!\vert}}})\) , a result that is surprising given their relative expressivity. As by-products, we solve open problems related to sister logics such as static ambient logic and modal separation logic.

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.

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.

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}(\ast ,\langle \neq \rangle )$ and $\text {MSL}(\ast ,\Diamond )$, where $\ast $ is the separating conjunction, $\Diamond $ is the standard modal operator and $\langle \neq \rangle $ is the difference modality. The calculi only use the logical languages at hand (no external features such as labels) and can be divided in two main parts. First, normal forms for formulae are designed and the calculi allow to transform every formula into a formula in normal form. Second, another part of the calculi is dedicated to the axiomatization for formulae in normal form, which may still require non-trivial developments but is more manageable.

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.

It is often advantageous to be able to extract resource requirements in resource logics of strategic ability, rather than to verify whether a fixed resource requirement is sufficient 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 2EXPTIME-complete.

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.

International audience

We study the expressivity and complexity of two modal logics interpreted on finite forests and equipped with standard modalities to reason on submodels. The logic ML(|) extends the modal logic K with the composition operator | from ambient logic, whereas ML(*) features the separating conjunction * from separation logic. Both operators are second-order in nature. We show that ML(|) is as expressive as the graded modal logic GML (on trees) whereas ML(*) is strictly less expressive than GML. Moreover, we establish that the satisfiability problem is Tower-complete for ML(*), whereas it is (only) AExpPol-complete for ML(|), a result which is surprising given their relative expressivity. As by-products, we solve open problems related to sister logics such as static ambient logic and modal separation logic.

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 (QCTLt) admits a non-elementary Tower-complete satisfiability problem. We investigate the complexity of strict fragments of QCTLtas well as of the modal logic K with propositional quantification under the tree semantics. More specifically, we show that QCTLtrestricted to the temporal operator EX is already Tower-hard, which is unexpected as EX can only enforce local properties. When QCTLtrestricted 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 QCTLtrestricted to EF or to EXEF and of the well-known modal logics K, KD, GL, S4, K4 and D4, with propositional quantification under a semantics based on classes of trees.

Abstract We introduce a modal separation logic MSL whose models are memory states from separation logic and the logical connectives include modal operators as well as separating conjunction and implication from separation logic. With such a combination of operators, some fragments of MSL can be seen as genuine modal logics whereas some others capture standard separation logics, leading to an original language to speak about memory states. We analyse the decidability status and the computational complexity of several fragments of MSL, obtaining surprising results by design of proof methods that take into account the modal and separation features of MSL. For example, the satisfiability problem for the fragment of MSL with $\Diamond $, the difference modality $\langle \neq \rangle $ and separating conjunction $\ast $ is shown Tower-complete whereas the restriction either to $\Diamond $ and $\ast $ or to $\langle \neq \rangle $ and $\ast $ is only NP-complete. We establish that the full logic MSL admits an undecidable satisfiability problem. Furthermore, we investigate variants of MSL with alternative semantics and we build bridges with interval temporal logics and with logics equipped with sabotage operators.

The list segment predicate $$\mathtt {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 $$\mathtt {ls}$$ to the full propositional 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 $$\mathtt {ls}$$ is added, providing numerous results about adding reachability predicates to propositional separation logic.

International audience

International audience

We address the entailment problem for separation logic with symbolic heaps admitting list pred- icates and permissions for memory cells that are essential to express ownership of a heap region. In the permission-free case, the entailment problem is known to be in P. Herein, we design new decision procedures for solving the satisfiability and entailment problems that are parameterised by the permission theories. This permits the use of solvers dealing with the permission theory at hand, independently of the shape analysis. We also show that the entailment problem without list predicates is coNP-complete for several permission models, such as counting permissions and binary tree shares but the problem is in P for fractional permissions. Furthermore, when list predicates are added, we prove that the entailment problem is coNP-complete when the entail- ment problem for permission formulae is in coNP, assuming the write permission can be split into as many read permissions as desired. Finally, we show that the entailment problem for any Boolean permission model with infinite width is coNP-complete.

and extended versions of the papers selected from the 6th of the Reachability Problems Workshop hosted by the University of Bordeaux, France from 17 till

We show that linear-time temporal logic over concrete domains made of finite strings and the prefix relation admits a PS pace -complete satisfiability problem. Actually, we extend a known result with the concrete domain made of the set of natural numbers and the greater than relation (corresponding to the singleton alphabet case) and we solve an open problem mentioned in several publications. Since the prefix relation is not a total ordering, it is not possible to take advantage of existing techniques dedicated to temporal logics with concrete domains that are essentially linearly ordered structures. Instead, we introduce an adequate encoding of string constraints into length constraints that allows us to reduce the problem on strings to the problem on natural numbers. To do so, we also propose an extended version of the logic on strings that is able to compare lengths of longest common prefixes and for which the satisfiability problem is shown in PS pace . Finally, we show how to lift the result for the branching-time case in order to get decidability when the underlying temporal logic is CTL*.

Separation logic is used as an assertion language for Hoare-style proof systems about programs with pointers, and there is an ongoing quest for understanding its complexity and expressive power. Herein, we show that first-order separation logic with one record field restricted to two variables and the separating implication (no separating conjunction) is as expressive as weak second-order logic, substantially sharpening a previous result. Capturing weak second-order logic with such a restricted form of separation logic requires substantial updates to known proof techniques. We develop these and, as a by-product, identify the smallest fragment of separation logic known to be undecidable: first-order separation logic with one record field, two variables, and no separating conjunction. Because we forbid ourselves the use of many syntactic resources, this underscores even further the power of separating implication on concrete heaps.

Separation logic is a well-known assertion language for Hoare-style proof systems. We show that first-order separation logic with a unique record field restricted to two quantified variables and no program variables is undecidable. This is among the smallest fragments of separation logic known to be undecidable, and this contrasts with the decidability of two-variable first-order logic. We also investigate its restriction by dropping the magic wand connective, known to be decidable with nonelementary complexity, and we show that the satisfiability problem with only two quantified variables is not yet elementary recursive. Furthermore, we establish insightful and concrete relationships between two-variable separation logic and propositional interval temporal logic (PITL), data logics, and modal logics, providing an inner circle of closely related logics.

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.

The covering and boundedness problems for branching vector addition systems are shown complete for doubly-exponential time.

Various logical formalisms with the freeze quantifier have been recently considered to model computer systems even though this is a powerful mechanism that often leads to undecidability. In this article, we study a linear-time temporal logic with past-time operators such that the freeze operator is only used to express that some value from an infinite set is repeated in the future or in the past. Such a restriction has been inspired by a recent work on spatio-temporal logics that suggests such a restricted use of the freeze operator. We show decidability of finitary and infinitary satisfiability by reduction into the verification of temporal properties in Petri nets by proposing a symbolic representation of models. This is a quite surprising result in view of the expressive power of the logic since the logic is closed under negation, contains future-time and past-time temporal operators and can express the nonce property and its negation. These ingredients are known to lead to undecidability with a more liberal use of the freeze quantifier. The article also contains developments about the relationships between temporal logics with the freeze operator and counter automata as well as reductions into first-order logics over data words.

We investigate the decidability and complexity status of model-checking problems on unlabelled reachability graphs of Petri nets by considering first-order, modal and pattern-based 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.

International audience

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, causes undecidability.

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.

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.

Temporal logics, first-order logics, and automata over data words have recently attracted considerable attention. A data word is a word over a finite alphabet, together with a datum (an element of an infinite domain) at each position. Examples include timed words and XML documents. To refer to the data, temporal logics are extended with the freeze quantifier, first-order logics with predicates over the data domain, and automata with registers or pebbles. We investigate relative expressiveness and complexity of standard decision problems for LTL with the freeze quantifier (LTL«), 2-variable first-order logic (FO2) over data words, and register automata. The only predicate available on data is equality. Previously undiscovered connections among those formalisms, and to counter automata with incrementing errors, enable us to answer several questions left open in recent literature. We show that the future-time fragment of LTL« which corresponds to FO2 over finite data words can be extended considerably while preserving decidability, but at the expense of non-primitive recursive complexity, and that most of further extensions are undecidable. We also prove that surprisingly, over infinite data words, LTL« without the 'unti' operator, as well as nonemptiness of one-way universal register automata, are undecidable even when there is only 1 register.

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.

We present a reduction from a new logic extending van der Meyden's dynamic logic of permission (DLP) into propositional dynamic logic (PDL), providing a 2EXPTIME decision procedure and showing that all the machinery for PDL can be reused for reasoning about dynamic policies. As a side-effect, we establish that DLP is EXPTIME-complete. The logic we introduce extends the logic DLP so that the policy set can be updated depending on its current value and such an update corresponds to add/delete transitions in the model, showing similarities with van Benthem's sabotage modal logic.

International audience

Propositional modal provability logics like G and Grz have arithmetical interpretations where □φ can be read as ‘formula φ is provable in Peano Arithmetic’. These logics are decidable but are characterized by classes of Kripke frames which are not first‐order definable. By abstracting the aspects common to their characteristic axioms we define the notion of a formula generation map F(P) in one propositional variable. We then focus our attention on the properly displayable subset of all (first‐order definable) Sahlqvist modal logics. For any logic L from this subset, we consider the (provability) logic LF obtained by the addition of an axiom based upon a formula generation map F(P) so that LF = L + F(P). The class of such logics includes G and Grz. By appropriately modifying the right introduction rules for □, we give (not necessarily cut‐free) display calculi for every such logic. We define the pseudo‐displayable subset of these logics as those whose display calculi enjoy cut‐elimination for sequents of the form ⊤ ⊢ φ for any formula φ. We then show that for any provability logic LF having a conservative tense extension, there is a map f on formulae such that LF is pseudo‐displayable if and only if f maps theorems of LF to theorems of the underlying logic L and vice versa. By using a standard renaming technique we can guarantee that there is a polynomial‐time translation from LF into L. All proofs are purely syntactic and show the versatility of display calculi since similar results using traditional Gentzen calculi are not possible for as broad a range of logics and require further conditions. Our maps generalize previously known maps from G into K4. An application of our results gives an O(n.log n)3) translation from the (‘second order’) provability logic Grz into a decidable subset of first‐order logic. Since each of our logics L is a Sahlqvist logic, it is first‐order definable, and hence each L has a translation into first‐order logic. Our results therefore show that all pseudo‐displayable logics LF are ‘essentially first‐order’ even though their characteristic axiom may not be first‐order definable.

We define display calculi for nominal tense logics extending the minimal nominal tense logic (MNTL) by addition of primitive axioms. To do so, we use the natural translation ofMNTL into the minimal tense logic of inequality (L≠) which is known to be properly displayable by application of Kracht's results. The rules of the display calculus δMNTL for MNTL mimic those of the display calculus δL≠ for L≠. We show that every MNTL‐valid formula admits a cut‐free derivation in δMNTL. We also show that a restricted display calculus δ−MNTL, is not only complete for MNTL, but that it enjoys cut‐elimination for arbitrary sequents. Finally, we give a weak Sahlqvist‐type theorem for two semantically defined extensions of MNTL. Using Kracht's techniques we obtain sound and complete display calculi for these two extensions based upon δMNTL and δ−MNTL respectively. The display calculi based upon δMNTL enjoy cut‐elimination for valid formulae only, but those based upon δ−MNTL enjoy cut‐elimination for arbitrary sequents.

A modal reduction principle of the form [i1] … [in]p ⇒ [j1] … [jn′]p can be viewed as a production rule i1 · … ·in → j1 · … · jn′ in a formal grammar. We study the extensions of the multimodal logic Km with m independent K modal connectives by finite addition of axiom schemes of the above form such that the associated finite set of production rules forms a regular grammar. We show that given a regular grammar G and a modal formula Ø, deciding whether the formula is satisfiable in the extension of Km with axiom schemes from G can be done in deterministic exponential‐time in the size of G and Ø, and this problem is complete for this complexity class. Such an extension of Km is called a regular grammar logic. The proof of the exponential‐time upper bound is extended to PDL‐like extensions of Km and to global logical consequence and global satisfiability problems. Using an equational characterization of context‐free languages, we show that by replacing the regular grammars by linear ones, the above problem becomes undecidable. The last part of the paper presents non‐trivial classes of exponential time complete regular grammar logics.

Invited talk

The nondeterministic information logic NIL has been introduced by Orłowska and Pawlak in 1984 as a logic for reasoning about total information systems with the similarity, the forward inclusion and the backward inclusion relations. In 1987, Vakarelov provides the first first-order characterization of structures derived from information systems and this has been done with the semantical structures of NIL. Since then, various extensions of NIL have been introduced and many issues for information logics about decidability and Hilbert-style proof systems have been solved. However, computational complexity issues have been seldom attacked in the literature mainly because the information logics are propositional polymodal logics with interdependent modal connectives. We show that NIL satisfiability is a PSPACE-complete problem. PSPACE-hardness is shown to be an easy consequence of PSPACE-hardness of the well-known modal logic S4. The main difficulty is to show that NIL satisfiability is in PSPACE. To do so we present an original construction that extends various previous works by Ladner (1977), Halpern and Moses (1992) and Spaan (1993).