logo ISTI

Istituto di Scienza e Tecnologie
dell’Informazione “A. Faedo”

an Institute of the National Research Council of Italy CNR

A Quantified Modal Logic for the Specification and Verification of Software Systems

22 October 2014, 11:00 - Location: B-76

Speakers:
Fabio Gadducci (Dipartimento di Informatica - Università di Pisa)
Referent:
Vincenzo Ciancia

Quantified modal logics (possibly extended with fixpoint operators) combine the modal operators with (existential) quantifiers: their intertwining allows for reasoning about the possible behavior of individual components within a software system. We present an extended Kripke semantics for such logics, based on labeled transition systems whose states are algebras and transitions are partial homomorphisms. Open formulae are interpreted over sets of state assignments (families of partial substitutions, associating formula variables to state components). Our proposal allows us to model and reason about the creation and deletion of components, as well as the merging of components, and it avoids the limitations of existing approaches. The talk is rounded up with some considerations about model checking and approximation techniques.

AREA DELLA RICERCA CNR DI PISA: VERSO LO SMART CAMPUS  (31 October 2014, 10:30)

31 Ottobre 2014 - Auditorium dell’Area della Ricerca CNR Via G. Moruzzi 1 – 56124 Pisa:

more news...