Affiliations: Automata and System Theory Group, Department of
Computer Science, Humboldt University, Germany | Communication and Operating Systems Group, Institute for Telecommunication Systems, TU Berlin, Germany | Computer Architecture and Communication Group, Department of
Computer Science, Humboldt University, Germany
Abstract: Non-reachability proofs in Timed Petrinets were usually done by
proving the non-reachability within the underlying timeless net. However, in
many cases this approach fails. In this paper, we present an approach to prove
non-reachability within the actual Timed Petrinet. For this purpose, we
introduce a state equation for Timed Petrinets in analogy to timeless nets.
Using this state equation, we can express reachability as a system of equations
and inequations, which is solvable in polynomial time.
Keywords: Timed Petrinet, duration net, state equation, non-reachability
