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
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.