Abstract / Description of output
Peled and Wilke [Inform. Process. Letters 63 (1997) 243] showed that the stutter-invariant languages expressible in linear propositional temporal logic (LTL) are precisely those expressible in LTL without the “next”-time operator. They did so by providing a translation, τ , which converts a stutter-invariant LTL formula ϕ to an equivalent formula τ(ϕ) not containing the “next” operator. Their τ(ϕ) is exponentially larger than ϕ , with a worst case upper bound of |τ(ϕ)|≤2O(n×k)×|ϕ| , where n is the number of distinct propositions in ϕ , and k is the “next”-depth of ϕ .
They asked whether this exponential blowup can be avoided. We give an improved translation, τ′ , which incurs a worst case blowup of |τ′(ϕ)|≤nO(k)×|ϕ| . This remains exponential in the “next”-depth of ϕ . However, if formulas are viewed as circuits, where identical subformulas are shared, and size is measured in terms of the number of distinct subformulas, one gets the following bound: |τ′(ϕ)|≤O(|ϕ|+n2) .
The computation complexity of major algorithms based on LTL, e.g., model checking and translation to automata, is only affected by the number of distinct subformulas. So, without loss of efficiency, one can work with LTL circuits rather than formulas for those purposes. As a particular application, our upper bound on circuit size gives an alternative proof of the PSPACE upper bound due to Peled et al. [Theoret. Comput. Sci. 195 (1998) 183] for checking stutter-invariance of a temporal property: simply apply the well known (and by now heavily optimized) algorithms for testing validity of LTL formulas of Sistla and Clarke [J. ACM 32 (1985) 733] and Vardi and Wolper [First Annual IEEE Symp. on Logic in Comput. Sci., 1986, p. 322] to the circuit for ϕ↔τ′(ϕ) .
They asked whether this exponential blowup can be avoided. We give an improved translation, τ′ , which incurs a worst case blowup of |τ′(ϕ)|≤nO(k)×|ϕ| . This remains exponential in the “next”-depth of ϕ . However, if formulas are viewed as circuits, where identical subformulas are shared, and size is measured in terms of the number of distinct subformulas, one gets the following bound: |τ′(ϕ)|≤O(|ϕ|+n2) .
The computation complexity of major algorithms based on LTL, e.g., model checking and translation to automata, is only affected by the number of distinct subformulas. So, without loss of efficiency, one can work with LTL circuits rather than formulas for those purposes. As a particular application, our upper bound on circuit size gives an alternative proof of the PSPACE upper bound due to Peled et al. [Theoret. Comput. Sci. 195 (1998) 183] for checking stutter-invariance of a temporal property: simply apply the well known (and by now heavily optimized) algorithms for testing validity of LTL formulas of Sistla and Clarke [J. ACM 32 (1985) 733] and Vardi and Wolper [First Annual IEEE Symp. on Logic in Comput. Sci., 1986, p. 322] to the circuit for ϕ↔τ′(ϕ) .
Original language | English |
---|---|
Pages (from-to) | 261-263 |
Number of pages | 3 |
Journal | Information Processing Letters |
Volume | 75 |
Issue number | 6 |
DOIs | |
Publication status | Published - 2000 |