On Formal Verification of ACT-R Architectures and Models
- Vincent Langenfeld, Department of Computer Science, Albert-Ludwigs-Universitat Freiburg, Freiburg, Germany
- Bernd Westphal, Department of Computer Science, Albert-Ludwigs-Universitat Freiburg ยจ, Freiburg, Germany
- Andreas Podelski, Department of Computer Science, Albert-Ludwigs-Universitat Freiburg, Freiburg, Germany
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.