 One of the most important logical decision problems is to determine whether a given formula of a given logic is valid (resp. satisfiable) in the semantics provided for that logic. Particularly efficient and practically useful for deciding satisfiability are the tableaux-based methods, originating from pioneering work of Beth, Hintikka, Smullyan, and Fitting. These methods are based on a systematic search of a satisfying model (resp. falsifying countermodel) if an input formula that is tested for satisfiability is provided, and they are guaranteed to find such a model whenever it exists. Tableaux-based methods have been successfully developed for constructive satisfiability testing for a variety of temporal logics. See Goré (1999) for a survey on tableaux systems for many temporal logics and more specifically: Ben-Ari et al. (1983) for the branching time logic UB; Emerson and Halpern (1985) for the computation tree logic CTL; Wolper (1985) for the linear time temporal logic LTL; Kontchakov et al. (2004) on temporalizing tableaux; Reynolds (2007) for CTL with bundled tree semantics; Goranko and Shkatov (2010) for ATL; Reynolds (2011) for the full computation tree logic CTL*; Reynolds (2014) for the real-time temporal logic RTL, etc.