A Quantified Modal Logic for the Specification and Verification of Software Systems
- Day - Time: 22 October 2014, h.11:00
- Place: Area della Ricerca CNR di Pisa - Room: B-76
Speakers
- Fabio Gadducci (Dipartimento di Informatica - Università di Pisa)
Referent
Abstract
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.