Author(s)
Kozura Vitaly
Abstract

In this paper, the model-checking algorithm from [22] is adapted to coloured Petri nets (CPN) [9, 10]. The state-based semantics of LTL for CPN is given and the correctness of the obtained approach is proven. It is also shown how to apply this model checking technique to interval-timed CPN.

File
kozura.pdf166.85 KB
Issue
Computer Science, № 15, 2001
Pages
83-101