An Expressive Probabilistic Temporal Logic

In order to reason about probabilistic knowledge, we must reason about time and actions as well. When we say, for example, that "the probability of'heads' after a coin toss is 50% and that of'tails' is 50%", we implicitly assume that there is an action (in this example, tossing a coin) which can bring the world to different states in the next moment in time. The uncertainty lies in the state transition: the world may end up in a state where the coin shows heads or in a state where it shows tails. Despite the evident dependence of our informal notion of probability on the notions of action and time, the formal mathematical languages that we use to talk about probabilities rarely support mentioning action and time explicitly. Kolmogorov's probability theory, for example, merely defines probability as the measure function in a measure space with total measure 1 [9]. The task of modeling time-dependent actions and their possible outcomes in terms of events in a probabilistic space remains informal. While this informality is not problematic in the simplest situations (e.g. when we are interested in the possible outcomes of a single action, or when multiple actions are independent of each other), slightly more complex situations may already lead to confusion and difficulty. A famous example is the Monty Hall problem [10]. Another inconvenience of dealing with probabilities just in terms of a measure space is that its set-theoretic language (where events are represented as subsets of the sample space) is rather limited.