• libFAUDES
• Reference  
• Type Index  
• Function Index  
• Literature  
•  
• Sections
• CoreFaudes  
  • CoreFaudes
  • Introduction
  • Generators
  • Alphabets
  • Reachability
  • Boolean Operations
  • Regular Expressions
  • Synchronous Composition
  • Projection
  • StateSet Conversion
  • Elementary Types
  • Miscellaneous
  • Vector Types
• CoordinationControl  
• Diagnosis  
  • Diagnosis
  • Introduction
  • Event-Diagnosis
  • Language-Diagnosis
  • Modular Diagnosis
  • Decentralized Diagnosis
  • Application Example
• Example  
• FaultTolerantControl  
  • FaultTolerantControl
  • Introduction
  • Example
  • Fault-Accommodation
  • Reconfiguration
  • Fault-Patterns
• HioSys  
  • HioSys
  • Introduction
  • Step-By-Step
  • Synthesis Procedure
  • Liveness Properties
  • Application Example
• Hybrid  
• IoSystem  
  • IoSystem
  • Introduction
  • Properties
  • Synthesis
• Multitasking  
  • Multitasking
  • Introduction
  • Functions
  • Observer
  • Optimal Color Set
  • Reachability
  • Synthesis
• Observer  
  • Observer
  • Introduction
  • Verification
  • Synthesis
  • Example
• Simulator  
  • Simulator
  • Introduction
  • Executor Classes
  • Hardware-In-The-Loop
  • IO-Devices
  • Simulator Interconnection
• Synthesis  
  • Synthesis
  • Introduction
  • Controllability
  • Normality
  • Omega-Controllability
  • Misc Functions
•  
• Types
• EventRelabelMap  
•  
• Functions
• InsertRelabeledEvents  
• IsLocallyControlConsistent  
• IsMsaObserver  
• IsMutuallyControllable  
• IsNaturalObserver  
• IsOutputControlConsistent  
• MsaObserver  
• MsaObserverLcc  
• NaturalObserverExtension  
• NaturalObserverLcc  
• NaturalObserverRelabeling  
•  

Observer Synthesis

Verification algorithms for various conditions on natural projections of plant languages L(G) that are sufficient for the nonblocking and maximally permissive hierarchical supervisor synthesis are provided on the Observer Test page. In contrast, the algorithms described on this page are concerned with the situation where these sufficient conditions are not fulfilled such that a given natural projection has to be modified in order to perform a hierarchical supervisor synthesis. In the observer plug-in, such modifications are offered for the natural observer condition (NaturalObserverExtension,NaturalObserverRelabeling) and the msa-observer condition (MsaObserver) in order to achieve nonblocking hierarchical control and for the combination of both conditions with local control consistency (NaturalObserverLcc,MsaObserverLcc) in order to achieve nonblocking and maximally permissive control.

The general approach taken in our algorithms is to extend the projection alphabet of a given natural projection until the repective sufficient condition is fulfilled. In the algorithmic implementation, we use the fact that all conditions can be represented in terms of a specific equivalence relation (quasi-congruence) for a dynamic system that is defined on the state space of the plant automaton G [O5]. After obtaining an appropriate dynamic system representation for each condition, either the heuristic alphabet extension algorithm in [O6] is used to obtain a suitable alphabet extension (NaturalObserverExtension, NaturalObserverLcc, MsaObserver, MsaObserverLcc) or an appropriate event relabeling is performed according to [O1] (NaturalObserverRelabeling).

libFAUDES 2.32b --- 2024.03.01 --- with "synthesis-observer-observability-diagnosis-hiosys-iosystem-multitasking-coordinationcontrol-timed-simulator-iodevice-luabindings-hybrid-example-pybindings"