Take the 2-minute tour ×
Theoretical Computer Science Stack Exchange is a question and answer site for theoretical computer scientists and researchers in related fields. It's 100% free, no registration required.

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

share|improve this question
1  
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$. –  Pål GD Jan 14 '13 at 15:22
    
Do you mean CTL* or ECTL* syntax? –  Vijay D Jan 15 '13 at 19:52
    
Thanks, corrected it to ECTL*. –  DaveBall aka user750378 Jan 15 '13 at 21:46
    
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. –  Vijay D Jan 15 '13 at 22:28
add comment

2 Answers 2

up vote 5 down vote accepted

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.

share|improve this answer
    
Thanks a lot - such a clean answer (+1). And it does say SMALLEST set :) –  DaveBall aka user750378 Jan 17 '13 at 18:22
    
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... –  DaveBall aka user750378 Jan 17 '13 at 18:31
2  
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}$. –  Dave Clarke Jan 17 '13 at 19:06
    
I'm jealous. That's a beautifully clear answer that I could not produce. –  Vijay D Jan 17 '13 at 23:39
1  
@VijayD: The credit should go to Pierce. I just knew were to find this description. –  Dave Clarke Jan 18 '13 at 5:15
add comment

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.

share|improve this answer
    
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. –  DaveBall aka user750378 Jan 15 '13 at 10:59
    
Thanks a lot for your thorough update. It explains the BNF I have given in my update, doesn't it? –  DaveBall aka user750378 Jan 15 '13 at 22:27
    
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? –  Vijay D Jan 15 '13 at 22:31
    
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*. –  DaveBall aka user750378 Jan 15 '13 at 22:37
    
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)? –  DaveBall aka user750378 Jan 15 '13 at 22:40
show 9 more comments

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

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