In the field of distributed artificial intelligence, the cooperation among intelligent agents is a matter of growing importance. We propose a new machine, called agency, which is devoted to solve complex problems by means of cooperation among agents, where each agent is able to perform inferential activities. The aim of this paper is to give rigorous and formal descriptions of agency and, using the descriptions, to define and prove some interesting properties. The descriptions are based on three formalisms: multilanguage systems, directed hypergraphs, ER Petri nets. The work is a step in the direction of building a methodology for the project and the development of systems operating in real-world applications. We give a theoretical background on which new techniques can be implemented for testing the requirements of systems of distributed artificial intelligence such as agencies. The fundamental formalism in describing agencies is multilanguage system; starting from it we capture some particular issues (i.e., structure and evolution of an agency) by means of hypergraphs and ER Petri nets. The formalisms support the definition and proof of properties (such as fairness of cooperation among agents). ©1999 John Wiley & Sons, Inc.