Proceedings of the Annual Meeting of the Cognitive Science Society

It is a long standing challenge to devise a formal model of ACT-R as a basis for formal reasoning on ACT-R. The ACT-R architecture is a composition of components (such as modules) with predefined interfaces between components and predefined interactions on the interfaces. Reasoning over the correctness of a formal model of ACT-R benefits from the separation of abstraction levels i.e. reasoning on the level of interfaces and interactions between components in isolation from the concrete behaviour of each component. We propose a formal semantics of ACT-R that preserves the structural properties of architectural components, i.e., the interfaces of modules to the remaining architecture as well as communication between modules within the architecture. We demonstrate how our new formal semantics of ACT-R serves to prove the correctness of the timed automaton based operational semantics for ACT-R (TA-ACT-R) on the level of architectural components.