• 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
• HioConstraint  
• HioController  
• HioEnvironment  
• HioPlant  
•  
• Functions
• HioFreeInput  
• HioShuffle  
• HioSynth  
• HioSynthHierarchical  
• HioSynthMonolithic  
• IsHioConstraintForm  
• IsHioControllerForm  
• IsHioEnvironmentForm  
• IsHioPlantForm  
•  

HioSys PlugIn

I/O-Based Liveness: Completeness and Yp-liveness

A majority of the approaches to control of DES that regard liveness use the technique of marking particular strings of plant and/or specification to express desired liveness properties. In most of these approaches, the respective objective of controller design is to achieve or preserve the permanent chance for any string of the closed loop to be extended to a marked string. Our notion of liveness is different in that it requires output events to occur persistently rather than strings/states to be reachable and thus is not based on marking. First, we define the notion of a YP-live language and then identify two coupled liveness properties adequate for our setting.

Definition: Y_P-liveness

Let L be a regular language and Y_P be an alphabet.

If (∀ w ∈ L^∞)[PYP(w) ∈ Y_P^w] , then L is said to be Y_P-live.

Apparently, any subset of a Y_P-live language is also Y_P-live, which is important for a) discussing the liveness of an I/O plant within different external configurations (modularity) and b) abstraction-based control. Using Y_P-liveness, we can describe the liveness properties of an I/O plant as follows.

Definition: I/O Plant - Liveness Properties

Let S_PE = (U_P,Y_P,U_E,Y_E,L_PE) be an I/O plant and let S_P = (U_P,Y_P,L_P) and S_E = (U_E,Y_E,L_E) be constraints.

• If L_P||L_PE||L_E is complete (see IsComplete), then S_PE said to be complete w.r.t. the constraints S_P and S_E.
• If (∀ w ∈ (L_P||L_PE||L_E)^∞)[PYP(w) ∈ Y_P^w] then the plant said to be Y_P-live w.r.t. the constraints S_P and S_E.

Completeness requires the plant to persistently issue events, i.e. prohibits deadlocks. Moreover, the completeness property guarantees that each sequence of events contributes to an infinite sequence of events in the language limit considered by Y_P-liveness. The second liveness property, Y_P-liveness, requires that any infinite sequence of events must include an infinite number of measurement events reported to the operator (no livelocks between any two Y_P-events). Hence, both properties when put together indeed guarantee that an infinite sequence of measurement events is generated by the plant under constraints and, in return, influence by the operator is persistently possible. Technically, L_P||L_PE||LE = 0 provokes both liveness conditions to be met trivially. The HioSys synthesis functions design an I/O controller such that the above liveness properties are met for the external view on the closed loop under constraints.

HioSys Home

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