Output details

Linear Temporal Logic LTL: Basis for admissible rules

<11>This paper solves a difficult open problem: we construct a basis for rules admissible in the linear temporal logic LTL, i.e. we solve the problem of logical consequence in LTL for inference rules. The basis allows for the derivation of all possible rules admissible in LTL. The logic LTL is an efficient tool for formal verification of computer programs, which is of vital importance for computer science. Inference rules can be applicable for self-modifying programs working in dynamic environment, e.g. distributed computing, web computations and programs interacting with external agents.