Abstract
There has been a major emphasis recently in the semiconductor industry on designing industrial-strength property specification languages. Two major languages are ForSpec and Sugar 2.0, which are both extensions of Pnueli’s LTL. Both ForSpec and Sugar 2.0 directly support reset/abort signals, in which a check for a property Ψ may be terminated and declared successful by a reset/abort signal, provided the check has not yet failed. ForSpec and Sugar 2.0, however, differ in their definition of failure. The definition of failure in ForSpec is syntactic, while the definition in Sugar 2.0 is semantic. In this work we examine the implications of this distinction between the two approaches, which we refer to as the reset approach (for ForSpec) and the abort approach (for Sugar 2.0). In order to focus on the reset/abort issue, we do not consider the full languages, which are quite rich, but rather the extensions of LTL with the reset/abort constructs. We show that the distinction between syntactic and semantic failure has a dramatic impact on the complexity of using the language in a model-checking tool.
We prove that Reset-LTL enjoys the “fast-compilation property”: there is a linear translation of Reset-LTL formulas into alternating Büchi automata, which implies a linear translation of Reset-LTL formulas into a symbolic representation of nondeterministic Büchi automata. In contrast, the translation of Abort-LTL formulas into alternating Büchi automata is nonelementary (i.e., cannot be bounded by a stack of exponentials of a bounded height); each abort yields an exponential blow-up in the translation. This complexity bounds also apply to model checking; model checking Reset-LTL formulas is exponential in the size of the property, while model checking Abort-LTL formulas is nonelementary in the size of the property (the same bounds apply to satisfiability checking).
A full version of this paper is available at http://www.cs.rice.edu/~vardi/.
Chapter PDF
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
R. Armoni, L. Fix, R. Gerth, B. Ginsburg, T. Kanza, A. Landver, S. Mador-Haim, A. Tiemeyer, E. Singerman, M.Y. Vardi, and Y. Zbar. The ForSpec temporal language: A new temporal property-specification language. In Proc. 8th Int’l Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’02), Lecture Notes in Computer Science 2280, pages 296–311. Springer-Verlag, 2002.
I. Beer, S. Ben-David, C. Eisner, D. Fisman, A. Gringauze, and Y. Rodeh. The temporal logic sugar. In Proc. Conf. on Computer-Aided Verification, LNCS 2102, pages 363–367, 2001.
J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill, and L.J. Hwang. Symbolic model checking: 1020 states and beyond. Information and Computation, 98(2):142–170, June 1992.
R. Gerth, D. Peled, M.Y. Vardi, and P. Wolper. Simple on-the-fly automatic verification of linear temporal logic. In P. Dembiski and M. Sredniawa, editors, Protocol Specification, Testing, and Verification, pages 3–18. Chapman & Hall, August 1995.
S.M. Nowick K. van Berkel, M.B. Josephs. Applications of asynchronous circuits. Proceedings of the IEEE, 1999. special issue on asynchronous circuits & systems.
O. Kupferman and M.Y. Vardi. Model checking of safety properties. Formal methods in System Design, 19(3):291–314, November 2001.
R.P. Kurshan. Formal verification in a commercial setting. In Proc. Conf. on Design Automation (DAC’97), volume 34, pages 258–262, 1997.
R.P. Kurshan. FormalCheck User’s Manual. Cadence Design, Inc., 1998.
H.R. Lewis. Complexity of solvable cases of the decision problem for the predicate calculus. In Foundations of Computer Science, volume 19, pages 35–47, 1978.
S. Miyano and T. Hayashi. Alternating finite automata on ω-words. Theoretical Computer Science, 32:321–330, 1984.
M.J. Morley. Semantics of temporal e. In T. F. Melham and F.G. Moller, editors, Banff’99 Higher Order Workshop (Formal Methods in Computation). University of Glasgow, Department of Computing Science Technical Report, 1999.
D.E. Muller, A. Saoudi, and P.E. Schupp. Alternating automata, the weak monadic theory of the tree and its complexity. In Proc. 13th Int. Colloquium on Automata, Languages and Programming, LNCS 226, 1986.
A. Pnueli. The temporal logic of programs. In Proc. 18th IEEE Symp. on Foundation of Computer Science, pages 46–57, 1977.
A.P. Sistla and E.M. Clarke. The complexity of propositional linear temporal logic. Journal ACM, 32:733–749, 1985.
A comparison of reset control methods: Application note 11. http://www.summitmicro.com/tech_support/notes/note11.htm, Summit Microelectronics, Inc., 1999.
W. Thomas. A combinatorial approach to the theory of ω-automata. Information and Computation, 48:261–283, 1981.
P. van Emde Boas. The convenience of tilings. In Complexity, Logic and Recursion Theory, volume 187 of Lecture Notes in Pure and Applied Mathetaics, pages 331–363, 1997.
M.Y. Vardi. An automata-theoretic approach to linear temporal logic. In Logics for Concurrency: Structure versus Automata, LNCS 1043, pages 238–266, 1996.
M.Y. Vardi and P. Wolper. An automata-theoretic approach to automatic program verification. In Proc. 1st Symp. on Logic in Computer Science, pages 332–344, 1986.
M.Y. Vardi and P. Wolper. Automata-theoretic techniques for modal logics of programs. Journal of Computer and System Science, 32(2):182–221, April 1986.
M.Y. Vardi and P. Wolper. Reasoning about infinite computations. Information and Computation, 115(1):1–37, November 1994.
H. Wang. Dominoes and the aea case of the decision problem. In Symposium on the Mathematical Theory of Automata, pages 23–55, 1962.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Armoni, R., Bustan, D., Kupferman, O., Vardi, M. (2003). Resets vs. Aborts in Linear Temporal Logic. In: Garavel, H., Hatcliff, J. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2003. Lecture Notes in Computer Science, vol 2619. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-36577-X_6
Download citation
DOI: https://doi.org/10.1007/3-540-36577-X_6
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-00898-9
Online ISBN: 978-3-540-36577-8
eBook Packages: Springer Book Archive