An Optimizing Compiler for Batches of Temporal Logic Formulas

Other Titles


Model checking based on validating temporal logic formulas has proven practical and effective for numerous applications from verifying hardware designs to proving the correctness of software. As systems based on this approach have become more mainstream, a need has arisen to deal effectively with large batches of formulas over a common model. Presently, most systems validate formulas one at a time, with little or no interaction between validation of separate formulas. This is the case despite the fact that for a wide range of applications a certain level of redundancy between domain-related formulas can be anticipated. This paper presents an optimizing compiler for batches of temporal logic formulas. A component of the Carnauba Model Checking System, this compiler addresses the need to handle batches of temporal logic formulas by leveraging the framework common to optimizing programming language compilers. Just as a traditional optimizing compiler attempts to exploit redundancy and other solvable properties in programs to reduce the demand on a runtime system, this compiler exploits similar properties in groups of formulas to reduce the demand on a model checking engine. Optimizations are performed via a set of distinct, interchangeable optimization passes operating on a common intermediate representation. The intermediate representation is capable of representing formulas over the full modal mu-calculus, and the optimization techniques are applicable to any temporal logic that can be translated into the modal mu-calculus. The compiler offers a unified framework for expressing well understood single-formula optimizations as well as numerous inter-formula optimizations that capitalize on redundancy and logical implication. The result is a system that, when applied to a potentially heterogeneous collection of formulas over a common problem domain, is able to measurably reduce the time and space requirements of the subsequent model checking engine.

Journal / Series

Volume & Issue



Date Issued



Cornell University


computer science; technical report


Effective Date

Expiration Date




Union Local


Number of Workers

Committee Chair

Committee Co-Chair

Committee Member

Degree Discipline

Degree Name

Degree Level

Related Version

Related DOI

Related To

Related Part

Based on Related Item

Has Other Format(s)

Part of Related Item

Related To

Related Publication(s)

Link(s) to Related Publication(s)


Link(s) to Reference(s)

Previously Published As

Government Document




Other Identifiers


Rights URI


technical report

Accessibility Feature

Accessibility Hazard

Accessibility Summary

Link(s) to Catalog Record