Abstract
Firstly in this paper, we propose a branching time logic BRTL (Branching time Regular Temporal Logic) which has automata connectives as temporal operators. BRTL is more expressive than CTL proposed by Clarke et.al. and it is modest in terms of model checking, i.e. it has a model checking algorithm which runs in time proportional both to the size of a given Kripke structure and to the length of a given formula, as shown in the paper.
Secondly, in order to improve the succinctness of the temporal logic formulas, we introduce the mechanism of substitutions to Boolean variables and references to the Boolean variables. We propose EBRTL(Extended BRTL), i.e. BRTL with the substitution mechanism, and show examples of descriptions of some temporal properties. We develop its model checking algorithm whose time complexity is linear both in the size of a given Kripke structure and in the length of a given formula and exponential in the number of the Boolean variables used in the formula.
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
E. M. Clarke, E. A. Emerson, and A. P. Sistla. Automatic Verification of Finite State Concurrent Systems Using Temporal Logic Specifications: A Practical Approach. In 10th ACM Symposium on Principles of Programming Languages, pages 117–126, January 1983.
M. C. Browne, E. M. Clarke, D. L. Dill, and B. Mishra. Automatic Verification of Sequential Circuits Using Temporal Logic. IEEE Transactions on Computers, C-35(12):1035–1044, December 1986.
H. Hiraishi. Design Verification of Sequential Machines Based on a Model Checking Algorithm of ɛ-free Regular Temporal Logic. In Computer Hardware Description Languages and their applications, pages 249–263, June 1989.
E. M. Clarke and O. Grümberg and R. P. Kurshan. A Synthesis of Two Approached for Verifying Finite State Concurrent Systems. Technical report, Carnegie Mellon University, 1987. manuscript.
P. Wolper. Temporal Logic Can Be More Expressive. In Proceedings of 22nd Annual Symposium on Foundations of Computer Science, pages 340–348, 1981.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1991 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Hamaguchi, K., Hiraishi, H., Yajima, S. (1991). Branching time regular temporal logic for model checking with linear time complexity. In: Clarke, E.M., Kurshan, R.P. (eds) Computer-Aided Verification. CAV 1990. Lecture Notes in Computer Science, vol 531. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0023739
Download citation
DOI: https://doi.org/10.1007/BFb0023739
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-54477-7
Online ISBN: 978-3-540-38394-9
eBook Packages: Springer Book Archive