Specification and Verification of Dynamics in Cognitive Agent Models
Citations Over TimeTop 1% of 2006 papers
Abstract
Within many domains, among which biological and cognitive areas, multiple interacting processes occur among agents with dynamics that are hard to handle. Current approaches to analyse the dynamics of such processes, often based on differential equations, are not always successful. As an alternative to differential equations, this paper presents the predicate logical temporal trace language (TTL) for the formal specification and analysis of dynamic properties. This language supports the specification of both qualitative and quantitative aspects, and therefore subsumes specification languages based on differential equations. A software environment has been developed for TTL, that 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 domains.
Related Papers
- → RealSpec: An Executable Specification Language for Modeling Control Systems(2009)5 cited
- The formalisation of specifications from specifications written in natural language(1996)
- → The PROFIBUS formal specification: a comparison between two FDTs(2001)6 cited
- A Formal Specification Language Supporting Specification Acquisition(2002)