2006/10/13 by Farn Wang, Wang, Farn
Computer Science · #D.3.1 #Embedded Systems Design Techniques #F.1.1 #F.4.3 #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Model-Driven Software Engineering Techniques #Software Engineering (cs.SE)
paper · pdf · doi:10.48550/arxiv.cs/0610085
openalex publication_date 2006/10/13 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
Intuitively, an (implementation) automata is simulated by a (specification) automata if every externally observable transition by the implementation automata can also be made by the specification automata. In this work, we present a symbolic algorithm for the simulation-checking of timed automatas. We first present a simulation-checking procedure that operates on state spaces, representable with convex polyhedra, of timed automatas. We then present techniques to represent those intermediate result convex polyhedra with zones and make the procedure an algorithm. We then discuss how to handle Zeno states in the implementation automata. Finally, we have endeavored to realize the algorithm and report the performance of our algorithm in the experiment.