Scholarlink

For the formal verification of concurrent programs, classical logic needs to be extended to handle time. This chapter introduces a temporal logic, which is an extension of propositional logic with several modal operators. The semantics of temporal logic is presented, as well as the extended semantic tableaux method. The chapter shows by example how concurrent programs can be verified (e.g., via model checking).

错误：搜索内容不能为空，请输入英文关键词
错误：关键词超出字数限制，请精简
高级检索

Temporal Logic

  • 章节

  • 发表日期：

    2025年

查看全文
  • Hantao Zhang,
  • Jian Zhang

摘要

For the formal verification of concurrent programs, classical logic needs to be extended to handle time. This chapter introduces a temporal logic, which is an extension of propositional logic with several modal operators. The semantics of temporal logic is presented, as well as the extended semantic tableaux method. The chapter shows by example how concurrent programs can be verified (e.g., via model checking).