Specification and Verification of Dynamics in Agent Models

T. Bosse, C.M. Jonker, L. van der Meij, O. Sharpanskykh, J. Treur

Research output: Contribution to JournalArticleAcademicpeer-review


Within many domains, among which biological, cognitive, and social areas, multiple interacting processes occur among agents with dynamics that are hard to handle. This paper presents the predicate logical Temporal Trace Language (TTL) for the formal specification and analysis of dynamic properties of agents and multi-agent systems. This language supports the specification of both qualitative and quantitative aspects, and therefore subsumes specification languages based on differential equations and qualitative, logical approaches. A software environment has been developed for TTL, which supports editing TTL properties and enables the formal verification of properties against a set of traces. The TTL environment proved its value in a number of projects within different biological, cognitive and social domains. © 2009 World Scientific Publishing Company.
Original languageEnglish
Pages (from-to)167-193
JournalInternational Journal of Cooperative Information Systems
Publication statusPublished - 2009

Bibliographical note



Dive into the research topics of 'Specification and Verification of Dynamics in Agent Models'. Together they form a unique fingerprint.

Cite this