We introduce a multi-agent logic of knowledge with time where F? stands for "there is an informative event after which ?." Formula F? is true in a model iff it is true in all its refinements (i.e., atoms and back are satisfied; the dual of simulation). The logic is almost normal, and positive knowledge is preserved. The meaning of F? is also "after the agents become aware of new factual information, ? is true," and on finite models it is also "there is an event model (M,s) after which ?." The former provides a correspondence with bisimulation quantifiers in a setting with epistemic operators.
['Hans van Ditmarsch', 'Tim French']
Simulation and Information: Quantifying over Epistemic Events