The paper introduces the input/output (I/O) automaton model, a tool for modeling concurrent and distributed discrete event systems. I/O automata are particularly useful for systems where components operate asynchronously and continuously receive input from their environment. Each component is modeled as an I/O automaton, which has actions classified as input, output, or internal. The model distinguishes between actions controlled by the automaton and those controlled by the environment, with the automaton unable to block inputs. I/O automata can be nondeterministic, and their composition allows for the modeling of complex systems. The paper defines the model formally, provides examples using candy vending machines and customers, and discusses fairness and problem specifications. It also outlines proof techniques, including modular decomposition, for reasoning about the behavior of automata and their satisfaction of problem specifications.The paper introduces the input/output (I/O) automaton model, a tool for modeling concurrent and distributed discrete event systems. I/O automata are particularly useful for systems where components operate asynchronously and continuously receive input from their environment. Each component is modeled as an I/O automaton, which has actions classified as input, output, or internal. The model distinguishes between actions controlled by the automaton and those controlled by the environment, with the automaton unable to block inputs. I/O automata can be nondeterministic, and their composition allows for the modeling of complex systems. The paper defines the model formally, provides examples using candy vending machines and customers, and discusses fairness and problem specifications. It also outlines proof techniques, including modular decomposition, for reasoning about the behavior of automata and their satisfaction of problem specifications.