Injective envelopes of transition systems and Ferrers languages

We consider reflexive and involutive transition systems over an ordered alphabet A equipped with an involution. We give a description of the injective envelope of any two-element set in terms of Galois lattice, from which we derive a test of its finiteness. Our description leads to the notion of Ferrers language.