A Proof System for a Unified Temporal Logic

Abstract

Theorem proving is a widely used approach to the verification of computer systems, and its theoretical basis is generally a proof system for formal derivation of logic formulas. In this paper, we propose a proof system for Propositional Projection Temporal Logic (PPTL) with indexed expressions, which is a unified temporal logic that subsumes the well-used Linear Temporal Logic (LTL). First, the syntax, semantics and logic laws of PPTL that allows indexed expressions are introduced, and the representation of LTL constructs by PPTL formulas is shown. Then, the proof system for the logic is presented which consists of axioms and inference rules for the derivation of both basic constructs and indexed expressions of PPTL. To show the capability of the proof system, several examples of formal proofs are provided. Finally, the soundness of the proof system is demonstrated.

This research is supported by the NSFC Grant Nos. 61751207, 61732013, 61672403, and 61572386.

1 Introduction

Projection Temporal Logic (PTL) [3] is an extension of Interval Temporal Logic (ITL) [13] by introducing a new projection construct and supporting both finite and infinite timeline. Within the PTL framework, Propositional PTL (PPTL) is proved to have the full regular expressiveness [18], and its decision problem has been solved [5]. Further, Modeling, Simulation and Verification Language (MSVL) [7], an executable subset of PTL armed with a framing technique, is defined as the language for system modeling. Based on these theoretical work, a unified model checking [2] approach with PTL is developed for formal verification of computer systems [4, 20].

The advantage of the model checking approach is that verification can be done automatically. However, it suffer from the state explosion problem and thus less suitable to verify data intensive applications. Another approach to system verification widely used in practice is theorem proving [10], in which a proof system for a specific logic, usually a temporal logic, is constructed in terms of axioms and inference rules. To verify whether a computer system satisfies a desired property, both the system and the property are characterized by formulas S and P of the logic, respectively. Then, the problem is to check whether $S\rightarrow P$ can be proved formally by the axioms and inference rules of the proof system. Generally, such a verification process involves human assistance and can be done semi-automatically. The advantage of theorem proving is that it avoids the state explosion problem and can verify both finite-state and infinite-state systems, including data intensive applications.

In the past three decades, a number of proof systems for Liner Temporal Logic (LTL), Computing Tree Logic (CTL) and other temporal logics have emerged [9, 11, 12]. However, the expressive power of these logics is weaker than ITL or PPTL. Within the ITL community, several researchers have investigated axiomatic systems with different extensions. Rosner and Pnueli [16] present a proof system for a propositional choppy logic with chop, next and until operators. Bowman and Thompson provide a completeness proof and a tableau-based decision procedure for PITL with projection over finite intervals [1]. Moszkowski proposes an axiom system over finite intervals for PITL, and later extends the work to infinite intervals [14]. Besides, two proof systems are formalized for PPTL [8] and PTL [17], respectively.

A recent study [6] extends PPTL with indexed expressions that take the form of $\bigvee _{i\in \mathbb {N}}R[i]$. Although indexed expressions are obtained by applying the syntax rules countably infinitely many times, they have definite semantics and certain good properties. Especially, they can equivalently represent the strong until $\mathsf {U}$ and weak until $\mathsf {W}$ constructs of LTL. As a result, PPTL with indexed expressions is a unified temporal logic that involves LTL as one of its subsets.

To employ PPTL and the indexed-expression technique to system verification in the theorem proving approach, we develop a proof system $\varPi$ for the unified logic in this paper. Specifically, $\varPi$ consists of two sub-systems of axioms and inference rules. The first sub-system is provided for formal proof of basic PPTL constructs, such as next, projection, always and chop plus. The second sub-system is designed especially for formal derivation of formulas with indexed expressions. We provide a few examples to show how the proof system $\varPi$ works, and demonstrate its soundness that every formula proved by $\varPi$ is valid.

The paper is organized as follows. The next section introduces PPTL, including indexed expressions and their capability of representing LTL. Then, Sect. 3 presents our proof system in terms of axioms and inference rules and Sect. 4 provides examples of formal proofs with the proof system. In Sect. 5, the soundness of the proof system is demonstrated. Finally, conclusions are drawn in Sect. 6 with a discussion on potential future work.

2 Propositional Projection Temporal Logic

We first introduce basic notions of Propositional Projection Temporal Logic (PPTL) [3]. Let ${\mathcal {P}}$ be a countable set of atomic propositions and the boolean domain. Usually, we use small letters, possibly with subscripts, like $p, q, r_1$, to denote atomic propositions in ${\mathcal {P}}$ and capital letters, possibly with subscripts, like $P, Q, R_1$, to represent general PPTL formulas. Formally, the formulas of PPTL are inductively defined by the following syntax:

$$\begin{aligned} \begin{array}{lllr} P &{} {:}{:}{=} &{} q~|~\lnot P~|~P \wedge P ~|~\bigcirc P~|~(P^{[+]})\mathsf {\,prj\,\,}P &{} \\ P^{[+]} &{} {:}{:}{=} &{} P~|~P,P^{[+]} &{} \end{array} \end{aligned}$$

where $P^{[+]}$ represents a finite sequence of PPTL formulas separated by commas. For simplicity, some previous publications of PPTL, such as [3, 18], use the syntax defined as follows.

$$\begin{aligned} P\,{:}{:}\,{=}\,q~|~\lnot P~|~P_{1}\wedge P_{2}~|~\bigcirc P~|~(P_{1},\ldots , P_{m})\mathsf {\,prj\,\,}P \end{aligned}$$

It is trivial to prove that the two definitions are equivalent. Notice that $\bigcirc \, \text{(next) }$, and $\mathsf {\,prj\,\,}\text{(projection) }$ are temporal operators, while $\lnot$ and $\wedge$ are defined as they are in classical propositional logic. A formula is called a state formula if it does not contain any temporal operators.

In the semantics of PTL, formulas are interpreted upon intervals. An interval $\sigma = \langle s_0, s_1, \ldots \rangle$ is a non-empty sequence of states, finite or infinite, while a state s is a mapping from ${\mathcal {P}}$ to $\mathbb {B}$. The length of an interval $\sigma$, denoted as $|\sigma |$, is the number of states in $\sigma$ minus one if $\sigma$ is finite; or the smallest infinite ordinal $\omega$ if $\sigma$ is infinite. Let $\mathbb {N}$ denote the set of natural numbers. To have a uniform notation for both finite and infinite intervals, we use extended natural numbers as indices, that is $\mathbb {N}_{\omega }=\mathbb {N}\cup \{\omega \}$, and extend the comparison operators, $=, <,\le$, to $\mathbb {N}_{\omega }$ by considering $\omega = \omega$ and for all $i\in \mathbb {N}$, $i<\omega$. Moreover, we write $\preceq$ as $\le -\{(\omega ,\omega )\}$. To simplify definitions, we denote $\sigma$ by $\langle s_0,\cdots , s_{|\sigma |}\rangle$, where $s_{|\sigma |}$ is undefined if $\sigma$ is infinite. With such a notation, $\sigma _{(i..j)}$ $(0\le i \preceq j \le |\sigma |)$ denotes a sub-interval $\langle s_i , \cdots , s_j\rangle$.

To formalize the semantics of the projection construct $\mathsf {prj}$, we define an auxiliary operator $\downarrow$ to get rid of singleton points. For an interval $\sigma$ and natural numbers $i_0 \le \ldots \le i_m$ $(m \in \mathbb {N})$, $\sigma \downarrow (i_0, \ldots , i_m)$ denotes the interval obtained from $\sigma$ by preserving only states with non-repeated indices from $i_l$ $(0\le l\le m)$. For example, $\langle s_0, s_1, s_2, s_3, s_4\rangle \downarrow (0, 0, 2, 2, 2, 3) = \langle s_0, s_2, s_3 \rangle$. In addtion, we use $\sigma \cdot \sigma '$ to denote the concatenation of two intervals $\sigma$ and $\sigma '$, provided $\sigma$ is finite.

An interpretation is a tuple $\mathcal{I}=(\sigma ,k,j)$, where $\sigma =\langle s_{0},s_{1},\ldots \rangle$ is an interval, $k\in \mathbb {N}$ and $j\in \mathbb {N}_{\omega }$ with $0\le k \le j \le |\sigma |$. For a PPTL formula P, $\mathcal{I}\models P$ denotes that $\mathcal{I}$ is an interpretation of P, defined inductively as follows. Intuitively, it means that P is interpreted over the subinterval $\sigma _{(k..j)}$ of $\sigma$ with the current state being $s_{k}$.

Fig. 1.

Possible interpretations of $(P_1,P_2,P_3)\mathsf {\,prj\,\,}Q$

The projection construct $(P_1,\ldots ,P_m)\mathsf {\,prj\,\,}Q$ is a key operator of PPTL, which has potential applications for compositional reasoning about concurrent systems. The construct allows formulas $P_1,\ldots ,P_m,Q$ to be autonomous, each interpreted in its own interval. Specifically, two different time scales exist, where $P_1,\ldots ,P_m$ are interpreted over a series of fine-grained intervals while Q is interpreted over a coarse-grained projected interval. In particular, the sequence of $P_1,\ldots ,P_m$ and Q may terminate at different time points. The intuition of $(P_1,P_2,P_3)\mathsf {\,prj\,\,}Q$ is shown in Fig. 1.

A formula P is satisfied by an interval $\sigma$, denoted by $\sigma \models P$, if $(\sigma ,0,|\sigma |) \models P$. A formula P is satisfiable if $\sigma \models P$ for some $\sigma$ while a formula P is valid, denoted by $\models P$, if $\sigma \models P$ for all intervals $\sigma$. The abbreviations such as , , $\vee$, $\rightarrow$ and $\leftrightarrow$ are defined as usual. Some derived formulas of PPTL are shown below. They are useful in characterizing various temporal properties.

The empty formula $\varepsilon$ means that the current state is the last one of the interval, and the chop construct P; Q means the sequential composition of P and Q. Besides, the sometimes construct $\Diamond P$ (resp. always construct $\Box P$) indicates P holds at some state (resp. every state) from the current state on. The meaning of the chop plus construct $P^{+}$ (resp. chop star construct $P^{*}$) is as usual, i.e., P holds repeatedly for one or more (resp. zero or more) times. Then, $\mathsf {halt}(P)$ and $\mathsf {final}(P)$ say that P holds at the last state of the interval, while $\mathsf {halt}(P)$ also requires P holds only at the last state. The formula $\mathsf {keep}(P)$ (resp. $\mathsf {rem}(P)$) means that P holds at every state that has a next (resp. previous) state in the interval. In addition, $\mathsf {fin}$ (resp. $\mathsf {inf}$) indicates the interval is finite (resp. infinite), and $\mathsf {ln}(n)$ claims that the length of the remaining interval is exactly n. Finally, the parallel construct $P~ \Vert ~ Q$ means that P and Q are interpreted in parallel.

We denote $\models P\leftrightarrow Q$ by $P \equiv Q$ (equivalence), and $\models P\rightarrow Q$ by $P \subset Q$ (strong implication). Some logic laws of PPTL are provided as follows, whose proofs can be found in [3].

2.1 Indexed Expression

Generally, a well-formed formula of PPTL is constructed by applying the syntax rules finitely many times. However, some formulas formed by applying the syntax rules countably infinitely many times, such as $\bigvee _{i\in \mathbb {N}}\bigcirc ^i P$, have definite semantics and good properties.

A recent work [6] studies a kind of such formulas, namely indexed expressions, which are of the form $\bigvee _{i\in \mathbb {N}}R[i]$ where R[i] is a well-formed formula with an index $i\in \mathbb {N}$. Specifically, R[i] may contain sub-formulas such as $\bigcirc ^i P$, $P^{i}$ and $P^{(i)}$. For $i\in \mathbb {N}$, $\bigcirc ^i P$ is the application of the next operator to P for i times, $P^{i}$ means P holds repeatedly for i times, while $P^{(i)}$ means P holds at the consecutive i states from the current state on. Formally, they are defined as follows.

The semantics of an indexed expression is clear. Let $\mathcal{I}$ be an interpretation.

$$\begin{aligned} \mathcal{I} \models \bigvee _{i\in \mathbb {N}}R[i] \qquad \text{ iff } \text{ there } \text{ exists } i\in \mathbb {N} \text{ such } \text{ that } \mathcal{I} \, \models \, R[i] \end{aligned}$$

Intuitively, $\bigvee _{i\in \mathbb {N}}R[i]$ means some R[i] holds for $i\in \mathbb {N}$. From now on, we consider PPTL with indexed expressions in that a formula may contain indexed expression(s) as its sub-formula(s). Nevertheless, it is good that indexed expressions do not occur nested, since R[i] in $\bigvee _{i\in \mathbb {N}}R[i]$ is a well-formed formula.

To avoid excessive use of parentheses, we specify the precedence of operators as: 1. $+$, $*$; 2. $\lnot$, $\bigcirc$, $\Box$, $\Diamond$, $\mathsf {prj}$; 3. $\wedge$; 4. $\bigvee _{i\in \mathbb {N}}$; 5. $\vee$; 6. $\; \mathbf ; \,$; 7. $\Vert$; 8. $\rightarrow$; 9. $\leftrightarrow$, where 1 = highest and 9 = lowest.

Fig. 2.

Intuitive meaning of $p~\mathsf {U}~q$ (see (a)) and $p~\mathsf {W}~q$ (see (a) or (b))

Indexed expressions of the form $\bigvee _{i\in \mathbb {N}}P^{(i)} \wedge \bigcirc ^i Q$ are closely related to the recursive equation $X \equiv Q \vee P \wedge \bigcirc X$ [6], shown by the following lemmas.

Lemma 1

The recursive equation $X \equiv Q \vee P \wedge \bigcirc X$ has exactly two solutions: $\bigvee _{i\in \mathbb {N}}P^{(i)} \wedge \bigcirc ^i Q$ and .

Lemma 2

Let X be a formula satisfying $X \equiv Q \vee P \wedge \bigcirc X$, then

• 1. $X \subset \Diamond Q$ iff $X \equiv \bigvee _{i\in \mathbb {N}}P^{(i)} \wedge \bigcirc ^i Q$, and

• 2. iff .

Many cases of indexed expressions are intrinsically well-formed in that they are equivalent to well-formed formulas. Specifically, we have the following logic laws. Most of the laws are proved using the above lemmas, the others are proved by the fixed-point induction approach [19].

2.2 Representing Linear Temporal Logic

Linear Temporal Logic (LTL) [15] is a well-known temporal logic, which is based on a linear-time perspective and defined over an infinite interval. Usually, LTL refers to the propositional subset of LTL which has been widely used in practice. In LTL, the most prominent operators are strong until $\,\mathsf {U}$ and weak until $\,\mathsf {W}$, which is a weak version of $\mathsf {U}$. Their intuitive meanings are shown in Fig. 2 and more details can be found in [2].

We show that both the strong until and weak until operators can be represented as PPTL formulas with indexed expressions. Suppose $(P\,\mathsf {U}\,Q)_{\mathsf P}$ and $(P\,\mathsf {W}\,Q)_{\mathsf P}$ are PPTL formulas that have the same meaning as $P\,\mathsf {U}\,Q$ and $P\,\mathsf {W}\,Q$, respectively. Then, both $(P\,\mathsf {U}\,Q)_{\mathsf P}$ and $(P\,\mathsf {W}\,Q)_{\mathsf P}$ satisfy the recursive equation $X \equiv Q\wedge \mathsf {inf}\vee P\wedge \lnot Q\wedge \bigcirc X$. In addition, they satisfy $(P\,\mathsf {U}\,Q)_{\mathsf P} \subset \Diamond (Q\wedge \mathsf {inf})$ and . According to Lemma 2, we have

Therefore, we can simply define the two operators in PPTL in the following way.

On the other hand, except $\mathsf {U}$ and $\mathsf {W}$, every construct of LTL has a direct counterpart in PPTL. As a result, PPTL with indexed expressions is a unified temporal logic that subsumes LTL.

3 Proof System

This section presents the proof system $\varPi$ for PPTL with indexed expressions, consisting of a set of axioms and inference rules. Each axiom defines a formula that can be directly derived by the system, and each inference rule defines a one-step derivation of a conclusion formula from one or more hypothesis formulas.

A formal proof (or formal derivation) of a formula P is a sequence of formulas $P_0, \ldots , P_n$ $(n\in \mathbb {N})$ such that $P_n = P$ and each $P_i$ $(0 \le i \le n)$ is either an axiom or the conclusion formula of an inference rule, provided every hypothesis formula of the rule has occurred in the preceding formulas $P_0, \ldots , P_{i-1}$. If such a formal proof exists, we say that P is proved by $\varPi$ or P is a theorem of $\varPi$, denoted as $\vdash _{\varPi } P$. When there is no confusion, we omit the subscript and simply write $\vdash P$.

Specifically, the proof system $\varPi$ is composed of two parts: axioms and inference rules $\varPi _B$ for basic constructs, such as next and projection, and those $\varPi _I$ for indexed expressions, i.e. $\varPi = \varPi _B\cup \varPi _I$.

3.1 Axioms and Inference Rules for Basic Constructs

A proof system for basic constructs of PPTL has been proposed in [8], which adopts a relatively complex version of syntax that considers a projection-plus construct $(P_1,\ldots , (P_i,\ldots ,P_j)^{\oplus }, \ldots , P_m) \mathsf {\,prj\,\,}Q$ as a basic construct. Here, we provide $\varPi _B$, an equivalent but more concise presentation of the proof system, based on the current version of syntax considering the projection construct instead of the projection-plus construct.

Let S denote a state formula and $\varOmega$ represent a finite sequence of formulas, which is possible the empty sequence $\tau$. For convenience, we define $(\tau ) \mathsf {\,prj\,\,}P$ to be P. The set of axioms of $\varPi _B$ are presented as follows.

Intuitively, an axiom is a formula that is supposed to be valid. Especially, the validity of a formula $P \leftrightarrow Q$ means that P and Q are equivalent.

The set of inference rules of $\varPi _B$ are presented as follows.

The rule MP is the classic rule of modus ponens for propositional logic. And in the rule SUB, P(Q) denotes a formula P with a sub-formula Q, and $P(Q')$ is the formula obtained from P(Q) by substituting Q with $Q'$. Intuitively, an inference rule means: if the hypothesis formulas are all valid, the conclusion formula is also valid. More explanations of these axioms and inference rules can be found in [8].

3.2 Axioms and Inference Rules for Indexed Expressions

We propose a proof (sub-)system $\varPi _I$ to reason about PPTL formulas with indexed expressions. The set of axioms of $\varPi _I$ are presented as follows. Here, P denotes a formula without any index.

$$\begin{aligned} \begin{array}{l@{\quad }l@{\quad }l@{\quad }l} {\textsf {IST}} &{} \bigvee _{i\in \mathbb {N}}Q^i \leftrightarrow Q^*\\ {\textsf {INS}} &{} R[i] \rightarrow \bigvee _{i\in \mathbb {N}}R[i] &{} {\textsf {INR}} &{} \bigvee _{i\in \mathbb {N}}R[i] \leftrightarrow R[0] \vee \bigvee _{i\in \mathbb {N}}R[i+1] \\ {\textsf {INA}} &{} \bigvee _{i\in \mathbb {N}}P\wedge R[i] \leftrightarrow P\wedge \bigvee _{i\in \mathbb {N}}R[i] &{} {\textsf {INO}} &{} \bigvee _{i\in \mathbb {N}}(P\vee R[i]) \leftrightarrow P\vee \bigvee _{i\in \mathbb {N}}R[i] \\ {\textsf {INN}} &{} \bigvee _{i\in \mathbb {N}}\bigcirc R[i] \leftrightarrow \bigcirc \bigvee _{i\in \mathbb {N}}R[i] &{} {\textsf {INC}} &{} \bigvee _{i\in \mathbb {N}}(P\; \mathbf ; \,R[i]) \leftrightarrow P\; \mathbf ; \,\bigvee _{i\in \mathbb {N}}R[i] \\ \end{array} \end{aligned}$$

Among the axioms, IST indicates that an indexed expression $\bigvee _{i\in \mathbb {N}}Q^i$ can always be replaced by the star construct $Q^*$. In fact, both the formulas mean that P holds repeatedly for zero or more times. Then, INS and INR reflect two standard property of the infinite disjunction operator $\bigvee _{i\in \mathbb {N}}$. In addition, INA, INO, INN and INC indicate that the and, or, next and chop operators are distributive over the infinite disjunction operator, respectively.

The set of inference rules of $\varPi _I$ are presented as follows.

Among the inference rules, INM indicates that the infinite disjunction operator is monotonic. Besides, REF and REI are provided for solving R from the recursive biconditional “equation” $R \leftrightarrow Q\vee P\wedge \bigcirc R$. The solution is in the form of an indexed expression, possibly in disjunction with a specific always formula. Intuitively, REF and REI are in accordance with the two cases of Lemma 2 that the recursion is made for finitely many times and for possibly infinitely many times, respectively.

The approach of theorem proving can be applied to verify properties of systems formally. First, both a system and a desired property are specified by PPTL formulas S and P, respectively. Then, the system satisfies the property if and only if we can find a formal proof of $\vdash S\rightarrow P$ by the proof system $\varPi$.

4 Examples of Formal Proofs

To show the capability of the proof system $\varPi$, we provided a few examples of formal proofs. Notice that once $\vdash P$ is proved, P is a theorem of the system and can be used in the formal proof of other formulas.

Example 1

$\vdash \mathsf {keep}(P) \leftrightarrow \varepsilon \vee P\wedge \bigcirc \mathsf {keep}(P)$. The theorem is denoted as T1, whose formal proof is given as follows. Recall that and .

Example 2

$\vdash \Diamond P \leftrightarrow P \vee \bigcirc \Diamond P$. The theorem is denoted as T2, whose formal proof is given as follows. Recall that $\Box P = \lnot \Diamond \lnot P$ for any formula P.

Example 3

$\vdash \bigvee _{i\in \mathbb {N}}\bigcirc ^i Q \leftrightarrow \Diamond Q$. This theorem is denoted as T3, whose formal proof is given as follows.

Intuitively, the indexed expression $\bigvee _{i\in \mathbb {N}}\bigcirc ^i Q$ means Q must hold at some state, which is equivalently characterized by the well-formed formula $\Diamond Q$.

Example 4

$\vdash \bigvee _{i\in \mathbb {N}}P^{(i)} \wedge \bigcirc ^i Q \rightarrow \Diamond Q$. This theorem is denoted as T4, whose formal proof is given as follows.

The intuition of T4 is that the indexed expression $\bigvee _{i\in \mathbb {N}}P^{(i)} \wedge \bigcirc ^i Q$ implies Q must hold at some state.

Example 5

. This theorem is denoted as T5, whose formal proof is given as follows. Recall that for any formula P.

Intuitively, the formula with an indexed expression means that the current interval is either finite or infinite and P keeps holding at every non-final state, which is equivalently characterized by the well-formed formula $\mathsf {keep}(P)$.

Example 6

$\vdash P\,\mathsf {U}\,Q \leftrightarrow \mathsf {inf}\wedge \bigvee _{i\in \mathbb {N}}P^{(i)} \wedge \bigcirc ^i Q$. This theorem is denoted as T6, whose formal proof is given as follows. Recall that $P\,\mathsf {U}\,Q = \mathsf {inf}\wedge \bigvee _{i\in \mathbb {N}}(P \wedge \lnot Q)^{(i)} \wedge \bigcirc ^i Q$.

T6 indicates that the representation of $P\,\mathsf {U}\,Q$ can be simplified by replacing the indexed expression $\bigvee _{i\in \mathbb {N}}(P\wedge \lnot Q)^{(i)} \wedge \bigcirc ^i Q$ with a relatively concise one $\bigvee _{i\in \mathbb {N}}P^{(i)} \wedge \bigcirc ^i Q$. Intuitively, the former indexed expression means that P holds until Q holds for the first time, and the latter indexed expression means that P holds until sometimes Q holds. These meanings are actually equivalent.

5 Soundness

An observation about the examples presented in the previous section is that many theorems of the proof system $\varPi$ coincide with the logic laws of PPTL. For instance, $\bigvee _{i\in \mathbb {N}}\bigcirc ^i Q \leftrightarrow \Diamond Q$ is a theorem (T3), and there is a logic law $\bigvee _{i\in \mathbb {N}}\bigcirc ^i Q \equiv \Diamond Q$ which means the formula $\bigvee _{i\in \mathbb {N}}\bigcirc ^i Q \leftrightarrow \Diamond Q$ is valid.

In fact, this is a universal phenomenon. We are going to show that the proof system $\varPi$ is sound, i.e., each theorem proved by $\varPi$ is valid.

For this, we first establish the soundness of axioms and inference rules of $\varPi$. On the one hand, each axiom is a valid formula. On the other hand, the conclusion formula of each inference rule is valid, provided all the hypothesis formulas are valid.

Theorem 1

(Soundness of Axioms and Inference Rules). Each axiom or inference rule of $\varPi$ is sound, in that

• 1. $\models P$ if P is an axiom of $\varPi$, and

• 2. $\models P$ if $\begin{array}{c} P_1\ \ \cdots \ \ P_n \\ \hline P \end{array}$ is an inference rule of $\varPi$ $(n\ge 1)$ and $\models P_i$ for each $1\le i\le n$.

The proof of Theorem 1 is presented in the Appendix of this paper.

As a natural deduction of Theorem 1, every formula proved by $\varPi$ is valid. That is, the proof system $\varPi$ is sound.

Theorem 2

(Soundness of $\varPi$). For each PPTL formula P, $\vdash P$ implies $\models P$.

Proof

$\vdash P$ means there is a formal proof $P_1,\ldots ,P_n$ $(n\ge 1)$ with $P_n=P$. According to Theorem 1, $\models P_i$ for each $1\le i\le n$. This involves $\models P$. $\square$

6 Conclusions

In this paper, we develop a proof system $\varPi$ for PPTL with indexed expressions, which is a unified temporal logic that subsumes the well-used LTL. Specifically, $\varPi$ consists of axioms and inference rules for formal derivation of both basic PPTL constructs and indexed expressions. We provide a few examples to show how the proof system works. In addition, we demonstrate $\varPi$ is sound in that every formula proved by $\varPi$ is valid.

In the near future, we are going to prove the completeness of $\varPi$, i.e., every valid formula can also be proved formally by $\varPi$. This may be achieved by studying the normal form of indexed expressions and then making structural induction based on the normal form. We also plan to explore more meaningful styles of indexed expressions other than $\bigvee _{i\in \mathbb {N}}Q^{i}$ and $\bigvee _{i\in \mathbb {N}}P^{(i)} \wedge \bigcirc ^i Q$, including their logic laws and relation with specific recursive equations. Which styles of indexed expressions have equivalent well-formed formulas is still an open question.

Appendix

This appendix presents the proof of Theorem 1.

Proof

We only need to prove the soundness of axioms and inference rules in $\varPi _I$. The soundness of axioms and inference rules in $\varPi _B$ has been proved in [8].

(IST) For any interval $\sigma$, we have

which indicates $\sigma \models \bigvee _{i\in \mathbb {N}}Q^i \leftrightarrow Q^*$. Recall that $Q^*= \varepsilon \vee Q^+$.

(INS) For any interval $\sigma$, we have

$$\begin{aligned} \begin{array}{lll} &{} \sigma \models R[i] \\ \Longrightarrow &{} \sigma \models R[i] \text{ for } \text{ some } i\in \mathbb {N}\\ \Longleftrightarrow &{} \sigma \models \bigvee _{i\in \mathbb {N}}R[i] \\ \end{array} \end{aligned}$$

which indicates $\sigma \models R[i] \rightarrow \bigvee _{i\in \mathbb {N}}R[i]$.

(INR) For any interval $\sigma$, we have

$$\begin{aligned} \begin{array}{lll} &{} \sigma \models \bigvee _{i\in \mathbb {N}}R[i] \\ \Longleftrightarrow &{} \sigma \models R[i] \text{ for } \text{ some } i\in \mathbb {N}\\ \Longleftrightarrow &{} \sigma \models R[0] \text{ or } \sigma \models R[i+1] \text{ for } \text{ some } i\in \mathbb {N}\\ \Longleftrightarrow &{} \sigma \models R[0] \text{ or } \sigma \models \bigvee _{i\in \mathbb {N}}R[i+1] \\ \end{array} \end{aligned}$$

which indicates $\sigma \models \bigvee _{i\in \mathbb {N}}R[i] \leftrightarrow R[0]\vee \bigvee _{i\in \mathbb {N}}R[i+1]$.

(INA) For any interval $\sigma$, we have

$$\begin{aligned} \begin{array}{lll} &{} \sigma \models \bigvee _{i\in \mathbb {N}}P\wedge R[i] \\ \Longleftrightarrow &{} \sigma \models P\wedge R[i] \text{ for } \text{ some } i\in \mathbb {N}\\ \Longleftrightarrow &{} \sigma \models P \text{ and } \sigma \models R[i] \text{ for } \text{ some } i\in \mathbb {N}\\ \Longleftrightarrow &{} \sigma \models P \text{ and } \sigma \models \bigvee _{i\in \mathbb {N}}R[i] \\ \end{array} \end{aligned}$$

which indicates $\sigma \models \bigvee _{i\in \mathbb {N}}P\wedge R[i] \leftrightarrow P\wedge \bigvee _{i\in \mathbb {N}}R[i]$. The proofs of (INO), (INN) and (INC) are similar.

(INM) Suppose $\models R[i]\rightarrow R'[i]$. Then, for any interval $\sigma$, $\sigma \models R[i]$ implies $\sigma \models R'[i]$. So, for any interval $\sigma$, $\sigma \models R[i]$ for some $i\in \mathbb {N}$ implies $\sigma \models R'[i]$ for some $i\in \mathbb {N}$, which means $\sigma \models \bigvee _{i\in \mathbb {N}}R[i]$ implies $\sigma \models \bigvee _{i\in \mathbb {N}}R'[i]$, or equivalently $\sigma \models \bigvee _{i\in \mathbb {N}}R[i]\rightarrow \bigvee _{i\in \mathbb {N}}R'[i]$.

(REF) Suppose $\models R\leftrightarrow Q\vee P\wedge \bigcirc R$ and $\models R\rightarrow \Diamond Q$. Then, $R \equiv Q\vee P\wedge \bigcirc R$ and $R \subset \Diamond Q$. According to Lemma 2, $\bigvee _{i\in \mathbb {N}}P^{(i)} \wedge \bigcirc ^i Q \equiv R$, which means $\models \bigvee _{i\in \mathbb {N}}P^{(i)} \wedge \bigcirc ^i Q \leftrightarrow R$. The proof of (REI) is similar. $\square$