4
$\begingroup$

In [1], the extended computation tree logic ECTL* is inductively defined as the propositional formulas over all E($A(F_1,..F_n)$), where E is the existential path quantifier and $A$ some Büchi automaton whose alphabet is $2^{\{F_1,..,F_n\}}$ for some ECTL* formulas $F_1,..F_n$.

Obviously E($A(F_1)$) with $F_1=$E$(A(F_1)$) is not well-defined for some Büchi automata. So what does inductively defined exactly mean in this case?

Maybe that no $F_1,..,F_n$ may use $F_1,..,F_n$ in their respective Büchi automata, but the Büchi automata may occur recursively if the alphabet is correctly exchanged. Or may, e.g., $F_1$ use $F_2,..,F_n$, as long as there is no mutual recursion between the $F_i$?


Update: Does the following define ECTL*'s syntax?

$\langle\text{sf}\rangle::=\; \langle\text{atomic prop}\rangle\;\big\vert\; \langle\text{sf}\rangle \vee \langle\text{sf}\rangle\;\big\vert \neg\langle\text{sf}\rangle\;\big\vert\; \text{E }\langle \text{Buechi}\;\mathcal{A}\rangle (\langle\text{sf}\rangle,\dots,\langle\text{sf}\rangle); $

(as opposed to $\langle\text{sf}\rangle::=\; \langle\text{atomic prop}\rangle\;\big\vert\; \langle\text{sf}\rangle \vee \langle\text{sf}\rangle\;\big\vert \neg\langle\text{sf}\rangle\;\big\vert\; \text{E }\langle \text{Buechi}\;\mathcal{A}\rangle (F_1,\dots,F_n); $ where the $F_i$ are ECTL* formulas).


In detail,

[1] says

Formulas of ECTL* are inductively defined as usual and built from propositional variables using boolean connectives and containing the formula $E(A)$ for each Büchi automaton $A$ over an alphabet $2^{\{F_1,..,F_n\}}$ where the $F_i$ are ECTL* formulas.


[1] CTL* and ECTL* as fragements of the modal $\mu$-calculus by Mads Dam

$\endgroup$
3
  • 1
    $\begingroup$ Probably the first you say, i.e., that each $F_i$ is defined by some BNF and thus cannot refer to any other $F_j$. $\endgroup$
    – Pål GD
    Jan 14, 2013 at 15:22
  • $\begingroup$ Do you mean CTL* or ECTL* syntax? $\endgroup$
    – Vijay D
    Jan 15, 2013 at 19:52
  • $\begingroup$ I would choose the first definition you give. The two are equivalent to me, but if your confusion is notational, I would stick with the first one. $\endgroup$
    – Vijay D
    Jan 15, 2013 at 22:28

2 Answers 2

5
$\begingroup$

I think the key problem here is not understanding how inductive definitions of syntax work. Here are three approaches to understanding what a BNF grammar means.

Consider a simple grammar:

$$ t ::= \mathtt{true} ~~|~~ \mathtt{false} ~~|~~ 0 ~~|~~ \mathtt{succ}\ t ~~|~~ \mathtt{if}\ t\ \mathtt{then}\ t\ \mathtt{else}\ t$$

Following Pierce's Types and Programming Languages pages 26-27, the set of terms defined by this grammar is given by the following three equivalent ways.

Inductively

The set of terms is the smallest set $\mathcal{T}$ such that:

  1. $\{\mathtt{true},\mathtt{false},0\}\subseteq\mathcal{T}$.
  2. if $t_1\in\mathcal{T}$, then $\mathtt{succ}\ t_1\in\mathcal{T}$.
  3. if $t_1,t_2,t_3\in\mathcal{T}$, then $\mathtt{if}\ t_1\ \mathtt{then}\ t_2\ \mathtt{else}\ t_3\in\mathcal{T}$.

By Inference Rules

The set of terms is defined by the following rules:

$$\mathtt{true}\in\mathcal{T} \qquad \mathtt{false}\in\mathcal{T} \qquad 0\in\mathcal{T}$$

$$\dfrac{t_1\in\mathcal{T}}{\mathtt{succ}\ t_1\in\mathcal{T}} \qquad \dfrac{t_1\in\mathcal{T}\quad t_2\in\mathcal{T}\quad t_3\in\mathcal{T}}{\mathtt{if}\ t_1\ \mathtt{then}\ t_2\ \mathtt{else}\ t_3\in\mathcal{T}}$$

Concretely

For each natural number $i$, define set $S_i$ as follows:

  1. $S_0=\emptyset$.
  2. $S_{i+1}=\{\mathtt{true},\mathtt{false},0\}\cup\{\mathtt{succ}\ t_1\mid t_1\in S_i\} \cup \{\mathtt{if}\ t_1\ \mathtt{then}\ t_2\ \mathtt{else}\ t_3 \mid t_1,t_2,t_3\in S_i\}$

Finally, $S=\bigcup_i S_i$ is the set of all terms.

$\endgroup$
5
  • $\begingroup$ Thanks a lot - such a clean answer (+1). And it does say SMALLEST set :) $\endgroup$ Jan 17, 2013 at 18:22
  • $\begingroup$ Suppose you state: $t ::= 0~|~ 0 w$ with $w \in \mathcal{L}$, the language currently being defined. Is this still a BNF? Or does only the inductive way apply? If only the inductive way applies, you do need to state that $\mathcal{L}$ must be the smallest such set. That's what the discussion with Vijay D was about... $\endgroup$ Jan 17, 2013 at 18:31
  • 2
    $\begingroup$ You cannot refer to the language currently being defined like that in BNF. Of course, you can refer to the top non-terminal instead of $w$ to achieve the same effect. I do need to say the smallest set in the inductive definition above; that's what makes it inductive. If I allowed any other set, then there could be other junk in $\mathcal{T}$. $\endgroup$ Jan 17, 2013 at 19:06
  • $\begingroup$ I'm jealous. That's a beautifully clear answer that I could not produce. $\endgroup$
    – Vijay D
    Jan 17, 2013 at 23:39
  • 1
    $\begingroup$ @VijayD: The credit should go to Pierce. I just knew were to find this description. $\endgroup$ Jan 18, 2013 at 5:15
6
$\begingroup$

The formula in your statement

Obviously E(A(F1)) with F1=E(A(F1)) is not well-defined for some Büchi automata. So what does inductively defined exactly mean in this case?

cannot arise if you built ECTL* inductively. This means, in standard academic parlance, we would present a syntax definition of the form below.

Let $Prop$ be a set of propositions and $p$ range over $Prop$. If $\varphi_1, \ldots, \varphi_n$ are formulae of ECTL* let $\mathcal{A}[\varphi_1, \ldots, \varphi_n]$ denote an automaton $\mathcal{A}$ over the alphabet $\mathcal{P}(\{\varphi_1, \ldots, \varphi_n\})$ of subsets of the $n$ formulae shown.

$ \varphi ::= p ~\mid~ \varphi \land \varphi ~\mid~ \neg \varphi ~\mid~ \mathsf{E}(\mathcal{A}[\varphi_1, \ldots, \varphi_n])$

I believe there is some confusion in how you may be reading the presentation above. In academic terms this qualifies as BNF. I see that the Wikipedia page gives a slightly different presentation. However, the definition above is equivalent to the BNF grammar you give below. It is not a "relaxed BNF" to use your terminology. It is just an inductive definition where some BNF is used where convenient.

BNF: $\langle\text{sf}\rangle::=\; \langle\text{atomic prop}\rangle\;\big\vert\; \langle\text{sf}\rangle \vee \langle\text{sf}\rangle\;\big\vert \neg\langle\text{sf}\rangle\;\big\vert\; \text{E }\langle \text{Buechi}\;\mathcal{A}\rangle (\langle\text{sf}\rangle,\dots,\langle\text{sf}\rangle); $

Academic writing mixes English and BNF when we make inductive definitions because it is convenient. To see the need for convenience, consider your grammar. It does not inform the reader what $\langle\mathrm{atomic~prop}\rangle$ and what $\langle \mathrm{sf}\rangle$ are. You have chosen an intuitive naming convention, so one can guess the first represents atomic propositions. But in general, we want to have short symbols in our papers, so we prefer a one-time cost of verbose English, which is why we write something like "where $\varphi$ is an ECTL* formula". This text does not in any way change the language being defined.

To your specific question: Your formula $F$ with $F = E(A(F))$ is not a formula of ECTL*. This type of formula cannot arise as the result of an inductive of the form above. This impossibility has nothing to do with the difference in presentation between BNF as you write it and inductive definitions in papers. To derive your formula, you need some atomic propositions, and a sequence of syntactic compositions to build up the more complex formula.

Now about fixed points. There is some confusion here too. BNF grammars are specific ways to present certain inductive definitions. They are not the only way and they do not cover all inductive definitions. Inductive definitions are a more general class and can be presented in many ways. Least fixed points are a strict generalisation of inductive definitions. Below I will only give an example of how both the BNF grammar above and the inductive definition I gave define a least fixed point. I emphasise that both definitions give rise to the same least fixed point.

Let's assume that $Prop = \{q,r,s\}$ is a set of atomic propositions and $p$ ranges over $Prop$. Consider a lattice $L$ which contains all sets of sequences of symbols appearing in the definitions above. The formulae of ECTL* are one specific element of this lattice. Consider a function $G:L \to L$, which is generated by the definitions above.

$G(\emptyset) = Props$, which accounts for $q$, $r$ and $s$ being formulae, or for the instantiation of $\langle \mathrm{atomic~prop}\rangle$ in BNF.

$G(G(\emptyset)) = G(Props)$, which is the set containing elements, $q \land r$, $q \land s$, $r \land s$, $\neg q$, $\neg s$, $\neg r$, $E(\mathcal{A}(\{q\}))$, $E(\mathcal{A}(\{r\}))$, $E(\mathcal{A}(\{s\}))$, $E(\mathcal{A}(\{q,r\}))$, $E(\mathcal{A}(\{q,s\}))$, $E(\mathcal{A}(\{r,s\}))$, $E(\mathcal{A}(\{q,r,s\}))$. This is equivalent to applying the formation rules $\langle \mathrm{sf} \rangle \lor \langle \mathrm{sf} \rangle$, $\neg \langle \mathrm{sf} \rangle $ and the others with $\langle \mathrm{sf} \rangle$ being replaced by $\langle \mathrm{atomic~prop}\rangle$. Alternatively, this is equivalent to one unwinding of the inductive definition where we say, if $\varphi_1$ and $\varphi_2$ are atomic propositions, then $\varphi_1 \land \varphi_2$, $\neg \varphi_1$, $E(\mathcal{A}(\{\varphi_1, \varphi_2\}))$, etc are formulae.

The set $G(G(G(\emptyset)))$ contains $q \land r\land s$, $r \land \neg s$, $\neg (q \land s)$, $\neg E(\mathcal{A}(\{r\}))$, $E(\mathcal{A}(\{q \land s, \neg r\}))$ and so on.

The set of ECTL* formulae is the least fixed point of the function $G$ above. Note that I have not explicitly defined it, but this is possible to do and might be an insightful exercise to work out the details. Equivalently, you can obtain exactly the same fixed point by the BNF grammar or the inductive definition I give.

The kind of formula you suggest will occur in a fixed point that is not a least fixed point. I emphasise that both the BNF grammar and the inductive definition I give generate the same function $G$, hence they have the same least fixed point and the same set of fixed points. So, if the inductive definition allows for a certain formula, your BNF must allow for the at formula, and vice versa.

$\endgroup$
14
  • $\begingroup$ Thanks for the answer (+1). I've updated my question. Is my syntax definition correct? Is it a direct consequence of "inductively defined"? Because what confuses me in Mads Dam's and your text is "let f_i be formulae". Do you have any reference where ECTL*'s syntax is defined rigorously? Thx. $\endgroup$ Jan 15, 2013 at 10:59
  • $\begingroup$ Thanks a lot for your thorough update. It explains the BNF I have given in my update, doesn't it? $\endgroup$ Jan 15, 2013 at 22:27
  • $\begingroup$ I am having difficulty understanding your comment. My expansion is for the grammar I gave. Maybe I am used to the way BNF is used in the academic literature, while you are reading it slightly differently. How can the grammar I gave admit the formula you wrote? $\endgroup$
    – Vijay D
    Jan 15, 2013 at 22:31
  • $\begingroup$ Let $\varphi_1:=E(A(\varphi_1))$. Then $\varphi_1$ is a fixpoint of your BNF, thus you could argue it is in ECTL*. This problem does not arise in my definition where all syntactic elements are created by the BNF, without using $F_i \in$ ECTL*. $\endgroup$ Jan 15, 2013 at 22:37
  • $\begingroup$ Can you show me other academic literature where a language $L$ is defined by a BNF that uses $F_i \in L$ (as opposed to non-terminal symbols creating that syntactic element)? $\endgroup$ Jan 15, 2013 at 22:40

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.