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.

Models of computation (Turing machines, etc.) (msc 68Q05), Analysis of algorithms and problem complexity (msc 68Q25), Specification and verification (program logics, model checking, etc.) (msc 68Q60)
CWI
Department of Computer Science [CS]

Romijn, J.M.T, & Vaandrager, F.W. (1995). A note on fairness in I/O automata. Department of Computer Science [CS]. CWI.