期刊名称：International Journal of Hybrid Information Technology
印刷版ISSN：1738-9968
出版年度：2013
卷号：6
期号：6
出版社：SERSC
摘要：This paper presents a case study for symbolic model checking (SMC) with PropositionalProjection Temporal Logic (PPTL). First, PPTL is brie.y introduced. Then an outline ofsymbolic model checking algorithm for PPTL proposed in [21] is presented. As a case study,a single-track railroad crossing control system (STRCCS) is employed to illustrate how SMCfor PPTL can be utilized in the specification and verification of embedded real-time systems
关键词：Propositional Projection Temporal Logic; Symbolic Model Checking; Veri-;fication; Embedded Real-Time Systems
