Document Type
Report
Date
11-1991
Keywords
Automata, Design Methodology, Constructive Type Theory, Program specification, Real-Time systems, Temporal Logic, Visualization. CR Categories: C.3, D.1.7, D.2.10, J.7, F.1.1, F.3.1.
Language
English
Disciplines
Computer Sciences
Description/Abstract
A new class of communicating automata called typed Timed lnput/Output Automata (tTAi/os) is introduced. A tTAi/o is a predicate automaton used for specifying and reasoning about real-time systems. The typing discipline suggested for predicate automata is in the tradition of Martin-Löf's constructive type theory. A type A is a proposition, which is defined when a prescription for constructing a proof of A is given. A fragment of Girard's linear logic is used in classifying state types. An illustration of the use of tTAi/os in specifying a light-controller is presented. An abstract program is extracted during a proof of an automaton specification. To illustrate the methodology in constructive reasoning about a tTAi/o, a proof which derives a partial abstract program is given.
Recommended Citation
Peters, J. F. III, "Constructively Typed Timed Automata" (1991). Electrical Engineering and Computer Science - Technical Reports. 109.
https://surface.syr.edu/eecs_techreports/109
Source
local
Additional Information
School of Computer and Information Science, Syracuse University, SU-CIS-91-23