Probabilistic-Temporal Logic with Actions

Abstract

Temporal logics are formal systems that allow reasoning about sentences referring to time and they find many applications in computer science [7]. The most standard division of temporal logics is into linear and branching time. In linear temporal logics (LTL) each moment of time has a unique possible future, while in temporal logics with brunching time for each moment there can be two or more possible futures. Propositional branching time temporal logic with the standard operators ⃝ (next), U (until) and A (universal path operator) is introduced in [8], usually called Computation tree logic (CTL). Full computation tree logic (CT L∗) is introduced in [15]. Uncertain reasoning has emerged as one of the main fields in artificial in- telligence, with many different tools developed for representing and reasoning with uncertain knowledge. A particular line of research concerns the formal- ization in terms of logic, and the questions of providing an axiomatization and decision procedure for probabilistic logic attracted the attention of researchers and triggered investigation about formal systems for probabilistic reasoning [1, 9, 10, 11, 14, 16]. The probabilistic logic for reasoning about degrees of confirmation (LP P conf 2 ) is introduced in [3]. The language of the logic allows statements as ”Probability of A is at most one half” and ”B confirms A with degree of at least one half” which means that the posterior probability of A on the evidence B is greater than the prior probability of A by at least one half. Degree of confirmation is measured as c(A, B) = μ(A|B) − μ(A), where μ(A|B) = μ(A∩B) μ(B) if μ(B) ̸ = 0 or undefined if μ(B) = 0. The probabilistic logic for reasoning about actions in time (pCT L∗ A) is developed in [2]. The language of the logic extend the language of P AL [19, 20] by employing the full power of CT L∗ and probabilistic operators from logic LP P2 [14], where we can formalize statements as ”Probability that the precondition of the action A will hold in the next moment is at least one half”. In this talk we extend the logic pCT L∗ A with new probabilistic operators from [3] to allow measuring how some actions confirms the other action in time. Our main results are sound and strongly complete (every consistent set of formulas is satisfiable) axiomatization. We prove strong completeness using an adaptation of Henkin’s construction, modifying some of our earlier methods [4, 6, 5, 14, 16]. Our axiom system contains infinitary rules of inference. In the infinitary rule for temporal part of the logic the premises and conclusions are in the form of so called k-nested implications. This form of infinitary rules is a technical solution already used in probabilistic, epistemic and temporal logics for obtaining various strong necessitation results [12, 13, 17, 18]. In the axiomatization we use this form of rules only on the part of temporal logic, because we do not allow iteration of probability operators.