Cutting diamonds: A temporal logic with probabilistic distributions

Temporal logics, as formalisms capable of expressing properties evolving over time, have been successfully employed to represent and verify processes in many different settings. A common staple in most of these logics is the eventuality (or diamond) constructor, which expresses that some property will hold at some point in the future. While useful in practice, the specification of the diamond operator is too rough; indeed, one often has an idea—albeit uncertain—about when the property may hold. We introduce TLD, an extension of linear temporal logic (LTL) that refines the diamond operator with a new constructor expressing a probability distribution for the time until the property is observed. We study the main properties of this logic and describe methods for deciding satisfiability, and performing probabilistic inferences in a restricted version of the logic. These methods rely on known properties of LTL.