Schedule: 1 October, 11:30 – 12.30
Place: GSSI – MLH, v. Francesco Crispi 7

Speaker: Mohammad Reza Mousavi
School of Informatics – Data-Oriented Software Engineering, University of Leicester, UK 
https://www2.le.ac.uk/departments/informatics/people/mohammad-mousavi

Title: Combining Epistemic and Operational Aspects in Compositional Verification of Protocols

Abstract: We propose a framework to reason about what rational agents know or believe, when they observe and relate different operational runs (histories) of the protocol. Our framework is based on a combination of modal mu-calculus and epistemic logic. We investigate decompositional verification methods for this type of reasoning. Finally, we draw parallels to between epistemic reasoning and reasoning about causality and present initial ideas on a decompositional method for reasoning about causality.

(Based on joint work with Georgiana Caltais, Francien Dechesne, Stefan Leue, and Simona Orzan) 

 

Combining Epistemic and Operational Aspects in Compositional Verification of Protocols

Leave a Reply

Your email address will not be published. Required fields are marked *