TYPED TIMED INPUT OUTPUT AUTOMATA IN REAL-TIME, CYBERNETIC EXPLANATION

This paper presents a basis for real-time, cybernetic explanation in t erms of typed timed input/output automata (tTA(i/o)s). These are a for m of Muller automata with typed states, input, and output. The typing of a tTA(i/o) is carried out intuitionistically in the tradition begun by Martin-Lof. The explanation of choice in the behavior specified by a tTA(i/o) is given in terms of the choice operators from Girard's li near logic. The meaning of a timed behavior specified by a tTA(i/o) is explained with real-time temporal logic. As a result of this approach to cybernetic explanation, a framework for reasoning about time for a specified behavior is given.