arxiv: 2602.09360 · v2 · submitted 2026-02-10 · 💻 cs.FL

Recognition: no theorem link

The Similarity Control Problem with Required Events

Yu Wang , Zhaohui Zhu , Rob van Glabbeek , Jinjin Zhang , Yixuan Li

Authors on Pith no claims yet

Pith reviewed 2026-05-16 06:21 UTC · model grok-4.3

classification 💻 cs.FL

keywords discrete event systemssupervisory controlsimilarity controlrequired eventscovariant-contravariant simulationmaximally permissive supervisorsafety constraints

0 comments

The pith

Covariant-contravariant simulation gives a necessary and sufficient condition for solving the similarity control problem with required events.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper extends the similarity control problem in discrete event systems to enforce both safety constraints and requirements that certain events must be enabled in given states. It treats covariant-contravariant simulation as the behavioral relation that captures these combined demands more tightly than ordinary simulation. From this relation the authors derive a necessary and sufficient condition for the existence of a supervisor and supply an explicit construction for the maximally permissive one.

Core claim

The similarity control problem with required events is solvable precisely when a covariant-contravariant simulation relation holds between the specification and the plant; the largest such relation yields a maximally permissive supervisor that restricts the plant so that all safety prohibitions and required-event mandates are met.

What carries the argument

Covariant-contravariant simulation, which requires that every required event in the specification is matched by a corresponding transition in the plant while controllable events may be restricted in the opposite direction, serving as the precise behavioral relation for the combined constraints.

If this is right

The supervisor can be obtained directly from the largest covariant-contravariant simulation relation.
The resulting controller is guaranteed to be the most permissive one that still meets both safety and required-event specifications.
The same relation supplies an algorithmic test for solvability by checking existence of the simulation.
The approach extends ordinary supervisory control by treating mandatory event enablement as a first-class constraint alongside forbidden events.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

The same simulation relation could be reused as a verification oracle inside existing model-checking tools for discrete-event systems.
The construction suggests a route to on-line supervisor synthesis when the plant is only partially known.
Generalizing the relation to handle timing or probabilities would produce analogous solvability conditions for timed or stochastic variants of the problem.

Load-bearing premise

Covariant-contravariant simulation exactly encodes both safety prohibitions and required-event mandates without missing valid behaviors or imposing extra ones.

What would settle it

A concrete plant, specification, and supervisor that satisfies every safety and required-event condition yet admits no covariant-contravariant simulation relation between the controlled plant and the specification.

Figures

Figures reproduced from arXiv: 2602.09360 by Jinjin Zhang, Rob van Glabbeek, Yixuan Li, Yu Wang, Zhaohui Zhu.

**Figure 1.** Figure 1: The plant G (left) and specification R (right) The plant G starts when a customer presses the start button to initiate the check-out process. Then, an item is scanned 1 arXiv:2602.09360v1 [cs.FL] 10 Feb 2026 [PITH_FULL_IMAGE:figures/full_fig_p001_1.png] view at source ↗

**Figure 2.** Figure 2: The supervisor S (left) and supervised system S||G (right) by the scanner which nondeterministically transitions to one of two states x2 and x3. In the state x2, the customer can choose to either put the item in a bag or cancel the transaction, while in the state x3, the only option available is to put the item in the bag. As auditors of the system we judge not providing the option to cancel in the state … view at source ↗

**Figure 3.** Figure 3: The plant G (left), specification R (middle) and reachable part of supervisor A(E) (right) Example 9 Consider the plant G = (X, Σ, −→, {x0}) and specification R = (Z, Σ, −→, {z0}) in [PITH_FULL_IMAGE:figures/full_fig_p005_3.png] view at source ↗

**Figure 4.** Figure 4: The reachable part of supervised system A(E)||G Theorem 14 Let G and R be two automata. There exists a Σuc-admissible supervisor S such that S||G ⊑cc R iff there exists a Σucr-controllability set E from G to R. Proof. This immediately follows from Lemma 11 and 13. □ Given W, W′ ∈ E ⊆ ℘(X × Z) and σ ∈ Σ, the time complexity of verifying matchG,R(W, σ, W′ ) is O(|X| 2 |Z| 2 ). Hence, for each W ∈E, the time … view at source ↗

**Figure 5.** Figure 5: The plant G (left) and specification R (right) Clearly, there exists a Σucr-simulation relation from G to R, e.g., Φ = {(x0, z0),(x1, z1),(x3, z2)}. Assume that there exists a Σucr-controllability set E from G to R. Then we 3Given a set X, a set E ⊆ ℘(X) is a cover of X if X = S E. have {(x0, z0)} ∈ W0 ∈ E for some W0. Hence, by the clause (6 − b) in Definition 6 and z0 l −→ z1 with l ∈ Σr, there exists x … view at source ↗

**Figure 6.** Figure 6: The plant G (left) and specification R (right) Lemma 22 For any deterministic automata G and R, if Φ : G ⊑ucr R then Φ is uniform w.r.t. Σr. Proof. This immediately follows from the fact that, for any s ∈ Σ ∗ , there exists at most one s-reachable state in each deterministic automaton. □ The following corollary follows immediately from Observation 17, Lemma 20 and 22 and Theorem 14. It provides another ne… view at source ↗

read the original abstract

In order to guarantee that a supervised system satisfies safety requirements of the specification, as well as requirements saying that in certain states certain events must be enabled, this paper introduces required events for discrete event systems and reconsiders the similarity control problem while taking all requirements from the specification into account. The notion of a covariant-contravariant simulation, which is finer than the conventional notion of simulation, is adopted to act as the behavioral relation of supervisory control theory. A necessary and sufficient condition for the solvability of this problem is established and a method for synthesizing a maximally permissive supervisor is provided.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

The paper adds required events to the similarity control problem and uses covariant-contravariant simulation to claim a necessary and sufficient condition plus a synthesis method for the maximally permissive supervisor.

read the letter

The main point is that this work adds the concept of required events to the similarity control problem in discrete event systems. These are events that must be enabled in certain states of the specification. To handle both the usual safety requirements and these new mandatory ones, the authors adopt covariant-contravariant simulation as the behavioral relation instead of standard simulation. They prove a necessary and sufficient condition for when the problem has a solution and give a way to synthesize a maximally permissive supervisor. This is genuinely new. The prior literature on similarity control didn't include required events, and applying covariant-contravariant simulation here is a reconsideration that fits the dual constraints. The paper does well in clearly defining the problem and outlining the results in a concise way. The formal setup looks standard and appropriate for the area. If the proofs check out, the synthesis method could be useful for applications where some events are obligatory. A soft spot is the justification for using the finer simulation relation. The stress test raises a valid concern: the necessity claim assumes that any valid supervisor must satisfy the covariant-contravariant properties. If ordinary simulation is enough to enforce the required events, then this approach might exclude some valid supervisors and fail to be maximally permissive. The abstract doesn't provide a counterexample or reduction to show the extra clauses are needed, so the full paper needs to address this directly. This is targeted at specialists in formal methods for discrete event systems. Someone in supervisory control or behavioral equivalences would find it relevant and could cite the condition or synthesis algorithm. It engages honestly with the literature and has enough technical content to merit a full review. I recommend sending it to peer review.

Referee Report

1 major / 2 minor

Summary. The paper introduces required events into discrete event systems to capture both safety and mandatory event-enabling constraints within the similarity control problem. It adopts covariant-contravariant simulation (finer than ordinary simulation) as the behavioral relation, establishes a necessary and sufficient condition for solvability, and provides a synthesis procedure for a maximally permissive supervisor.

Significance. If the N&S condition and synthesis method are correct, the work extends supervisory control theory by handling required-event constraints through a refined simulation relation. This could support controller design for systems with both permissive and mandatory behaviors, provided the necessity of the contravariant clauses is verified.

major comments (1)

[Abstract and N&S condition section] Abstract and the section establishing the N&S condition: the necessity claim that any valid supervisor must induce a covariant-contravariant simulation (rather than ordinary simulation) is load-bearing for both the condition and the maximality of the synthesized supervisor. No counter-example or reduction is indicated showing that ordinary simulation would admit supervisors violating required-event semantics; without this, the condition may reject valid solutions.

minor comments (2)

[Preliminaries] Clarify the precise definition of required events and how they are encoded in the plant and specification automata before the main theorems.
[Abstract] The abstract states the existence of the N&S condition and synthesis method; the main body should explicitly reference the theorem numbers for these results.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for the careful reading and constructive comments on our manuscript. We address the major comment below.

read point-by-point responses

Referee: [Abstract and N&S condition section] Abstract and the section establishing the N&S condition: the necessity claim that any valid supervisor must induce a covariant-contravariant simulation (rather than ordinary simulation) is load-bearing for both the condition and the maximality of the synthesized supervisor. No counter-example or reduction is indicated showing that ordinary simulation would admit supervisors violating required-event semantics; without this, the condition may reject valid solutions.

Authors: We appreciate the referee's observation on the load-bearing nature of the necessity claim. The covariant-contravariant simulation is required because required events impose mandatory enabling constraints (i.e., certain events must remain enabled in specified states). The contravariant clause in the simulation relation directly encodes this 'must' semantics, ensuring the supervisor cannot disable required events. This follows from the problem formulation and is used in the proof of the N&S condition to show that any valid supervisor induces such a relation. We acknowledge that an explicit counterexample would clarify why ordinary simulation is insufficient and could admit invalid supervisors. In the revised manuscript, we will add a concise counterexample demonstrating a supervisor that satisfies ordinary simulation but disables a required event, thereby violating the specification. This addition will also reinforce the maximality claim for the synthesized supervisor. revision: yes

Circularity Check

0 steps flagged

No circularity: N&S condition derived directly from definitions

full rationale

The paper adopts covariant-contravariant simulation as the behavioral relation to capture both safety and required-event constraints, then states a necessary and sufficient solvability condition and a synthesis procedure. No quoted step reduces the central theorem to a self-definition, a fitted input renamed as prediction, or a load-bearing self-citation chain. The derivation remains self-contained from the problem definitions and the chosen simulation preorder; the necessity direction is proved within the paper rather than imported by construction.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 1 invented entities

The central claim rests on the newly introduced notion of required events and the adoption of covariant-contravariant simulation as the behavioral relation; no free parameters are mentioned.

axioms (1)

domain assumption Covariant-contravariant simulation is a suitable finer behavioral relation for supervisory control with required events
Explicitly adopted in the abstract as the relation for the similarity control problem.

invented entities (1)

required events no independent evidence
purpose: To model requirements that certain events must be enabled in certain states of the discrete event system
New concept introduced to extend the specification beyond safety requirements.

pith-pipeline@v0.9.0 · 5393 in / 1149 out tokens · 32280 ms · 2026-05-16T06:21:30.274423+00:00 · methodology

discussion (0)

Reference graph

Works this paper leans on

25 extracted references · 25 canonical work pages

[1]

Aceto, I

L. Aceto, I. F´ abregas, D. de Frutos Escrig, A. Ing´ olfsd´ ottir, and M. Palomino. Relating modal refinements, covariant- contravariant simulations and partial bisimulations. InFun- damentals of Software Engineering: 4th IPM International Conference, pages 268–283, 2012

work page 2012
[2]

Aceto, I

L. Aceto, I. F´ abregas, D. de Frutos Escrig, A. Ing´ olfsd´ ottir, and M. Palomino. On the specification of modal systems: A comparison of three frameworks.Science of Computer Pro- gramming, 78(12):2468–2487, 2013

work page 2013
[3]

F´ abregas, D

I. F´ abregas, D. de Frutos-Escrig, and M. Palomino. Non- strongly stable orders also define interesting simulation re- lations. In Proceedings Third International Conference on Algebra and Coalgebra in Computer Science, volume 5728 of LNCS, pages 221–235. Springer, 2009

work page 2009
[4]

F´ abregas, D

I. F´ abregas, D. de Frutos Escrig, and M. Palomino. Logics for contravariant simulations. InInternational Conference on Formal Methods for Open Object-Based Distributed Systems, pages 224–231, 2010

work page 2010
[5]

van Glabbeek

R.J. van Glabbeek. The linear time - branching time spec- trum I. InHandbook of Process Algebra, pages 3–99. Elsevier Science, 2001

work page 2001
[6]

Howie.Fundamentals of Semigroup Theory, page 16

John M. Howie.Fundamentals of Semigroup Theory, page 16. Number 12 in LMS Monograph. Clarendon Press, 1995

work page 1995
[7]

Kimura and S

K. Kimura and S. Takai. Bisimilarity control of nondeter- ministic discrete event systems under event and state obser- vations.IEICE Transactions on Information and Systems, E97.D(5):1140–1148, 2014

work page 2014
[8]

Kimura and S

K. Kimura and S. Takai. Maximally permissive similarity enforcing supervisors for nondeterministic discrete event sys- tems under event and state observations.IEICE Transactions Fundamentals, E79-A(7):1500–1507, 2014

work page 2014
[9]

Kushi and S

N. Kushi and S. Takai. Synthesis of similarity enforcing su- pervisors for nondeterministic discrete event systems.IEEE Transactions on Automatic Control, 63(5):1457–1464, 2018

work page 2018
[10]

K. G. Larsen. Modal specifications. In J. Sifakis, editor,Auto- matic Verification Methods for Finite State Systems, volume 407 of LNCS, pages 232–246. Springer, 1990

work page 1990
[11]

Larsen and B

K.G. Larsen and B. Thomsen. A modal process logic. InThird Annual Symposium on Logic in Computer Science, pages 203– 210, 1988

work page 1988
[12]

Li and S

J. Li and S. Takai. Maximally permissive nonblocking super- visors for similarity control of nondeterministic discrete event systems under event and state observations.IEICE Transac- tions on Fundamentals of Electronics, Communications and Computer Sciences, 102(2):399–403, 2019

work page 2019
[13]

Li and S

J. Li and S. Takai. Synthesis of maximally permissive supervi- sors for similarity control of partially observed nondetermin- istic discrete event systems.Automatica, 135, 2022. 11

work page 2022
[14]

Li and S

J. Li and S. Takai. Maximally permissive supervisors for nonblocking similarity control of nondeterministic discrete- event systems.IEEE Transactions on Automatic Control, 68(6):3529–3544, 2023

work page 2023
[15]

F. Liu, H. Lin, and Z. Dziong. Bisimilarity control of partially observed nondeterministic discrete event systems and a test algorithm.Automatica, 47(4):782–788, 2011

work page 2011
[16]

Milner.A Calculus of Communicating Systems

R. Milner.A Calculus of Communicating Systems. Springer- Verlag, 1980

work page 1980
[17]

P. J. Ramadge and W. M. Wonham. Supervisory control of a class of discrete event processes.SIAM Journal on Control and Optimization, 25(1):206–230, 1987

work page 1987
[18]

Y. Sun, H. Lin, and Ben M. Chen. Bisimilarity enforcing su- pervisory control for deterministic specifications.Automatica, 50(1):287–290, 2014

work page 2014
[19]

S. Takai. Bisimilarity enforcing supervisory control of nonde- terministic discrete event systems with nondeterministic spec- ifications.Automatica, 108:108470, 2019

work page 2019
[20]

S. Takai. Synthesis of maximally permissive supervisors for nondeterministic discrete event systems with nondeterminis- tic specifications.IEEE Transactions on Automatic Control, 66(7):3197–3204, 2021

work page 2021
[21]

A. Tarski. A lattice-theoretical fixpoint theorem and its ap- plications.Pacific Journal of Mathematics, 55(2):285–309, 1955

work page 1955
[22]

Y. Wang, Z. Zhu, Rob J. van Glabbeek, S. Takai, J. Zhang, and L. Tan. More on maximally permissive similarity control of discrete event systems, 2024. Available athttps://arxiv. org/abs/2407.08068

work page arXiv 2024
[23]

Yamada and S

H. Yamada and S. Takai. Nonblocking similarity control of nondeterministic discrete event systems under event and state observations.IEICE Transactions Fundamentals, E101- A(2):328–337, 2018

work page 2018
[24]

Zhou and R

C. Zhou and R. Kumar. Control of nondeterministic discrete event systems for simulation equivalence.IEEE transactions on automation science and engineering, 4(3):340–349, 2007

work page 2007
[25]

C. Zhou, R. Kumar, and S. Jiang. Control of nondeterminis- tic discrete-event systems for bisimulation equivalence.IEEE Transactions on Automatic Control, 51(5):754–765, 2006. Y u W angis currently a Ph.D. student at the College of Computer Science and Technology, Nanjing University of Aeronautics and Astro- nautics. His research includes formal methods a...

work page 2006