5-year VIDI Project funded by the Innovational Research Incentives Scheme of the Dutch Science Foundation.
Reasoning about Quantum Interaction: logical modelling and verification of multi-agent quantum protocols (1 June 2010 - 1 June 2015)
ILLC, University of Amsterdam
As for classical computing, logic plays an essential role in the understanding of quantum computation and quantum information, and especially in the formal verification of quantum communication protocols. Such multi-agent applications involve quantum information flow and classical knowledge transfer (by classical communication) between the agents. One of our aims in this project was to develop the logical tools for modelling complex situations where different types of informational dynamics (classical and quantum) are combined. Our goal was to develop and use a combined classical-quantum logic for the full specification and formal verification of agent-based quantum protocols for secure communication. Towards this goal, we have used formalisms based on modal logic, especially combinations of dynamic (or temporal) logics and epistemic (or spatial) logics. But also other logical formalisms, such as probabilistic logic, linear logic and coalgebraic logic (or categorical logic, in general), have been studied in this context.