Authors: Dautović, Šejla 
Doder, Dragan
Ognjanović, 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
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.
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 

Show full item record

Page view(s)

checked on May 9, 2024

Google ScholarTM


This item is licensed under a Creative Commons License Creative Commons