×

Finding state solutions to temporal logic queries. (English) Zbl 1213.68377

Davies, Jim (ed.) et al., Integrated formal methods. 6th international conference, IFM 2007, Oxford, UK, July 2–5, 2007. Proceedings. Berlin: Springer (ISBN 978-3-540-73209-9/pbk). Lecture Notes in Computer Science 4591, 273-292 (2007).
Summary: Different analysis problems for state-transition models can be uniformly treated as instances of temporal logic query-checking, where solutions to the queries are restricted to states. In this paper, we propose a symbolic query-checking algorithm that finds exactly the state solutions to a query. We argue that our approach generalizes previous specialized techniques, and this generality allows us to find new and interesting applications, such as finding stable states. Our algorithm is linear in the size of the state space and in the cost of model checking, and has been implemented on top of the model checker NuSMV, using the latter as a black box. We show the effectiveness of our approach by comparing it, on a gene network example, to the naive algorithm in which all possible state solutions are checked separately.
For the entire collection see [Zbl 1120.68004].

MSC:

68Q60 Specification and verification (program logics, model checking, etc.)

Software:

NuSMV
PDFBibTeX XMLCite
Full Text: DOI