kouken

0.LTLとは　

　LTL(エルティエル)は、Linear Tempral Logic(リニア テンポラル ロジック)の略です。日本語では線形時相論理式です。
　名前は難しいですが、とても簡単です。
　LTLは、未来の出来事を表現するためのものです。例えば、

□(私は呼吸する)

と書けば、「将来ずっと」私は呼吸し続けることを意味します。また、

◇(私は結婚する)


と記述すると、「将来いつか」私は結婚するということを意味します。

ま、こんな感じです。