Integrating temporal logics and model checking algorithms

Teodor Rus, Eric van Wyk

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

5 Scopus citations

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.

Original languageEnglish (US)
Title of host publicationTransformation-Based Reactive Systems Development - 4th International AMAST Workshop on Real-Time Systems and Concurrent and Distributed Software, ARTS 1997, Proceedings
EditorsMiquel Bertran, Teodor Rus
PublisherSpringer- Verlag
Number of pages1
ISBN (Print)3540630104, 9783540630104
DOIs
StatePublished - Jan 1 1997
Event4th International AMAST Workshop on Real-Time Systems and Concurrent and Distributed Software, ARTS 1997 - Palma, Mallorca, Spain
Duration: May 21 1997May 23 1997

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume1231
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other4th International AMAST Workshop on Real-Time Systems and Concurrent and Distributed Software, ARTS 1997
CountrySpain
CityPalma, Mallorca
Period5/21/975/23/97

Fingerprint Dive into the research topics of 'Integrating temporal logics and model checking algorithms'. Together they form a unique fingerprint.

Cite this