Nick Papanikolaou’s research career has spanned a remarkably diverse range of fields, from quantum cryptography and formal methods through to cloud security, privacy, artificial intelligence and policy enforcement. A common thread running through all of his work is a fascination with trust in complex computer systems: how can we be certain that a system behaves correctly, protects sensitive information and complies with the rules that govern it? Rather than approaching these questions solely from a practical engineering perspective, he has often drawn upon mathematics, formal logic and computer science theory to develop rigorous methods for specifying, analysing and verifying the behaviour of computing systems.
One of his earliest areas of research involved the design of formal languages and logical frameworks for describing and analysing computational processes. Working with researchers including Paulo Mateus and Pedro Baltazar, he contributed to the development of EpCTL, a probabilistic temporal logic built upon Exogenous Probabilistic Propositional Logic (EPPL). The objective of this work was to provide powerful mathematical tools capable of reasoning about systems whose behaviour involves uncertainty and probability. Such formalisms allow researchers to express complex properties that a system should satisfy and then verify whether those properties hold. This line of research sits at the intersection of logic, computer science and mathematics, providing the theoretical foundations upon which reliable and trustworthy computational systems can be built.
Perhaps his most distinctive contributions came in the emerging field of quantum computing and quantum cryptography. At a time when the discipline was still largely confined to specialised research groups, he worked on applying formal verification techniques to quantum communication protocols. In collaboration with Rajagopal Nagarajan and Simon Gay, he helped develop QMC, a model checker designed specifically for analysing quantum communication and quantum cryptographic protocols. To the best of the researchers’ knowledge at the time, QMC was the first tool of its kind. The project was particularly ambitious because it sought to unite two traditionally separate worlds: the well-established field of formal verification and the fundamentally different mathematical framework of quantum information theory. By providing automated techniques for analysing quantum protocols, this work helped bring greater rigour to a rapidly developing field whose security guarantees depend upon subtle and highly complex physical and mathematical principles.
His interest in quantum systems extended beyond verification tools and into the design of programming languages themselves. During his undergraduate work, he expanded upon existing research into the formal verification of the BB84 quantum cryptographic protocol, one of the most famous protocols in quantum information science. He was also involved in the early development of Communicating Quantum Processes (CQP), a quantum process algebra equipped with a formal semantics and type system for describing quantum computations and communications. Building upon these foundations, he developed a quantum specification language for use with the QMC model checker, complete with both an operational semantics and a practical implementation. This research helped provide the conceptual and technical infrastructure required for treating quantum programs as rigorously analysable software artefacts rather than merely theoretical constructs.
In later years, his interests broadened into cloud computing, privacy, security, accountability and policy enforcement. Here he explored how organisations can ensure that information systems comply with legal, regulatory and organisational requirements, and how users can maintain confidence that their personal data is being handled appropriately. His work investigated mechanisms for formalising privacy policies, automating compliance processes, and connecting legal requirements with technical controls. More recently, these themes have naturally extended towards areas such as natural language processing and applied artificial intelligence, where automated systems increasingly need to interpret, enforce and reason about complex rules and policies. Taken together, his research portfolio reflects a consistent and ambitious vision: to develop methods that allow society to place greater trust in increasingly sophisticated computing systems, whether they are quantum communication networks, cloud platforms or the intelligent digital systems of the future.
Research Interests:
- cloud security and privacy
- policy formalisation and enforcement
- natural language processing, applied AI
- model checking and process algebra
- quantum cryptography
- Design of languages, logics and tools for protocol specification and verification
- In joint work with Paulo Mateus and Pedro Baltazar (IST Lisbon), Nick helped to develop EpCTL, a probabilistic temporal logic that uses EPPL (exogenous probabilistic propositional logic) as its core.
- Model checking
- In collaboration with Rajagopal Nagarajan and Simon Gay Nick developed a model checker, QMC, for the analysis of properties of quantum communication and quantum cryptographic protocols. QMC is the first of its kind to our knowledge. Earlier work has included the use of a classical, probabilistic model checker for the analysis of similar protocols. This work combined classical verification techniques and models with the mathematics of quantum computing and quantum information, so this is clearly interdisciplinary.
- Syntax and semantics of languages for quantum programming
- Nick’s undergraduate final year project ‘Formal Specification and Verification of Quantum Protocols’ extended the work ofSimon Gay and Rajagopal Nagarajan on verifying the security of the BB84 protocol using classical process algebra and the probabilistic model checker PRISM. He was involved in the early stages of development of CQP (Communicating Quantum Processes), a quantum process algebra with a formal semantics and type system. Nick developed a quantum specification language for use in conjunction with the QMC model checker; the language has an operational semantics and an implementation.