Symbolic Simulation-Checking of Dense-Time Systems

Details Symbolic Simulation-Checking of Dense-Time Systems Symbolic Simulation-Checking of Dense-Time Systems

2006-10-13

arxiv.org/abs/cs/0610085v1

Computer Science

Logic in Computer Science

16 pages, 1 figure

Scientific paper

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.

Affiliated with

Also associated with

No associations

Rating

Symbolic Simulation-Checking of Dense-Time Systems does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.

If you have personal experience with Symbolic Simulation-Checking of Dense-Time Systems, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Symbolic Simulation-Checking of Dense-Time Systems will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-664605