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

Rybakov, Vladimir V. (2007) Until-since temporal logic based on parallel time with common past. Deciding algorithms. In: International Symposium on Logical Foundations of Computer Science 2007, 4th June 2007 - 7th June 2007, New York, NY, USA.

File not available for download.

Abstract

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