Simulation and statistical model-checking of logic-based multi-agent system models

摘要

This thesis presents SALMA (Simulation and Analysis of Logic-Based Multi-udAgent Models), a new approach for simulation and statistical model checkingudof multi-agent system models.udStatistical model checking is a relatively new branch of model-based approximativeudverification methods that help to overcome the well-known scalabilityudproblems of exact model checking. In contrast to existing solutions,udSALMA specifies the mechanisms of the simulated system by means of logicaludaxioms based upon the well-established situation calculus. Leveragingudthe resulting first-order logic structure of the system model, the simulationudis coupled with a statistical model-checker that uses a first-order variant ofudtime-bounded linear temporal logic (LTL) for describing properties. This isudcombined with a procedural and process-based language for describing agentudbehavior. Together, these parts create a very expressive framework for modelingudand verification that allows direct fine-grained reasoning about the agents’udinteraction with each other and with their (physical) environment.udSALMA extends the classical situation calculus and linear temporal logicud(LTL) with means to address the specific requirements of multi-agent simulationudmodels. In particular, cyber-physical domains are considered whereudthe agents interact with their physical environment. Among other things,udthe thesis describes a generic situation calculus axiomatization that encompassesudsensing and information transfer in multi agent systems, for instanceudsensor measurements or inter-agent messages. The proposed model explicitlyudaccounts for real-time constraints and stochastic effects that are inevitable inudcyber-physical systems.udIn order to make SALMA’s statistical model checking facilities usable alsoudfor more complex problems, a mechanism for the efficient on-the-fly evaluationudof first-order LTL properties was developed. In particular, the presented algorithmuduses an interval-based representation of the formula evaluation stateudtogether with several other optimization techniques to avoid unnecessary computation.udAltogether, the goal of this thesis was to create an approach for simulationudand statistical model checking of multi-agent systems that builds uponudwell-proven logical and statistical foundations, but at the same time takes audpragmatic software engineering perspective that considers factors like usability,udscalability, and extensibility. In fact, experience gained during several smalludto mid-sized experiments that are presented in this thesis suggest that theudSALMA approach seems to be able to live up to these expectations.