Thursday, December 07, 2006

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) = sumk=12n Sk2n k!

where Regions(2n) is the number of equivalence classes over 2n clocks each constrained to lie in the interval (0,1), and Sk2n 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 :-)

No comments: