Algorithms and Temporal Logics
Dr. John C. McCabe-Dansted (The University of Western Australia)
LOGIC AND COMPUTATION SEMINARDATE: 2013-04-16
TIME: 14:00:00 - 15:00: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:
Dr John McCabe-Dansted will present an overview of his work on logics for branching time and general linear flows of times. His thesis was on RoCTL*, and extension to the common branching time logic CTL* for reasoning about robustness. RoCTL* is no more expressive than CTL* but is shown to be exponentially succinct. Recent work has been on decision tableau for a weaker logics including BCTL* and Non-Local BCTL*.
The Non-Local tableau is used in ongoing work on automatic verification of rewrite rules with sample applications for crowd-sourcing and automatically generating rewrite rules. Other ongoing research includes a model checker of a recently specified language for expressing models for any satisfiable Real Temporal Logic formula, and potential extensions to Metric Temporal Logic.
BIO:
Dr John McCabe-Dansted is currently working at University of Western Australian on Metric and Linear logics. UWA was where he did his PhD on RoCTL*, a branching time logic for representing robustness. His masters thesis from the University of Auckland studied the computational properties of a voting rule suggested by Lewis Carroll. Current interests include tableaux, rewrite rules, Metric Logics and model checking Zeno properties.
