Generating Linear Temporal Logics Based on Property Specification Templates

Weibin Luo, Hironori Washizaki*, Yoshiaki Fukazawa


研究成果: Chapter


Temporal logics are widely used in software verification such as model checking. However, creating temporal logics such as linear temporal logics (LTLs) based on property specifications written in a natural language is difficult due to practitioners’ unfamiliarity with property specifications and notations of temporal logics. Although property specification patterns have been introduced to help write correct temporal logics, creating temporal logics using property specification patterns requires an understanding of the pattern system. Since some patterns are difficult to understand, especially for beginners, and the final temporal logics are usually complicated, creating temporal logics using pattern systems is time consuming and error-prone. Here, we introduce a method to create LTLs based on property specification patterns. We experimentally compare the required time and accuracy of our approach to those using property specification patterns. Our approach can improve the creation of LTLs in terms of speed and accuracy. Although our experiment is implemented in Japanese, the results should be applicable to other languages such as English. We also provide a visualization scheme so that practitioners can understand the generated LTLs and confirm that they are correct.

ホスト出版物のタイトルStudies in Computational Intelligence
出版社Springer Verlag
出版ステータスPublished - 2020


名前Studies in Computational Intelligence

ASJC Scopus subject areas

  • 人工知能


「Generating Linear Temporal Logics Based on Property Specification Templates」の研究トピックを掘り下げます。これらがまとまってユニークなフィンガープリントを構成します。