Synthesis of controllers with MBP

Index

• Overview
• Controller synthesis
• (Controlled) Plant simulation
• Download
• Examples
• References

---

Overview

MBP tool along with plan synthesis allows to synthesize (maximally permissive) controllers. It takes as the input a plant (or domain; a state-transition system) written in SMV language, and requirements as CTL formulae. Also, MBP allows one to simulate behaviours of both the uncontrolled plant (domain) and the controlled one. Finally, it benefits from the common language with NuSMV Symbolic Model Checker. Once a plant is implemented in SMV, it can be verified using this model checker. Such a verification might be useful to ensure the correctness of the complex plants' models.

Controller synthesis

To synthesize the controller, run

MBP <smv_file>

Run "MBP -h" for many other options.

(Controlled) Plant simulation

With MBP it is possible to simulate both controlled and uncontrolled plant. For uncontrolled plant (domain) simulation run

MBP -dsimulate <smv_file>

For controlled plant (plan) simulation run

MBP -simulate_plan <smv_file>

Download

Here you can download the binary version of MBP, modified to allow for (maximally permissive) controller synthesis. Binary is compiled for PCs supporting Linux.

Examples

Simple Transfer Line (STL)

STL consists of two machines M1 and M2, followed by a test unit TU, linked by buffers B1 and B2. A workpiece tested by TU may be accepted or rejected; if accepted, it is released from the system; if rejected, it is returned to B1 for reprocessing by M2. The capacities of B1 and B2 are assumed to be 3 and 1 respectively. For detailed description see, for example Prof. Wonham's notes on Supervisory Control of Discrete-Event Systems.

• stline_straightforward.smv – straightforward implementation of the problem with dummy CTL specification.
• stline.smv – plant behaviour relaxed adding selfloops for buffers. That is if buffer is full(empty), then upon put(get) nothing happens to its value – a piece is lost (taken from nowhere). The specification designed to prevent undesired behaviour.

Transfer Line (TL)

In order to increase complexity of the problem, authors of the paper on STCT proposed two axis of extensions for the Simple Transfer Line example. One possibility is to allow all components to handle M workpieces. The second is to connect L Transfer Lines in a sequence with additional buffers between each pair of M-extended Tranfer Lines. Thus, we obtain an (L,M)-extended Transfer Line.

• gen_tl.pl – gzipped perl script for generating (L,M)-extended Transfer Line. Run with "-h" for the help.

References

1. A. Gromyko, M. Pistore, and P. Traverso. Supervisory Control via Symbolic Model Checking Submitted.
   Download pdf.