Alloy Models for Several Variants of the Supervisory Control Theory

We develop several modules, written in Alloy, that model variants of the Supervisory Control Theory. They are part of a project, called MELODIES (Modeling Environment for LOgical DIscrete Event Systems), aimed at providing a prototyping environment to novices in the domain, which is in constant evolution. This environment can also be used to solve control problems. At the present time, the following variants are available in MELODIES.

  1. State-based control theory
    1. Total observation (Module SBCDES_Total_Observation)
    2. Partial observation (Module SBCDES_Partial_Observation)
  2. Language-based control theory (Module Automaton)
    1. Core of the language-based control theory (Module BasicProperties)
      1. Controllability property
      2. Normality property
    2. Decentralized control architecture (Module DistributedArchitectures)
      1. Module Automaton
      2. Test for the module Automaton
      3. Module Generator
      4. Test for the module Generator
      5. Simple observability property
      6. Unconditional observability properties
      7. Conditional observability properties
    3. Hierarchical control architecture (Module Component)
      1. Condition on the standard control technology for the agent
      2. Consistency of marking
      3. Observer property (observational equivalence)