Finding Minimal Unsatisfiable Subsets in Temporal Logic

Research areas

Temporary Supervisor

Professor Rajeev Gore

Description

Temporal logic extends classical propositional logic by adding connectives for "eventually in the future" (F), "always in the future" (G), "tomorrow" (X), and "until" (U). Thus we can express "always in the future, if we get a request to open a bank account ro then eventually we have to conduct a risk assessment ra" as G(ro => F ra). Temporal logic can be used to encode a collection of rules and is commonly used to specify banking rules as shown in the above example. It is quite common for a collection of rules to be inconsistent and it is important to be able to find a minimal set of inconsistent rules, so that one or more of them can be changed to remove the inconsistency. Recently, it has been shown by Jinbo Huang that binary decision diagrams (BDDs) can be used to find minimal inconsistent sets of formulae in classical propositional logic.

Goals

The project is to extend this method to find minimal inconsistent subsets in temporal logic.

Requirements

You will have a good background in discrete mathematics and ideally will have already taken some courses in logic e.g. COMP2600, COMP2620, COMP6430. You will also need a good background in programming, and this will be an important part of the project.

Background Literature

You will need to study the procedure by Huang and will need to study how BDDs are used in temporal logic (we will give you the papers). You will then need to combine the use of BDDs in temporal logic, with the algorithm by Huang to solve the problem. You will also need to do a literature review of other methods for finding minimal inconsistent sets in temporal logic.

Gain

Successful completion may lead to a publication in an international conference.

Keywords

temporal logic, automated reasoning, logic

Updated:  1 June 2019/Responsible Officer:  Dean, CECS/Page Contact:  CECS Marketing