Shaowen Miao | Search arXiv

arXiv2026

Supervisory Control under Partial Observation: Where Observation Consistency Becomes Decidable

Observation consistency (OC) and modified observation consistency (MOC) are structural conditions used in hierarchical and modular supervisory control under partial observation. Their verification for languages generated by deterministic finite automata is PSPACE-hard, whereas decidability was open. We answer this question by showing that both problems are undecidable, that is, there are no algorithms verifying OC or MOC. On the positive side, we identify a decidable class defined by a restriction on the plant: if every cycle of the automaton contains a transition labeled by an observable high-level event, then verification of both conditions is PSPACE-complete.

cs.FL↗

arXiv2025

Active prognosis and diagnosis of modular discrete-event systems

This paper addresses the verification and enforcement of prognosability and diagnosability for discreteevent systems (DESs) modeled by deterministic finite automata. We establish the equivalence between prognosability (respectively, diagnosability) and pre-normality over a subset of the non-faulty language (respectively, a suffix of the faulty language). We then demonstrate the existence of supremal prognosable (respectively, diagnosable) and normal sublanguages. Furthermore, an algorithm is then designed to compute the supremal controllable, normal, and prognosable (respectively, diagnosable) sublanguages. Since DESs are typically composed of multiple components operating in parallel, pure local supervisors are generally insufficient, as prognosability and diagnosability are global properties of a system. Given the limited work on enforcing prognosability or diagnosability in modular DESs, where these properties are enforced through local supervisors, this paper leverages a refined version of pre-normality to compute modular supervisors for local subsystems. The resulting closed-loop system is shown to be globally controllable, normal, and prognosable/ diagnosable. Examples are provided to illustrate the proposed method.

eess.SY↗