# Injective envelopes of transition systems and Ferrers languages

## TL;DR

This paper explores the injective envelopes of transition systems over ordered alphabets with involution, introducing Ferrers languages and providing a Galois lattice-based characterization and finiteness test.

## Contribution

It introduces Ferrers languages and characterizes injective envelopes of transition systems using Galois lattices, offering new insights into their structure and finiteness properties.

## Key findings

- Injective envelopes can be described via Galois lattices.
- Finiteness of these envelopes can be tested.
- Introduction of Ferrers languages as a new concept.

## Abstract

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.