首页 | 本学科首页   官方微博 | 高级检索  
     


Expressiveness of propositional projection temporal logic with star
Authors:Cong TianZhenhua Duan
Affiliation:
  • ICTT and ISN Laboratory, Xidian University, Xi’an, 710071, PR China
  • Abstract:This paper investigates the expressiveness of Propositional Projection Temporal Logic with Star (PPTL*). To this end, Büchi automata and ω-regular expressions are first extended as Stutter Büchi Automata (SBA) and Extended Regular Expressions (ERE) to include both finite and infinite strings. Further, by equivalent transformations among PPTL* formulas, SBAs and EREs, PPTL* is proved to represent exactly the full regular language. Moreover, some fragments of PPTL* are characterized, and finally, PPTL* and its fragments are classified into five different language classes.
    Keywords:Temporal logic   Expressiveness   Automata theory   Regular expressions   Verification
    本文献已被 ScienceDirect 等数据库收录!
    设为首页 | 免责声明 | 关于勤云 | 加入收藏

    Copyright©北京勤云科技发展有限公司  京ICP备09084417号