A NOTE ON FAIRNESS IN I O AUTOMATA

Notions of weak and strong fairness are studied in the setting of the I/O automaton model of Lynch and Tuttle. The concept of a fair I/O aut omaton is introduced and it is shown that a fair I/O automaton paired with the set of its fair executions is a live I/O automaton provided t hat (1) in each reachable state at most countably many fairness sets a re enabled, and (2) input actions cannot disable strong fairness sets. This result, which generalizes previous results known from the Litera ture, was needed to solve a problem posed by Broy and Lamport for the Dagstuhl Workshop on Reactive Systems.