In Processes, We Believe! On Marrying Process Algebra and Epistemic Logic

Mohammad Mousavi

(Eindhoven University of Technology)

Process algebras, on one hand, provide a convenient means for specifying protocols. Epistemic models, on the other hand, are appropriate for specifying knowledge-related properties of such protocols (e.g., anonymity or secrecy). These two approaches to specification and verification have so far developed in parallel and one has either to define ad-hoc correctness criteria for the process-algebraic model or use complicated epistemic models to specify the behavioral aspects.

We work towards bridging this gap by proposing a combined framework which allows for modeling the behavior of a protocol in a process language with an operational semantics and supports reasoning about properties expressed in a rich logic which combines temporal and epistemic operators.

Further, we report on an extension of this framework with cryptographic construct and its influence on the epistemic aspects and conclude with a brief comparison of our semantic framework with the interpreted systems model of Fagin and Vardi. This talk does not assume any pre-knowledge of either of the two fields (and in particular of process algebras).
Thursday 23rd August 2012, 14:00
Board room
Department of Computer Science