Model Checking for Linear Temporal Logic: An Efficient Implementation

Abstract

This report provides evidence to support the claim that model checking for linear temporal logic (LTL) is 'practically efficient.' Two implementations of a linear temporal logic model checker is described. One is based on transforming the model checking problem into a satisfiability problem; the other checks an LTL formula for a finite model by computing the cross- product of the finite state transition graph of the program with a structure containing all possible models for the property. An experiment was done with a set of mutual exclusion algorithms and tested safety and liveness under fairness for these algorithms. (CP)

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Jun 01, 1990
Accession Number
ADA225189

Entities

People

  • Amir Pnueli
  • Rivi Sherman

Organizations

  • University of Southern California

Tags

Communities of Interest

  • Materials and Manufacturing Processes

DTIC Thesaurus Topics

  • Abstracts
  • Air Force
  • Algorithms
  • Automatic
  • Classification
  • Computations
  • Computer Programming
  • Computer Science
  • Computers
  • Consistency
  • Construction
  • Guarantees
  • Language
  • Programming Languages
  • Semantics
  • Transitions
  • Verification

Fields of Study

  • Computer science

Readers

  • Mathematical Modeling and Probability Theory.
  • Systems Analysis and Design