Title: Scalable Current-State Estimation of Discrete-Timed Automata

Time：Tuesday, 7 July 2026 10:00-11:00

Venue：Building 5, SKLCS, Institute of Software, CAS

Speaker：Julian Klein. Technical University of Berlin (TUB)

Timed automata are a standard formalism for modeling real-time systems with timing-dependent behavior. In partially observable settings, an external observer sees only visible events and their timing information, giving rise to the current-state estimation problem: given an observation, determine the set of states in which the system may currently be. While exact current-state estimation is undecidable for dense-time timed automata, it becomes tractable for discrete-timed automata, where time is represented by discrete tick events. However, existing constructions scale exponentially with the largest timing constant M of the input system, since they require explicit enumeration of all timesteps up to M. To address this limitation, we have proposed threshold estimators, which store and propagate symbolic threshold timestamps instead of constructing all time-successor states explicitly. Recently, we have identified structural conditions under which threshold estimators scale independently of M. Instead, our construction scales only with the total number of timing constraints. This yields a more scalable framework for current-state estimation in discrete-timed automata with large timing constants and enables our method for real-world applications that satisfy our structural conditions.