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_α with various branching factor α ∈N ∪ {ω} 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_α. We prove that any logic PTL_α is decidable w.r.t. admissible consecutions (inference rules), as a consequence, we solve satisfiability problem and show that any PTL_α itself is decidable.