A framework for the formal operational description of ACT-R.

Psychological theories can be validated by comparing the predictions of an ACT-R model, which implements the psychological theory, to experimental data. For this approach, the model needs to be valid, i.e., the implementation of the model must not contain defects that skew the model’s predictions and may thus lead to acceptance of an incorrect psychological theory or vice versa. In recent work we presented formal analysis methods allowing for the exhaustive exploration of ACT-R models for defects. These methods rely on manual formalizations of ACT-R models and of the architecture, which determines possible model executions (e.g., by rule selection or buffer actions). Both formalization steps present threats to the validity of the analysis: Defects in an ACT-R model may remain undetected in case of errors. Our contribution addresses both formalization activities. We present a Timed Automata based framework for the operational formal description of cognitive architectures. The framework defines interfaces and invariants such that each implementation of the interface (by particular formalisations of modules) supports the execution of ACT-R model formalisations. We provide one exemplary implementation as a formalisation of ACT-R’s textual architecture description. Given the well-structured formalisation of the architecture, the formalisation of a model can be automatised. Overall, we obtain an automatic analysis of ACT-R models for defects on a formal model of the ACT-R architecture, as well as a strong perspective for the definition and analysis of other module implementations or whole other architectures.