Number of Regions in a Timed Automaton

While working on the book Reactive Systems: Modelling, Specification and Verification, my co-authors and I were looking for a formula counting the number of regions in a timed automaton exactly in order to motivate the introduction of the notion of zone. Thanks to Rajeev Alur and Tom Henzinger, I now know the answer, which I report here in case anybody else is interested.

There is a characterization of the number of regions where all clocks lie between 0 and 1 in terms of Stirling numbers of the second kind in this paper (page 13 bottom).

Peter Kopke's PhD thesis available from Tom's web page at http://mtc.epfl.ch/~tah/Students/kopke.pdf also contains that characterization. The section that starts on page 164 (of the file) offers the following formula:

Regions(2n) = sum_k=1²ⁿ S_k²ⁿ k!

where Regions(2n) is the number of equivalence classes over 2n clocks each constrained to lie in the interval (0,1), and S_k²ⁿ is the number of ways of partitioning a set with 2n elements into k subsets. So Regions(2n) is exactly the number of ways of partitioning a set with 2n elements into k ordered subsets.

As the algebraic combinatorialists here at Reykjavík University know well, I am always very impressed by these counting formulae :-)