Developing Strategies for Specialized Theorem Proving about Untimed, Timed, and Hybrid I/O Automata

Abstract

In this paper we discuss how we intend to develop a specialized theorem proving environment for the Hybrid I/O Automata (HIOA) framework over the PVS theorem prover, and some of the issues involved. In particular, we describe approaches to using PVS that allow and encourage the development of useful proof strategies, and note some desired PVS features that would further help us to do so for our HIOA environment.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Sep 08, 2003
Accession Number
ADA465057

Entities

People

  • Myla Archer
  • Sayan Mitra

Organizations

  • Massachusetts Institute of Technology

Tags

Communities of Interest

  • Energy and Power Technologies

DTIC Thesaurus Topics

  • Abstracts
  • Automata
  • Computer Science
  • Environment
  • Information Operations
  • Language
  • Machines
  • Military Research
  • Simulations
  • Standards
  • Template Patterns
  • Theoretical Computer Science

Fields of Study

  • Mathematics

Readers

  • Defense Acquisition Program Management
  • Mathematical Modeling and Probability Theory.