Authors: | Doder, Dragan Ognjanović, Zoran |
Affiliations: | Mathematics Mathematical Institute of the Serbian Academy of Sciences and Arts |
Title: | Probabilistic temporal logic with countably additive semantics | Journal: | Annals of Pure and Applied Logic | Volume: | 175 | Issue: | 9 | First page: | 103389 | Issue Date: | 2024 | Rank: | ~M21 | ISSN: | 0168-0072 | DOI: | 10.1016/j.apal.2023.103389 | Abstract: | This work presents a proof-theoretical and model-theoretical approach to probabilistic temporal logic. We present two novel logics; each of them extends both the language of linear time logic (LTL) and the language of probabilistic logic with polynomial weight formulas. The first logic is designed for reasoning about probabilities of temporal events, allowing statements like “the probability that A will hold in next moment is at least the probability that B will always hold” and conditional probability statements like “probability that A will always hold, given that B holds, is at least one half”, where A and B are arbitrary statements. We axiomatize this logic, provide corresponding sigma additive semantics and prove that the axiomatization is sound and strongly complete. We show that the satisfiability problem for our logic is decidable, by presenting a procedure which runs in polynomial space. We also present a logic with much richer language, in which probabilities are not attached only to temporal events, but the language allows arbitrary nesting of probability and temporal operators, allowing statements like “probability that tomorrow the chance of rain will be less than 80% is at least a half”. For this logic we prove a decidability result. |
Keywords: | Linear-time temporal logic | Probabilistic logic | Completeness theorem | Decidability | Publisher: | Elsevier |
Files in This Item:
File | Description | Size | Format | |
---|---|---|---|---|
ZOgnjanovic.pdf | 1.33 MB | Adobe PDF | View/Open |
Page view(s)
23
checked on Nov 8, 2024
Download(s)
7
checked on Nov 8, 2024
Google ScholarTM
Check
Altmetric
Altmetric
This item is licensed under a Creative Commons License