Supremica is a tool for formal verification and synthesis of discrete event control functions based on discrete event models of the uncontrolled plant and specifications of the desired closed-loop behavior. This approach has its roots in the Supervisory Control Theory, originally formulated by Ramadge and Wonham. The modeling framework in Supremica is based on finite automata extended with variables, guard conditions, and action functions. In order to handle large-scale systems of industrially interesting sizes, Supremica implements both compositional abstraction-based techniques, as well as binary decision diagram base methods. Since the modeling language and algorithms are generic these techniques are useful in many application areas including control functions implemented in hardware. Supremica has been used in a number of industrial research projects to synthesize control functions for industrial robots and flexible manufacturing systems.

Below are shown some experimental results taken from “A Framework for Compositional Synthesis of Modular Nonblocking Supervisors” by Mohajerani, Malik, Fabian. These experiments were all run on a standard desktop PC using a single 2.66 GHz CPU, and Supremica running under a JVM with 1 GB of memory.

**agv**Automated guided vehicle coordination based on the Petri net model by Moody and Antsaklis. To make the example blocking in addition to uncontrollable, there is also a variant,

**agvb**, with an additional zone added at the input station.

**aip**Automated manufacturing system of the Atelier Interetablissement de Productique by Brandin and Charbonnier.

**fencaiwon09**Model of a production cell in a metal-processing plant from Feng, Cai and Wonham.

**tbed**Model of a toy railroad system based on the testbed described by Leduc. Two versions present different control objectives.

**verriegel**Models of the central locking system of a BMW car. There are two variants, a three-door model

**verriegel3**, and a four-door model

**verriegel4**. These models are derived from the KORSYS project.

**6link**Models of a cluster tool for wafer processing previously studied for synthesis by Su, van Schuppen and Rooda.

**tline**Parametrised model of a manufacturing transfer line from the lecture notes of Professor Wonham with different numbers of serially connected cells.

In Table 1 above, for each model, the row holds the number of automata (Aut), the number of reachable states (Size), and whether the model is nonblocking (Nonb.) or controllable (Cont.). Next, the row holds the size of the largest synchronous composition encountered during abstraction (Peak States), the total runtime (Time), the total amount of memory used (Mem.), the number of modular supervisors computed (Num.), and the number of states of the largest supervisor automaton (Largest). The table furthermore shows the number of events replaced by renaming (Ren.) and the number of events removed by self-loop removal (SR), and finally the number of states removed by halfway synthesis (HS), bisimulation (Bis.), and weak synthesis observation equivalence (WSOE).

**tline100**and

**tline1000**rows. These represent 100 and 1000, respectively serially connected models of the transfer line from the lecture notes of Professor Wonham. Even though the models have huge state-spaces, these models are highly structured and the compositional abstraction-based algorithm finds and exploits this structure without any prior knowledge or human intervention; for each model, it generates 201 and 2001 supervisors, respectively, each (except one in each case) of 79 states. This exploitation of the existing structure can be further seen in the graph below, which shows the runtimes and supervisor sizes for instances of the transfer line example with 100–1000 serially connected cells. Although the state-space for these models grows exponentially, the cells are identical and the practical complexity of the system is small. Even with no knowledge of the symmetry of the model, the compositional synthesis algorithm successfully computes modular supervisors for transfer lines with up to 1000 serially connected cells. The graph shows a linear relationship between the number of connected cells and the total number of supervisor states. Moreover, the relation between the number of cells and the execution time is quadratic. This behavior is due to the complexity of evaluating and choosing subsystems from growing lists. This experiment shows that the compositional synthesis algorithm automatically discovers that the cells are identical and produces identical supervisors accordingly.