Inductive definition of ECTL*: how are recursive formulas forbidden? 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
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.