Abstract
This text includes verification of the basic algorithm in Simple On-the-fly Automatic Verification of Linear Temporal Logic (LTL). LTL formula can be transformed to Buchi automaton, and this transforming algorithm is mainly used at Simple On-the-fly Automatic Verification. In this article, we verified the transforming algorithm itself. At first, we prepared some definitions and operations for transforming. And then, we defined the Buchi automaton and verified the transforming algorithm.
MML identifier: MODELC 3, version: 7.9.03 4.108.1028
Language: English
Page range: 339 - 353
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, Yasunari Shidama, published by University of Białystok
This work is licensed under the Creative Commons License.