Computing combinatorial types of trajectories in Pfaffian Dynamics

Suppose that the state space of a dynamical system has a finite partition, and each element of the partition is labelled by a letter of some alphabet. Then every trajectory of the system is naturally labelled by a word in this alphabet. This word is called the combinatorial type of the trajectory. In applications it is important to decide whether among a certain family of trajectories there is at least one trajectory of a given type, or whether all the trajectories in this family have the same type. In this paper we construct algorithms for solving this sort of questions for a wide class of Pfaffian dynamical systems, which have elementary (doubly-exponential) upper complexity bounds.