Real-Time Symbolic Model Checking for Discrete Time Models

Abstract

The BDD-based symbolic model checking algorithm given in (4.10) is extended to handle real-time properties using the bounded until operator (9). We believe that this algorithm which is based on discrete time is able to handle many real-time properties that arise in practical problems. One example of such a property is priority increasing. This is a serious problem that can make real- time systems unpredictable in subtle ways. Our work discusses this problem and presents one possible solution. The solution is formalized and verified using the modified algorithm. We also propose another extension to the model checking algorithm. Timed transition graphs are transition graphs in which events may take non-unit time to occur. The time it takes for a transition in a TTG to happen is determined by a time interval. This allows the construction of smaller and more realistic models. A symbolic model checking algorithm is given for formulas using the bounded until operator in TTG models.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
May 02, 1994
Accession Number
ADA282878

Entities

People

  • Edmund M. Clarke
  • Sergio V. Campos

Organizations

  • Carnegie Mellon University

Tags

Communities of Interest

  • Materials and Manufacturing Processes
  • Sensors

DTIC Thesaurus Topics

  • Air Traffic
  • Air Traffic Control Systems
  • Algorithms
  • Computations
  • Computer Science
  • Computers
  • Control Systems
  • Information Science
  • Intervals
  • Inversion
  • Iterations
  • Radar
  • Simulations
  • Specifications
  • Time Intervals
  • Transitions
  • Verification

Fields of Study

  • Computer science
  • Mathematics

Readers

  • Applied Combinatorial Optimization and Logic Circuit Design.
  • Computational Modeling and Simulation
  • Parallel and Distributed Computing.