On Formal Verification of ACT-R Architectures and Models

AbstractSubject of this article is the question whether the potential for automatic defect analysis for symbolic timed ACT-R models as demonstrated in earlier work can be developed into a scalable and comprehensible technique. We present a formal, operational model of an ACT-R architecture and a translation scheme of ACT-R models into timed automata. We have applied this translation to ACT-R models and report on scalability experiments with automatic defect analysis.

Return to previous page