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

Abstract

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
Volume18
DOIs
Publication statusPublished - 2009

Fingerprint

Specifications
Specification languages
Multi agent systems
Differential equations
Industry
Formal specification
Formal verification

Bibliographical note

IJCIS09

Cite this

@article{4eec0663a03f487287ce98b594a8e85a,
title = "Specification and Verification of Dynamics in Agent Models",
abstract = "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. {\circledC} 2009 World Scientific Publishing Company.",
author = "T. Bosse and C.M. Jonker and {van der Meij}, L. and O. Sharpanskykh and J. Treur",
note = "IJCIS09",
year = "2009",
doi = "10.1142/S0218843009001987",
language = "English",
volume = "18",
pages = "167--193",
journal = "International Journal of Cooperative Information Systems",
issn = "0218-8430",
publisher = "World Scientific Publishing Co. Pte Ltd",

}

Specification and Verification of Dynamics in Agent Models. / Bosse, T.; Jonker, C.M.; van der Meij, L.; Sharpanskykh, O.; Treur, J.

In: International Journal of Cooperative Information Systems, Vol. 18, 2009, p. 167-193.

Research output: Contribution to JournalArticleAcademicpeer-review

TY - JOUR

T1 - Specification and Verification of Dynamics in Agent Models

AU - Bosse, T.

AU - Jonker, C.M.

AU - van der Meij, L.

AU - Sharpanskykh, O.

AU - Treur, J.

N1 - IJCIS09

PY - 2009

Y1 - 2009

N2 - 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.

AB - 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.

U2 - 10.1142/S0218843009001987

DO - 10.1142/S0218843009001987

M3 - Article

VL - 18

SP - 167

EP - 193

JO - International Journal of Cooperative Information Systems

JF - International Journal of Cooperative Information Systems

SN - 0218-8430

ER -