Discrete linear-time probabilistic logics: completeness, decidability and complexity. (English) Zbl 1102.03022
Summary: We introduce a propositional and a first-order logic for reasoning about discrete linear time and finitely additive probability. The languages of these logics allow formulae that say ‘sometime in the future, \(\alpha\) holds with probability at least \(s\)’. We restrict our study to so-called measurable models. We provide sound and complete infinitary axiomatizations for the logics. Furthermore, in the propositional case decidability is proved by establishing a periodicity argument for \(\omega\)-sequences extending the decidability proof of standard propositional temporal logic LTL. Complexity issues are examined and a worst-case complexity upper bound is given. Extensions of the presented results and open problems are described in the final part of the paper.
MSC:
03B48 | Probability and inductive logic |
03B44 | Temporal logic |
68T27 | Logic in artificial intelligence |
03B25 | Decidability of theories and sets of sentences |