Implementing a real-time process algebra in HOL

Richard Gerber, Elsa L. Gunter, Insup Lee

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

Abstract

In [6] a real-time process algebra was discussed, a model for the algebra was developed, and the axiomatization was shown to be sound and complete for reasoning about equality and containment of processes for this model. In this work we show how to implement this theory in HOL and to develop a procedure for proving the equality of finite processes.

Original languageEnglish (US)
Title of host publicationProceedings of the 1991 International Workshop on the HOL Theorem Proving System and Its Applications
EditorsMyla Archer, Jeffrey J. Joyce, Karl N. Levitt, Phillip J. Windley
PublisherInstitute of Electrical and Electronics Engineers Inc.
Pages144-154
Number of pages11
ISBN (Electronic)0818624604, 9780818624605
DOIs
StatePublished - 1991
Externally publishedYes
Event1991 International Tutorial and Workshop on the HOL Theorem Proving System and Its Applications - Davis, United States
Duration: Aug 28 1991Aug 30 1991

Publication series

NameProceedings of the 1991 International Workshop on the HOL Theorem Proving System and Its Applications

Conference

Conference1991 International Tutorial and Workshop on the HOL Theorem Proving System and Its Applications
CountryUnited States
CityDavis
Period8/28/918/30/91

ASJC Scopus subject areas

  • Computational Theory and Mathematics
  • Logic
  • Computer Science Applications
  • Hardware and Architecture
  • Software
  • Artificial Intelligence

Fingerprint Dive into the research topics of 'Implementing a real-time process algebra in HOL'. Together they form a unique fingerprint.

Cite this