Complexity and expressivity of propositional dynamic logics with finitely many variables

TL;DR

This paper explores the complexity and expressive power of finite-variable fragments of propositional dynamic logics, showing that variable-free fragments are as expressive as full logics and that complexity remains unchanged.

Contribution

It demonstrates that variable-free fragments of various PDL variants are as expressive as the full logics and that their satisfiability complexity remains the same.

Findings

Variable-free fragments are as expressive as full logics.

Complexity of satisfiability remains unchanged in variable-free fragments.

Undecidability persists in certain PDL variants without variables.

Abstract

We investigate the complexity of satisfiability for finite-variable fragments of propositional dynamic logics. We consider three formalisms belonging to three representative complexity classes, broadly understood,---regular PDL, which is EXPTIME-complete, PDL with intersection, which is 2EXPTIME-complete, and PDL with parallel composition, which is undecidable. We show that, for each of these logics, the complexity of satisfiability remains unchanged even if we only allow as inputs formulas built solely out of propositional constants, i.e. without propositional variables. Moreover, we show that this is a consequence of the richness of the expressive power of variable-free fragments: for all the logics we consider, such fragments are as semantically expressive as entire logics. We conjecture that this is representative of PDL-style, as well as closely related, logics.

Equations

$$\phi :=p\mid \perp \mid (\phi \to \phi )\mid [\alpha ]\phi ,$$

$$\alpha :=a\mid \phi ?\mid (\alpha ;\alpha )\mid (\alpha \cup \alpha )\mid (\alpha \cap \alpha )\mid {\alpha }^{\ast },$$

$$\Theta =p_{n+1}\wedge [{\gamma }^{\ast }](⟨\gamma ⟩p_{n+1}\to p_{n+1}).$$

$$\hat{\phi }=\Theta \wedge {\phi }^{\prime }.$$

$$A_m=⟨b{⟩}^m[b]\perp \wedge \neg ⟨b{⟩}^{m+1}[b]\perp \wedge ⟨b⟩(⟨b⟩\top \wedge [b]⟨b⟩\top ).$$

$$B_m=⟨b⟩A_m.$$

$${\phi }^{\ast }=\sigma (\hat{\phi })$$

$$\Theta =p_{n+1}\wedge \underset{i=1}{\overset{k}{\bigwedge }}\underset{j=1}{\overset{n_k-1}{\bigwedge }}[{\alpha }_1^i]\dots [{\alpha }_j^i](⟨{\alpha }_{j+1}^i⟩p_{n+1}\to p_{n+1}).$$

$$\hat{\phi }=\Theta \wedge {\phi }^{\prime }.$$

Full text

Keywords: propositional dynamic logic, finite-variable fragments, satisfiability, computational complexity, undecidability, expressivity

1 Introduction

The propositional dynamic logic, PDL, introduced in [8], has ever since been used for reasoning about the input-output behaviour of terminating programs. Over the years, it has been extended in various ways to deal with a wider variety of terminating programs [20, 12, 21, 19, 10]. Also, various formalisms closely linked to PDL have been developed for applications in areas other than reasoning about programs; among them are knowledge representation [9, 7, 16], querying semistructured data [1], data analysis [5], and linguistics [14].

Clearly, the complexity of satisfiability—equivalently, validity—problem for all of these variants of PDL is of crucial importance to their applications in the above-mentioned domains. Typically, for formulas containing an arbitrary number of propositional variables, the complexity of satisfiability problem for variants of PDL is rather high: it ranges from EXPTIME-complete [8] to undecidable [2].

It has, however, been observed that, in practice, one rarely uses formulas containing a large number of propositional variables—usually, this number is rather small. This raises the question of whether the complexity of satisfiability for PDL can be tamed by restricting the language to a finite number of propositional variables. Such an effect is not, after all, entirely unknown: for many logics, the complexity of satisfiability goes down from “intractable” to “tractable” once we place a limit on the number of propositional variables that can be used in the construction of formulas. For the classical propositional logic, as well as for the normal extensions of the modal logic K5 [17], which include logics K45, KD45, and S5 (see also [11]), the complexity of satisfiability goes down from NP-complete to polynomial-time computable once we restrict the number of propositional variables to any finite number. Similarly, as follows from [18], the complexity of satisfiability for intuitionistic propositional logic goes down from PSPACE-complete to polynomial-time computable if we consider only formulas of one variable.

The main contribution of the present paper is to show that for propositional dynamic logics this route to reducing the complexity of satisfiability seems to be closed: even formulas built out of propositional constants, and thus containing no propositional variables at all, are as hard to test for satisfiability as formulas with an arbitrary number of propositional variables.

We suspect that this behaviour is representative of PDL-style logics. It would, however, be difficult to make an exhaustive case, given a wild proliferation of such formalisms. What we do instead is pick three examples that are representative in the sense of their satisfiability problems belonging to three representative complexity classes (broadly understood, i.e., treating “undecidable” as a complexity class); namely, we consider regular PDL, which has an EXPTIME-complete satisfiability problem [8], PDL with intersection, which has a 2EXPTIME-complete satisfiability problem [15], and PDL with parallel composition, which has an undecidable satisfiability problem [2]. We show that satisfiability problem for the variable-free fragment of each of these logics is as hard as for the entire logic. Moreover, we show that this is a consequence of the richness of the expressive power of variable-free fragments: for all the logics we consider, variable-free fragments are as semantically expressive as entire logics.

Similar results for other propositional modal logics have been obtained in [3], [11], [13], [6], [22], and [4]. The techniques used in those studies are not directly applicable to obtain the results presented in this paper; we do, however, substantially draw on the ideas from [3] and [11].

The paper is organised as follows. In section 2, we recall the syntax and semantics of the logics we consider. Then, in section 3, we present our results about complexity and expressivity of their variable-free fragments. We conclude in section 4.

2 Syntax and semantics

In this section, we recall the syntax and semantics of PDL with intersection (IPDL), regular PDL (PDL), and PDL with parallel composition (PRSPDL).

The language of IPDL contains a countable set $\textit{{Var}}=\{p_{1},p_{2},\ldots\}$ of propositional variables, the propositional constant $\perp$ (“falsehood”), the Boolean connective $\rightarrow$, and modalities of the form $[\,\alpha\,]\,$, where $\alpha$ ranges over program terms built out of a countable set $AP=\{a_{1},a_{2},\ldots\}$ of atomic program terms as well as formulas, using the operations ? (test), $\,;\,$ (composition), $\cup$ (choice), $\,\cap\,$ (intersection), and ∗ (iteration). The intended meaning of the formula $[\,\alpha\,]\,\varphi$ is that every execution of the program $\alpha$ at the current state results in a state where $\varphi$ holds. Formulas $\varphi$ and program terms $\alpha$ are simultaneously defined by the following BNF expressions:

[TABLE]

[TABLE]

where $p$ ranges over Var and $a$ ranges over $AP$. The other connectives are defined as usual. Formulas are evaluated in Kripke models. A Kripke model is a tuple $\mathfrak{M}=(\mathcal{S},\{\mathcal{R}_{a}\}_{a\in AP},V)$, where $\mathcal{S}$ is a non-empty set (of states), $\mathcal{R}_{a}$ is a binary (accessibility) relation on $\mathcal{S}$, and $V$ is a (valuation) function $V:\textit{{Var}}\rightarrow 2^{\mathcal{S}}$. Accessibility relations for non-atomic program terms as well as the satisfaction relation between models, states, and formulas are defined by simultaneous induction as follows:

• •

$(s,t)\in\mathcal{R}_{\varphi?}$ $\leftrightharpoons$ $s=t$ and $\mathfrak{M},s\models\varphi$;

• •

$(s,t)\in\mathcal{R}_{\alpha\,;\,\beta}$ $\leftrightharpoons$ $(s,u)\in\mathcal{R}_{\alpha}$ and $(u,t)\in\mathcal{R}_{\beta}$, for some $u\in\mathcal{S}$;

• •

$(s,t)\in\mathcal{R}_{\alpha\cup\beta}$ $\leftrightharpoons$ $(s,t)\in\mathcal{R}_{\alpha}$ or $(s,t)\in\mathcal{R}_{\beta}$;

• •

$(s,t)\in\mathcal{R}_{\alpha\,\cap\,\beta}$ $\leftrightharpoons$ $(s,t)\in\mathcal{R}_{\alpha}$ and $(s,t)\in\mathcal{R}_{\beta}$;

• •

$(s,t)\in\mathcal{R}_{\alpha^{*}}$ $\leftrightharpoons$ $(s,t)\in\mathcal{R}^{\ast}_{\alpha}$, where $\mathcal{R}^{\ast}_{\alpha}$ is the reflexive, transitive closure of $\mathcal{R}_{\alpha}$;

• •

$\mathfrak{M},s\models p_{i}$ $\leftrightharpoons$ $s\in V(p_{i})$;

• •

$\mathfrak{M},s\models\bot$ never holds;

• •

$\mathfrak{M},s\models\varphi\rightarrow\psi$ $\leftrightharpoons$ $\mathfrak{M},s\models\varphi$ implies $\mathfrak{M},s\models\psi$;

• •

$\mathfrak{M},s\models[\,\alpha\,]\,\varphi$ $\leftrightharpoons$ $\mathfrak{M},t\models\varphi$ whenever $(s,t)\in\mathcal{R}_{\alpha}$.

A formula is satisfiable if it is satisfied at some state of some model. A formula is valid if it is satisfied by every state of every model. Formally, by IPDL, we mean the set of all valid formulas in this language.

The language of PDL differs from that of IPDL in that it does not contain program operations $\,\cap\,$ and ?. The semantics is modified accordingly.

The language of PRSPDL is interpreted on models made up of states possessing inner structure: a state $s$ is a composition $x\ast y$ of states $x$ and $y$ if $s$ can be separated into components $x$ and $y$; in general, there is no requirement that, given states $x$ and $y$, a composition $x\ast y$ is a unique state. The program terms are formed out of atomic program terms as well as four special program terms $r_{1}$, $r_{2}$ (recovery of the first and second $\ast$-components, respectively, of a state), $s_{1}$, and $s_{2}$ (storing a state as the first and second $\ast$-components, respectively, of a composite state), using the operations ? (test), ∗ (iteration), and $||$ (parallel composition). Note that the language of PRSPDL does not contain the operation of union of program terms. A Kripke model is a tuple $\mathfrak{M}=(\mathcal{S},\{\mathcal{R}_{a}\}_{a\in AP},\ast,V)$, where $\mathcal{S}$, $\mathcal{R}_{a}$, and $V$ have the same meaning as in Kripke models for IPDL, and $\ast$ is a function $\mathcal{S}\times\mathcal{S}\to 2^{\mathcal{S}}$. The meaning of $||$, $r_{1}$, $r_{2}$, $s_{1}$, and $s_{2}$ is given by the following clauses:

• •

$(s,t)\in\mathcal{R}_{\alpha\,||\,\beta}$ $\leftrightharpoons$ there exist $x_{1},y_{1},x_{2},y_{2}\in\mathcal{S}$ such that $s\in x_{1}\ast x_{2}$, $t\in y_{1}\ast y_{2}$, $(x_{1},y_{1})\in\mathcal{R}_{\alpha}$, and $(x_{2},y_{2})\in\mathcal{R}_{\beta}$;

• •

$(s,t)\in\mathcal{R}_{r_{1}}$ $\leftrightharpoons$ there exists $u\in\mathcal{S}$ such that $s\in t\ast u$;

• •

$(s,t)\in\mathcal{R}_{r_{2}}$ $\leftrightharpoons$ there exists $u\in\mathcal{S}$ such that $s\in u\ast t$;

• •

$(s,t)\in\mathcal{R}_{s_{1}}$ $\leftrightharpoons$ there exists $u\in\mathcal{S}$ such that $t\in s\ast u$;

• •

$(s,t)\in\mathcal{R}_{s_{2}}$ $\leftrightharpoons$ there exists $u\in\mathcal{S}$ such that $t\in u\ast s$.

The models thus defined are referred to in [2] as “$\ast$-separated.” The authors of [2] consider a number of logics in the same language, which differ in the conditions placed on the function $\ast$ in their semantics. For our purposes, it suffices to consider only one of the logics from [2],—the rest can be dealt with in a similar way.

The notions of satisfiability and validity are defined as for IPDL and PDL.

For each of the logics we consider, by a variable-free fragment we mean the subset of the logic containing only variable-free formulas—i.e., formulas not containing any propositional variables. Given formulas $\varphi$, $\psi$ and a propositional variable $p$, we denote by $\varphi(p/\psi)$ the result of uniformly substituting $\psi$ for $p$ in $\varphi$.

3 Finite-variable fragments

In this section, we show that variable-free fragments of IPDL, PDL, and PRSPDL have the same expressive power and computational complexity as the entire logics, by embedding each logic into its variable-free fragment; in the case of IPDL and PDL, the embeddings are polynomial-time computable. We initially work with IPDL and subsequently point out how that work carries over to PDL and PRSPDL.

Let $\varphi$ be an arbitrary IPDL-formula. Assume that $\varphi$ only contains propositional variables $p_{1},\ldots,p_{n}$ and atomic program terms $a_{1},\ldots,a_{l}$. Let $\gamma=a_{1}\,\cup\,\ldots\,\cup\,a_{l}$. First, recursively define translation $\cdot^{\prime}$ as follows:

[TABLE]

Second, define

[TABLE]

Finally, let

[TABLE]

Lemma 3.1

Formula $\varphi$ is satisfiable if, and only if, formula $\widehat{\varphi}$ is satisfiable.

Proof. Suppose $\widehat{\varphi}$ is not satisfiable. Then, $\neg\widehat{\varphi}\in{\bf IPDL}$ and, since IPDL is closed under substitution, $\neg\widehat{\varphi}(p_{n+1}/\top)\in{\bf IPDL}$. As $\widehat{\varphi}(p_{n+1}/\top)\leftrightarrow\varphi\in{\bf IPDL}$, we have $\neg\varphi\in{\bf IPDL}$; thus, $\varphi$ is not satisfiable.

Suppose that $\widehat{\varphi}$ is satisfiable. In particular, let $\mathfrak{M},s_{0}\models\widehat{\varphi}$ for some model $\mathfrak{M}$ and some $s_{0}$ in $\mathfrak{M}$. Define $\mathfrak{M}^{\prime}$ to be the smallest submodel of $\mathfrak{M}$ such that

• •

$s_{0}$ is in $\mathfrak{M^{\prime}}$;

• •

if $x$ is in $\mathfrak{M^{\prime}}$, $x\mathcal{R}_{\gamma}y$, and $\mathfrak{M},y\models p_{n+1}$, then $y$ is also in $\mathfrak{M^{\prime}}$.

Notice that $p_{n+1}$ is universally true in $\mathfrak{M}^{\prime}$. It is straightforward to show that, for every subformula $\psi$ of $\varphi$ and every $s$ in $\mathfrak{M}^{\prime}$, we have $\mathfrak{M},s\models\psi^{\prime}$ if, and only if, $\mathfrak{M^{\prime}},s\models\psi$. As $\mathfrak{M},s_{0}\models\varphi^{\prime}$, this gives us $\mathfrak{M^{\prime}},s_{0}\models\varphi$; hence, $\varphi$ is satisfiable. $\Box$

Remark 3.2

It follows from the proof of Lemma 3.1 that, if $\widehat{\varphi}$ is satisfiable, then it is satisfiable in a model where $p_{n+1}$ is universally true. Indeed, if $\widehat{\varphi}$ is satisfiable, then $\varphi$ is satisfiable in a model where $p_{n+1}$ is universally true. The claim follows from the fact that $\varphi$ is equivalent to $\widehat{\varphi}(p_{n+1}/\top)$.

Now, consider the following class $\sf{M}$ of finite models. Let $b$ be the lexicographically first atomic program term of $\varphi$ if $\varphi$ contains such terms; otherwise, let $b$ be $a_{1}$. For every $m\in\{1,\ldots,n+1\}$, where $p_{1},\ldots,p_{n}$ are the variables in $\varphi$, class $\sf{M}$ contains a unique member $\mathfrak{M}_{m}$, defined as follows: $\mathfrak{M}_{m}=(\mathcal{S}_{m},\{\mathcal{R}_{a}\}_{a\in AP},V_{m})$, where

• •

$\mathcal{S}_{m}=\{r_{m},t^{m},s_{1}^{m},s_{2}^{m},\ldots,s_{m}^{m}\}$;

• •

$\mathcal{R}_{b}$ is the transitive closure of the relation $\{\langle r_{m},t^{m}\rangle,\langle t^{m},t^{m}\rangle,\langle r_{m},s_{1}^{m}\rangle\}\linebreak\,\cup\,\{\langle s_{i}^{m},s_{i+1}^{m}\rangle:1\leq i\leq m-1\}$;

• •

$\mathcal{R}_{a}=\varnothing$ if $a\neq b$;

• •

$V_{m}(p)=\varnothing$ for every $p\in\textit{{Var}}$.

The model $\mathfrak{M}_{m}$ is depicted in Figure 1, where arrows represent $\mathcal{R}_{b}$; to avoid clutter, arrows are omitted whenever the presence of $\mathcal{R}_{b}$ can be deduced from its transitivity; the circle represents a state related by $\mathcal{R}_{b}$ to itself, and solid dots represent states without such loops.

We now define formulas that will be true at the roots of models from $\sf{M}$. For $j\geqslant 0$, inductively define the formula $\langle b\rangle^{j}\psi$ as follows: $\langle b\rangle^{0}\psi=\psi$; $\langle b\rangle^{k+1}\psi=\langle b\rangle\,\langle b\rangle^{k}\psi$. Next, for every $m\in\{1,\ldots,n+1\}$, define

[TABLE]

Lemma 3.3

Let $\mathfrak{M}_{k}\in\sf{M}$ and let $x$ be a state in $\mathfrak{M}_{k}$. Then, $\mathfrak{M}_{k},x\models A_{m}$ if, and only if, $k=m$ and $x=r_{m}$.

Proof. Straightforward. $\Box$

Now, define

[TABLE]

Let $\sigma$ be a (substitution) function that, given an IPDL-formula $\psi$, replaces all occurrences of $p_{i}$ in $\psi$ by $B_{i}$, where $1\leqslant i\leqslant n+1$. Finally, define

[TABLE]

to produce a variable-free formula $\varphi^{*}$.

Lemma 3.4

Formula $\varphi$ is satisfiable if, and only if, formula $\varphi^{*}$ is satisfiable.

Proof. Suppose that $\varphi$ is not satisfiable. Then, by Lemma 3.1, $\widehat{\varphi}$ is not satisfiable, either, and hence $\neg\widehat{\varphi}\in{\bf IPDL}$. Since IPDL is closed under substitution, $\neg\varphi^{*}\in{\bf IPDL}$ and, thus, $\varphi^{*}$ is not satisfiable.

Suppose that $\varphi$ is satisfiable. Then, in view of Lemma 3.1 and Remark 3.2, $\mathfrak{M},s_{0}\models\widehat{\varphi}$ for some $\mathfrak{M}$ such that $p_{n+1}$ is true at every state of $\mathfrak{M}$ and some $s_{0}$ in $\mathfrak{M}$. Define model $\mathfrak{M^{\prime}}$ as follows. Attach to $\mathfrak{M}$ all the models from $\sf{M}$; then, for every $x$ in $\mathfrak{M}$, put $x\mathcal{R}_{b}r_{m}$ (where $r_{m}$ is the root of $\mathfrak{M}_{m}\in\sf{M}$) exactly when $\mathfrak{M},x\models p_{m}$. Notice that $r_{n+1}$ is accessible in $\mathfrak{M^{\prime}}$ from every $x$ in $\mathfrak{M}$.

To conclude the proof, it suffices to show that $\mathfrak{M^{\prime}},s_{0}\models\varphi^{*}$. It is easy to check that $\mathfrak{M^{\prime}},s_{0}\models\sigma(\Theta)$. It then remains to show that $\mathfrak{M^{\prime}},s_{0}\models\sigma(\varphi^{\prime})$. To that end, it suffices to show that $\mathfrak{M},x\models\psi^{\prime}$ if, and only if, $\mathfrak{M^{\prime}},x\models\sigma(\psi^{\prime})$, for every subformula $\psi$ of $\varphi$ and every $x$ in $\mathfrak{M}$. This can be done by induction on $\psi$; we only consider the base case, leaving the rest to the reader.

Let $\mathfrak{M^{\prime}},x\models B_{i}$. Then, for some $y$ in $\mathfrak{M}^{\prime}$, we have $x\mathcal{R}^{\prime}_{b}y$ and $\mathfrak{M^{\prime}},y\models A_{i}$. This is only possible if $y$ is not in $\mathfrak{M}$. Indeed, suppose otherwise. Then, $\mathfrak{M^{\prime}},y\models p_{n+1}$, and therefore, $y\mathcal{R}^{\prime}_{b}r_{n+1}$. Hence, $\mathfrak{M^{\prime}},y\models\langle b\rangle^{i+1}[\,b\,]\,\bot$, and therefore, $\mathfrak{M^{\prime}},y\not\models A_{i}$, resulting in a contradiction. Thus, $y$ is in $\mathfrak{M}_{m}$, for some $m\in\{1,\ldots,n+1\}$. Then, by Lemma 3.3, $y=r_{i}$, and therefore, by definition of $\mathfrak{M}^{\prime}$, we have $\mathfrak{M},x\models p_{i}$. The other direction is straightforward. $\Box$

Theorem 3.5

There exists a mapping that embeds IPDL into its variable-free fragment in polynomial time.

We now look at the complexity-theoretic implications of Theorem 3.5. It has been shown in [15] that the fragment of IPDL containing a single atomic program term is 2EXPTIME-complete. This gives us the following:

Theorem 3.6

The satisfiability problem for the fragment of IPDL containing variable-free formulas with a single atomic program term is 2EXPTIME-complete.

We now point out how the work we have done so far for IPDL carries over to PDL and PRSPDL.

It is easy to check that the construction presented above works for PDL, as well, if we omit the details peculiar to IPDL. This gives us the following:

Theorem 3.7

There exists a mapping that embeds PDL into its variable-free fragment in polynomial time.

Since satisfiability problem for PDL with a single atomic program term is EXPTIME-complete [8], we have the following:

Theorem 3.8

The satisfiability problem for the fragment of PDL containing variable-free formulas with a single atomic program term is EXPTIME-complete.

We next show how to modify the above argument for PRSPDL. We remind the reader that we confine our attention to PRSPDL over $\ast$-separated models; other variants of this formalism considered in [2] can be treated in essentially the same way. We first need to construct the analogue of formula $\widehat{\varphi}$. It is straightforward to define the translation $\cdot^{\prime}$:

[TABLE]

We next define the analogue of formula $\Theta$. As PRSPDL does not have the operation of choice on program terms, we proceed as follows. Let

$\alpha^{1}_{1}\dots\alpha^{1}_{n_{1}}$

…

$\alpha^{k}_{1}\dots\alpha^{k}_{n_{k}}$

be all sequences of nested program terms in $\varphi$. Then,

[TABLE]

Finally, let

[TABLE]

From here on, we argue exactly as in the case of IPDL to obtain the following:

Theorem 3.9

There exists a mapping that embeds PRSPDL over $\ast$-separated models into its variable-free fragment.

Theorem 3.10

The variable-free fragment of PRSPDL over $\ast$-separated models is undecidable.

Remark 3.11

It is well-known that the consequence relation for propositional dynamic logics is not compact, as the formula $[\,a^{\ast}\,]\,\varphi$ follows from the infinite set $\{[\,a\,]\,^{n}\varphi:n\geqslant 0\}$ of formulas but not from any of its finite subsets; thus, the consequence relation is not reducible to satisfiability for formulas. The technique presented above can be used to reduce the consequence relation for the logics we have considered to the consequence relation for their variable-free fragments. To that end, unless the number of propositional variables occurring in the premises is finite, we need to use an extra atomic program term corresponding to the accessibility relation connecting the roots of the models attached in the proof of Lemma 3.4 to the original model. This is necessary as in the proof of Lemma 3.4 we relied on the variable $p_{n+1}$, used as a marker of the worlds of the original model, having the maximal index of all the variables of the formula $\varphi$.

4 Conclusion

We have shown that for three variants of propositional dynamic logic representative of various complexity classes, broadly understood, the complexity of satisfiability remains the same if we restrict the language to formulas built out of propositional constants, i.e., without the use of propositional variables. This is a consequence of the richness of the expressive power of the variable-free fragments—as we have shown, they are as expressive as the logics with an infinite supply of propositional variables.

We suspect that these results are representative of how PDL-style formalisms behave. If this is indeed so, the important question for future research is to find out if there are ways to tame the complexity of satisfiability that might be applicable en masse to a wide range of PDL-style logics and that might be of relevance to how these formalisms are applied in practice.

Acknowledgements

We thank the two anonymous referees for their remarks, which have helped to substantially improve the presentation of the paper. In particular, the paper has become shorter and more focused.