Symbolic model checking for a discrete clocked tempporal logic with intervals

摘要

In this paper we present a new model checking algorithm for interval based timed structures and temportal logic formulas. Besides the treatment of time intervals the new algorithm leads to a significant performance gain compared to previous approaches. For the symbolic representation we used extended characteristic functions, which are implemented by MTBDDs.