Preconditions for Realisability

Potential supervisors: 
Research groups/keywords: 
Description: 

 

Satisfiability, Realisability, and Synthesis

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.

In recent years, temporal logic is used also for automatically producing programs that are ensured to satisfy the specifications. The events that the formula relates to are partitioned to input and output and the requirement is for a machine that will receive inputs and reply with outputs in a way that satisfies the specification. For example, here  this technique is used to produce a plan for a robot from a high level specification of its desired behavior.

In this context the relevant questions are those of realisability - does there exist an open system (can receive all inputs) that sets the outputs so that the specification holds - and synthesis - the actual production of such a system.

In general, realisability is computationally demanding and sometimes specifications are wrong. We want to check preconditions for realisability that will be easier to check. For example, an unsatisafiable formula is clearly not realisable. Checking satisfiability is much easier than checking realisablity.

The project:

The goal of this project is to find preconditions for realisability that are easier to check and evaluate whether they are interesting in practice.

For the theoretical part - after getting to understand the involved issues - we could discuss several preliminary ideas on which direction to follow. For example, projecting out the outputs and checking the universality of the resulting automaton is one option. Other options include analysis of the formula so that *locally* it allows all the required options, but does not care about the long term goals required.

For the practical part - one can rely on tools for analysis of formulas and their translation to automata as well as many analysis tools that are available for automata. Synthesis competitions can be a source for interesting benchmarks.

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

Prerequisites: Programming (Java, Python, …), automata theory, logic.

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

Contact: Nir Piterman (piterman@chalmers.se)

Date range: 
September, 2020 to September, 2025