  The system of Type PDL ($\tau$PDL) is an extension of Propositional Dynamic
Logic (PDL) and its main goal is to provide a formal basis for reasoning about
types of actions (modeled by their preconditions and effects) and agent
capabilities. The system has two equivalent interpretations, namely the
standard relational semantics and the type semantics, where process terms are
interpreted as types, i.e. sets of binary relations. Its satisfiability problem
is decidable, as a NExpTime decision procedure was provided based on a
filtration argument and it was suggested that the satisfiability problem for
$\tau$PDL should be solvable in deterministic, single exponential time. In this
paper, we address the problem of the complexity of the satisfiability problem
of $\tau$PDL. We present a deterministic tableau-based satisfiability algorithm
and prove that it is sound and complete and that it runs in ExpTime.
Additionally, the algorithm detects satisfiability as earlier as possible, by
restricting or-branching whenever possible.
