Tableau-based automata construction for dynamic linear time temporal logic*