Theoretical Projects about Finite Automata and Temporal Logic

Potential supervisors: 
Research groups/keywords: 

General Background

Temporal logic is a popular language to write specifications of programs. A temporal logic formula is evaluated over traces (of programs) and is either true or false for a given trace. Normally, a very important property is that of satisfiability - the existence of a trace that satisfies a property. Clearly, if a formula is unsatisfiable it is not very interesting to check whether a given trace satisfies it or not as the answer is always no.

Accordingly, temporal logic is used to write specifications of programs and, for example, a program can be model checked to ensure that all its traces satisfy the property or a program can be monitored during runtime to ensure that the produced trace satisfies the property.

Algorithmically, a logic formula is hard to work with. One of the most successful approaches for handling temporal logic is called the Automata-Theoretic Approach to Temporal Logic. In general, temporal logic formulas are translated to automata and algorithms are applied to automata rather than to logic formulas directly.

The project

The project covers a range of options for working on temporal logic and automata. A few concrete ideas are suggested below. But there are many interesting options to explore that can be decided by negotiation with the supervisor.

  • Create a version of alternating timed automata that can be reasoned on. This has implications for constructions that relate to metric temporal logic.
  • Extend quantitative versions of temporal logic and design algorithms for reasoning about them.

The student will have to ramp up on the theoretical part - understanding the involved issues and the models of computation involved. The rest of the project consists of interacting with mathematical ideas and proving things about them.

Related Courses: Finite automata theory and formal languages, Formal Methods in Software Development

Prerequisites: Automata theory, logic, discrete mathematics

Desired: Temporal logics and formal verification, formal modelling and verification tools

Date range: 
September, 2020 to September, 2025