Abstract
In this paper we describe the ForSpec Temporal Logic (FTL), the new temporal property-specification logic of ForSpec, Intel’s new formal specification language. The key features of FTL are as follows: it is a linear temporal logic, based on Pnueli’s LTL, it is based on a rich set of logical and arithmetical operations on bit vectors to describe state properties, it enables the user to define temporal connectives over time windows, it enables the user to define regular events, which are regular sequences of Boolean events, and then relate such events via special connectives, it enables the user to express properties about the past, and it includes constructs that enable the user to model multiple clock and reset signals, which is useful in the verification of hardware design.
A longer version of this paper can be found at www.cs.rice.edu/~vardi/papers/
Supported in part by NSF grants CCR-9700061, CCR-9988322, IIS-9908435, IIS-9978135, and EIA-0086264, by BSF grant 9800096, and by a grant from the Intel Corporation.
Chapter PDF
Similar content being viewed by others
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. Alur and T.A. Henzinger. Logics and models of real time: a survey. In J.W.de Bakker, K. Huizing, W.-P. de Roever, and G. Rozenberg, editors, Real Time: Theory in Practice, Lecture Notes in Computer Science 600, pages 74–106. Springer-Verlag, 1992.
B. Banieqbal and H. Barringer. Temporal logic with fixed points. In B. Banieqbal, H. Barringer, and A. Pnueli, editors, Temporal Logic in Specification, volume 398 of Lecture Notes in Computer Science, pages 62–74. Springer-Verlag, 1987.
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 (CAV’00), volume 2102 of Lecture Notes in Computer Science, pages 363–367. Springer-Verlag, 2001.
I. Beer, S. Ben-David, and A. Landver. On-the-fly model checking of RCTL formulas. In Computer Aided Verification, Proc. 10th International Conference, volume 1427 of Lecture Notes in Computer Science, pages 184–194. Springer-Verlag, 1998.
A. Cimatti, E.M. Clarke, F. Giunchiglia, and M. Roveri. Nusmv: a new symbolic model checker. It’l J. on Software Tools for Technology Transfer, 2(4):410–425, 2000.
R. Cleaveland, G. Luttgen, and M. Mendler. An algebraic theory of multiple clocks. In Proc. 8th Int’l Conf. on Concurrency Theory (CONCUR’97), volume 1243 of Lecture Notes in Computer Science, pages 166–180. Springer-Verlag, 1998.
E.A. Emerson. Temporal and modal logic. In J. Van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B, chapter 16, pages 997–1072. Elsevier, MIT press, 1990.
E.A. Emerson and R.J. Trefler. Generalized quantitative temporal reasoning: An automata theoretic. In Proc. Theory and Practice of Software Development (TAPSOFT), volume 1214 of Lecture Notes in Computer Science, pages 189–200. Springer-Verlag, 1997.
B. Finkbeiner. Symbolic refinement checking with nondeterministic BDDs. In Tools and algorithms for the construction and analysis of systems, Lecture Notes in Computer Science. Springer-Verlag, 2001.
M.J. Fischer and R.E. Ladner. Propositional dynamic logic of regular programs. Journal of Computer and Systems Sciences, 18:194–211, 1979.
J.G. Henriksen and P.S. Thiagarajan. Dynamic linear time temporal logic. Annals of Pure and Applied Logic, 96(1–3):187–207, 1999.
D. Kozen. Results on the propositional μ-calculus. Theoretical Computer Science, 27:333–354, 1983.
O. Kupferman, N. Piterman, and M.Y. Vardi. Extended temporal logic revisited. In Proc. 12th International Conference on Concurrency Theory, volume 2154 of Lecture Notes in Computer Science, pages 519–535, August 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.
O. Kupferman and M.Y. Vardi. Model checking of safety properties. Formal methods in System Design, 19(3):291–314, November 2001.
C. Liu and M.A. Orgun. Verification of reactive systems using temporal logics with clocks. Theoretical Computer Science, 220:377–408, 1999.
O. Lichtenstein, A. Pnueli, and L. Zuck. The glory of the past. In Logics of Programs, volume 193 of Lecture Notes in Computer Science, pages 196–218, Brooklyn, June 1985. Springer-Verlag.
M.J. Morley. Semantics of temporal e. In T. F. Melham and F.G. Moller, editors, Banff’99 Higher OrderWorkshop (Formal Methods in Computation). University of Glasgow, Department of Computing Science Technical Report, 1999.
A. Pnueli. In transition from global to modular temporal reasoning about programs. In K. Apt, editor, Logics and Models of Concurrent Systems, volume F-13 of NATO Advanced Summer Institutes, pages 123–144. Springer-Verlag, 1985.
T. Schlipf, T. Buechner, R. Fritz, M. Helms, and J. Koehl. Formal verification made easy. IBM Journal of Research and Development, 41(4:5), 1997.
A.P. Sistla, M.Y. Vardi, and P. Wolper. The complementation problem for Büchi automata with applications to temporal logic. Theoretical Computer Science, 49:217–237, 1987.
M.Y. Vardi. An automata-theoretic approach to linear temporal logic. In F. Moller and G. Birtwistle, editors, Logics for Concurrency: Structure versus Automata, volume 1043 of Lecture Notes in Computer Science, pages 238–266. Springer-Verlag, Berlin, 1996.
M.Y. Vardi. Branching vs. linear time: Final showdown. In Proc. Tools and Algorithms for the Construction and Analysis of Systems (TACAS), volume 2031 of Lecture Notes in Computer Science, pages 1–22. Springer-Verlag, 2001.
M.Y. Vardi and P. Wolper. Reasoning about infinite computations. Information and Computation, 115(1):1–37, November 1994.
P. Wolper. Temporal logic can be more expressive. Information and Control, 56(1–2):72–99, 1983.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Armoni, R. et al. (2002). The ForSpec Temporal Logic: A New Temporal Property-Specification Language. In: Katoen, JP., Stevens, P. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2002. Lecture Notes in Computer Science, vol 2280. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-46002-0_21
Download citation
DOI: https://doi.org/10.1007/3-540-46002-0_21
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-43419-1
Online ISBN: 978-3-540-46002-2
eBook Packages: Springer Book Archive