Editing Star height problem (section)

==Computing the star height of regular languages==
In contrast, the second question turned out to be much more difficult, and the question became a famous open problem in formal language theory for over two decades.{{sfn|Brzozowski|1980}} For years, there was only little progress. The [[pure-group language]]s were the first interesting family of regular languages for which the star height problem was proved to be [[Decidable language|decidable]].{{sfn|McNaughton|1967}} But the general problem remained open for more than 25 years until it was settled by [[Kosaburo Hashiguchi|Hashiguchi]], who in 1988 published an algorithm to determine the [[star height]] of any regular language.{{sfn|Hashiguchi|1988}} The algorithm wasn't at all practical, being of non-[[ELEMENTARY|elementary]] complexity. To illustrate the immense resource consumptions of that algorithm, {{harvtxt|Lombardy|Sakarovitch|2002}} give some actual numbers:

{{Quotation|text=[The procedure described by Hashiguchi] leads to computations that are by far impossible, even for very small examples. For instance, if ''L'' is accepted by a 4 state automaton of loop complexity 3 (and with a small 10 element transition monoid), then a ''very low minorant'' of the number of languages to be tested with ''L'' for equality is:

<math>\left(10^{10^{10}}\right)^{\left(10^{10^{10}}\right)^{\left(10^{10^{10}}\right)}}.</math>|author=S. Lombardy and J. Sakarovitch|title=''Star Height of Reversible Languages and Universal Automata''|source=LATIN 2002}}

Notice that alone the number <math>10^{10^{10}}</math> has 10 billion zeros when written down in [[decimal notation]], and is already ''by far'' larger than the [[Observable universe#Matter content|number of atoms in the observable universe]].

A much more efficient algorithm than Hashiguchi's procedure was devised by Kirsten in 2005.{{sfn|Kirsten|2005}} This algorithm runs, for a given [[nondeterministic finite automaton]] as input, within double-[[EXPSPACE|exponential space]]. Yet the resource requirements of this algorithm still greatly exceed the margins of what is considered practically feasible.

This algorithm has been optimized and generalized to trees by Colcombet and Löding in 2008,{{sfn|Colcombet|Löding|2008}} as part of the theory of regular cost functions.
It has been implemented in 2017 in the tool suite Stamina.{{sfn|Fijalkow|Gimbert|Kelmendi|Kuperberg|2017}}