Analysis And Control Of Partially-Observed Discrete-Event .
Analysis and Control ofPartially-Observed Discrete-Event Systems:Introduction and Recent AdvancesXiang YinEECS Department, University of MichiganDepartment of Automation, Shanghai Jiao-Tong UniversityMay 27, 2016, Shanghai, ChinaX.Yin (UMich)SJTU 2016May 20160/31
Myself Name: 殷翔 EducationBorn: Jan 1991, Hefei, Anhui- Zhejiang University, College of Electrical EngineeringBachelor of Engineering, Major: Power ElectronicsJune 2012- University of Michigan, Ann Arbor, Department of EECS* Master of Science, Major: Control & MathDec 2013* PhD Candidate, Major: Control & MathApril 2017 (expected)* Advisor: Prof. Stephane Lafortune* Thesis Committee: D. Teneketzis, D. Tilbury & N. Ozay Research- Control of discrete-event/hybrid systems- Model-based fault diagnosis/prognosis- Privacy and security in cyber-physical systemsX.Yin (UMich)SJTU 2016May 20161/31
Outline Motivation: Why we study discrete-event system Partially-Observed Discrete-Event Systems Analysis of Partially-Observed DES- Verification of Security/Diagnosability/Prognosability Control of Partially-Observed DES- Synthesis of supervisory control strategies- Synthesis of sensor activation strategies Applications:- Location-Based Services (analysis, security issue)- Vehicular Electrical Power Systems (control, safety-critical systems) Conclusion and Future DirectionsX.Yin (UMich)SJTU 2016May 20162/31
Cyber-Physical Control SystemsCyber-Physical Control SystemsPerceptionDiscreteDecision orExternal Dynamic EnvironmentX.Yin (UMich)SJTU 2016May 20163/31
Cyber-Physical Control SystemsCyber-Physical Control SystemsPerceptionDiscreteDecision ical LayerSensor Continuous Dynamic Low Level ControllerExternal Dynamic EnvironmentX.Yin (UMich)SJTU 2016May 20163/31
Cyber-Physical Control SystemsCyber-Physical Control SystemsPerceptionCyber Layer Abstracted Model High Level Controller(Supervisor)DiscreteDecision ical LayerSensor Continuous Dynamic Low Level ControllerExternal Dynamic EnvironmentX.Yin (UMich)SJTU 2016May 20163/31
Continuous v.s. Discretephysical, continuous𝑥𝑝 𝑓𝑝 (𝑥𝑝 , 𝑢, 𝜂)𝑠 𝑔𝑝 (𝑥𝑝 , 𝑢, 𝜇)𝑥𝑐 𝑓𝑝 (𝑥𝑐 , 𝑠)𝑢 𝑔𝑝 (𝑥𝑐 , 𝑠)Model: Differential EquationSpecification: Stability,reference tracking, optimality X.Yin (UMich)SJTU 2016May 20164/31
Continuous v.s. Discretephysical, continuouscomputational, discrete𝑥𝑝 𝑓𝑝 (𝑥𝑝 , 𝑢, 𝜂)𝑠 𝑔𝑝 (𝑥𝑝 , 𝑢, 𝜇)20Model: Differential EquationSpecification: Stability,reference tracking, optimality X.Yin (UMich)41𝑥𝑐 𝑓𝑝 (𝑥𝑐 , 𝑠)𝑢 𝑔𝑝 (𝑥𝑐 , 𝑠)35𝑆: 𝑂𝑏𝑠(𝐿 𝐺 ) 2𝐸Model: Discrete-event systems, automata,transition systems, formal languagesSpecification: Safety, liveness,diagnosability, securitySJTU 2016May 20164/31
Current PracticeCurrent Control Design Process for Cyber-Physical Systems Given some spec (plain English) use art of design (engineering intuition,experience) and extensive testing to come up with a single solution Ad hoc approaches, Large lists of “if-then-else” rules Little or no formal guarantees on correctnessX.Yin (UMich)SJTU 2016May 20165/31
Current PracticeCurrent Control Design Process for Cyber-Physical Systems Given some spec (plain English) use art of design (engineering intuition,experience) and extensive testing to come up with a single solution Ad hoc approaches, Large lists of “if-then-else” rules Little or no formal guarantees on correctnessBetter Alternative Formal Methods!X.Yin (UMich)SJTU 2016May 20165/31
Formal Approach: Verification and SynthesisFormal Methods(Model-Based Approach)Requirementson the systembehaviorAssumptionson verificationsynthesisSatisfiedViolatedController No such( certificate) ( counterexm) (Correction solutionGuaranteed)X.Yin (UMich)SJTU 2016May 20166/31
Formal Approach: Verification and SynthesisDiscrete-event systems Model: Automata Specification: Formal LanguagesFormal Methods(Model-Based Approach)Requirementson the systembehaviorAssumptionson verificationsynthesisSatisfiedViolatedController No such( certificate) ( counterexm) (Correction solutionGuaranteed)X.Yin (UMich)SJTU 2016May 20166/31
Formal Approach: Verification and SynthesisDiscrete-event systems Model: Automata Specification: Formal LanguagesFormal Methods(Model-Based Approach)Requirementson the systembehaviorAssumptionson theenvironmentSystemVerification (Analysis) Formal guarantee for ationsynthesisSatisfiedViolatedController No such( certificate) ( counterexm) (Correction solutionGuaranteed)X.Yin (UMich)SJTU 2016May 20166/31
Formal Approach: Verification and SynthesisDiscrete-event systems Model: Automata Specification: Formal LanguagesFormal Methods(Model-Based Approach)Requirementson the systembehaviorAssumptionson theenvironmentSystemVerification (Analysis) Formal guarantee for ationsynthesisSynthesis (Control Design) Reactive to environment, e.g.,uncontrollability & unobservability Correct-by-construction!(No need to verify)X.Yin (UMich)SatisfiedViolatedController No such( certificate) ( counterexm) (Correction solutionGuaranteed)SJTU 2016May 20166/31
Why Discrete-Event ModelsWhy Discrete-Event Models Many systems are Inherently Event-Driven and have Discrete State-SpacesManufacturing Systems, Software Systems, PLCs, Protocols- Z.-W. Li,, and M.-C. Zhou. "Elementary siphons of Petri nets and their application to deadlock preventionin flexible manufacturing systems." IEEE Trans Systems, Man and Cybernetics, Part A, 34.1, 2004.- Y. Pencolé, and M. Cordier. "A formal framework for the decentralised diagnosis of large scale discrete eventsystems and its application to telecommunication networks." Artificial Intelligence, 164.1, 2005.- H.-W. Liao, et al. "Eliminating concurrency bugs in multithreaded software: A new approach based on discreteevent control." IEEE Trans Control Systems Technology, 21.6, 2013.X.Yin (UMich)SJTU 2016May 20167/31
Why Discrete-Event ModelsWhy Discrete-Event Models Many systems are Inherently Event-Driven and have Discrete State-SpacesManufacturing Systems, Software Systems, PLCs, Protocols- Z.-W. Li,, and M.-C. Zhou. "Elementary siphons of Petri nets and their application to deadlock preventionin flexible manufacturing systems." IEEE Trans Systems, Man and Cybernetics, Part A, 34.1, 2004.- Y. Pencolé, and M. Cordier. "A formal framework for the decentralised diagnosis of large scale discrete eventsystems and its application to telecommunication networks." Artificial Intelligence, 164.1, 2005.- H.-W. Liao, et al. "Eliminating concurrency bugs in multithreaded software: A new approach based on discreteevent control." IEEE Trans Control Systems Technology, 21.6, 2013. DES Model comes from Finite Abstraction of the original continuous systemLinear Systems, Nonlinear Systems, Stochastic Systems, Networked Systems- P. Tabuada and G. Pappas. "Linear time logic control of discrete-time linear systems." IEEE Trans AutomaticControl, 51.12, 2006.- A. Girard, G. Pola, and P. Tabuada. "Approximately bisimilar symbolic models for incrementally stable switchedsystems." IEEE Trans Automatic Control, 55.1, 2010.- M. Zamani, A. Abate, and A. Girard. "Symbolic models for stochastic switched systems: a discretization and adiscretization-free approach." Automatica, 55,2015.- M. Lahijanian, S. Andersson, and C. Belta. "Formal verification and synthesis for discrete-time stochasticsystems." IEEE Trans Automatic Control 60.8, 2015- J. Liu, and N. Ozay. "Finite abstractions with robustness margins for temporal logic-based controlsynthesis." Nonlinear Analysis: Hybrid Systems, 22, 2016.X.Yin (UMich)SJTU 2016May 20167/31
Discrete-Event Systems System Model𝐺 (𝑋, 𝐸, 𝑓, 𝑥0 , 𝑋𝑚 ) is a deterministic FSA-𝑋 is the finite set of states𝐸 is the finite set of events𝑓: 𝑋 𝐸 𝑋 is the partial transition function𝑥0 is the initial state;𝑋𝑚 is the set of marked states.X.Yin (UMich)SJTU 2016𝑎2𝑎0𝑐1𝑏𝑐𝑐𝑎345Plant GMay 20168/31
Discrete-Event Systems System Model𝐺 (𝑋, 𝐸, 𝑓, 𝑥0 , 𝑋𝑚 ) is a deterministic FSA-𝑋 is the finite set of states𝐸 is the finite set of events𝑓: 𝑋 𝐸 𝑋 is the partial transition function𝑥0 is the initial state;𝑋𝑚 is the set of marked states.𝑎2𝑎0𝑐1𝑏𝑐𝑐𝑎345Plant G System’s Behaviors-String: a sequence of events, e.g., 𝑎𝑏𝑐𝑐𝑎𝑏 .X.Yin (UMich)SJTU 2016May 20168/31
Discrete-Event Systems System Model𝐺 (𝑋, 𝐸, 𝑓, 𝑥0 , 𝑋𝑚 ) is a deterministic FSA-𝑋 is the finite set of states𝐸 is the finite set of events𝑓: 𝑋 𝐸 𝑋 is the partial transition function𝑥0 is the initial state;𝑋𝑚 is the set of marked states.𝑎2𝑎0𝑐1𝑏𝑐𝑐𝑎345Plant G System’s Behaviors-String: a sequence of events, e.g., 𝑎𝑏𝑐𝑐𝑎𝑏 .-Language: a set of stringsX.Yin (UMich)SJTU 2016May 20168/31
Discrete-Event Systems System Model𝐺 (𝑋, 𝐸, 𝑓, 𝑥0 , 𝑋𝑚 ) is a deterministic FSA-𝑋 is the finite set of states𝐸 is the finite set of events𝑓: 𝑋 𝐸 𝑋 is the partial transition function𝑥0 is the initial state;𝑋𝑚 is the set of marked states.𝑎2𝑎0𝑐1𝑏𝑐𝑐𝑎345Plant G System’s Behaviors-String: a sequence of events, e.g., 𝑎𝑏𝑐𝑐𝑎𝑏 .-Language: a set of strings-Generated language: ℒ 𝐺 *𝑠 𝐸 : 𝑓 𝑥0 , 𝑠 ! ℒ 𝐺 *𝝐, 𝑎, 𝑎𝑎, 𝑎𝑏, 𝑎𝑏𝑐, X.Yin (UMich)SJTU 2016May 20168/31
Discrete-Event Systems System Model𝐺 (𝑋, 𝐸, 𝑓, 𝑥0 , 𝑋𝑚 ) is a deterministic FSA-𝑋 is the finite set of states𝐸 is the finite set of events𝑓: 𝑋 𝐸 𝑋 is the partial transition function𝑥0 is the initial state;𝑋𝑚 is the set of marked states.𝑎2𝑎0𝑐1𝑏𝑐𝑐𝑎345Plant G System’s Behaviors-String: a sequence of events, e.g., 𝑎𝑏𝑐𝑐𝑎𝑏 .-Language: a set of strings-Generated language: ℒ 𝐺 *𝑠 𝐸 : 𝑓 𝑥0 , 𝑠 ! ℒ 𝐺 *𝝐, 𝒂, 𝑎𝑎, 𝑎𝑏, 𝑎𝑏𝑐, X.Yin (UMich)SJTU 2016May 20168/31
Discrete-Event Systems System Model𝐺 (𝑋, 𝐸, 𝑓, 𝑥0 , 𝑋𝑚 ) is a deterministic FSA-𝑋 is the finite set of states𝐸 is the finite set of events𝑓: 𝑋 𝐸 𝑋 is the partial transition function𝑥0 is the initial state;𝑋𝑚 is the set of marked states.𝑎2𝑎0𝑐1𝑏𝑐𝑐𝑎345Plant G System’s Behaviors-String: a sequence of events, e.g., 𝑎𝑏𝑐𝑐𝑎𝑏 .-Language: a set of strings-Generated language: ℒ 𝐺 *𝑠 𝐸 : 𝑓 𝑥0 , 𝑠 ! ℒ 𝐺 *𝝐, 𝒂, 𝒂𝒂, 𝑎𝑏, 𝑎𝑏𝑐, X.Yin (UMich)SJTU 2016May 20168/31
Discrete-Event Systems System Model𝐺 (𝑋, 𝐸, 𝑓, 𝑥0 , 𝑋𝑚 ) is a deterministic FSA-𝑋 is the finite set of states𝐸 is the finite set of events𝑓: 𝑋 𝐸 𝑋 is the partial transition function𝑥0 is the initial state;𝑋𝑚 is the set of marked states.𝑎2𝑎0𝑐1𝑏𝑐𝑐𝑎345Plant G System’s Behaviors-String: a sequence of events, e.g., 𝑎𝑏𝑐𝑐𝑎𝑏 .-Language: a set of strings-Generated language: ℒ 𝐺 *𝑠 𝐸 : 𝑓 𝑥0 , 𝑠 ! ℒ 𝐺 *𝝐, 𝒂, 𝒂𝒂, 𝒂𝒃, 𝑎𝑏𝑐, X.Yin (UMich)SJTU 2016May 20168/31
Formal Specifications Formal Specifications Safety: Regular language 𝐿𝑎𝑚 Non-blockingness: no deadlocks or livelocks5 Deadlock10324Livelock Other properties: Observation properties, Temporal logicsX.Yin (UMich)SJTU 2016May 20169/31
Partially-Observed Discrete-Event Systems230415𝑠Projection/Mask𝑃(𝑠)Plant G Not all behaviors can be observed- Internal behavior- Limited sensor capability: energy, communication constraintX.Yin (UMich)SJTU 2016May 201610/31
Partially-Observed Discrete-Event Systems230415𝑠Projection/Mask𝑃(𝑠)Plant G Not all behaviors can be observed- Internal behavior- Limited sensor capability: energy, communication constraint Observation Model𝐸 𝐸𝑜 𝐸𝑢𝑜 Natural Projection 𝑃: 𝐸 𝐸𝑜 erase events in 𝐸𝑢𝑜- 𝐸 𝑎, 𝑏, 𝑐 , 𝐸𝑜 𝑎, 𝑏 , 𝑃 𝑎𝑏𝑐𝑐𝑎 𝑎𝑏𝑎- 𝑃(𝐿 𝐺 ) is the behavior we can observeX.Yin (UMich)SJTU 2016May 201610/31
Property Verification of Partially-Observed DES230415𝑠Projection/Mask𝑃(𝑠)Plant GDoes the system satisfy some property ? Opacity: Security and privacy issue in information-flow Diagnosability: Fault detection and isolation Prognosability: Fault prediction and alarmX.Yin (UMich)SJTU 2016May 201611/31
Opacity230415𝑠Projection/MaskPlant G𝑃(𝑠)Intruder/ Malicious ObserverThe system has a secret OpacityThe system’s secret cannot be revealed based on the intruder’s observation.X.Yin (UMich)SJTU 2016May 201612/31
Opacity23041𝑠Projection/Mask5Plant G𝑃(𝑠)Intruder/ Malicious ObserverThe system has a secret OpacityThe system’s secret cannot be revealed based on the intruder’s observation.𝑠Current State Opacity A set of secret states 𝑋s 𝑋 The intruder never know the system isat secret state Ex: I know that you are visiting hospitalX.Yin (UMich)𝑃 𝑠 𝑃(𝑡)SSJTU 2016𝑡NSMay 201612/31
K-Step Opacity and Infinite-Step Opacity K-Step OpacityThe intruder cannot infer that the system was at a secret state for somespecific instant K-step ahead in the past. Infinite-Step OpacityThe intruder cannot infer that the system was at a secret state for any specificinstant in the past.X.Yin (UMich)SJTU 2016May 201613/31
K-Step Opacity and Infinite-Step Opacity K-Step OpacityThe intruder cannot infer that the system was at a secret state for somespecific instant K-step ahead in the past. Infinite-Step OpacityThe intruder cannot infer that the system was at a secret state for any specificinstant in the 𝑏7𝑢𝑜10𝑏11𝐸𝑜 *𝑜, 𝑎, 𝑏 X.Yin (UMich)SJTU 2016May 201613/31
K-Step Opacity and Infinite-Step Opacity K-Step OpacityThe intruder cannot infer that the system was at a secret state for somespecific instant K-step ahead in the past. Infinite-Step OpacityThe intruder cannot infer that the system was at a secret state for any specificinstant in the past.𝑿 𝒔 𝟎 6𝑏7𝑢𝑜10𝑏11𝐸𝑜 *𝑜, 𝑎, 𝑏 X.Yin (UMich)SJTU 2016May 201613/31
K-Step Opacity and Infinite-Step Opacity K-Step OpacityThe intruder cannot infer that the system was at a secret state for somespecific instant K-step ahead in the past. Infinite-Step OpacityThe intruder cannot infer that the system was at a secret state for any specificinstant in the past.𝑿 𝒔 𝟏 6𝑏7𝑢𝑜10𝑏11𝐸𝑜 *𝑜, 𝑎, 𝑏 X.Yin (UMich)SJTU 2016May 201613/31
K-Step Opacity and Infinite-Step Opacity K-Step OpacityThe intruder cannot infer that the system was at a secret state for somespecific instant K-step ahead in the past. Infinite-Step OpacityThe intruder cannot infer that the system was at a secret state for any specificinstant in the past.𝑿 𝒔 𝟐 6𝑏7𝑢𝑜10𝑏11𝐸𝑜 *𝑜, 𝑎, 𝑏 X.Yin (UMich)SJTU 2016May 201613/31
K-Step Opacity and Infinite-Step Opacity K-Step OpacityThe intruder cannot infer that the system was at a secret state for somespecific instant K-step ahead in the past. Infinite-Step OpacityThe intruder cannot infer that the system was at a secret state for any specificinstant in the past.𝑿 𝒔 𝟐 (𝒐)0𝑜1𝑜2𝑜3It is not 2-step 0𝑏11𝐸𝑜 *𝑜, 𝑎, 𝑏 X.Yin (UMich)SJTU 2016May 201613/31
Verification of K-Step Opacity and Infinite-Step Opacity Previous Result- K-step opacity can be verified in 𝑂( 𝐸𝑜 2 𝑋 𝐸𝑜 12𝐾)- Infinite-step opacity can be verified in 𝑂( 𝐸𝑜 2 𝑋 2 𝑋 )[Saboori & Hadjicostis, 2011][Saboori & Hadjicostis, 2013]- Different approaches for different propertiesX.Yin (UMich)SJTU 2016May 201614/31
Verification of K-Step Opacity and Infinite-Step Opacity Previous Result- K-step opacity can be verified in 𝑂( 𝐸𝑜 2 𝑋 𝐸𝑜 1𝐾)2- Infinite-step opacity can be verified in 𝑂( 𝐸𝑜 2 𝑋 2 𝑋 )[Saboori & Hadjicostis, 2011][Saboori & Hadjicostis, 2013]- Different approaches for different properties Recent Advances- New approach for the verification of K-step and infinite-step opacity- A unified approach based on a separation principle- K-Step: 𝑂( 𝐸𝑜 2 𝑋 𝐦𝐢𝐧* 𝑬𝒐 𝑲 , 𝟐 𝑿 ) vs 𝑂( 𝐸𝑜 2 𝑋 𝑬𝒐 𝟏𝑲)𝟐- Infinite-Step: 𝑂( 𝐸𝑜 2 𝑋 𝟐 𝑿 ) vs 𝑂( 𝐸𝑜 2 𝑋 𝟐 𝑿 )X. Yin and S. Lafortune. “A new approach for the verification of infinite-step and K-stepopacity using two-way observer," Automatica, under review, 2016.X. Yin and S. Lafortune. “On two-way observer and its application to the verification ofinfinite-step and K-step opacity," 13th Int. Workshop on Discrete Event Systems, 2016.X.Yin (UMich)SJTU 2016May 201614/31
Application of Opacity: Location-Based ServicesLocation-Based Services Provide services to mobile users by exploiting their location information Finding nearby restaurants, tracking users’ running routes, etc. May not be secure!UserX.Yin (UMich)NetworkServerSJTU 2016May 201615/31
Application of Opacity: Location-Based ServicesLocation-Based Services Provide services to mobile users by exploiting their location information Finding nearby restaurants, tracking users’ running routes, etc. May not be secure!Attack Model for the Intruder Is located at the LBS server Has mobility patterns of users Receives location information in LBS queriesIntruderUserX.Yin (UMich)NetworkServerSJTU 2016May 201615/31
Application of Opacity: Location-Based ServicesY.-C. Wu, K. Sankararaman and S. Lafortune. "Ensuring privacy in location-based services: Anapproach based on opacity enforcement." WODES14, 47.2 (2014): 33-38.X.Yin (UMich)SJTU 2016May 201616/31
Application of Opacity: Location-Based Services Is state 6 (cancer center) opaque? No! Consider string 𝒄𝒅𝒅Y.-C. Wu, K. Sankararaman and S. Lafortune. "Ensuring privacy in location-based services: Anapproach based on opacity enforcement." WODES14, 47.2 (2014): 33-38.X.Yin (UMich)SJTU 2016May 201616/31
Recent Advances on Fault Diagnosis and Fault PrognosisDiagnosability [Sampath, et al, 1995]The occurrence of any fault event can be detected unambiguously within a finite delay.Prognosability [Genc & Lafortune, 2009, Kumar & Takai, 2011]The occurrence of any fault event can be predicted with no miss-alarm and no false-alarm.X.Yin (UMich)SJTU 2016May 201617/31
Recent Advances on Fault Diagnosis and Fault PrognosisDiagnosability [Sampath, et al, 1995]The occurrence of any fault event can be detected unambiguously within a finite delay.Prognosability [Genc & Lafortune, 2009, Kumar & Takai, 2011]The occurrence of any fault event can be predicted with no miss-alarm and no false-alarm.0𝑜2𝑎X.Yin (UMich)𝑜𝑜𝒇1𝑏3SJTU 2016May 201617/31
Recent Advances on Fault Diagnosis and Fault PrognosisDiagnosability [Sampath, et al, 1995]The occurrence of any fault event can be detected unambiguously within a finite delay.Prognosability [Genc & Lafortune, 2009, Kumar & Takai, 2011]The occurrence of any fault event can be predicted with no miss-alarm and no false-alarm.0𝑜2𝑎X.Yin (UMich)𝑜𝑜𝒇1𝑏3SJTU 2016May 201617/31
Recent Advances on Fault Diagnosis and Fault PrognosisDiagnosability [Sampath, et al, 1995]The occurrence of any fault event can be detected unambiguously within a finite delay.Prognosability [Genc & Lafortune, 2009, Kumar & Takai, 2011]The occurrence of any fault event can be predicted with no miss-alarm and no false-alarm.0𝑜2𝑎X.Yin (UMich)𝑜𝑜𝒇1𝑏3Not diagnosable if we cannot see event aSJTU 2016May 201617/31
Recent Advances on Fault Diagnosis and Fault PrognosisDiagnosability [Sampath, et al, 1995]The occurrence of any fault event can be detected unambiguously within a finite delay.Prognosability [Genc & Lafortune, 2009, Kumar & Takai, 2011]The occurrence of any fault event can be predicted with no miss-alarm and no false-alarm.Recent Advances Diagnosability and observability are equivalent- X. Yin and S. Lafortune, “Codiagnosability and coobservability under dynamic observations:transformation and verification." Automatica, vol.61, pp. 241-252, 2015. (Regular Paper) Performance and reliability issue in decentralized fault prognosis- X. Yin and Z.-J. Li. “Decentralized fault prognosis of discrete event systems with guaranteedperformance bound,” Automatica, vol.69, pp. 375-379, 2016.- X. Yin and Z.-J. Li. “Reliable decentralized fault prognosis of discrete-event systems,”IEEE Trans. Systems, Man, and Cybernetics: Systems, vol.46, no.8, 2016.X.Yin (UMich)SJTU 2016May 201617/31
From Verification to Synthesis What if Verification Fails?- For example: LBS exampleX.Yin (UMich)SJTU 2016May 201618/31
From Verification to Synthesis What if Verification Fails?- For example: LBS example Synthesis!- Synthesis of supervisory control strategies- Synthesis of sensor activation strategiesX.Yin (UMich)SJTU 2016May 201618/31
Supervisory Control Property Enforcement via Supervisory Control230System Property 𝑠415Plant G𝑆(𝑠)𝑃𝑆: 𝐸𝑜 ΓSupervisor𝑃(𝑠)ObservationProperty Observation:𝐸 𝐸𝑜 𝐸𝑢𝑜 Supervisor:𝐸 𝐸𝑐 𝐸𝑢𝑐 , 𝐸𝑢𝑐 uncontrollable events (environment)Disable events in 𝐸𝑐 based on its observationsX.Yin (UMich)SJTU 2016May 201619/31
Formal Specifications System Property- Safety: never visited illegal states- Non-blockingness: no deadlocks or livelocksX.Yin (UMich)SJTU 2016May 201620/31
Formal Specifications System Property- Safety: never visited illegal states- Non-blockingness: no deadlocks or livelocks Observation Property- Opacity, Diagnosability, Prognosability, ObservabilityX.Yin (UMich)SJTU 2016May 201620/31
Formal Specifications System Property- Safety: never visited illegal states- Non-blockingness: no deadlocks or livelocks Observation Property- Opacity, Diagnosability, Prognosability, Observability Maximal Permissiveness- Optimality criterion is set inclusion.Only disable an event if absolutely necessaryX.Yin (UMich)SJTU 2016May 201620/31
Formal Specifications System PropertyStandard Supervisory Control- Safety: never visited illegal states[Ramadge & Wonham, 1980s]- Non-blockingness: no deadlocks or livelocks Observation Property- Opacity, Diagnosability, Prognosability, Observability Maximal Permissiveness- Optimality criterion is set inclusion.Only disable an event if absolutely necessaryX.Yin (UMich)SJTU 2016May 201620/31
Property Enforcing Supervisory Control usAssumptionsNone𝐸𝑎 𝐸𝑜𝐸𝑐 𝐸𝑜𝐸𝑐 𝐸𝑜𝐸𝑐 𝐸𝑜N/A𝐸𝑐 𝐸𝑜[1] [Lin and Wonham, 1988][2] [Cieslak et al., 1988][3] [Ben Hadj-Alouane et al., 1996][4] [Dubreil et al., 2010]X.Yin (UMich)Anonymity Attractability[5] [Saboori and Hadjicostis, 2011][6] [Sampath et al., 1998][7] [Shu and Lin, 2013][8] [Schmidt and Breindl, 2014]SJTU 2016May 201621/31
Property Enforcing Supervisory Control usAssumptionsNone𝐸𝑎 𝐸𝑜𝐸𝑐 𝐸𝑜𝐸𝑐 𝐸𝑜𝐸𝑐 𝐸𝑜N/A𝐸𝑐 𝐸𝑜OurAssumptionNone𝐸𝑎 𝐸𝑜NoneNone𝐸𝑎 𝐸𝑜None[1] [Lin and Wonham, 1988][2] [Cieslak et al., 1988][3] [Ben Hadj-Alouane et al., 1996][4] [Dubreil et al., 2010]Anonymity Attractability[5] [Saboori and Hadjicostis, 2011][6] [Sampath et al., 1998][7] [Shu and Lin, 2013][8] [Schmidt and Breindl, 2014]A Uniform ApproachX. Yin and S. Lafortune, “A uniform approach for synthesizing property-enforcing supervisors forpartially-observed DES." IEEE Transactions Automatic Control, vol.61, no.8, 2016. (Regular Paper)X.Yin (UMich)SJTU 2016May 201621/31
A Uniform Approach for Property Enforcement Information State: a set of states; 𝐼 2𝑋 . State Estimate: all possible states consistent with 𝑜𝑜𝑜𝑐26𝑐1 Supervisor 𝑆 disables nothing 𝐼 𝑜 3,4 , 𝐼 𝑜𝑜 *5,6 8𝐸𝑐 *𝑐1 , 𝑐2 , 𝐸𝑜 *𝑜 X.Yin (UMich)SJTU 2016May 201622/31
A Uniform Approach for Property Enforcement Information State: a set of states; 𝐼 2𝑋 . State Estimate: all possible states consistent with observation Information-State Based Property: 𝜑: 2𝑋 *0,1 It contains: safety, opacity, diagnosability, detectability, attractability,anonimity, �𝑜𝑐26𝑐1 Supervisor 𝑆 disables nothing 𝐼 𝑜 3,4 , 𝐼 𝑜𝑜 *5,6 8𝐸𝑐 *𝑐1 , 𝑐2 , 𝐸𝑜 *𝑜 X.Yin (UMich)SJTU 2016May 201622/31
A Uniform Approach for Property Enforcement Information State: a set of states; 𝐼 2𝑋 . State Estimate: all possible states consistent with observation Information-State Based Property: 𝜑: 2𝑋 *0,1 It contains: safety, opacity, diagnosability, detectability, attractability,anonimity, etc.𝝋 𝒊 𝟎 𝒊 𝑩𝑨𝑫 �𝑐26𝑐1 Supervisor 𝑆 disables nothing 𝐼 𝑜 3,4 , 𝐼 𝑜𝑜 *5,6 8𝐸𝑐 *𝑐1 , 𝑐2 , 𝐸𝑜 *𝑜 X.Yin (UMich)SJTU 2016May 201622/31
A Uniform Approach for Property Enforcement Information State: a set of states; 𝐼 2𝑋 . State Estimate: all possible states consistent with observation Information-State Based Property: 𝜑: 2𝑋 *0,1 It contains: safety, opacity, diagnosability, detectability, attractability,anonimity, etc. Key Result:Any IS-based property can be enforced by an IS-based ���𝑜𝑜𝑐26𝑐1 Supervisor 𝑆 disables nothing 𝐼 𝑜 3,4 , 𝐼 𝑜𝑜 *5,6 8𝐸𝑐 *𝑐1 , 𝑐2 , 𝐸𝑜 *𝑜 X.Yin (UMich)SJTU 2016May 201622/31
A Uniform Approach for Property Enforcement Basic Idea: Construct an information structure that captures all possiblecontrolled behaviors of the system All Inclusive Controller:- A “Game” between environment and controller- Two kinds of states: Y-states and Z-states- It embeds (infinite many) solutions in its finite 𝑜4𝑜6𝑐1{3,4,5},{𝑐1 }8𝑜𝑜{3,4}* 𝑜*𝑐2 𝑜{3,4,6},{𝑐2 }{3,4},{ }𝐸𝑐 *𝑐1 , 𝑐2 , 𝐸𝑜 *𝑜 X.Yin (UMich){0,1,2},{ }*𝑐1 𝑜𝑐2{}SJTU 2016May 201623/31
A Uniform Approach for Property Enforcement Basic Idea: Construct an information structure that captures all possiblebehaviors All Inclusive Controller:- A “Game” between environment and controller- Two kinds of states: Y-states and Z-states- It embeds (infinite many) solutions in its finite structureSynthesis: Pick a locally maximal control decision at each Y-state 6𝑐1{3,4,5},{𝑐1 }8𝑜𝑜{3,4}* 𝑜*𝑐2 𝑜{3,4,6},{𝑐2 }{3,4},{ }𝐸𝑐 *𝑐1 , 𝑐2 , 𝐸𝑜 *𝑜 X.Yin (UMich){0,1,2},{ }*𝑐1 𝑜𝑐2{}SJTU 2016May 201623/31
A Uniform Approach for Property Enforcement Basic Idea: Construct an information structure that captures all possiblebehaviors All Inclusive Controller:- A “Game” between environment and controller- Two kinds of states: Y-states and Z-states- It embeds (infinite many) solutions in its finite structureSynthesis: Pick a locally maximal control decision at each Y-state 6𝑐1{3,4,5},{𝑐1 }8𝑜𝑜{3,4}* 𝑜*𝑐2 𝑜{3,4,6},{𝑐2 }{3,4},{ }𝐸𝑐 *𝑐1 , 𝑐2 , 𝐸𝑜 *𝑜 X.Yin (UMich){0,1,2},{ }*𝑐1 𝑜𝑐2{}SJTU 2016May 201623/31
A Uniform Approach for Property Enforcement Basic Idea: Construct an information structure that captures all possiblebehaviors All Inclusive Controller:- A “Game” between environment and controller- Two kinds of states: Y-states and Z-states- It embeds (infinite many) solutions in its finite structureSynthesis: Pick a locally maximal control decision at each Y-state ess{ } is not{0,1,2},{ }{0}an IS-BasedProp!3𝑜4𝑐2𝑜6𝑐1{3,4,5},{𝑐1 }8𝑜{3,4}* 𝑜*𝑐2 𝑜{3,4,6},{𝑐2 }{3,4},{ }𝐸𝑐 *𝑐1 , 𝑐2 , 𝐸𝑜 *𝑜 X.Yin (UMich)𝑜*𝑐1 𝑜SJTU 2016May 201623/31
Standard Supervisory Control ProblemSafetySafe MaxSafe NBSafe NB MaxCentralizedUpper [3]OPENOPENOPENDecentralizedUpper tralizedRange[2],[6]OPENUndecidableUndecidable[1] [Lin and Wonham, 1988][4][Ben Hadj-Alouane et al., 1996] [7][Tripakis, 2004][2] [Cieslak et al., 1988][5][Yoo and Lafortune, 2006][8][Thistle, 2005][3][Rudie and Wonham, 1990] [6][Rudie and Wonham, 1992]X.Yin (UMich)SJTU 2016May 201624/31
Standard Supervisory Control ProblemSafetySafe MaxSafe NBSafe NB MaxCentralizedUpper ],[3]SolvedOPENOPENDecentralizedUpper tralizedRange[2],[6]OPENUndecidableUndecidable [1] [Lin and Wonham, 1988][4][Ben Hadj-Alouane et al., 1996] [7][Tripakis, 2004][2] [Cieslak et al., 1988][5][Yoo and Lafortune, 2006][8][Thistle, 2005][3][Rudie and Wonham, 1990] [6][Rudie and Wonham, 1992]Recent AdvancesX. Yin and S. Lafortune, “Synthesis of maximally permissive supervisors for partially observed DES."IEEE Transactions Automatic Control, vol.61, no.5, 2016. (Regular Paper)X. Yin and S. Lafortune. "Synthesis of maximally-permissive supervisors for the range control problem,"IEEE Transactions Automatic Control, under review, 2016. (Regular Paper)X.Yin (UMich)SJTU 2016May 201624/31
Standard Supervisory Control ProblemSafetySafe MaxSafe NBSafe NB MaxCentralizedUpper ],[3]SolvedOPENOPENDecentralizedUpper tralizedRange[2],[6]OPENUndecidableUndecidable [1] [Lin and Wonham, 1988][4][Ben Hadj-Alouane et al., 1996] [7][Tripakis, 2004][2] [Cieslak et al., 1988][5][Yoo and Lafortune, 2006][8][Thistle, 2005][3][Rudie and Wonham, 1990] [6][Rudie and Wonham, 1992]Recent AdvancesX. Yin and S. Lafortune, “Synthesis of maximally permissive supervisors for partially observed DES."IEEE Transactions Automatic Control, vol.61, no.5, 2016. (Regular Paper)X. Yin and S. Lafortune. "Synthesis of maximally-permissive supervisors for the range control problem,"IEEE Transactions Automatic Control, under review, 2016. (Regular Paper)X.Yin (UMich)SJTU 2016May 201624/31
Non-blocking Control ProblemObservation: 2𝑋 is not sufficient to make a decision 6𝑐1{3,4,5},{𝑐1 }8𝑜𝑜{3,4}* 𝑜*𝑐2 𝑜{3,4,6},{𝑐2 }{3,4},{ }𝐸𝑐 *𝑐1 , 𝑐2 , 𝐸𝑜 *𝑜 X.Yin (UMich){0,1,2},{ }*𝑐1 𝑜𝑐2{}SJTU 2016May 201625/31
Non-blocking Control ProblemObservation: 2𝑋 is not sufficient to make a decision 6𝑐1{3,4,5},{𝑐1 }8𝑜𝑜{3,4}* 𝑜*𝑐2 𝑜{3,4,6},{𝑐2 }{3,4},{ }𝐸𝑐 *𝑐1 , 𝑐2 , 𝐸𝑜 *𝑜 X.Yin (UMich){0,1,2},{ }*𝑐1 𝑜𝑐2{}SJTU 2016May 201625/31
Non-blocking Control ProblemObservation: 2𝑋 is not sufficient to make a decision 6𝑐1{3,4,5},{𝑐1 }8𝑜𝑜{3,4}* 𝑜*𝑐2 𝑜{3,4,6},{𝑐2 }{3,4},{ }𝐸𝑐 *𝑐1 , 𝑐2 , 𝐸𝑜 *𝑜 X.Yin (UMich){0,1,2},{ }*𝑐1 𝑜𝑐2{}SJTU 2016May 201625/31
Non-blocking Control ProblemObservation: 2𝑋 is not sufficient to make a de
Why Discrete-Event Models X.Yin (UMich) SJTU 2016 May 2016 Why Discrete-Event Models Many systems are Inherently Event-Driven and have Discrete State-Spaces Manufacturing Systems, Software Systems, PLCs, Protocols - Z.-W. Li,, and M.-C. Zhou. "Elementary siphons o
It is extremely important to always cover or uncover the pool completely. Never leave the pool partially covered. A partially covered pool presents a serious danger as people or pets may drown under the cover. 7!2.).' A partially covered pool can pose a safety hazard. Never leave the cover over the pool in a partially covered position.
Pet owner emergency preparedness survey report: Taranaki and Wellington Regions v1.1 2010 18 dog muzzles and leashes If you have dogs, do you have a muzzle and leash for each dog? 17% 0% 79% 2% 2% Yes (leads and muzzles for each dog) Partially -Some/all muzzles but no leads Partially -Some/all leads but no muzzles Partially -some leads and some .
The roof may partially (Figures 1 and 2) or fully cover the feeding pens (Figures 3 and 4). In a partially covered design, the roof would cover the feed bunk only or the bunk plus about one third of the pen area. The sides of the structure may be closed, partially closed or open. As a minimum, the feed bunk area should be covered. Fully
partially filled with water for a second throw. Some bags have open webbing partially exposing the rope in the bag. These bags expose the rope and make a second throw with a partially filled bag difficult. Third, UV light breaks down nylon and changes the color of nylon to white. This provides a visual check of the fabric.
Control theories commonly used today are classical control theory (also called con-ventional control theory), modern control theory, and robust control theory.This book presents comprehensive treatments of the analysis and design of control systems based on the classical control theory and modern control theory.A brief introduction of robust
Present ICE Analysis in Environmental Document 54 Scoping Activities 55 ICE Analysis Analysis 56 ICE Analysis Conclusions 57 . Presenting the ICE Analysis 59 The ICE Analysis Presentation (Other Information) 60 Typical ICE Analysis Outline 61 ICE Analysis for Categorical Exclusions (CE) 62 STAGE III: Mitigation ICE Analysis Mitigation 47 .
37 Engine Control #5 38 Engine Control #6 39 Machine Control Module 40 Engine Control #7 41 Engine Control #8 42 Engine Control #9 43 Engine Control #10 47 Backup Engine Control 49 VIMS Main Module 50 VIMS Analysis Module 51 VIDS Main Module 52 Graphical Display Module #2 D6R Track-Type Tractor 9PN00001-UP (MACHINE) POWERED BY 3306 Engine(SEB .
AN ISO 50001 AUDIT Form Title Revision No. Effective Date Page : FEn-TNI-001 : 1: 15.09.2015 : 4 of 6 yes no partially Has the management system been defined in a manual according to clause 4.1 of ISO 50001:2011? yes no partially Is the control of docu
