  Software developers cannot always anticipate how users will actually use
their software as it may vary from user to user, and even from use to use for
an individual user. In order to address questions raised by system developers
and evaluators about software usage, we define new probabilistic models that
characterise user behaviour, based on activity patterns inferred from actual
logged user traces. We encode these new models in a probabilistic model checker
and use probabilistic temporal logics to gain insight into software usage. We
motivate and illustrate our approach by application to the logged user traces
of an iOS app.
