Until-since temporal logic based on parallel time with common past. Deciding algorithms

We present a framework for constructing algorithms recognizing admissible inference rules (consecutions) in temporal logics with Until and Since based on Kripke/Hintikka structures modeling parallel time with common past. Logics PTL alpha with various branching factor alpha E N boolean OR {w} after common past are considered. The offered technique looks rather flexible, for instance, with similar approach we showed [33] that temporal logic based on sheafs of integer numbers with common origin is decidable by admissibility. In this paper we extend obtained algorithms to logics PTL alpha We prove that any logic PTL alpha, is decidable w.r.t. admissible consecutions (inference rules), as a consequence, we solve satisfiability problem and show that any PTL alpha, itself is decidable.