  We propose an interdisciplinary framework that combines Bayesian predictive
inference, a well-established tool in Machine Learning, with Formal Methods
rooted in the computer science community. Bayesian predictive inference allows
for coherently incorporating uncertainty about unknown quantities by making use
of methods or models that produce predictive distributions, which in turn
inform decision problems. By formalizing these decision problems into
properties with the help of spatio-temporal logic, we can formulate and predict
how likely such properties are to be satisfied in the future at a certain
location. Moreover, we can leverage our methodology to evaluate and compare
models directly on their ability to predict the satisfaction of
application-driven properties. The approach is illustrated in an urban mobility
application, where the crowdedness in the center of Milan is proxied by
aggregated mobile phone traffic data. We specify several desirable
spatio-temporal properties related to city crowdedness such as a fault-tolerant
network or the reachability of hospitals. After verifying these properties on
draws from the posterior predictive distributions, we compare several
spatio-temporal Bayesian models based on their overall and property-based
predictive performance.
