Specifica e verifica di proprietà di sistemi aperti per mezzo di logica computazionale - Marco Alberti (Università di Ferrara)

I sistemi aperti sono quelli in cui interagiscono componenti osservabili solo attraverso il loro comportamento e che perseguono interessi propri; sono stati oggetto di studi approfonditi nelle aree dei sistemi multi-agente, dei servizi web e dei sistemi normativi.

Fra le tecniche della logica computazionale, i linguaggi di programmazione logica abduttiva e a vincoli forniscono espressività sufficiente per specificare le proprietà di un'ampia classe di sistemi aperti, mentre le loro controparti operazionali, grazie alle proprietà di correttezza rispetto alle rispettive semantiche dichiarative, costituiscono un appropriato meccanismo di verifica.

Il seminario verterà su alcune applicazioni ed estensioni di queste tecniche per la specifica e verifica di sistemi aperti.