Encodings of bounded LTL model checking in effectively propositional logic

Juan Antonio Navarro-Pérez, Andrei Voronkov

    Research output: Chapter in Book/Report/Conference proceedingConference contribution


    We present an encoding of LTL bounded model checking problems within the Bernays-Schönfinkel fragment of first-order logic. This fragment, which also corresponds to the category of effectively propositional problems (EPR) of the CASC system competitions, allows a natural and succinct representation of both a software/hardware system and the property that one wants to verify. The encoding for the transition system produces a formula whose size is linear with respect to its original description in common component description languages used in the field (e.g. smv format) preserving its modularity and hierarchical structure. Likewise, the LTL property is encoded in a formula of linear size with respect to the input formula, plus an additional component, with a size of O(log k) where k is the bound, that represents the execution flow of the system. The encoding of bounded model checking problems by effectively propositional formulae is the main contribution of this paper. As a side effect, we obtain a rich collection of benchmarks with close links to real-life applications for the automated reasoning community. © Springer-Verlag Berlin Heidelberg 2007.
    Original languageEnglish
    Title of host publicationLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)|Lect. Notes Comput. Sci.
    PublisherSpringer Nature
    Number of pages15
    ISBN (Print)3540735941, 9783540735946
    Publication statusPublished - 2007
    Event21st International Conference on Automated Deduction, CADE-21 2007 - Bremen
    Duration: 1 Jul 2007 → …


    Conference21st International Conference on Automated Deduction, CADE-21 2007
    Period1/07/07 → …


    • Computer Science, Artificial Intelligence


    Dive into the research topics of 'Encodings of bounded LTL model checking in effectively propositional logic'. Together they form a unique fingerprint.

    Cite this