Time-constrained automata

In this paper, we augment the input-output automaton model in order to reason about time in concurrent systems, and we prove simple properties of this augmentation. The input-output automata model is a useful model for reasoning about computation in concurrent and distributed systems because it allows fundamental properties such as fairness and compositionality to be expressed easily and naturally. A unique property of the model is that systems are modeled as the composition of autonomous components. This paper describes a way to add a notion of time to the model in a way that preserves these properties. The result is a simple, compositional model for real-time computation that provides a convenient notation for expressing timing properties such as bounded fairness.