Simple bounded LTL model checking

61Citations
Citations of this article
40Readers
Mendeley users who have this article in their library.
Get full text

Abstract

We present a new and very simple translation of the bounded model checking problem which is linear both in the size of the formula and the length of the bound. The resulting CNF-formula has a linear number of variables and clauses. bounded model checking, LTL, linear translation, NuSMV. © Springer-Verlag 2004.

Cite

CITATION STYLE

APA

Latvala, T., Biere, A., Heljanko, K., & Junttila, T. (2004). Simple bounded LTL model checking. Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 3312, 186–200. https://doi.org/10.1007/978-3-540-30494-4_14

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free