Jie An

Mining DTA with SMT by Exploiting Simple Elementary Language and Timed Augmented Prefix Acceptor

Timed automata, which extend finite state automata by introducing clock variables, serve as a popular formalism for specifying and analyzing the timed behaviors of real-time systems. Extracting the timed behaviors of a black-box, safety-critical system is crucial for designing and analyzing its real-time requirements,...