Temporal logics and their applications to formal design verification of finite-state machines 時相論理とその有限状態機械の形式的設計検証への応用

Access this Article

Search this Article

Author

    • 濱口, 清治 ハマグチ, キヨハル

Bibliographic Information

Title

Temporal logics and their applications to formal design verification of finite-state machines

Other Title

時相論理とその有限状態機械の形式的設計検証への応用

Author

濱口, 清治

Author(Another name)

ハマグチ, キヨハル

University

京都大学

Types of degree

博士 (工学)

Grant ID

乙第8182号

Degree year

1993-03-23

Note and Description

博士論文

Table of Contents

  1. 論文目録 / (0001.jp2)
  2. Contents / p6 (0008.jp2)
  3. Abstract / p1 (0005.jp2)
  4. 1 Introduction / p1 (0009.jp2)
  5. 1.1 Background / p1 (0009.jp2)
  6. 1.2 Outline of the Thesis / p6 (0012.jp2)
  7. 2 Preliminaries / p10 (0014.jp2)
  8. 2.1 Logic Functions / p10 (0014.jp2)
  9. 2.2 Regular Sets and Finite Automata / p11 (0014.jp2)
  10. 2.3 Sequential Machines and Sequential Circuits / p15 (0016.jp2)
  11. 3 Temporal Logics and Formal Design Verification / p18 (0018.jp2)
  12. 3.1 Temporal Logics / p19 (0018.jp2)
  13. 3.2 Formal Design Verification Based on Model Checking Method / p26 (0022.jp2)
  14. 4 ∞Regular Temporal Logic (∞RTL) / p33 (0025.jp2)
  15. 4.1 Introduction / p33 (0025.jp2)
  16. 4.2 Syntax and Semantics / p34 (0026.jp2)
  17. 4.3 Expressive Power of ∞RTL / p39 (0028.jp2)
  18. 4.4 Complexity of Model Checking Problem / p41 (0029.jp2)
  19. 4.5 Remarks and Discussions / p44 (0031.jp2)
  20. 5 Branching Time Regular Temporal Logic(BRTL) / p46 (0032.jp2)
  21. 5.1 Introduction / p46 (0032.jp2)
  22. 5.2 BRTL / p47 (0032.jp2)
  23. 5.3 Expressive Power of BRTL / p53 (0035.jp2)
  24. 5.4 Model Checking Algorithm / p58 (0038.jp2)
  25. 5.5 Symbolic Model Checking Algorithm / p62 (0040.jp2)
  26. 5.6 Remarks and Discussions / p72 (0045.jp2)
  27. 6 Verification of Asynchronous Circuits / p74 (0046.jp2)
  28. 6.1 Introduction / p74 (0046.jp2)
  29. 6.2 Modeling of Circuits / p75 (0046.jp2)
  30. 6.3 Specification / p78 (0048.jp2)
  31. 6.4 Experimental Results / p79 (0048.jp2)
  32. 6.5 Remarks and Discussions / p83 (0050.jp2)
  33. 7 Verification of Microprocessors / p85 (0051.jp2)
  34. 7.1 Introduction / p85 (0051.jp2)
  35. 7.2 The KUE-CHIP2 Microprocessor / p86 (0052.jp2)
  36. 7.3 Modeling of the Microprocessor / p86 (0052.jp2)
  37. 7.4 Specification / p88 (0053.jp2)
  38. 7.5 Experimental Results / p93 (0055.jp2)
  39. 7.6 Remarks and Discussions / p94 (0056.jp2)
  40. 8 Verification of Speed-Independent Systems / p97 (0057.jp2)
  41. 8.1 Introduction / p97 (0057.jp2)
  42. 8.2 One-Safe Place/Transition Net / p98 (0058.jp2)
  43. 8.3 Inverse Image Computation for Nets / p99 (0058.jp2)
  44. 8.4 Experimental Results / p100 (0059.jp2)
  45. 8.5 Remarks and Discussions / p103 (0060.jp2)
  46. 9 Conclusions / p104 (0061.jp2)
  47. References / p108 (0063.jp2)
  48. Acknowledgment / p115 (0066.jp2)
  49. List of Publications by the Author / p117 (0067.jp2)
4access

Codes

  • NII Article ID (NAID)
    500000094288
  • NII Author ID (NRID)
    • 8000000094514
  • DOI(NDL)
  • NDLBibID
    • 000000258602
  • Source
    • NDL ONLINE
    • NDL Digital Collections

Export

Page Top