cs.FLJun 29, 2026

Destination-Labeled Self-Looping Systems with Dwell: Intrinsic Characterization, Realization Cost, and Recognition

Authors: Reda Belaiche

Organizations: Department of Computer Science, University Institute of Technology of Créteil-Vitry, Paris-Est Créteil University, 122 rue Paul Armangot, Vitry-sur-Seine, 94400, France

Abstract

We study a finite-state symbolic controller for systems in which the admissible visible transitions are fixed in advance and each visible state carries a minimum dwell requirement. The resulting model, which we call a destination-labeled self-looping system with dwell (DLSL system), records the visible graph together with local decision maps; dwell memory appears only after phase expansion. The main structural issue is that, once dwell is imposed, the current visible state no longer determines whether a departure is allowed. This leads to the converse problem: which deterministic transducers arise as phase-expanded realizations of DLSL systems over a fixed visible graph? We show that the answer is exactly the class of fiber-linear graph-respecting transducers. Under natural reachability and realizable-departure assumptions, equivalent accessible realizations over the same visible graph are isomorphic; in particular, the visible transduction determines the dwell vector and the local decision maps. We also prove that any graph-preserving deterministic realization enforcing dwell values (di)(d_i) requires exactly idi\sum_i d_i control states. Finally, we give an O(QΩ)O(|Q||Ω|) recognition and reconstruction procedure, and extend the analysis to an edge-entry variant in which transitions may enter interior phases of successor fibers.

Explore similar work

CardsList
  1. SemML 2.0: Synthesizing Controllers for LTL

    Apr 27, 2026Jan Křetínský, Tobias Meggendorfer, Maximilian ProkopLinear Temporal LogicsConstraint-Aware Synthesis

  2. Symbolic Synthesis for LTLf+ Obligations

    Apr 20, 2026Giuseppe De Giacomo, Christian Hagemeier, Daniel Hausmann +1Linear Temporal LogicsConstraint-Aware Synthesis