Linear-time temporal logic (LTL) is one of the most prominent logics for the specification and verification of reactive and concurrent systems. Its basic principle is to specify the correctness of a program as a set of infinite sequences, called traces, which define the acceptable executions of the system. The classical approach using LTL does not suffice for properties of traces which relate multiple execution traces. Such properties (termed hyperproperties) are of prime interest in information flow security, where dependencies between the secret inputs and the publicly observable outputs of a system are considered potential security violations. There are two modern approaches to define logics for hyperproperties: 1) Hyperlogics HyperLTL, HyperCTL etc. which extend classical temporal logics with named quantification of traces, 2) Team based logics TeamLTL, TeamCTL etc. which use the so-called team semantics to express hyperproperties directly without trace quantifiers.
The goal of this project is to develop the theory of team based logics for hyperproperties. The concrete direction the student takes is quite flexible. One exciting direction would be to develop the theory of quantitative hyperproperties which can express, e.g., fairness properties such as a request is granted in 75% of the time, and to study the related expressivity and complexity issues therein. The student will have the possibility to collaborate with prominent international experts, e.g., from CISPA Helmholtz Center for Information Security, University of Helsinki, Leibniz Universität Hannover, and University of Münster.
Related work on TeamLTL and related logics:
Ideas how to implement quantitative features to TeamLTL can be drawn, e.g., from the following papers:
Applicants should hold a very good degree (preferably a masters) in a relevant subject (i.e., Logic, Computer Science, or Mathematics). Candidates with exceptional undergraduate Honours degrees are also considered. The project requires a good understanding of logic, and the willingness to learn the necessary mathematical background in computational complexity theory.
If English is not your first language, you must have an IELTS score of 6.5 overall, with no less than 6.0 in each component.
To apply for the studentship, applicants need to apply directly to the University of Sheffield using the online application system. Please name Dr Jonni Virtema as your proposed supervisor.
Complete an application for admission to the standard Computer Science PhD programme
Applications should include a research proposal, CV, transcripts and two references.
The research proposal (up to 4 A4 pages, including references) should outline your reasons for applying for this scholarship and how you would approach the researching, including details of your skills and experience in logic and complexity theory.