Output details

Rules admissible in transitive temporal logic T_S4, sufficient condition

<11>We study the open problem of the existence of an algorithm recognizing rules admissible in temporal branching-time logic T_S4. The paper finds sufficient (computable) conditions for admissibility of inference rules in T_S4, which is an important achievement in the area since 2004, when first steps towards admissible rules in temporal logics appeared. Branching time temporal logics are used in various areas of computer science where the most important task is verification of the correctness of computations, or making decisions in concurrent environments. The additional rules, which are permissible, allow us to simplify search and to discover incorrect computations.