Integrating temporal logics and model checking algorithms

Abstract

Temporal logic and model checking algorithms are often used for checking system properties in various environments. The diversity of systems and environments implies a diversity of logics and algorithms. But there are no tools to aid the logician or practitioner in the experimentation with different varieties of temporal logics and model checkers. Such tools could give users the ability to modify and extend a temporal logic and model checker as their problem domain changes. We have developed a set of tools that provide these capabilities by placing the model checking problem in an algebraic framework. These tools provide a temporal logic test bed that allows for quick prototyping and easy extension to logics and model checkers. Here we discuss the usage of these tools to generate model checker algorithms as algebraic mappings (i.e., embeddings of one algebra into another algebra by derived operations) with the temporal logic as the source algebra and the sets of nodes of a model as the target algebra. We demonstrate these tools by extending CTL and its model checker by introducing formulas that quantify the paths over which the satisfaction of the temporal operators is defined. This is made possible by permitting propositions to label the edges as well as the nodes in the model. We use this logic and its model checker to analyze program process graphs during the parallelization phase of an algebraic compiler.