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.
- State-based control theory
- Total observation (Module SBCDES_Total_Observation)
- Cat-and-mouse problem with five rooms
- Cat-and-mouse problem with eight rooms
- Two-train problem with six sections
- Two-train problem with eight sections
- Two-train problem with ten sections
- Two-train problem (SFBC function)
- Elementary component jack211r (boom)
- Elementary component suction cup (hook)
- Injector of the distribution station
- Crane of the distribution station
- Distribution station (intensional description of the predicate)
- Distribution station
- Partial observation (Module SBCDES_Partial_Observation)
- Language-based control theory (Module Automaton)
- Core of the language-based control theory (Module BasicProperties)
- Controllability property
- Simple example
- Two-train problem
- Elementary component jack211r (boom)
- Elementary component suction cup (hook)
- Injector of the distribution station
- Crane of the distribution station
- Distribution station
- Normality property
- Decentralized control architecture (Module DistributedArchitectures)
- Module Automaton
- Test for the module Automaton
- Module Generator
- Test for the module Generator
- Simple observability property
- Unconditional observability properties
- Example from DEDS, 12 (3), Prop. 3 with H of Fig. 4b
- Example from DEDS, 12 (3), Prop. 3 with H of Fig. 6
- Example from DEDS, 12 (3), Prop. 4 with H of Fig. 8b
- Example from DEDS, 12 (3), Prop. 5 with H of Fig. 11b
- Conditional observability properties
- Hierarchical control architecture (Module Component)
- Condition on the standard control technology for the agent
- Consistency of marking
- Observer property (observational equivalence)