zbMATH — the first resource for mathematics

A note on fairness in I/O automata. (English) Zbl 0875.68651
Summary: 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 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 and Lamport for the Dagstuhl Workshop on Reactive Systems.

68Q45 Formal languages and automata
Full Text: DOI
[1] Abadi, M.; Lamport, L., An old-fashioned recipe for real time, ACM trans. programming languages systems, 16, 5, 1543-1571, (1994)
[2] Alpern, B.; Schneider, F.B., Defining liveness, Inform. process. lett., 21, 181-185, (1985) · Zbl 0575.68030
[3] Broy, M.; Lamport, L., Specification problem, (), to appear
[4] Gawlick, R.; Segala, R.; Søgaard-Andersen, J.F.; Lynch, N., Liveness in timed and untimed systems, () · Zbl 0917.68152
[5] a full version is available as MIT Tech. Rept. MIT/LCS/TR-587.
[6] B. Jonsson, Compositional specification and verification of distributed systems, ACM Trans. Programming Languages Systems\bf16 (2) (19940 259-303.
[7] Lamport, L., The temporal logic of actions, ACM trans. programming languages systems, 16, 3, 872-923, (1994)
[8] Lynch, N.A.; Tuttle, M.R., Hierarchical correctness proofs for distributed algorithms, (), 137-151
[9] A full version is available as MIT Tech. Rept. MIT/LCS/TR-387.
[10] Manna, Z.; Pnueli, A., The temporal logic of reactive and concurrent systems: specification, (1992), Springer Berlin
[11] Romijn, J.M.T., Tackling the RPC-memory specification problem with I/O automata, (), to appear
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.