Linear temporal logic with until and next, logical consecutions

While specifications and verifications of concurrent systems employ Linear Temporal Logic ( L T L ), it is increasingly likely that logical consequence in L T L will be used in the description of computations and parallel reasoning. Our paper considers logical consequence in the standard L T L with temporal operations U (until) and N (next). The prime result is an algorithm recognizing consecutions admissible in L T L , so we prove that L T L is decidable w.r.t. admissible inference rules. As a consequence we obtain algorithms verifying the validity of consecutions in L T L and solving the satisfiability problem. We start by a simple reduction of logical consecutions (inference rules) of L T L to equivalent ones in the reduced normal form (which have uniform structure and consist of formulas of temporal degree 1). Then we apply a semantic technique based on L T L -Kripke structures with formula definable subsets. This yields necessary and sufficient conditions for a consecution to be not admissible in L T L . These conditions lead to an algorithm which recognizes consecutions (rules) admissible in L T L by verifying the validity of consecutions in special finite Kripke structures of size square polynomial in reduced normal forms of the consecutions. As a consequence, this also solves the satisfiability problem for L T L .