P.C. Yue, C.K. Wong
Journal of the ACM
The most natural, compositional, way of modeling real-time systems uses a dense domain for time. The satisfiability of timing constraints that are capable of expressing punctuality in this model, however, is known to be undecidable. We introduce a temporal language that can constrain the time difference between events only with finite, yet arbitrary, precision and show the resulting logic to be EXPSPACE-complete. This result allows us to develop an algorithm for the verification of timing properties of real-time systems with a dense semantics.
P.C. Yue, C.K. Wong
Journal of the ACM
Vladimir Yanovski, Israel A. Wagner, et al.
Ann. Math. Artif. Intell.
Ismail Akhalwaya, Shashanka Ubaru, et al.
ICLR 2024
Alain Vaucher, Philippe Schwaller, et al.
AMLD EPFL 2022