Symbolic Simulation-Checking of Dense-Time Systems

TL;DR

This paper introduces a symbolic algorithm for simulation-checking of dense-time systems modeled as timed automata, utilizing convex polyhedra and zones to efficiently verify implementation versus specification automata.

Contribution

The work presents a novel symbolic simulation-checking algorithm for timed automata that handles convex polyhedra, zones, and Zeno states, with practical implementation and experimental results.

Findings

Efficient symbolic algorithm for timed automata simulation-checking.

Representation of state spaces with convex polyhedra and zones.

Successful handling of Zeno states in the verification process.

Abstract

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.