Bounds on sizes of finite bisimulations of pfaffian dynamical systems

We study finite bisimulations of dynamical systems in ℝ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.The first author was partly supported by Grant Scientific School-4413.2006.1, DFG-RFBR 436 RUS 06/01/04. The second author was supported in part by the European RTN Network RAAG (contract HPRN-CT-2001-00271)