Efficient temporal-logic query checking for presburger systems
Title | Efficient temporal-logic query checking for presburger systems |
Publication Type | Conference Papers |
Year of Publication | 2005 |
Authors | Zhang D, Cleaveland R |
Conference Name | Proceedings of the 20th IEEE/ACM international Conference on Automated software engineering |
Date Published | 2005/// |
Publisher | ACM |
Conference Location | New York, NY, USA |
ISBN Number | 1-58113-993-4 |
Keywords | Formal Methods, Model checking, on-the-fly symbolic model checking, Presburger systems, query checking |
Abstract | 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. |
URL | http://doi.acm.org/10.1145/1101908.1101915 |
DOI | 10.1145/1101908.1101915 |