Reasoning in Interval Temporal Logic,

Abstract

Predicate logis is a powerful and general descriptive formalism with a long history of development. However, since the logic's underlying semantics have no notion of time, statements such as I increases by 2 cannot be directly expressed. The authors discuss interval temporal logic (ITL), a formalism that augments standard predicate logic with operators for time-dependent concepts. Their earlier work used ITL to specify and reason about hardware. In this paper they show how ITL can also directly capture various control structures found in conventional programming languages. Constructs are given for treating assignment, iteration, sequential and parallel computations and scoping. The techniques used permit specification and reasoning about such algorithms as concurrent Quicksort. ITL is compared with the logic-based programming languages Lucid and Prolog.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Jul 01, 1983
Accession Number
ADA134062

Entities

People

  • Ben Moszkowski
  • Zohar Manna

Organizations

  • Stanford University

Tags

Communities of Interest

  • Materials and Manufacturing Processes

DTIC Thesaurus Topics

  • Applied Mathematics
  • Computations
  • Computer Programming
  • Computer Science
  • Computers
  • Formal Languages
  • Intervals
  • Iterations
  • Language
  • Parallel Computing
  • Parallel Processing
  • Programming Languages
  • Reasoning
  • Semantics
  • Sequences
  • Structured Programming

Fields of Study

  • Computer science

Readers

  • Computational Linguistics
  • Computational Modeling and Simulation