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

Audine Subias (LAAS-DISCO); Didier Le Botlan (LAAS-VERTICS); \'Eric Lubat (LAAS-VERTICS); Silvano Dal Zilio (LAAS-VERTICS); Yannick Pencol\'e (LAAS-DISCO)

REVIEW 3 major objections 5 minor 32 references

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

T0 review · 3 major / 5 minor · reviewed 2026-08-14 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read Firing matching transitions together in a Product TPN makes the state class graph compute the exact language intersection of two Time Petri nets.

desk verdict The product construction and tool are genuinely useful, but the core state-class correctness claim is unproven and the firability test as written appears to have reversed subscripts. read the letter →

arxiv 1908.02087 v1 pith:7NUSXR5I submitted 2019-08-06 cs.LO

Yannick Pencolé (LAAS-DISCO) , Éric Lubat (LAAS-VERTICS) , Silvano Dal Zilio (LAAS-VERTICS) , Didier Le Botlan (LAAS-VERTICS) , Audine Subias (LAAS-DISCO) This is my paper · ORCID

classification cs.LO MSC 68Q8568Q60

keywords TimePetrinetslanguageintersectionstateclassgraphsynchronousproductArnold-NivatsynchronizationdiagnosabilityDifferenceBoundMatrixtimedmodelchecking

verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

Two Time Petri nets share a timed trace when they can fire the same labels at the same dates. This paper introduces a product construction, Product TPN, that forces transitions with a common label to fire simultaneously, and proves its semantics is isomorphic to the synchronous product of the component semantics. It then extends the Linear State Class Graph abstraction to such products, so shared timed behavior can be explored symbolically with Difference Bound Matrices. The paper proves the extension adds no expressive power for safe right-closed nets and implements it in a new tool called Twina, with experiments showing the new graph is often much smaller than the previous approach via composable nets.

What carries the argument

The central object is the Product TPN, a superposition of two disjoint nets with projections $\#_1$ and $\#_2$, equipped with an Arnold-Nivat style synchronization rule. The carrying machinery is the extended Linear State Class Graph: state classes are pairs $(m,D)$ where $D$ is a domain of firing-date constraints represented as a Difference Bound Matrix, a system of bounds $\alpha_i\le x_i\le\beta_i$ and differences $x_i-x_j\le\gamma_{i,j}$ normalized so each solution set has a unique matrix. The new step is the synchronized-firing update, which adds $x_i=x_j$ and $x_i\le x_k$ before introducing primed variables and eliminating the unprimed ones; this is what lets one class represent all states reachable by firing two transitions at the same date.

What would settle it

Enumerate the concrete reachable timed states of a small bounded Product TPN with exact rational arithmetic for all firing schedules up to a fixed depth, then compare the resulting language and markings with the state class graph built by the synchronized-firing rule; any label sequence or marking that appears in one but not the other would refute the method.

Watch

Extended reading notes

Core claim

The paper's central claim is that the language intersection of two labelled Time Petri nets can be computed through a product operator, written $N_1\times N_2$, whose timed transition system $\llbracket N_1\times N_2\rrbracket_\times$ is isomorphic to the synchronous product $\llbracket N_1\rrbracket \parallel \llbracket N_2\rrbracket$ of the component systems (Theorem 1). The product adds one new rule: two transitions from different components that carry the same label and are both time-enabled fire simultaneously; labels not shared, and internal labels, fire asynchronously as in the usual semantics. The algorithmic contribution is an extension of the Linear State Class Graph construction to these synchronized firings: from a class $(m,D)$, firing the pair $(t_i,t_j)$ is computed by adding the constraints $x_i=x_j$ and $x_i\le x_k$, introducing new variables for the enabled transitions after the firing, and eliminating all old variables, producing a new Difference Bound Matrix. The paper asserts that this procedure gives a DBM characterization of the reachable states after synchronization. It also proves Theorem 2: every safe, right-closed Product TPN is weakly timed bisimilar to a composable TPN of linear size, so the product construction adds no expressive power within that class.

Load-bearing premise

The load-bearing premise is that the symbolic update for firing two synchronized transitions together exactly characterizes the reachable states after that firing, with no loss and no extra states; the paper uses this update to compute the graph but does not prove a correctness theorem for it.

Editorial extensions

If this is right

For bounded nets, the state class graph of the product is finite and its language is the intersection of the two component languages, so language intersection is computable without first building each component's full state space.
The twin-plant construction becomes a single product graph: checking diagnosability of a fault reduces to checking that every faulty execution in the product eventually reaches a time deadlock, a property the tool checks on the fly.
A timed property can be expressed as an observer net and checked on the product of the system with the observer, without modifying the system under test.
Because Product TPN add no expressive power for safe right-closed nets, optimization techniques developed for ordinary TPN state classes, such as symmetry reduction, should transfer to the product construction.
In the reported experiments, the linear state class graph of the product is smaller than the strong state class graph of the existing encoding, sometimes by two orders of magnitude.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

If the DBM update is exact, the same equality-based elimination should support synchronizing more than two transitions, giving k-ary products and synchronization vectors with no change to the abstraction; the paper notes this possibility but does not implement it.
A formal correctness proof of the synchronized-firing transformation is the missing piece: without it, the computational results rest on an unproven lemma, and a counterexample would not contradict any theorem in the paper.
The method's practical scalability likely depends on how often matching labels force simultaneous firings; benchmarks with many shared labels and high concurrency would test whether the product graph stays compact.
The quotient (residual) of two TPN languages, the dual of intersection, is a natural next target; a symbolic construction of the same kind would open supervisory control and assume-guarantee reasoning for timed nets.

Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Desk Editor's Note

read the letter

Worth your time. The genuinely new bit is the Product TPN construction with an LSCG algorithm for synchronized transition pairs, plus the Twina implementation. The benchmark table is credible: their LSCG-based method saves a lot of classes compared to the IPTPN/strong-SCG route, and the applications to twin-plant diagnosability and observer-based checking are sensible. Theorem 1 is essentially a definition check — the semantics is crafted so the isomorphism holds — but that's fine, the math is not circular where it matters. The expressiveness theorem (Theorem 2) uses an existing construction, is honestly limited to safe right-closed nets, and is only sketched, though the sketch is plausible.

Now the soft spots, and the first one is load-bearing. Section 4 gives a three-step DBM transformation for firing a synchronized pair (ti,tj), but no theorem states that this transformation exactly characterizes the reachable states after that firing. For a plain TPN this is classical, but the synchronized case is new and the correctness is asserted, not proven. The stress-test note found something concrete: the firability test says γ_{t,k} ≥ 0 for all t in {i,j} and k enabled. Given the paper's own convention x_i−x_j ≤ γ_{i,j}, to have a solution with x_i ≤ x_k (ti fires before or at tk) you need the lower bound of x_i−x_k to be ≤ 0, which is equivalent to γ_{k,i} ≥ 0, not γ_{i,k} ≥ 0. As written, the test uses the wrong orientation and would reject fireable pairs, under-approximating the reachable class graph and potentially missing valid traces. It may well be a typo, and the implementation might use the correct indices, but the written algorithm is wrong as stated and there is no proof to catch it.

Minor: the abstract overgeneralizes Theorem 2 by saying PTPN "does not add expressiveness" without the safe-right-closed caveat that appears in the theorem. Also, the reader's "circularity" concern is overstated: the isomorphism is by construction, but the LSCG part and the expressiveness result are not circular.

Bottom line: this deserves a real peer review. The construction is useful, the tool is real, and the problem is well-motivated. But the authors need to add a correctness proof for the synchronized LSCG construction and fix the firability condition. If those are addressed, this is a solid contribution.

Referee Report

3 major / 5 minor

Summary. The paper proposes a synchronous product construction for Time Petri Nets, called Product TPN (PTPN), whose semantics is designed so that the reachable behavior is isomorphic to the product of the component Timed Transition Systems (Theorem 1). The main algorithmic contribution is an extension of the Linear State Class Graph (LSCG) construction to PTPN, with a three-step DBM transformation for firing a synchronized pair of transitions (Section 4). The paper also claims that PTPN do not add expressive power over TPN for safe, right-closed nets (Theorem 2), and it reports on a tool, Twina, including experiments and applications to twin-plant diagnosability and observer-based verification.

Significance. If the construction is correct, the paper offers a direct and potentially much more efficient route to computing the intersection of TPN languages than existing encodings into timed automata or IPTPN, and the reported experiments show substantial reductions in state class counts compared to the strong SCG on IPTPN. The paper also ships a tool and benchmarks, which is valuable. However, the central algorithmic claim in Section 4 is not backed by a correctness proof, and the stated firability condition appears to have reversed subscripts. The expressiveness result in Section 5 is only sketched. These issues are load-bearing for the paper's main claims, although they seem fixable in a revision.

major comments (3)

[Section 4, synchronized firing condition] The firability test stated as 'γ_{t,k} ≥ 0 for all t∈{i,j} and k enabled' uses reversed indices relative to the DBM convention established in the same section, where x_i − x_j ≤ γ_{i,j}. For transition t to be fireable no later than k, one needs a solution with x_t − x_k ≤ 0. The lower bound on x_t − x_k is −γ_{k,t}, so the necessary and sufficient condition with a nonempty DBM is γ_{k,t} ≥ 0, not γ_{t,k} ≥ 0. For example, if the domain contains x_i∈[0,1], x_j∈[0,1], x_k∈[2,3], then γ_{i,k}=−1 and γ_{k,i}=3; the paper's test rejects the fireable pair (t_i,t_k), while the exact check γ_{k,i}≥0 accepts it. Hence the algorithm as written under-approximates the set of reachable classes and can miss valid traces, breaking the claimed language preservation.
[Section 4, correctness of the LSCG extension] No theorem or proof establishes that the three-step DBM transformation for firing a synchronized pair (t_i,t_j) computes the exact set of reachable timed states after that firing, nor that the resulting state class graph preserves the language of the PTPN. The paragraph beginning 'We can draw two useful observations from this result' is not a correctness argument. Since this construction is the central algorithmic contribution and the basis for the intersection computation, a formal correctness statement and proof are required; without it the main claim is unsupported.
[Section 5, Theorem 2] The proof of Theorem 2 is only a sketch. The auxiliary properties (L1) and (L2) are stated without proof, and the cited construction T1 from [27] is relied on without stating its exact hypotheses beyond a reference. As Theorem 2 is one of the paper's two main results, the proof needs to be completed or the statement demoted to a conjecture with supporting evidence.

minor comments (5)

[Abstract] The phrase 'can leads to' should be 'can lead to'.
[Section 2, Definition 2] The second TTS is written as S2 = (S2, s0_1, →2); the initial state should be s0_2, not s0_1.
[Section 6, Table 1] The text says 'ratio of classes saved' but the reported percentages appear to be ratios of SSCG classes to LSCG classes; please clarify the exact formula used.
[Introduction and Abstract] The introduction states that the method 'can be applied even when the TPN are not bounded', while the abstract claims efficiency only for bounded nets; please clarify whether boundedness is needed for termination or only for finiteness of the graph.
[Section 4] The observation that 'forcing the synchronization of transitions is strictly less constraining than using priorities' is presented as an indirect proof, but no formal comparison with priorities is given; either provide the argument or state it as a conjecture.

Circularity Check

1 steps flagged · score 4.0 of 10

The product-semantics isomorphism in Theorem 1 is built into Definition 5, making the 'congruence' claim partly definitional; the Section 4 LSCG extension is unproven, while the expressiveness and experimental parts are not circular.

self definitional [Section 3, Definition 5 (PTPN semantics) and Theorem 1; compare Definition 2 (product of TTS)]
"Definition 2: 's1 --α-->1 s′1 s2 --α-->2 s′2 α̸=ϵ / (s1,s2) --α--> (s′1,s′2)'. Definition 5: 'a =L(t1) =L(t2) ti∈ #iT / #is --a--> #is′∈ [ [#iN ] ] i∈ 1..2 / s --a--> s′'. Theorem 1: 'The TTS [ [N ] ]× is isomorph to the product [ [#1N ] ]‖ [ [#2N ] ]'."

The only new rule in the PTPN semantics is a direct transcription of the product-of-TTS synchronization rule: both components must take the same label simultaneously, and the non-shared-label and time-passing behavior is inherited from the same underlying TPN semantics. Thus the asserted isomorphism in Theorem 1 does not follow from independent semantic definitions; it is installed by construction in Definition 5. The theorem restates the definitional choice rather than supplying independent evidence that the product construction computes the language intersection. This is a mild but genuine self-definitional step, though the state-class construction and expressiveness results are not circular.

full rationale

The only genuinely circular element is Theorem 1. Definition 5's synchronization rule for a shared label is a direct transcription of Definition 2's product-of-TTS rule: both components must take the same label simultaneously, and the non-shared-label and time-passing cases are inherited from the same TPN semantics. Thus [[N]]_× ≅ [[#1N]]‖[[#2N]] holds essentially by construction; the theorem restates the definitional choice rather than providing independent evidence that the product computes the intersection. This is a self-definitional step, but it is not the whole story. The state-class construction of Section 4 is an algorithm asserted without a correctness theorem; the firability test 'γ_{t,k} ≥ 0' also appears to use the wrong DBM entry under the paper's own convention x_i − x_j ≤ γ_{i,j} (the condition for firing t_i before t_k should involve γ_{k,i}). These are correctness gaps, not circularity, so they do not raise the circularity score further. Theorem 2's expressiveness proof relies on the external construction T1 from [27] (Peres, Berthomieu, Vernadat), not on a self-citation, and the experimental comparison against IPTPN/SSCG is externally grounded. Overall the central derivation is only partially circular: the definitional Theorem 1 plus the unproven Section 4 procedure are load-bearing, but the expressiveness and experimental content are independent.

Assumptions & free parameters 0 free parameters · 4 assumptions · 1 invented entities

The paper's derivations rely on standard results in DBM theory and on established state class and composition constructions from the TPN literature. No parameters are fitted to data. The main invented entity is the Product TPN itself.

assumptions (4)

domain assumption The Linear State Class Graph construction for ordinary TPN preserves reachable markings and language (Berthomieu and Menasche [9]).
Used throughout Sections 3 and 4 as the basis for extending the construction to PTPN; standard result in the TPN literature, not proved in this paper.
domain assumption For every safe, right-closed TPN N, construction T1 of [27] produces a bisimilar composable TPN of size linear in N.
Invoked in the proof sketch of Theorem 2 (Section 5); the restriction to safe, right-closed nets and the linear size bound come from that construction, and the paper does not reproduce its proof.
domain assumption The product of two TTS preserves weak timed bisimulation (congruence property, [27]).
Used in property (L2) in the proof of Theorem 2.
standard math Difference Bound Matrices and their normal form represent difference systems exactly.
Relied on in Section 4 to encode firing domains and to justify that the domain after synchronization is a DBM.

invented entities (1)

Product TPN (PTPN)
purpose: A syntactic composition of two TPNs that enables synchronization on shared labels while keeping timing information in the firing domains.
PTPN is defined in this paper as a formal model; it makes no empirical prediction outside the paper. Its usefulness is demonstrated only through the paper's own algorithms and tool experiments, which compare state counts rather than validating against ground truth.

how reviews work

0 comments

Cite this review

Pith. "Pith review of A State Class Construction for Computing the Intersection of Time Petri Nets Languages." pith.science (2026). https://pith.science/paper/7NUSXR5I

@misc{pith2026190802087,
  author       = {Pith},
  title        = {Pith review of: A State Class Construction for Computing the Intersection of Time Petri Nets Languages},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/7NUSXR5I}},
  note         = {Machine review of arXiv:1908.02087}
}

read the original 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.

Figures

Figures reproduced from arXiv: 1908.02087 by the authors.

**Figure 2.** Example of IPTPN p0 t2 a p1 t4 t5 a b t0 b t3 b ]2,∞[ t1 a [PITH_FULL_IMAGE:figures/full_fig_p012_2.png] view at source ↗

**Figure 4.** Product of a TPN Nf (left) and its “twin” No (right) for the fault f. less this emphasizes the need to have methods that can build the intersection on the fly, without computing a symbolic representation for each component first. Diagnosability and the Twin Plant Method. One possible application of Twina—and our initial motivation for this work—is to check fault diagnosability [29] in systems modelled as TPN [5,17]… view at source ↗

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

32 extracted references · 22 canonical work pages

[27]

Discrete Event Dynamic Systems 21(3) (2011)

Peres, F., Berthomieu, B., Vernadat, F.: On the composition of time Petri nets. Discrete Event Dynamic Systems 21(3) (2011). https://doi.org/10.1007/s10626-011-0102-2

doi:10.1007/s10626-011-0102-2 2011
[1]

International Journal of Critical Computer-Based Systems (IJCCBS) 5(1/2) (2014)

Abid, N., Dal Zilio, S., Le Botlan, D.: A formal framework to spec- ify and verify real-time properties on critical systems. International Journal of Critical Computer-Based Systems (IJCCBS) 5(1/2) (2014). https://doi.org/10.1504/IJCCBS.2014.059593

work page arXiv 2014
[2]

Theoretical Computer Science 126(2) (1994)

Alur, R., Dill, D.L.: A theory of timed automata. Theoretical Computer Science 126(2) (1994). https://doi.org/10.1016/0304-3975(94)90010-8

doi:10.1016/0304-3975(94)90010-8 1994
[3]

Arnold, A.: Nivat’s processes and their synchronization. Theor. Comput. Sci. 281(1-2) (2002). https://doi.org/10.1016/S0304-3975(02)00006-3

work page doi:10.1016/s0304-3975(02)00006-3 2002
[4]

Journal of the ACM 49(2) (2002)

Asarin, E., Caspi, P., Maler, O.: Timed regular expressions. Journal of the ACM 49(2) (2002). https://doi.org/10.1145/506147.506151

arXiv 2002
[5]

IEEE Transactions on Automatic Control 62(3) (2017)

Basile, F., Cabasino, M.P., Seatzu, C.: Diagnosability analysis of labeled time Petri net systems. IEEE Transactions on Automatic Control 62(3) (2017). https://doi.org/10.1109/TAC.2016.2588736

work page arXiv 2017
[6]

In: Software Engineering and Formal Methods (SEFM)

Basu, A., Bozga, M., Sifakis, J.: Modeling Heterogeneous Real-Time Components in BIP. In: Software Engineering and Formal Methods (SEFM). IEEE (2006). https://doi.org/10.1109/SEFM.2006.27

work page doi:10.1109/sefm.2006.27 2006
[7]

In: Formal Modeling and Analysis of Timed Systems (FORMATS)

Bérard, B., Cassez, F., Haddad, S., Lime, D., Roux, O.H.: Comparison of the expressiveness of timed automata and time Petri nets. In: Formal Modeling and Analysis of Timed Systems (FORMATS). LNCS, vol. 3829. Springer (2005)

work page 2005

Show all 32 references

[8]

IEEE Trans

Berthomieu, B., Diaz, M.: Modeling and veriﬁcation of time dependent sys- tems using time Petri nets. IEEE Trans. on Software Engineering17(3) (1991). https://doi.org/10.1109/32.75415

1991 doi
[9]

In: Proceedings IFIP (1983)

Berthomieu, B., Menasche, M.: An enumerative approach for analyzing time Petri nets. In: Proceedings IFIP (1983)

1983
[10]

In: Formal Modeling and Anal- ysis of Timed Systems (FORMATS)

Berthomieu, B., Peres, F., Vernadat, F.: Bridging the gap between timed automata and bounded time Petri nets. In: Formal Modeling and Anal- ysis of Timed Systems (FORMATS). LNCS, vol. 4202. Springer (2006). https://doi.org/10.1007/11867340_7

2006 doi
[11]

In: Automated Technology for Veriﬁ- cation and Analysis (ATVA)

Berthomieu, B., Peres, F., Vernadat, F.: Model checking bounded prioritized time Petri nets. In: Automated Technology for Veriﬁ- cation and Analysis (ATVA). LNCS, vol. 4762. Springer (2007). https://doi.org/10.1007/978-3-540-75596-8_37

2007 doi
[12]

International Journal of Production Research 42(14) (2004)

Berthomieu, B., Ribet, P.O., Vernadat, F.: The tool TINA–construction of abstract state spaces for Petri nets and time Petri nets. International Journal of Production Research 42(14) (2004)

2004
[13]

In: TACAS

Berthomieu, B., Vernadat, F.: State class constructions for branching anal- ysis of Time Petri Nets. In: TACAS. LNCS, vol. 2619. Springer (2003). https://doi.org/10.1007/3-540-36577-X_33

2003 doi
[14]

Science of Computer Programming132(2) (2016)

Bourdil, P.A., Berthomieu, B., Dal Zilio, S., Vernadat, F.: Symmetry reduction for time Petri net state classes. Science of Computer Programming132(2) (2016). https://doi.org/10.1016/j.scico.2016.08.008

2016 doi
[15]

https://doi.org/10.1016/j.tcs.2008.03.030 Computing the Language Intersection of TPN 17

Bérard, B., Cassez, F., Haddad, S., Lime, D., Roux, O.H.: When are timed au- tomata weakly timed bisimilar to time Petri nets? Theoretical Computer Science 403(2-3) (2008). https://doi.org/10.1016/j.tcs.2008.03.030 Computing the Language Intersection of TPN 17

2008 doi
[16]

In: Formal Modeling and Analysis of Timed Systems (FORMATS)

Bérard, B., Gastin, P., Petit, A.: Intersection of Regular Signal-Event (Timed) Languages. In: Formal Modeling and Analysis of Timed Systems (FORMATS). LNCS, Springer (2006).https://doi.org/10.1007/11867340_5

2006 doi
[17]

IEEE Trans

Cabasino, M.P., Giua, A., Lafortune, S., Seatzu, C.: A new approach for diag- nosability analysis of petri nets using veriﬁer nets. IEEE Trans. Automat. Contr. 57(12) (2012). https://doi.org/10.1109/TAC.2012.2200372

2012
[18]

In: ICINCO-ICSO (2009)

Cabasino, M.P., Giua, A., Seatzu, C.: Discrete event diagnosis using Petri nets. In: ICINCO-ICSO (2009)

2009
[19]

Journal of Systems and Software 79(10) (2006)

Cassez, F., Roux, O.H.: Structural translation from time Petri nets to timed automata. Journal of Systems and Software 79(10) (2006). https://doi.org/10.1016/j.jss.2005.12.021

2006 doi
[20]

In: IJCAI (2003)

Cimatti, A., Pecheur, C., Cavada, R.: Formal veriﬁcation of diagnosability via symbolic model checking. In: IJCAI (2003)

2003
[21]

https: //projects.laas.fr/twina/ (2019)

Dal Zilio, S.: TWINA: A realtime model-checker for analyzing Twin-TPN. https: //projects.laas.fr/twina/ (2019)

2019
[22]

In: Computer Aided Veriﬁcation (CAV)

Gardey, G., Lime, D., Magnin, M., Roux, O.H.: Romeo: a tool for analyz- ing time petri nets. In: Computer Aided Veriﬁcation (CAV). Springer (2005). https://doi.org/10.1007/11513988_41

2005 doi
[23]

Discrete Event Dynamic Systems 27(1) (2017)

Gougam, H.E., Pencolé, Y., Subias, A.: Diagnosability analysis of patterns on bounded labeled prioritized Petri nets. Discrete Event Dynamic Systems 27(1) (2017). https://doi.org/10.1007/s10626-016-0234-5

2017 doi
[24]

IEEE Transactions on Automatic Control 46(8) (2001)

Jiang, S., Huang, Z., Chandra, V., Kumar, R.: A polynomial algorithm for testing diagnosability of discrete-event systems. IEEE Transactions on Automatic Control 46(8) (2001). https://doi.org/10.1109/9.940942

2001 doi
[25]

Journal of the ACM (JACM) 47(2) (2000)

Kupferman, O., Vardi, M.Y., Wolper, P.: An automata-theoretic approach to branching-time model checking. Journal of the ACM (JACM) 47(2) (2000). https://doi.org/10.1145/333979.333987

2000
[26]

Merlin, P.M.: A study of the recoverability of computing systems. Ph.D. thesis, Department of Information and Computer Science, University of California (1974)

1974
[28]

Proceedings of the IEEE77(1) (1989)

Ramadge, P.J., Wonham, W.M.: The control of discrete event systems. Proceedings of the IEEE77(1) (1989)

1989
[29]

IEEE Transactions on automatic control 40(9) (1995)

Sampath, M., Sengupta, R., Lafortune, S., Sinnamohideen, K., Teneketzis, D.: Diagnosability of discrete-event systems. IEEE Transactions on automatic control 40(9) (1995)

1995
[30]

In: Workshop on Future Trends of Distributed Com- puting Systems

Toussaint, J., Simonot-Lion, F., Thomesse, J.P.: Time constraint veriﬁcation meth- ods based on time Petri nets. In: Workshop on Future Trends of Distributed Com- puting Systems. IEEE (1997).https://doi.org/10.1109/FTDCS.1997.644736

1997
[31]

In: Formal Tech- niques in Real-Time and Fault-Tolerant Systems (FTRTFT) (2002)

Tripakis, S.: Fault diagnosis for timed automata. In: Formal Tech- niques in Real-Time and Fault-Tolerant Systems (FTRTFT) (2002). https://doi.org/10.1007/3-540-45739-9_14

2002 doi
[32]

IEEE Transactions on Automatic Control 60(9) (2015)

Wang, X., Mahulea, C., Silva, M.: Diagnosis of time Petri nets using fault diagnosis graph. IEEE Transactions on Automatic Control 60(9) (2015). https://doi.org/10.1007/978-3-642-15297-9_12

2015 doi

Pith tools

Reviewed August 14, 2026 · model on record in the stance chip above.

[1] [27]

Discrete Event Dynamic Systems 21(3) (2011)

Peres, F., Berthomieu, B., Vernadat, F.: On the composition of time Petri nets. Discrete Event Dynamic Systems 21(3) (2011). https://doi.org/10.1007/s10626-011-0102-2

doi:10.1007/s10626-011-0102-2 2011

[2] [1]

International Journal of Critical Computer-Based Systems (IJCCBS) 5(1/2) (2014)

Abid, N., Dal Zilio, S., Le Botlan, D.: A formal framework to spec- ify and verify real-time properties on critical systems. International Journal of Critical Computer-Based Systems (IJCCBS) 5(1/2) (2014). https://doi.org/10.1504/IJCCBS.2014.059593

work page arXiv 2014

[3] [2]

Theoretical Computer Science 126(2) (1994)

Alur, R., Dill, D.L.: A theory of timed automata. Theoretical Computer Science 126(2) (1994). https://doi.org/10.1016/0304-3975(94)90010-8

doi:10.1016/0304-3975(94)90010-8 1994

[4] [3]

Arnold, A.: Nivat’s processes and their synchronization. Theor. Comput. Sci. 281(1-2) (2002). https://doi.org/10.1016/S0304-3975(02)00006-3

work page doi:10.1016/s0304-3975(02)00006-3 2002

[5] [4]

Journal of the ACM 49(2) (2002)

Asarin, E., Caspi, P., Maler, O.: Timed regular expressions. Journal of the ACM 49(2) (2002). https://doi.org/10.1145/506147.506151

arXiv 2002

[6] [5]

IEEE Transactions on Automatic Control 62(3) (2017)

Basile, F., Cabasino, M.P., Seatzu, C.: Diagnosability analysis of labeled time Petri net systems. IEEE Transactions on Automatic Control 62(3) (2017). https://doi.org/10.1109/TAC.2016.2588736

work page arXiv 2017

[7] [6]

In: Software Engineering and Formal Methods (SEFM)

Basu, A., Bozga, M., Sifakis, J.: Modeling Heterogeneous Real-Time Components in BIP. In: Software Engineering and Formal Methods (SEFM). IEEE (2006). https://doi.org/10.1109/SEFM.2006.27

work page doi:10.1109/sefm.2006.27 2006

[8] [7]

In: Formal Modeling and Analysis of Timed Systems (FORMATS)

Bérard, B., Cassez, F., Haddad, S., Lime, D., Roux, O.H.: Comparison of the expressiveness of timed automata and time Petri nets. In: Formal Modeling and Analysis of Timed Systems (FORMATS). LNCS, vol. 3829. Springer (2005)

work page 2005