Modeling and Analyzing Spike Timing Dependent Plasticity With Linear Hybrid Automata
The authors propose a model for synaptic plasticity according to the Spike Timing Dependent Plasticity (STDP) theory using Linear Hybrid Automata (LHA). They first present a compositional LHA model in which each component corresponds to some process in STDP. They then abstract this model into a monolithic LHA model in order to enable formal analysis using hybrid model checking. They discuss how the availability of an LHA model as well as its formal analysis using the tool PHAVer can support a better understanding of the dynamics of STDP.