Abstract
We study model checking for a first-order linear-time temporal logic. The computation model is based on Abstract State Machines (ASMs) in which data and data operations are described using abstract sorts and uninterpreted function symbols. ASMs are suitable for describing Register-Transfer level designs. We then define a first-order linear-time temporal logic called L MDG which supports the abstract data representations. Both safety and liveness properties can be expressed in L MDG, however, only universal path quantification is possible. Fairness constraints can also be imposed. The property checking algorithms are based on implicit state enumeration of an ASM and implemented using Multiway Decision Graphs.
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
Cyrluk D. and Narendran P. Ground temporal logic: A logic for hardware verification. In D. L. Dill, editor, Computer Aided Verification, volume 818 of Lecture Notes in Computer Science. Springer Verlag, 1994.
Emerson E. A. and Lei C. L. Modalities for Model Checking: Branching Time Logic Strikes Back. Science of Computer Programming, 8:275–306, 1987.
Clarke E. M. and Emerson E., A. Design and Synthesis of synchronization skeletons using branching time temporal logic. In Workshop on Logics of Programs, number 131 in Lecture Notes in Computer Science, pages 52–71, New York, 1981. Springer-Verlag.
Corella F., Langevin M., Cerny E., Zhou Z., and Song X. State enumeration with abstract descriptions of state machines. In Proc. IFIP WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods (Charme'95), Frankfurt, Germany, October 1995.
Corella F., Zhou Z., Song X., Langevin M., and Cerny E. Multiway decision graphs for automated hardware verification. Formal Methods in System Design, 10(1):746, February 1997.
Hungar H., Grumberg O., and Damm W. What if Model Checking Must Be Truly Symbolic. In Workshop on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'95), Aarhus, Denmark, May 1995.
Burch J. R. and Dill D. L. Automatic verification of pipelined microprocessor control. In D. L. Dill, editor, Proc. Work. on Computer-Aided Verification, number 818 in Lecture Notes in Computer Science. Springer Verlag, 1994.
Burch J. R., Clarke E. M., and McMillan K. L. Symbolic model checking: 1020 States and Beyond. In LICS, 1990.
McMillan K. L. Symbolic model checking: An approach to the state explosion problem. PhD thesis, School of Computer Science, Carnegie Mellon University, Pittsburgh, 1992.
Aït Mohamed O., Cerny E., and Song X. MDG-based verification by retaining and combinational transformations. In Magdy A. Bayoumi and Graham Jullien, editors, Proc. of the Great Lakes Symposium on VLSI (GLS-VLSI'98, pages 356–361, Lafayette, Louisiana, USA, 1998. IEEE Computer Society Press.
Aït Mohamed O., Song X., and Cerny E. On the Non-termination of MDG-based Abstract State Enumeration. In Proc. IFIP W 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods (Charme'97), Montréal, October 1997. IFIP, Chapmann & Hall.
Coudert O. and Madre J. C. A unified framework for the formal verification of sequential circuits. In International Conference on Computer-Aided Design, 1990.
Hojati R., Dill D. L., and Brayton R. K. Verifying linear temporal properties of data insensitive controllers using finite instantiations. In Conference on Hardware Description Languages (CHDL'97), April 1997.
Hojati R. and Brayton R. K. Automatic datapath Abstraction In Hardware Systems. In Conference on Computer-Aided Verification, June 1995.
Kurshan R. P. Reducibility in Analysis of Coordination. volume 103 of Lecture Notes in Computer Science, pages 19–39. Springer-Verlag, 1987.
Xu Y. Model checking for a first-order branching time temporal logic based on abstract description of state machines. PhD thesis, D'IRO, University of Montréal, 1998. Draft.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1998 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Xu, Y., Cerny, E., Song, X., Corella, F., Aït Mohamed, O. (1998). Model checking for a first-order temporal logic using multiway decision graphs. In: Hu, A.J., Vardi, M.Y. (eds) Computer Aided Verification. CAV 1998. Lecture Notes in Computer Science, vol 1427. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0028747
Download citation
DOI: https://doi.org/10.1007/BFb0028747
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-64608-2
Online ISBN: 978-3-540-69339-0
eBook Packages: Springer Book Archive