Bounded Parametric Model Checking for Elementary Net Systems

详细信息    查看全文

• 作者：Micha? Knapik ; Maciej Szreter ; Wojciech Penczek
• 刊名：Lecture Notes in Computer Science
• 出版年：2010
• 出版时间：2010
• 年：2010
• 卷：6550
• 期：1
• 页码：42-71
• 全文大小：450.7 KB

文摘

Bounded Model Checking (BMC) is an efficient verification method for reactive systems. BMC has been applied so far to verification of properties expressed in (timed) modal logics, but never to their parametric extensions. In this paper we show, for the first time that BMC can be extended to PRTECTL – a parametric extension of the existential version of CTL. To this aim we define a bounded semantics and a translation from PRTECTL to SAT. The implementation of the algorithm for Elementary Net Systems is presented, together with some experimental results.