Student research opportunities
Finding Minimal Unsatisfiable Subsets in Temporal Logic
Project Code: CECS_867
This project is available at the following levels:
Honours
Please note that this project is only for undergraduate students.
Keywords:
temporal logic, automated reasoning, logic
Supervisors:
Professor Rajeev GoreDr Jinbo HUANG
Outline:
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 of this project
The project is to extend
this method to find minimal inconsistent subsets in temporal logic.
Requirements/Prerequisites
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.
Student Gain
Successful completion may lead to a publication in an international
conference.
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.
