# A State Class Construction for Computing the Intersection of Time Petri Nets Languages

## TL;DR

This paper introduces a novel method for computing the intersection of languages in Time Petri nets using a new product construction and the State Class approach, implemented in the Twina tool.

## Contribution

It presents a new product construction for TPN language intersection that is concise, expressive, and does not increase the model's expressive power.

## Key findings

- The method effectively computes TPN language intersections.
- The approach enables applications like diagnosability analysis and property checking.
- Experimental results demonstrate the tool's practical utility.

## Abstract

We propose a new method for computing the language intersection of two Time Petri nets (TPN); that is the sequence of labels in timed traces common to the execution of two TPN. Our approach is based on a new product construction between nets and relies on the State Class construction, a widely used method for checking the behaviour of TPN. We prove that this new construct does not add additional expressive power, and yet that it can leads to very concise representation of the result. We have implemented our approach in a new tool, called Twina. We report on some experimental results obtained with this tool and show how to apply our approach on two interesting problems: rst, to dene an equivalent of the twin-plant diagnosability methods for TPN; then as a way to check timed properties without interfering with a system.