On the Formal Analysis of the Dynamics of Simulated Agent Societies