Full article: Correction

Formulae display: $MathJax Logo$ ?Mathematical formulae have been encoded as MathML and are displayed in this HTML version using MathJax in order to improve their display. Uncheck the box to turn MathJax off. This feature requires Javascript. Click on a formula to zoom.

This article refers to:

A separation theorem for discrete-time interval temporal logic

Article title: A Separation Theorem for Discrete Time Interval Temporal Logic

Authors: Dimitar P. Guelev and Ben Moszkowski

Journal: Journal of Applied Non-Classical Logics

Bibliometrics: Volume 32, Number 01, pages 28–54

DOI: https://doi.org/10.1080/11663081.2022.2050135

Section 3.3 of the article has been resupplied because of a mistake that was found in a proof in this section's original version. The mistaken proof relied on using the equivalence $(B_{1} \lor B_{2})^{*} = (B_{1}; B_{2})^{*}$ to eliminate the use of $\lor$ in chop-star-formulas before extracting expanding modalities from the scope of chop-star in them, which was incorrect because extracting the expanding modalities from $B_{1}^{*}$ and $B_{2}^{*}$ can lead to introducing new occurrences of $\lor$ . The corrected proof makes no such use. The corrected Section 3.3 is reproduced below.

3.3. Extracting $◊_{l}$ and $◊_{r}$ from the scope of chop-star

So far we have shown how to handle the interaction of the expanding modalities with the chop operator of $ITL-NL$ . Since $⊨ ◯} A \equiv s k i p; A$ , this automatically extends to formulas with $◯}$ . In this section we consider chop-star. To make our transformations apply to $ITL-NL$ with chop-star included, we use the inter-expressibility between chop-star and propositional quantification in $I T L$ with just chop and $◯}$ : We first show that $◊_{l}$ - and $◊_{r}$ -subformulas can be taken out of the scope of chop-star at the cost of introducing propositional quantification. The quantified formula we obtain is a Boolean combination of introspective formulas and strictly past and strictly future formulas. Importantly the latter have no occurrences of the quantified propositional variables. This makes it possible to eliminate the quantifier introduced, possibly at the cost of re-introducing occurrences of chop-star, but only in the introspective formulas.

We use the validity of (13) $B^{*} \equiv B^{*} \land f i n i t e \lor (B^{*}; (B \land i n f)) \lor (B \land f i n i t e)^{*} \land i n f$ (13) and consider the cases which correspond to the three disjuncts on the RHS of ≡ in it separately. Since we are using strong chop, $⊨ B^{*}; (B \land i n f) \equiv (B^{*} \land f i n i t e); (B \land i n f)$ . Hence the case of $B^{*}; (B \land i n f)$ reduces to the case of $B^{*} \land f i n i t e$ .

The key observation that enables the use of propositional quantification for handling the cases of $B^{*} \land f i n i t e$ and $(B \land f i n i t e)^{*} \land i n f$ is that, once a timeline is fixed, the satisfaction of $◊_{d}$ -formulas depends only on the corresponding endpoint of the reference interval, and therefore, a $◊_{d}$ -formula can be denoted by a propositional variable. This means that, for an appropriate assignment to p on the given timeline, $[◊_{r} B / f i n p] A$ is equivalent to A for all formulas A.

Lemma 3.10

Let A and B be $ITL-NL$ formulas and $q \in A P ∖ V a r (A)$ . Let none of the occurrences of p in A be in the scope of $◊_{l}$ or $◊_{r}$ . Then $\begin{aligned} ⊨ [◊_{r} B / p] A \equiv \exists q (◻ (q \equiv ((e m p t y \land ◊_{r} B); t r u e)) \land [f i n q / p] A) \\ ⊨ [◊_{l} B / p] A \equiv \exists q (◻ (q \equiv ((e m p t y \land ◊_{l} B); t r u e)) \land [q / p] A) \end{aligned}$

Proof.

Given a timeline σ, let $σ^{'}$ be another timeline such that $d o m σ^{'} = d o m σ$ , $r \in (σ^{'})^{k}$ iff $r \in σ^{k}$ for all $r \in A P ∖ {q}$ and $k \in d o m σ$ , and let $q \in (σ^{'})^{k}$ iff $σ, l, k ⊨ ◊_{r} B$ for all $k \in d o m σ$ and any $i \in d o m σ$ such that $l \leq k$ . Then a direct check by induction on the construction of formulas C shows that $σ^{'}, i, j ⊨ [◊_{r} B / p] C \equiv [f i n q / p] C$ and $σ^{'}, i, j ⊨ ◻ (q \equiv ((e m p t y \land ◊_{r} B); t r u e))$ for all $i, j \in d o m σ$ such that $i \leq j$ . The equivalence about $[◊_{l} B / p] A$ is somewhat simpler, because of the time asymmetry of $◻$ , and the convention that $σ ⊨ p$ iff $p \in σ^{0}$ . The proof of its validity is similar.

The equivalence about $◊_{l} B$ in Lemma 3.10 can be written more concisely as the LHS of $⊨ \exists q (◻ (q \equiv ((empty \land ◊_{l} B); t r u e)) \land [q / p] A) \equiv \exists p (◻ (p \equiv ◊_{l} B) \land A) .$ In the lemma, the equivalence about $◊_{l} B$ was chosen to be the exact past mirror of the equivalence about $◊_{r} B$ , to enable a concise proof of Lemma below.

Note that $⊨ A$ does not imply $⊨ [B / p] A$ for arbitrary B in $I T L$ . Again, in both the future and the past cases, it is sufficient to consider B which are conjunctions of introspective formulas, past $◊_{l}$ -formulas and future $◊_{r}$ -formulas. For chop-star-free formulas, this follows from Lemma 3.7.

The following lemma extends Lemma 3.8 to chop-star formulas

Lemma 3.11

Let A and B be conjunctions of introspective formulas, past $◊_{l}$ -formulas and future $◊_{r}$ -formulas. Then $◊_{d} A$ , $d \in {l, r}$ , and A; B are equivalent to separated formulas. Let B be an arbitrary separated formula. Then $B^{*}$ are equivalent to separated formulas.

Proof.

The cases of $◊_{d} A$ , $d \in {l, r}$ , A;B are handled just like in the proof of Lemma 3.8, except that, because of the possibility for chop-star to occur in A and B, the transformations proposed in that proof must now be regarded as part of a proof by induction on the chop-star-height $h_{*}$ of the involved formulas: we let $h_{*} (B)$ denote the length of the longest chain of nested occurrences of chop-star in B. Observe that the transformations involved in the proofs of Lemma 3.5, Lemma 3.7 and Lemma 3.8 do not cause chop-star-height to increase. Below we do the remaining case of $B^{*}$ .

Let B, which we assume to be separated, be a boolean combination of some introspective formulas, the past $◊_{l}$ -formulas $◊_{l} P_{1}$ , …, $◊_{l} P_{u}$ and the future $◊_{r}$ -formulas $◊_{r} F_{1}$ , …, $◊_{r} F_{v}$ . By Lemma 3.7, we can assume that $P_{i}$ , $i = 1, \dots, u$ , are conjunctions of introspective and strictly past formulas. Similarly, we can assume that $F_{j}$ , $j = 1, \dots, v$ , are conjunctions of introspective and strictly future formulas.

We can assume that B is equivalent to some disjunction $B_{1} \lor \dots \lor B_{s}$ where $B_{t}$ is the conjunction of some introspective formula $H_{t}$ and, for the sake of simplicity, all the formulas $ϵ_{t, 1}^{p} ◊_{l} P_{1}$ , …, $ϵ_{t, u}^{p} ◊_{l} P_{u}$ and $ϵ_{t, 1}^{f} ◊_{r} F_{1}$ , …, $ϵ_{t, v}^{f} ◊_{r} F_{v}$ for some appropriate $ϵ_{t, 1}^{p}$ , …, $ϵ_{t, u}^{p}$ , $ϵ_{t, 1}^{f}$ , …, $ϵ_{t, v}^{f}$ , $t = 1, \dots, s$ : $B_{t} ≜ H_{t} \land ⋀_{i = 1}^{u} ϵ_{t, i}^{p} ◊_{l} P_{i} \land ⋀_{j = 1}^{v} ϵ_{t, j}^{f} ◊_{r} F_{j} .$ Lemma 3.10 and its time mirror imply that (14) ${(⋁_{t = 1}^{s} B_{t})}^{*} \equiv \exists p_{1} \dots \exists p_{u} \exists f_{1} \dots \exists f_{v} (\begin{array}{l} {(⋁_{t = 1}^{s} H_{t} \land ⋀_{i = 1}^{u} ϵ_{t, i}^{p} p_{i} \land ⋀_{j = 1}^{v} ϵ_{t, j}^{f} f i n f_{j})}^{*} \land \\ ⋀_{i = 1}^{u} ◻ (p_{i} \equiv ((e m p t y \land ◊_{l} P_{i}); t r u e)) \\ ⋀_{j = 1}^{v} ◻ (f_{j} \equiv ((e m p t y \land ◊_{r} F_{j}); t r u e)) \end{array})$ (14) Let $F_{j}$ be the conjunction $C_{j} \land G_{j}$ of some introspective formula $C_{j}$ and the conjunction $G_{j}$ of some possibly negated future $◊_{r}$ -formulas. (As mentioned above, we assume this by Lemma 3.7.) Let $C_{j, k}$ and $C_{j, k}^{'}$ , $k = 1, \dots, m_{j}$ , satisfy Lemma 3.5 for $C_{j}$ , $j = 1, \dots, u$ . Then (15) (17) $\begin{aligned} ⊨ ◻ (f_{j} \equiv ((e m p t y \land ◊_{r} F_{j}); t r u e)) \equiv \\ ◻ (f_{j} \supset ((e m p t y \land ◊_{r} F_{j}); t r u e)) \land ◻ (\neg f_{j} \supset \neg ((e m p t y \land ◊_{r} F_{j}); t r u e)) \\ ⊨ ◻ (f_{j} \supset ((e m p t y \land ◊_{r} F_{j}); t r u e)) \equiv \\ ⋀_{k = 1}^{m_{j}} (t r u e; (f_{j} \land C_{j, k} \land \neg (\underset{F_{j}}{\underset{⏟}{(C_{j} \land G_{j})}}; t r u e))) \supset ◊_{r} (C_{j, k}^{'} \land G_{j}) \\ ⊨ ◻ (\neg f_{j} \supset \neg ((e m p t y \land ◊_{r} F_{j}); t r u e)) \equiv \\ \neg (t r u e; (\neg f_{j} \land \underset{F_{j}}{\underset{⏟}{(C_{j} \land G_{j})}}); t r u e) \land ⋀_{k = 1}^{m_{j}} (t r u e; (\neg f_{j} \land C_{j, k})) \supset \neg ◊_{r} (C_{j, k}^{'} \land G_{j}) \end{aligned}$ (15) (17) Here (15) partitions the equivalence in the scope of $◻$ from its LHS, which appears in (14) into a forward implication and a backward implication. These two implications can be transformed into formulas with the designated occurrence of $◊_{r} F_{j}$ extracted from the scope of $◻$ and chop using (16) and (17), respectively.

To understand the RHS of (16), assume that it is evaluated at $σ, a, b$ . Then, if $f_{j} \in σ^{c}$ for some m such that $a \leq m \leq b$ , either $σ, m, c ⊨ F_{j}$ for some $c \leq b$ , of, if this is not the case, assuming k to be the unique one for which $σ, m, b ⊨ C_{j, k}$ , we also have $σ, b, d ⊨ C_{j, k}^{'} \land G_{j}$ for some $d \geq b$ . Since $σ, m, b ⊨ C_{j, k}$ and $σ, b, d ⊨ C_{j, k}^{'}$ jointly imply $σ, m, d ⊨ C_{j}$ by Lemma 3.5, and $σ, b, d ⊨ G_{j}$ is equivalent to $σ, c, d ⊨ G_{j}$ for $◊_{r}$ -formulas such as $G_{j}$ , this implies $σ, m, d ⊨ F_{j}$ . Hence, all in all, the RHS of (16) states that $σ, m, d ⊨ F_{j}$ for m such that $a \leq m \leq b$ and $f_{j} \in σ^{m}$ , with the cases of $d = c \leq b$ and $d \geq b$ considered separately. This is the meaning of the LHS of (16).

To understand the RHS of (17), assume that it is evaluated at $σ, a, b$ again. Then the left conjunct states that $F_{j}$ cannot be satisfied at intervals m, c such that $a \leq m \leq c \leq b$ and $f_{j} \notin σ^{m}$ . The right conjunct states that, if $σ, m, b ⊨ C_{j, k}$ , then no interval of the form b, d satisfies $C_{j, k}^{'} \land G_{j}$ . Since $σ, m, b ⊨ C_{j, k}$ and $σ, b, d ⊨ \neg C_{j, k}^{'}$ jointly imply $σ, m, d ⊨ \neg C_{j}$ by Lemma 3.5, and, just like in (16), $σ, b, d ⊨ G_{j}$ is equivalent to $σ, m, d ⊨ G_{j}$ for $◊_{r}$ -formulas such as $G_{j}$ , this means that $σ, m, d ⊭ F_{j}$ for all $d \geq b$ . Together with $σ, m, c ⊭ F_{j}$ for $c \leq b$ , this implies $σ, m, d ⊭ F_{j}$ for all m such that $a \leq m \leq b$ , $f_{j} \notin σ^{m}$ and all $d \geq m$ . This is the meaning of the LHS of (17).

The formulas on the RHS of ≡ in these equivalences have occurrences in the left operands of chop of $F_{j}$ , whose subformula $G_{j}$ is a conjunction of possibly negated future $◊_{r}$ -formulas. These $◊_{r}$ -formulas can be extracted from the scope of chop because $h_{◊_{r}} (G_{j}) = h_{◊_{r}} (F_{j}) < h_{◊_{r}} (◊_{r} F_{j}) = h_{◊_{r}} (B)$ and $h_{*} (G_{j}) = h_{*} (H_{u}) < h_{*} (B)$ . The equivalences (14), (16) and (17) are sufficient to extract $◊_{r} F_{1}$ , …, $◊_{r} F_{v}$ from the scope of chop-star while still bearing with the quantifier prefix $\exists p_{1} \dots \exists p_{u} \exists f_{1} \dots \exists f_{v}$ .

Similar equivalences can be written about $◊_{l} P_{1}$ , …, $◊_{l} P_{u}$ . The simpler form $◻ (p_{i} \equiv ◊_{l} P_{i})$ of $◻ (p_{i} \equiv ((e m p t y \land ◊_{l} P_{i}); t r u e))$ can be used in (14).

This leads to transforming (14) into a formula which is equivalent to B and has the form $\exists p_{1} \dots \exists p_{u} \exists f_{1} \dots \exists f_{v} B^{'}$ where $B^{'}$ , the result of applying the above equivalences and their mirrors, is separated.

To complete the transformations, the quantifier prefix $\exists p_{1} \dots \exists p_{u} \exists f_{1} \dots \exists f_{v}$ must be eliminated too. To do this, we observe that the $◊_{r}$ -subformulas and the $◊_{l}$ -subformulas which appear on the RHS of ≡ in (16) and (17), and their time mirror formulas) that become part of the separated formula $B^{'}$ have no occurrences of $p_{1}, \dots, p_{u}, f_{1}, \dots, f_{v}$ . They are linked to other subformulas in the scope of this quantifier prefix, which probably have such occurrences, by Boolean connectives only. Those other subformulas are introspective. Hence the $◊_{r}$ -subformulas and the $◊_{l}$ -subformulas can be taken out of the scope of $\exists p_{1} \dots \exists p_{u} \exists f_{1} \dots \exists f_{v}$ by first obtaining a DNF of its operand and then using the distributivity of $\exists p$ over $\lor$ and the validity of the equivalences $\exists p (X \land Y) \equiv X \land \exists p Y and \exists p X \equiv X, for X such that p \notin V a r (X) .$ This concludes the proof because propositional quantification can be eliminated in $I T L$ , where only the introspective operators chop and chop-star are allowed.

Theorem 2.2 with chop-star included follows from Lemma 3.11, together with Lemmas 3.7 and 3.8.

Correction

3.3. Extracting $◊_{l}$ and $◊_{r}$ from the scope of chop-star

Information for

Open access

Opportunities

Help and information

Correction

3.3. Extracting ◊l and ◊r from the scope of chop-star

Reprints and Corporate Permissions

Academic Permissions

Related research

To cite this article:

Download citation

Your download is now in progress and you may close this window

Login or register to access this feature

Information for

Open access

Opportunities

Help and information

Keep up to date

3.3. Extracting $◊_{l}$ and $◊_{r}$ from the scope of chop-star