Supervisory control theory with Alloy

Scientific literature reveals that the symbolic representation techniques underlying some formal methods are useful in verifying properties or synthesizing parts of large discrete event systems. They involve, however, encoding complex schemata and fine-tuning heuristic parameters in order to translate specific problems into efficient BDD- or SAT-based representations. This approach may be too costly when the main goal is to explore a theory, use simulation to understand its underlying concepts and computation procedures, and conduct experiments by applying them to problems in different fields as the theory evolves over time. To achieve this goal, this paper investigates the use of Alloy in modeling and prototyping varying fragments of the supervisory control theory, including the verification of nontrivial properties such as controllability, normality and observational equivalence. It also shows how to apply abstract models for synthesizing optimal supervisors and reports on an experiment suggesting that Alloy can be used to synthesize supervisors for concrete systems using hierarchical decomposition.