| Seminar on Computation
Theory
蔡益坤教授
(
臺灣大學資訊管理系 )
Decomposing and Composing Specifications in Temporal Logic
摘要
| | Temporal logic (specifically first-order Linear-Time Temporal Logic of Manna and Pnueli) is one convenient formalism for specifying and reasoning about concurrent systems and their properties. Fundamental concepts in formal verification such as refinement (implementation),hiding, and parallel composition can all be conveniently treated with the logic.In this talk, I will show how to prove that a concrete composite system implements an abstract composite system by reasoning about their constituent modules.I will also show how to write the specification of a reusable module and to derive properties from a composition of such modules.
(Note: The subject of this talk is intent to complement the
complexity- theoretical aspects of temporal logic addressed in earlier two talks by Professor Yen and Professor Lei.)
|
91年4月24日 (星期三)
16:10-17:00
台灣大學數學系新數館308室
|