Bounds on sizes of finite bisimulations of Pfaffian dynamical systems

We study finite bisimulations of dynamical systems in R-n defined by Pfaffian maps. The pure existence of finite bisimulations for a more general class of o-minimal systems was shown in Brihaye et al. (Lecture Notes in Comput. Sci. 2993, 219-233, 2004), Davoren (Theor. Inf. Appl. 33(4/5), 357-382, 1999), Lafferriere et al. (Math. Control Signals Syst. 13, 1-21, 2000). In Lecture Notes in Comput. Sci. 3210, 2004, the authors proved a double exponential upper bound on the size of a bisimulation in terms of the size of description of the dynamical system. In the present paper we improve it to a single exponential upper bound, and show that this bound is tight, by exhibiting a parameterized class of systems on which it is attained.