Visibly Linear Temporal Logic

We introduce Visibly Linear Temporal Logic (VLTL), a linear-time temporal logic that captures the full class of Visibly Pushdown Languages over infinite words. The novel logic avoids fix points and instead provides natural temporal operators with simple and intuitive semantics. We prove that the complexities of the satisfiability and visibly pushdown model checking problems are the same as for other well known logics, like CaRet and the nested word temporal logic NWTL, which in contrast are strictly more limited in expressive power than VLTL. Moreover, formulas of CaRet and NWTL can be translated inductively and in linear-time into VLTL.

1. From [7, 14]: “PSL and SVA balance well [...] expressiveness, usability, and implementability.”

2. The origin of the name \(M\)-substitution is minimally well-matched substitution, while \(S\)-closure stands for Strict Minimally Well-Matched Closure, see [11, 12].

3. Recall that \(F\subseteq \mathsf {M}\) and moves from secondary states lead to secondary states as well.

4. AJA are strictly more expressive than their non-deterministic counterpart [10].

We would like to acknowledge the anonymous reviewers for their feedback and numerous suggestions about how to improve this paper. This work was funded in part by Spanish MINECO (Projects TIN2012-39391-CA04-01 STRONGSOFT, TIN2012-38137-C02 VIVAC, and TIN2015-71819-P RISCO), by the Madrid Regional Government under project N-Greens Software-CM (S2013/ICE-2731) and by EU COST Action IC1402 ArVi.

Authors and Affiliations

1. Technical University of Madrid (UPM), Madrid, Spain

   Laura Bozzelli

2. IMDEA Software Institute, Madrid, Spain

   César Sánchez

3. Institute for Applied Physics, CSIC, Madrid, Spain

   César Sánchez

Corresponding author

Correspondence to César Sánchez.

A preliminary version of this paper appears in the Proceedings of the 7th International Joint Conference on Automated Reasoning (IJCAR’14), Vienna, Austria, July 19–22, 2014.

Appendix: From NVPA to Well-Formed VRE

In this section we prove the following result.

Theorem 9

Given an NVPA \(\mathcal {P}\), one can construct a well-formed VRE \(\alpha \) such that \(\mathcal {L}(\alpha )=\mathcal {L}(\mathcal {P})\).

In order to prove Theorem 9, we need additional definitions. We fix an NVPA \(\mathcal {P}=\langle Q,Q_{0},\varGamma ,\varDelta ,F \rangle \) over the pushdown alphabet \(\varSigma \). Given \(q,p\in Q\), a summary of \(\mathcal {P}\) from q to p is a run \(\pi \) of \(\mathcal {P}\) over some word \(w\in MWM (\varSigma )\) from a configuration of the form \((q,\beta )\) to a configuration of the form \((p,\beta ')\) for some stack contents \(\beta \) and \(\beta '\). Observe that if \(\pi \) is such a run over \(w\in MWM (\varSigma )\) from \((q,\beta )\) to \((p,\beta ')\), then \(\beta '=\beta \) and the portion of the stack corresponding to \(\beta \) is never read in \(\pi \). In particular, there is also a run of \(\mathcal {P}\) from \((q,\bot )\) to \((p,\bot )\) over w which uses the same transitions used by \(\pi \). Given a run \(\pi \) of \(\mathcal {\mathcal {P}}\) over some word w and \(\mathcal {S}\subseteq Q\times Q\), we say that the run \(\pi \) uses only sub-summaries from \(\mathcal {S}\) whenever for all \(q,p\in Q\), if there is sub-run of \(\pi \) which is a summary from q to p, then \((q,p)\in \mathcal {S}\).

Let \(\varLambda \) be the following alphabet, disjoint from \(\varSigma \), given by

For each \(\varLambda '\subseteq \varLambda \), we denote by \(\varSigma _{\varLambda '}\) the pushdown alphabet obtained by adding to \(\varSigma \) the additional symbols in \(\varLambda '\), which are interpreted as internal actions. Moreover, we define \(\mathcal {P}_\varLambda =\langle Q,Q_0,\varGamma ,\varDelta _\varLambda ,F \rangle \) as the NVPA over \(\varSigma _\varLambda \) obtained from \(\mathcal {P}\) by adding for each \((q,p)\in Q\times Q\), the internal transition \((q,\Box _{qp},p)\).

We prove that one can construct a well-formed VRE \(\alpha \) over \(\varSigma _\varLambda \) denoting \(\mathcal {L}(\mathcal {P})\) (the additional symbols in \(\varLambda \) are used only as parameters for intermediate substitutions). The proof consists of the following two Lemmata 8 and 9.

Lemma 8

Assume that for all \((q,p)\in Q\times Q\), one can construct a well-matched VRE \(\alpha (q,p)\) such that \(\mathcal {L}(\alpha (q,p))\) is the set of words in \( MWM (\varSigma )\) so that there is a summary of \(\mathcal {P}\) from q to p over w. Then, one can construct a well-formed VRE \(\alpha \) such that \(\mathcal {L}(\alpha )=\mathcal {L}(\mathcal {P})\).

Proof

Fix an ordering \(\{(q_1,p_1),\ldots ,(q_n,p_n)\}\) of \(Q\times Q\). Given a regular expression \(\xi \) over \(\varSigma _\varLambda \), let

be the VRE obtained from \(\xi \) by simultaneously replacing each occurrence of \(\Box _{q_i p_i}\) with the well-matched VRE \(\alpha (q_i,p_i)\). The following follows immediately:

Claim 5

The VRE given by Eq. (1) is well-formed and denotes the language

Let \(\mathcal {A}_1=\langle Q,Q_{0},\varDelta _1,F \rangle \) and \(\mathcal {A}_2=\langle Q,Q_{0},\varDelta _2,F \rangle \) be the non-deterministic finite-state automata (NFA) over \(\varSigma _{\varLambda }\), where \(\varDelta _1\) and \(\varDelta _2\) are defined as follows:

• \(\varDelta _1\) is obtained from the transition relation of \(\mathcal {P}_\varLambda \) by removing all the push and pop transitions, and by adding for each pop transition of \(\mathcal {P}_\varLambda \) of the form \((q,r,\bot ,p)\), the transition (q, r, p);

• \(\varDelta _2\) is obtained from the transition relation of \(\mathcal {P}_\varLambda \) by removing all the push and pop transitions, and by adding for each push transition \((q,c,p,\gamma )\) of \(\mathcal {P}_\varLambda \), the transition (q, c, p).

Let

where for all \(q,p\in Q\), \(\mathcal {L}_{1,q,p}\) and \(\mathcal {L}_{2,q,p}\) are the set of words w such that there is a run of the NFA \(\mathcal {A}_1\) and NFA \(\mathcal {A}_2\) over w from q to p. Then,

Moreover, from Kleene’s Theorem for regular expressions [18], \(\mathcal {L}_\textit{reg}\) can be effectively captured by a regular expression \(\xi \). By Claim 5 above, we obtain that the well-formed VRE

which denotes the language \(\mathcal {L}\)(\(\mathcal {P}\)), as desired. \(\square \)

Lemma 9

For all \((q,p)\in Q\times Q\), one can construct a well-matched VRE denoting the set of words in \( MWM (\varSigma )\) so that there is a summary of \(\mathcal {P}\) from q to p over w.

Proof

Given \((q,p)\in Q\times Q\), \(\mathcal {S}\subseteq Q\times Q\), and \(\varLambda '\subseteq \varLambda \), we define the following two languages:

• \(S(q,p,\mathcal {S},\varLambda ')\,\mathop {=}\limits ^{\text {def}}\,\) the set of words \(w\in MWM (\varSigma _{\varLambda '})\) such that there is a summary of \(\mathcal {P}_\varLambda \) over w from q to p which uses only sub-summaries from \(\mathcal {S}\).

• \( WM (q,p,\mathcal {S},\varLambda ')\,\mathop {=}\limits ^{\text {def}}\,\) the set of words \(w\in WM (\varSigma _{\varLambda '})\) such that there is a run of \(\mathcal {P}_\varLambda \) over w from \((q,\bot )\) to some configuration of the form \((p,\beta )\) which uses only sub-summaries from \(\mathcal {S}\) (note that \(\beta =\bot \)).

We show by induction on the cardinality of the finite set \(\mathcal {S}\) that the languages \(S(q,p,\mathcal {S},\varLambda ')\), \( WM (q,p,\mathcal {S},\varLambda ')\), and \(\{c\}\cdot WM (q,p,\mathcal {S},\varLambda ') \cdot \{r\}\) with \(c\in \varSigma _{ call }\) and \(r\in \varSigma _{ ret }\) can be effectively denoted by well-matched VRE over \(\varSigma _{\varLambda '}\). The Lemma follows from this claim.

Base case: \(\mathcal {S}=\emptyset \). The result for \(S(q,p,\emptyset ,\varLambda ')\) follows immediately because \(S(q,p,\emptyset ,\varLambda ')=\emptyset \). We only need to prove that the language \( WM (q,p,\emptyset ,\varLambda ')\) can be effectively denoted by a regular expression over the set of internal actions given by \(\varSigma _{ int }\cup \varLambda '\). Let \(\mathcal {A}=\langle Q,Q_{0},\varDelta ',F \rangle \) be the non-deterministic finite-state automaton (NFA) over \(\varSigma _{ int }\cup \varLambda '\), where \(\varDelta '\) is obtained from the transition relation of \(\mathcal {P}_\varLambda \) by removing all push and pop transitions, and all internal transitions \((q',\Box _{q'p'},p')\) with \(\Box _{q'p'}\notin \varLambda '\). Since no word in \( WM (q,p,\emptyset ,\varLambda ')\) contains occurrences of calls or occurrences of returns, \( WM (q,p,\emptyset ,\varLambda ')\) is the set of words w over \(\varSigma _{ int }\cup \varLambda '\) such that there is a run of \(\mathcal {A}\) over w from q to p. Kleene’s Theorem [18] guarantees that one can construct a regular expression over \(\varSigma _{ int }\cup \varLambda '\) denoting \( WM (q,p,\emptyset ,\varLambda ')\).

Induction step: \(\mathcal {S}\ne \emptyset \). Let \((q',p')\in \mathcal {S}\) and \(P_{q'\rightarrow p'}\) be the set:

So, \(P_{q'\rightarrow p'}\) is the set of tuples \((s,c,r,s')\) such that there is a push transition from \(q'\) to s reading the call c and a matching pop transition from \(s'\) to \(p'\) reading r. It easily follows that

By the induction hypothesis, the sets \(\{c\}\cdot WM (s,s',\mathcal {S}\setminus \{(q,'p')\},\varLambda '\cup \{\Box _{q'p'}\})\cdot \{r\}\) and \(\{c\}\cdot WM (s,s',\mathcal {S}\setminus \{(q,'p')\},\varLambda ')\cdot \{r\}\) can be effectively denoted by well-matched VRE. Thus, for each \((q',p')\in \mathcal {S}\), the set \(S(q',p',\mathcal {S},\varLambda ')\) can be effectively denoted by a well-matched VRE.

Fix an ordering \(\{(p_1,q_1),\ldots ,(p_n,q_n)\}\) of \(\mathcal {S}\) and let \(\varLambda _\mathcal {S}\) be the subset of \(\varLambda \) given by \(\{\Box _{q_1 p_1},\ldots ,\Box _{q_n p_n} \}\). Now, we observe that for all calls c and returns r,

Moreover, note that if \((q,p)\notin \mathcal {S}\), then \(S(q,p,\mathcal {S},\varLambda ')=\emptyset \). Hence, the result follows. \(\square \)

Reprints and permissions