A note on stutter-invariant PLTL

作者：Cong Tian; Duan Zhenhua^*

来源：Information Processing Letters, 2009, 109(13): 663-667.

DOI：10.1016/j.ipl.2009.02.020

• Formal language
• Propositional Linear Temporal Logic
• Stutter-invariant
• Partial order reduction
• Normal from

Peled and Wilke proved that every stutter-invariant propositional linear temporal property is expressible in Propositional Linear Temporal Logic (PLTL) without O (next) operators. To eliminate next operators, a translation tau which converts a stutter-invariant PLTL formula phi to an equivalent formula tau(phi) not containing O operators has been given. By T, for any formula O phi. where phi contains no phi operators, a formula with the length of O(4(n) vertical bar phi vertical bar) is always produced, where n is the number of distinct propositions in phi, and vertical bar phi vertical bar is the number of symbols appearing in phi. Etessami presented an improved translation tau'. By tau', for O phi, a formula with the length of O(n x 2(n)vertical bar phi vertical bar) is always produced. We further improve Etessami's

• 出版日期2009-6-15
• 单位西安电子科技大学