LTL generalized model checking revisited

被引：8

作者：

Godefroid P. ^{[1
]}

Piterman N. ^{[2
]}

机构：

[1] Microsoft Research, Redmond

[2] Imperial College London, London

来源：

International Journal on Software Tools for Technology Transfer | 2011年 / 13卷 / 6期

基金：

英国工程与自然科学研究理事会;

关键词：

Automata; Generalized model checking; Model checking; Partial kripke structures; Verification;

D O I：

10.1007/s10009-010-0169-3

中图分类号：

学科分类号：

摘要：

Given a 3-valued abstraction of a program (possibly generated using static program analysis and predicate abstraction) and a temporal logic formula, generalized model checking (GMC) checks whether there exists a concretization of that abstraction that satisfies the formula. In this paper, we revisit generalized model checking for linear time (LTL) properties. First, we show that LTL GMC is 2EXPTIME-complete in the size of the formula and polynomial in the model, where the degree of the polynomial depends on the formula, instead of EXPTIME-complete and quadratic as previously believed. The standard definition of GMC depends on a definition of concretization which is tailored for branching-time model checking. We then study a simpler linear completeness preorder for relating program abstractions. We show that LTL GMC with this weaker preorder is only EXPSPACE-complete in the size of the formula, and can be solved in linear time and logarithmic space in the size of the model. Finally, we identify classes of formulas for which the model complexity of standard GMC is reduced. © 2010 Springer-Verlag.

引用

页码：571 / 584

页数：13

共 32 条

[1]

Antonik A., Huth M., Larsen K., Nyman U., Wasowski A., 20 years of mixed and modal specifications, Bulletin of the European Association For Theoretical Computer Science, (2008)

[2]

Asarin E., Maler O., Pnueli A., Sifakis J., Controller synthesis for timed automata, IFAC Symp. On System Structure and Control, pp. 469-474, (1998)

[3]

Bruns G., Godefroid P., Model checking partial state spaces with 3-valued temporal logics, 11th Computer Aided Verification, pp. 274-287, (1999)

[4]

Bruns G., Godefroid P., Generalized model checking: Reasoning about partial state spaces, 11th Concurrency Theory. Lecture Notes In Computer Science, 1877, pp. 168-182, (2000)

[5]

Ball T., Rajamani S., The SLAM Toolkit, 13th Computer Aided Verification. Lecture Notes In Computer Science, 2102, pp. 260-264, (2001)

[6]

Gurfinkel A., Chechik M., How thorough is thorough enough?, 13th Correct Hardware Design and Verification Methods, (2005)

[7]

Godefroid P., Huth M., Model checking vs. generalized model checking: Semantic minimizations for temporal logics, 20th Logic In Computer Science, pp. 158-167, (2005)

[8]

Godefroid P., Huth M., Jagadeesan R., Abstraction-based model checking using modal transition systems, 12th Concurrency Theory. Lecture Notes In Computer Science, Vol, 2154, pp. 426-440, (2001)

[9]

Godefroid P., Jagadeesan R., Automatic abstraction using generalized model checking, 14th Computer Aided Verification. Lecture Notes In Computer Science, 2404, pp. 137-150, (2002)

[10]

Godefroid P., Jagadeesan R., On the Expressiveness of 3-valued models, 4th Verification, Model Checking and Abstract Interpretation. Lecture Notes In Computer Science, 2575, pp. 206-222, (2003)

← 1 2 3 4 →