Authors: Dautović, Šejla Doder, DraganOgnjanović, Zoran Affiliations: Mathematics Mathematical Institute of the Serbian Academy of Sciences and Arts Title: Probabilistic-Temporal Logic with Actions First page: 19 Last page: 20 Related Publication(s): Book of Abstracts Conference: 11th International Conference Logic and Applications, LAP 2022, September 26 - 29, 2022, Dubrovnik, Croatia Issue Date: 2022 Rank: M34 URL: http://imft.ftn.uns.ac.rs/math/cms/uploads/Main/LAP2022-Book_of_Abstracts.pdf Abstract: Temporal logics are formal systems that allow reasoning about sentencesreferring to time and they find many applications in computer science [7]. Themost standard division of temporal logics is into linear and branching time. Inlinear temporal logics (LTL) each moment of time has a unique possible future,while in temporal logics with brunching time for each moment there can betwo or more possible futures. Propositional branching time temporal logic withthe standard operators ⃝ (next), U (until) and A (universal path operator) isintroduced in [8], usually called Computation tree logic (CTL). Full computationtree 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 reasoningwith uncertain knowledge. A particular line of research concerns the formal-ization in terms of logic, and the questions of providing an axiomatization anddecision procedure for probabilistic logic attracted the attention of researchersand triggered investigation about formal systems for probabilistic reasoning[1, 9, 10, 11, 14, 16]. The probabilistic logic for reasoning about degrees ofconfirmation (LP P conf2 ) is introduced in [3]. The language of the logic allowsstatements as ”Probability of A is at most one half” and ”B confirms A withdegree of at least one half” which means that the posterior probability of Aon the evidence B is greater than the prior probability of A by at least onehalf. 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] byemploying the full power of CT L∗ and probabilistic operators from logic LP P2[14], where we can formalize statements as ”Probability that the preconditionof 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 operatorsfrom [3] to allow measuring how some actions confirms the other action in time.Our main results are sound and strongly complete (every consistent set offormulas is satisfiable) axiomatization. We prove strong completeness using anadaptation of Henkin’s construction, modifying some of our earlier methods[4, 6, 5, 14, 16]. Our axiom system contains infinitary rules of inference. Inthe infinitary rule for temporal part of the logic the premises and conclusionsare in the form of so called k-nested implications. This form of infinitary rulesis a technical solution already used in probabilistic, epistemic and temporallogics for obtaining various strong necessitation results [12, 13, 17, 18]. In theaxiomatization we use this form of rules only on the part of temporal logic,because we do not allow iteration of probability operators. Keywords: Probabilistic logic | Temporal logic | Completeness Publisher: University Center Dubrovnik, Croatia Project: Advanced artificial intelligence techniques for analysis and design of system components based on trustworthy BlockChain technology - AI4TrustBC

#### Page view(s)

59
checked on May 9, 2024