Open Access. Powered by Scholars. Published by Universities.®
Physical Sciences and Mathematics Commons™
Open Access. Powered by Scholars. Published by Universities.®
Articles 1 - 2 of 2
Full-Text Articles in Physical Sciences and Mathematics
Constructively Typed Timed Automata, J. F. Peters Iii
Constructively Typed Timed Automata, J. F. Peters Iii
Electrical Engineering and Computer Science - Technical Reports
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 …
Constructing Real-Time Systems From Temporal I/O Automata, J. F. Peters Iii, S. Ramanna
Constructing Real-Time Systems From Temporal I/O Automata, J. F. Peters Iii, S. Ramanna
Electrical Engineering and Computer Science - Technical Reports
A new class of communicating automata called Temporal Input/Output Automata (TAi/os) is introduced. A TAi/o is a predicate automaton used to specify real-time systems. The specification provided by a TAi/o includes state predicates with proof expressions and abstract program syntax as attributes. An abstract program is extracted during a constructive proof of the specification using the proof expressions. A TAi/o specification also includes hard, real-time constraints on program behavior. The predictability of deterministic, temporally complete TAi/o is investigated. The formulation of real-time system transductions and transduction rules for TAi/os in explicit clock temporal logic is given. An illustration of the …