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 & Tuttle. The concept of a fair I/O automaton 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 that (1) in each reachable state at most countably many fairness sets are enabled, and (2) input actions cannot disable strong fairness sets. This result, which generalizes previous results known from the literature, was needed to solve a problem posed by Broy & Lamport for the Dagstuhl Workshop on Reactive Systems.