CSSE Seminar Series (CSSESS)
Welcome to the web page describing past, present, and future seminars presented by staff, students, and visitors to the Department of Computer Science and Software Engineering.
View past or future seminars; or view the CSSESS Home Page.
Seminar
Axiomatizing Propositional Linear Temporal Logic at home of A. Prior.
Speaker: Nikolai V. Shilov, visiting Erskine Fellow.
Institute: Russian Academy of Science.
Time/Place: 10:00 AM, Wed, 6 Aug, in Room 031, Erskine Building.
Abstract
The modern temporal logic was founded by Arthur N. Prior, Professor of Philosophy at Canterbury University College (1952-58). His J. Locke Lectures "Time and Modality" delivered in the University of Oxford (1955 -56) have been published and translated several times.
Anir Pnueli was the first to propose the use of temporal logic for reasoning about the programs. His paper "Temporal Logic of Programs" (1981) was inspirited by A. Prior lectures "Time and Modality". In 1996 A. Pnueli became a laureate of the ACM Turing Award "for seminal work introducing temporal logic into computing science and for outstanding contributions to program and systems verification".
Propositional version of the temporal logic of A. Pnueli is known as Propositional Linear Temporal Logic (PLTL). It is a very popular formalism for specification and verification of computer programs and systems. Fundamental results on decidability and axiomatization for PLTL have become a part of the Computer Science classics. The decidability issues for PLTL have been studied in Theoretical Computer Science and Applied Mathematical Logic communities on base of modal logic tradition and within automata-theoretic approach. In contrast, axiomatizations for PLTL were examined in the line of pure model logic tradition only.
The talk presents NEW axiomatization of PLTL based on pure Computer Science approach that combines automata-theoretic decidability coupled with tableau for local model checking.
Biography
View past or future seminars; or view the CSSESS Home Page.