2013 | OriginalPaper | Buchkapitel
Bounded Model Checking for Propositional Projection Temporal Logic
verfasst von : Zhenhua Duan, Cong Tian, Mengfei Yang, Jia He
Erschienen in: Computing and Combinatorics
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
This paper presents a bounded model checking approach for propositional projection temporal logic (PPTL). To this end, first PPTL is briefly introduced. Then, bounded semantics of PPTL is defined according to its semantics in logic theory. Further, a reduction method from BMC to SAT is given in detail. In addition, an example is presented to illustrate how the approach works. Our experience shows that BMC approach for PPTL proposed in the paper is useful and feasible.