We consider the problem of verifying properties in processes with durational actions. The properties are expressed in terms of a discrete-time extension of ACTL. The algorithm for model checking formulae in this logic over finite state timed transition systems is provided. We consider processes that have infinite models due to the increase of the value of the clock and show how to reduce the verification problem over the infinite models to the one over their compact finite representations.
展开▼
