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.
Keywords:
DOI:
Issue
Pages:
83-101
File:
kozura.pdf
(166.85 KB)