Supervisory Control under Partial Observation: Where Observation Consistency Becomes Decidable

I. INTRODUCTION

• Hierarchical control synthesizes on a smaller high-level abstraction and implements on the original plant, requiring high-level properties to transfer to low level.This addresses limitations caused by the size of the plant model.Source: §I · p. 1
• OC supports transfer of observability, while MOC supports transfer of normality and computation of supremal normal sublanguages that commutes with abstraction.MOC requires a matching realization to preserve the observation of a low-level realization fixed in advance.Source: §I · p. 1
• MOC also supports modular normal-supervisor composition and modular enforcement of properties including critical observability, non-weak opacity, diagnosability, and prognosability.The passage also describes applications to networked and cyber-attacked DESs through nondeterministic counterparts.Source: §I · p. 1
• Earlier verification was PSPACE-hard, while applications used easy-to-check alphabetic sufficient conditions that are strictly stronger than OC and MOC.Whether any verification algorithm existed remained open.Source: §I · p. 1
• Verification of OC and MOC is undecidable, even with five events, two observable events, and three high-level events.The reductions encode universality of rational relations.Source: §I · p. 1
• When the two projections synchronize after a bounded number of events, verification of both conditions is PSPACE-complete.The paper presents this plant restriction as a decidable class.Source: §I · p. 2

II. PRELIMINARIES

• A projection retains events in its target alphabet and erases other events, extending to strings as a concatenation morphism.The preliminaries also define finite alphabets, languages, and prefix closure.Source: §II · p. 2
• A DFA has a partial transition function; its generated language is prefix-closed, and equals its marked language when every reachable state is marked.The preliminaries distinguish generated and marked languages.Source: §II · p. 2
• OC requires two strings with indistinguishable high-level projections to have low-level realizations with the same low-level observation.The condition is defined for a prefix-closed language with respect to Q, P, and Phi.Source: §II · p. 2
• MOC differs in quantifier order: it fixes the first low-level string in advance and requires a matching realization with the same observation.MOC implies OC [4, Lemma 10].Source: §II · p. 2

A. Rational Relations

• A rational relation can be represented by a regular language over a finite alphabet and two morphisms into the component alphabets.The passage defines rationality through a regular language H and morphisms f and g.Source: A. Rational Relations · p. 2
• Rational relations are closed under union and concatenation, and Cartesian products of regular languages are rational.They are also closed under Kleene star.Source: A. Rational Relations · p. 2
• Universality of a rational relation is undecidable, and disjoint renamed copies of its alphabets preserve rationality and universality.The disjointness requirement for the regular-language representation therefore imposes no restriction.Source: A. Rational Relations · p. 2

III. CHARACTERIZATIONS OF THE CONDITIONS

• MOC holds exactly when high-level strings with equal Phi-projections have equal sets of compatible low-level observations.The proof establishes equality by showing each observation set is included in the other.Source: §III · p. 3
• OC holds exactly when every pair of high-level strings with equal Phi-projections has intersecting low-level observation sets.A common observation supplies the matching low-level realizations required by OC.Source: §III · p. 3
• For disjoint observable and high-level alphabets, MOC requires all high-level strings to have equal observation sets, whereas OC requires pairwise nonempty intersections.In this case all their Phi-projections are equal.Source: §III · p. 3
• MOC is equivalent to CL ⊆ RL; because RL ⊆ CL, the characterization reduces MOC to the reverse inclusion.RL is rational when L is regular.Source: §III · p. 3

IV. MAIN RESULTS

• Lemma 1 makes L = Ω* ∪ Ka prefix-closed and regular, and its DFA can be constructed in polynomial time.The construction adds a sink to the DFA for K, then adds a state reached by a-transitions from marked states and marks all states.Source: §IV · p. 3
• Lemma 2 constructs a rational relation S over two-letter alphabets whose range is B* and whose universality is equivalent to that of R.The reduction uses fixed-length injective encodings; rationality follows from closure under concatenation and union.Source: §IV · p. 3
• The construction establishes that S is universal if and only if R is universal.The two final terms of S cover pairs outside the encoded domains, leaving the encoded pairs to preserve the original relation's universality.Source: §IV · p. 3
• Theorem 1 uses disjoint A and B, while the reduction in Section B uses A = B.Lemma 1 does not require A and B to be disjoint.Source: §IV · p. 3

A. Undecidability of MOC Verification

• MOC verification for DFA-generated languages is undecidable even with five events, two observable events, and three high-level events.The reduction constructs a DFA language that is MOC exactly when the given rational relation is universal.Source: A. Undecidability of MOC Verification · p. 4
• The reduction uses disjoint two-letter alphabets A and B, adds a fresh event a, and defines Σ = (A ∪ B) ∪ {a}, Σo = A, and Σhi = B ∪ {a}.Lemma 1 makes the resulting language prefix-closed and effectively represented by a DFA.Source: A. Undecidability of MOC Verification · p. 4
• For each t ∈ B*, the language construction gives OL(ta) = A* exactly when the constructed relation S is universal.Strings with high-level projection ta end in the unobservable event a; strings ut supply each u ∈ A* for high-level projection t.Source: A. Undecidability of MOC Verification · p. 4
• Because MOC holds exactly when S is universal, the construction makes MOC hold if and only if the original relation R is universal.Thus an algorithm deciding MOC would decide rational-relation universality.Source: A. Undecidability of MOC Verification · p. 4

• The construction encodes a rational relation using an injective morphism and projections that recover its two component strings.The relation is represented by a regular language, with the encoded input recovered alongside the outputs f(k) and g(k).Source: B. Undecidability of OC Verification · p. 4
• For the constructed strings, the observation sets for 2xa and 3ya intersect exactly when (x, y) belongs to the rational relation.The encoding separates the sentinel observations from strings e(k), making a shared encoded observation correspond to a witness k.Source: B. Undecidability of OC Verification · pp. 4–5
• OC verification for DFAs is undecidable, even with |Σ|=5, |Σo|=2, and |Σhi|=3.Source: B. Undecidability of OC Verification · pp. 4–5
• The constructed language is OC exactly when the rational relation contains every pair in V* × V*, so an OC decider would decide relation universality.Source: B. Undecidability of OC Verification · p. 5

• I-boundedness means a uniform bound on consecutive events outside I; equivalently, no cycle uses only events outside I.For reachable-state DFAs, the condition can be checked in linear time by deleting I-labeled transitions and testing the remaining reachable graph for cycles.Source: §V · p. 5
• Bounded non-I blocks between shared events yield unique alternating encodings of projection pairs over a finite block alphabet.The encoding interleaves each pair of non-I blocks with the shared event that synchronizes the projections.Source: §V · p. 5
• The proof constructs regular encodings of the induced relations, reducing MOC verification to language inclusion.Source: §V · pp. 5–6
• OC verification is likewise reduced to inclusion between regular languages using encodings of pairs of high-level strings with matching observations.Source: §V · p. 6
• The encoded automata are represented succinctly despite the exponential block alphabet, and on-the-fly inclusion testing gives the PSPACE upper bound.The complexity comes from the inclusion test rather than explicitly constructing the alphabet.Source: §V · p. 6
• The bounded class includes both a language that is neither OC nor MOC and one that is MOC.The prefix closure of (ac + xc)* is I-bounded but fails both conditions, whereas c* is I-bounded and MOC.Source: §V · pp. 6–7
• The PSPACE-hardness reduction already applies to I-bounded instances with N=3.Thus the exponential size of the block alphabet in general is not needed for hardness.Source: §V · p. 7
• OC and MOC verification on I-bounded plants are PSPACE-complete.The PSPACE-hardness holds even when the bound is N=3.Source: §V · pp. 5, 7

• For prefix-closed regular languages represented by DFAs, OC and MOC verification are undecidable; the bounded-synchronization restriction instead yields a PSPACE-complete class.When the automaton has no cycle labeled solely by events outside the shared alphabet, the induced relations become regular over finite block alphabets.Source: §VI · p. 7