Efficient temporal-logic query checking for presburger systems

TitleEfficient temporal-logic query checking for presburger systems
Publication TypeConference Papers
Year of Publication2005
AuthorsZhang D, Cleaveland R
Conference NameProceedings of the 20th IEEE/ACM international Conference on Automated software engineering
Date Published2005///
Conference LocationNew York, NY, USA
ISBN Number1-58113-993-4
KeywordsFormal Methods, Model checking, on-the-fly symbolic model checking, Presburger systems, query checking

This paper develops a framework for solving temporal-logic query-checking problems for a class of infinite-state system models that compute with integer-valued variables (so-called Presburger systems, in which Presburger formulas are used to define system behavior). The temporal-logic query checking problem may be formulated as follows: given a model and a temporal logic formula with placeholders, compute a set of assignments of formulas to placeholders such that the resulting temporal formula is satisfied by the given model. Temporal-logic query checking has proved useful as a means for requirements and design understanding; existing work, however, has focused only on propositional temporal logic and finite-state systems.Our method is based on a symbolic model-checking technique that relies on proof search. The paper first introduces this model-checking approach and then shows how it can be adapted to solving the temporal queries in which formulas may contain integer variables. We also present experimental results showing the computational efficacy of our approach.