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.
The test cases include the following complex industrial models and case studies, which are taken from different application areas such as manufacturing systems and automotive body electronics:
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.
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.
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).
Of particular interest are the
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.
