Optimizing CTL Satisfiability Tableaux Methods

James Thomson (SoCS CECS)

CS HDR MONITORING Logic & Computation Research Group

DATE: 2010-04-16
TIME: 10:00:00 - 10:30:00
LOCATION: RSISE Seminar Room, ground floor, building 115, cnr. North and Daley Roads, ANU
CONTACT: JavaScript must be enabled to display this email address.

ABSTRACT:
Digital circuits and parallel programs are growing in complexity, and designing them to meet a specification is increasingly difficult. Using temporal logics such as Computational Tree Logic (CTL) to specify the desired behaviour of these systems allows for automatic verification and is a well explored topic using the technology of "model checking".

Less explored is the problem of determining whether it is possible for any design to satisfy the specification (known as satisfiability) which is part of the larger problem of generating a design to meet a specification. Methods for CTL model checking cannot be used to determine satisfiability, so new, efficient methods are required.

I present the satisfiability problem for CTL along with the current state of the art, and propose some potential optimizations to a method based on Tableaux.
BIO:
PhD student in Computer Science.