Questa tesi mostra una formalizzazione delle reti neurali spiking ottenuta tramite automi temporizzati. Tali reti, a differenza di quelle di seconda generazione, tengono conto anche della dimensione temporale. Sono mostrate due codifiche, sincrona e asincrona, del modello "leaky integrate and fire": i neuroni sono modellati come automi temporizzati che attendono impulsi su dei canali di ingresso e aggiornano il potenziale in base agli input presenti e passati, modulati dai pesi delle rispettive sinapsi e tanto più influenti quanto più recenti. Se il potenziale supera una certa soglia, l'automa emette un segnale sul canale di uscita. Dopo ogni emissione i neuroni rimangono silenti per un periodo refrattario fissato per poi resettarsi. Nel modello asincrono gli input si assumono molto frequenti ma non possono essere contemporanei. In quello sincrono tutti gli impulsi ricevuti nello stesso periodo di accumulazione sono simultanei. Una rete neurale è ottenuta eseguendo in parallelo più automi che condividono canali opportunamente. Anche le sequenze in input sono specificate tramite automi temporizzati, detti generatori, ottenuti tramite un procedimento automatico, da un linguaggio che modella sequenze di spike e pause. Per il modello sincrono si verifica la capacità di riprodurre alcuni comportamenti noti in letteratura. Esso è poi sfruttato per trovare i pesi sinaptici che permettano ad una rete di riprodurre un comportamento dato, espresso tramite logica temporale. Ciò è ottenuto tramite un algoritmo che identifica gli errori commessi dai neuroni di output e applica delle azioni correttive sulle loro sinapsi in ingresso. Le informazioni sulle azioni correttive adeguate vengono poi propagate all'indietro verso gli altri neuroni della rete. Questo processo è ripetuto fino alla riproduzione del comportamento desiderato. Due gli approcci implementativi presentati: uno basato sulla simulazione e uno basato sul model-checking.