Abstract
This article provides the definition of linear temporal logic (LTL) and its properties relevant to model checking based on [9]. Mizar formalization of LTL language and satisfiability is based on [2, 3].
Language: English
Page range: 231 - 245
Published on: Mar 20, 2009
Published by: University of Białystok
In partnership with: Paradigm Publishing Services
Publication frequency: 1 issue per year
Related subjects:
© 2009 Kazuhisa Ishida, published by University of Białystok
This work is licensed under the Creative Commons License.