Integrating Temporal Logics and Model Checking Algorithms
1997
Loading...
View/Download File
Persistent link to this item
Statistics
View StatisticsJournal Title
Journal ISSN
Volume Title
Title
Integrating Temporal Logics and Model Checking Algorithms
Authors
Published Date
1997
Publisher
Type
Report
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.
Keywords
Description
Associated research group: Minnesota Extensible Language Tools
Related to
Replaces
License
Series/Report Number
Funding information
Isbn identifier
Doi identifier
Previously Published Citation
In Proc. of the 4th AMAST Workshop on Real-Time Systems held in Mallorca, Spain May 21-23, 1997. Springer Verlag Lecture Notes in Computer Science volume 1231.
Suggested citation
Rus, Teodor; Van Wyk, Eric. (1997). Integrating Temporal Logics and Model Checking Algorithms. Retrieved from the University Digital Conservancy, https://hdl.handle.net/11299/217300.
Content distributed via the University Digital Conservancy may be subject to additional license and use restrictions applied by the depositor. By using these files, users agree to the Terms of Use. Materials in the UDC may contain content that is disturbing and/or harmful. For more information, please see our statement on harmful content in digital repositories.