pith. sign in

arxiv: 2606.02007 · v1 · pith:JMTHKUJQnew · submitted 2026-06-01 · 💻 cs.DC

TAPAAL SMC: Statistical Model Checking of Stochastic Timed-Arc Petri Nets

Tanguy Dubois , Kim G. Larsen , Jiri Srba This is my paper

Pith reviewed 2026-06-28 12:42 UTC · model grok-4.3

classification 💻 cs.DC
keywords statistical model checkingtimed-arc Petri netsstochastic semanticsTAPAALmodel verificationtimed systemsPetri netssimulation-based verification
0
0 comments X

The pith

TAPAAL gains the first stochastic semantics for timed-arc Petri nets plus statistical model checking algorithms.

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

The paper defines the first stochastic semantics for Timed-Arc Petri Nets so that token ages, time intervals, inhibitor arcs, place invariants and transport arcs can be combined with random timing and firing choices. It then implements both quantitative and qualitative Statistical Model Checking procedures inside the TAPAAL tool and proves that the chosen semantics is well-behaved. The motivation is that exact verification of these nets is often undecidable or intractable, while real-life systems frequently require stochastic aspects. SMC therefore supplies a practical route to checking properties that would otherwise remain out of reach. Case studies illustrate that the implementation can already handle non-trivial examples.

Core claim

We suggest the first stochastic semantics for TAPNs and design and implement the quantitative and qualitative Statistical Model Checking (SMC) algorithms in the model checker TAPAAL. We argue for the semantic choices we made in the stochastic semantics and prove that the semantics is well-behaving.

What carries the argument

Stochastic semantics for Timed-Arc Petri Nets that assigns probabilities to enabled transitions while preserving token ages and respecting all timing constraints, together with the quantitative and qualitative SMC algorithms that estimate probabilities or decide properties from simulation traces.

If this is right

  • Systems containing both deterministic timing constraints and random delays become amenable to automated verification inside TAPAAL.
  • Both probability estimation and qualitative property checking become available without requiring full state-space exploration.
  • Models that include inhibitor arcs, place invariants and transport arcs can now be analysed under stochastic assumptions.
  • Verification effort shifts from proving undecidable problems to running a sufficient number of simulations.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The same stochastic semantics could be reused as a basis for simulation-based techniques in other timed Petri-net dialects.
  • Hybrid approaches that combine SMC with partial exact analysis on the deterministic parts of a net become worth exploring.
  • If the semantics is adopted more widely, libraries of benchmark TAPN models with stochastic extensions may appear for comparing SMC tools.

Load-bearing premise

The chosen probability rules for firing and aging produce a model whose statistical properties remain faithful enough that SMC results can be trusted for verification.

What would settle it

A concrete system whose exact probability of reaching a bad state can be computed by hand or by another exact method, yet the TAPAAL SMC implementation returns a statistically different estimate.

Figures

Figures reproduced from arXiv: 2606.02007 by Jiri Srba, Kim G. Larsen, Tanguy Dubois.

Figure 1
Figure 1. Figure 1: Stochastic TAPN modelling a produced with two consumers [PITH_FULL_IMAGE:figures/full_fig_p003_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: Stochastic timed semantics for Petri nets [PITH_FULL_IMAGE:figures/full_fig_p004_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: Examples of stochastic timed-arc Petri nets [PITH_FULL_IMAGE:figures/full_fig_p011_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: TAPAAL’s GUI with a running example and its SMC verification output [PITH_FULL_IMAGE:figures/full_fig_p018_4.png] view at source ↗
Figure 5
Figure 5. Figure 5: Colored stochastic Petri net model of fireflies [PITH_FULL_IMAGE:figures/full_fig_p019_5.png] view at source ↗
Figure 6
Figure 6. Figure 6: Cumulative synchronization probability for 4 (left) and 10 (right) fireflies [PITH_FULL_IMAGE:figures/full_fig_p020_6.png] view at source ↗
Figure 7
Figure 7. Figure 7: Random fit (left) and first fit (right) spectrum allocation for 16QAM [PITH_FULL_IMAGE:figures/full_fig_p021_7.png] view at source ↗
Figure 8
Figure 8. Figure 8: Manufacturing process of wooden windows [41] [PITH_FULL_IMAGE:figures/full_fig_p022_8.png] view at source ↗
Figure 9
Figure 9. Figure 9: Average number of orders and unprocessed coated windows over a year [PITH_FULL_IMAGE:figures/full_fig_p023_9.png] view at source ↗
Figure 10
Figure 10. Figure 10: BSDC bit generation and sender behaviour [PITH_FULL_IMAGE:figures/full_fig_p025_10.png] view at source ↗
Figure 11
Figure 11. Figure 11: BSDC receiver behaviour and monitor by remembering that the last received bit is 0. Upon the arrival of the first qubit, the receiver fires the transition received qubit, interprets it as receiving the bit 1, and places a token to done where it waits to the next time slot. It also places a token into the place got first one where it remembers that on the arrival of the next qubit, it should decode in whic… view at source ↗
Figure 12
Figure 12. Figure 12: Decoherence Frequency 1-Error 2-Error 3-Error 4-Error 5-Error Throughput Corrected 5 µs 0.994 0.986 0.970 0.941 0.890 200 kbit/s 64 kbit/s 5.5 µs 0.492 0.356 0.236 0.146 0.082 182 kbit/s 83 kbit/s 6 µs 0.290 0.130 0.031 0.010 0.002 167 kbit/s 101 kbit/s 6.5 µs 0.311 0.138 0.031 0.009 0.002 154 kbit/s 93 kbit/s 7 µs 0.350 0.156 0.036 0.010 0.002 143 kbit/s 86 kbit/s 7.5 µs 0.382 0.176 0.045 0.013 0.003 133… view at source ↗
Figure 13
Figure 13. Figure 13: Error probabilities for sending 50 bits of information for a given number of bit-flips and [PITH_FULL_IMAGE:figures/full_fig_p028_13.png] view at source ↗
Figure 14
Figure 14. Figure 14: Number of transferred bits at 6 µs frequency to 50 minutes on a Mac Studio with Apple M2 Max 12-core CPU. The memory requirements for SMC are negligible (less than 50 MB). The results are displayed in [PITH_FULL_IMAGE:figures/full_fig_p029_14.png] view at source ↗
read the original abstract

Timed-Arc Petri net (TAPN) is a timed extension of the classical Petri net model where tokens have their age and input arcs are associated with time intervals restricting the ages of tokens available for transition firing. Additionally, a TAPN can also contain place invariants constraining the ages of tokens in places, inhibitor arcs preventing a transition from firing and transport arcs that preserve token ages upon firing. This set of features, as much as it allows us to model complex systems, also often makes verification problems computationally hard or even undecidable. Moreover, in order to model real-life examples, additional stochastic aspects are often necessary to capture the desired behaviour. We suggest the first stochastic semantics for TAPNs and design and implement the quantitative and qualitative Statistical Model Checking (SMC) algorithms in the model checker TAPAAL. We argue for the semantic choices we made in the stochastic semantics and prove that the semantics is well-behaving. On a number of case studies we demonstrate the practical applicability of our modelling formalism and its SMC implementation.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

1 major / 2 minor

Summary. The paper introduces the first stochastic semantics for Timed-Arc Petri Nets (TAPNs), which extend classical Petri nets with token ages, time intervals on arcs, place invariants, inhibitor arcs, and transport arcs. It designs and implements quantitative and qualitative Statistical Model Checking (SMC) algorithms within the TAPAAL model checker, argues for the chosen semantic rules, proves that the semantics is well-behaved, and evaluates applicability on several case studies.

Significance. If the well-behavedness proof holds and the SMC implementation is faithful to the semantics, the work provides a practical route to verifying probabilistic timed properties in systems where exact model checking is undecidable due to the combination of timing and stochasticity. The explicit argument for semantic choices and the machine-checked or detailed proof (as claimed) strengthen the foundation for trusting the statistical results.

major comments (1)
  1. [§4] §4 (Semantics and Well-behavedness Proof): The claim that the stochastic semantics is 'well-behaved' (enabling reliable SMC) rests on the proof; the abstract states such a proof is given, but without explicit verification of the key lemmas (e.g., that the induced probability measure is a valid probability space and that the race condition resolution is memoryless), it is difficult to assess whether the proof covers all features including transport arcs and place invariants.
minor comments (2)
  1. [Abstract] The abstract and introduction should explicitly state the precise stochastic model (e.g., exponential vs. general distributions) used for transition firing times, as this choice directly affects the SMC algorithms.
  2. [Case Studies] Case-study section: clarify whether the reported confidence intervals are obtained from the same number of simulation runs across all examples or whether the number was adapted post-hoc.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for the positive assessment and the recommendation for minor revision. We address the single major comment below.

read point-by-point responses

  1. Referee: [§4] §4 (Semantics and Well-behavedness Proof): The claim that the stochastic semantics is 'well-behaved' (enabling reliable SMC) rests on the proof; the abstract states such a proof is given, but without explicit verification of the key lemmas (e.g., that the induced probability measure is a valid probability space and that the race condition resolution is memoryless), it is difficult to assess whether the proof covers all features including transport arcs and place invariants.

    Authors: We appreciate the referee's request for clearer verification of the key properties. Section 4 defines the stochastic semantics for all TAPN features (including transport arcs, which preserve token ages in the firing distributions, and place invariants, which are folded into the enabledness predicate and the resulting probability measure) and then proves well-behavedness. The proof shows that the construction yields a valid probability space on the measurable space of infinite runs and that the continuous-time race among enabled transitions is memoryless. To make the structure and coverage explicit, the revised version will add numbered key lemmas (e.g., the probability-space lemma and the memoryless-race lemma) with self-contained proofs that reference each TAPN feature. revision: yes

Circularity Check

0 steps flagged

No significant circularity

full rationale

The paper defines a new stochastic semantics for TAPNs, argues for the semantic choices made, proves the semantics is well-behaving, and implements SMC algorithms. No equations, parameters, or claims reduce by construction to fitted inputs or prior self-referential results. The central contribution is a definitional extension plus independent proof of properties, with no self-citation chains or ansatzes smuggled in. The derivation is self-contained against external benchmarks.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 1 invented entities

The paper introduces a new stochastic semantics as its core contribution; this is an invented modeling entity whose justification rests on domain assumptions about real-life stochastic behaviour rather than independent evidence.

axioms (1)
  • domain assumption TAPN model with tokens having ages, time intervals on arcs, place invariants, inhibitor arcs, and transport arcs
    The work builds directly on the existing Timed-Arc Petri Net formalism described in the abstract.
invented entities (1)
  • Stochastic semantics for TAPNs no independent evidence
    purpose: To incorporate randomness for modeling real-life systems
    Newly proposed in this work with a proof of well-behaved properties.

pith-pipeline@v0.9.1-grok · 5711 in / 1356 out tokens · 41816 ms · 2026-06-28T12:42:55.953779+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

50 extracted references · 24 canonical work pages

  1. [1]

    Stochastic Methods: A Handbook for the Natural and Social Sciences

    Gardiner C. Stochastic Methods: A Handbook for the Natural and Social Sciences. Springer Series in Synergetics. Springer Berlin Heidelberg, 2010. ISBN 9783642089626

    2010

  2. [2]

    Statistical Model Checking, pp

    Legay A, Lukina A, Traonouez LM, Yang J, Smolka SA, Grosu R. Statistical Model Checking, pp. 478–

  3. [3]

    doi:10.1007/978-3-319-91908-9\ 23

    Springer International Publishing, 2019. doi:10.1007/978-3-319-91908-9\ 23

    work page doi:10.1007/978-3-319-91908-9 2019

  4. [4]

    Stochastic Petri nets: Properties, applications and tools.Microelectronics Reliability, 1991.31(4):669–697

    Florin G, Fraize C, Natkin S. Stochastic Petri nets: Properties, applications and tools.Microelectronics Reliability, 1991.31(4):669–697. doi:10.1016/0026-2714(91)90009-V

    work page doi:10.1016/0026-2714(91)90009-v 1991

  5. [5]

    Stochastic Petri Nets: An Introduction to the Theory

    Bause F, Kritzinger P. Stochastic Petri Nets: An Introduction to the Theory. AMS, 2013. ISBN 978-3- 528-15535-3

    2013

  6. [6]

    Introduction to Generalized Stochastic Petri Nets, pp

    Balbo G. Introduction to Generalized Stochastic Petri Nets, pp. 83–131. Springer, 2007. doi:10.1007/ 978-3-540-72522-0\ 3

    2007

  7. [7]

    Stochastic well-formed colored nets and symmetric modeling applications.IEEE Transactions on Computers, 1993.42(11):1343–1360

    Chiola G, Dutheillet C, Franceschinis G, Haddad S. Stochastic well-formed colored nets and symmetric modeling applications.IEEE Transactions on Computers, 1993.42(11):1343–1360. doi:10.1109/12. 247838

    work page doi:10.1109/12 1993

  8. [8]

    Qualitative and quantitative evaluation of stochastic Time Petri Nets

    Cicirelli F, Nigro C, Nigro L. Qualitative and quantitative evaluation of stochastic Time Petri Nets. In: 2015 Federated Conference on Computer Science and Information Systems (FedCSIS). 2015 pp. 763–772. doi:10.15439/2015F69. URLhttps://ieeexplore.ieee.org/abstract/document/7321519

    work page doi:10.15439/2015f69 2015

  9. [9]

    From timed Petri nets to timed LOTOS.Proceedings of the IFIP WG6.1 Tenth International Symposium on Protocol, 1990

    Bolognesi T, Lucidi F, Trigila S. From timed Petri nets to timed LOTOS.Proceedings of the IFIP WG6.1 Tenth International Symposium on Protocol, 1990. pp. 395–408

    1990

  10. [10]

    Analysis of place/transition nets with timed arcs and its application to batch process control

    Hanisch HM. Analysis of place/transition nets with timed arcs and its application to batch process control. In: Application and Theory of Petri Nets 1993. Springer, 1993 pp. 282–299

    1993

  11. [11]

    Verification of Timed-Arc Petri Nets

    Jacobsen L, Jacobsen M, Møller MH, Srba J. Verification of Timed-Arc Petri Nets. In: ˇCern´a I, Gyim´othy T, Hromkoviˇc J, Jefferey K, Kr ´alovi´c R, Vukoli´c M, Wolf S (eds.), SOFSEM 2011: Theory and Practice of Computer Science. Springer, Berlin, Heidelberg. ISBN 978-3-642-18381-2, 2011 pp. 46–72. doi: 10.1007/978-3-642-18381-2\ 4

    work page doi:10.1007/978-3-642-18381-2 2011

  12. [12]

    On the Compared Expressiveness of Arc, Place and Transition Time Petri Nets

    Boyer M, Roux OH. On the Compared Expressiveness of Arc, Place and Transition Time Petri Nets. Fundam. Inf., 2008.88(3):225–249

    2008

  13. [13]

    Comparing the Expressiveness of Timed Automata and Timed Extensions of Petri Nets

    Srba J. Comparing the Expressiveness of Timed Automata and Timed Extensions of Petri Nets. In: Proceedings of the 6th International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS’08), volume 5215 ofLNCS. Springer-Verlag, 2008 pp. 15–32

    2008

  14. [14]

    TAPAAL 2.0: Integrated Development Environment for Timed-Arc Petri Nets

    David A, Jacobsen L, Jacobsen M, Jørgensen K, Møller M, Srba J. TAPAAL 2.0: Integrated Development Environment for Timed-Arc Petri Nets. In: Proceedings of the 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’12), volume 7214 ofLNCS. Springer- Verlag, 2012 pp. 492–497

    2012

  15. [15]

    Principles of model checking

    Baier C, Katoen J. Principles of model checking. MIT Press, 2008. ISBN 978-0-262-02649-9

    2008

  16. [17]

    Importance Splitting for Statistical Model Checking Rare Prop- erties

    Jegourel C, Legay A, Sedwards S. Importance Splitting for Statistical Model Checking Rare Prop- erties. 2013 p. 576. doi:10.1007/978-3-642-39799-8\ 38. URLhttps://inria.hal.science/ hal-01087826

    work page doi:10.1007/978-3-642-39799-8 2013

  17. [18]

    Command-based importance sampling for statistical model checking

    Jegourel C, Legay A, Sedwards S. Command-based importance sampling for statistical model checking. Theoretical Computer Science, 2016.649:1–24. doi:10.1016/j.tcs.2016.08.009. URLhttps://www. sciencedirect.com/science/article/pii/S0304397516303966

    work page doi:10.1016/j.tcs.2016.08.009 2016

  18. [19]

    Probabilistic and Topological Semantics for Timed Automata

    Baier C, Bertrand N, Bouyer P, Brihaye T, Gr ¨oßer M. Probabilistic and Topological Semantics for Timed Automata. In: Arvind V , Prasad S (eds.), FSTTCS 2007: Foundations of Software Technology and Theo- retical Computer Science. Springer, Berlin, Heidelberg, 2007 pp. 179–191

    2007

  19. [20]

    Statistical Model Checking for Networks of Priced Timed Automata

    David A, Larsen KG, Legay A, Mikucionis M, Poulsen DB, van Vliet J, Wang Z. Statistical Model Checking for Networks of Priced Timed Automata. In: Fahrenberg U, Tripakis S (eds.), Formal Modeling and Analysis of Timed Systems - 9th International Conference, FORMATS 2011, Aalborg, Denmark, September 21-23, 2011. Proceedings, Lecture Notes in Computer Scienc...

    work page doi:10.1007/978-3-642-24310-3 2011

  20. [21]

    Time for Statistical Model Checking of Real- Time Systems

    David A, Larsen KG, Legay A, Mikucionis M, Wang Z. Time for Statistical Model Checking of Real- Time Systems. In: Gopalakrishnan G, Qadeer S (eds.), Computer Aided Verification - 23rd International Conference, CA V 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings, Lecture Notes in Computer Science. Springer, 2011 pp. 349–355. doi:10.1007/978-3-642-2...

    work page doi:10.1007/978-3-642-22110-1 2011

  21. [22]

    The ORIS Tool: Quantitative Evaluation of Non-Markovian Systems.IEEE Transactions on Software Engineering, 2021.47(6):1211–1225

    Paolieri M, Biagi M, Carnevali L, Vicario E. The ORIS Tool: Quantitative Evaluation of Non-Markovian Systems.IEEE Transactions on Software Engineering, 2021.47(6):1211–1225. doi:10.1109/TSE.2019. 2917202. Conference Name: IEEE Transactions on Software Engineering, URLhttps://ieeexplore. ieee.org/document/8719961

    work page doi:10.1109/tse.2019 2021

  22. [23]

    On Petri nets with deterministic and exponentially distributed firing times

    Marsan MA, Chiola G. On Petri nets with deterministic and exponentially distributed firing times. In: Rozenberg G (ed.), Advances in Petri Nets 1987. Springer, Berlin, Heidelberg. ISBN 978-3-540-47743-3, 1987 pp. 132–145. doi:10.1007/3-540-18086-9\ 23

    work page doi:10.1007/3-540-18086-9 1987

  23. [24]

    TimeNET 4.0: A Software Tool for the Performability Evaluation with Stochastic and Colored Petri Nets

    Zimmermann A, Knoke M. TimeNET 4.0: A Software Tool for the Performability Evaluation with Stochastic and Colored Petri Nets. In: User manual. 2007

    2007

  24. [25]

    Statistical Model Checking for Hybrid Petri Nets with Multiple General Transitions

    Pilch C, Remke A. Statistical Model Checking for Hybrid Petri Nets with Multiple General Transitions. In: 2017 47th Annual IEEE/IFIP International Conference on Dependable Systems and Networks (DSN). 2017 pp. 475–486. doi:10.1109/DSN.2017.41. ISSN: 2158-3927, URLhttps://ieeexplore.ieee. org/abstract/document/8023146

    work page doi:10.1109/dsn.2017.41 2017

  25. [26]

    HYPEG: Statistical Model Checking for hybrid Petri nets: Tool Paper

    Pilch C, Edenfeld F, Remke A. HYPEG: Statistical Model Checking for hybrid Petri nets: Tool Paper. In: Proceedings of the 11th EAI International Conference on Performance Evaluation Methodologies and Tools, V ALUETOOLS 2017. Association for Computing Machinery, New York, NY , USA. ISBN 978- 1-4503-6346-4, 2017 pp. 186–191. doi:10.1145/3150928.3150956. URL...

    work page doi:10.1145/3150928.3150956 2017

  26. [27]

    Comparison of the Expressiveness of Arc, Place and Transition Time Petri Nets

    Boyer M, Roux OH. Comparison of the Expressiveness of Arc, Place and Transition Time Petri Nets. In: Kleijn J, Yakovlev A (eds.), Petri Nets and Other Models of Concurrency – ICATPN 2007. Springer, Berlin, Heidelberg. ISBN 978-3-540-73094-1, 2007 pp. 63–82. doi:10.1007/978-3-540-73094-1\ 7

    work page doi:10.1007/978-3-540-73094-1 2007

  27. [28]

    Comparison of Different Semantics for Time Petri Nets

    B ´erard B, Cassez F, Haddad S, Lime D, Roux OH. Comparison of Different Semantics for Time Petri Nets. In: Peled DA, Tsay YK (eds.), Automated Technology for Verification and Analysis. Springer Berlin Heidelberg, Berlin, Heidelberg. ISBN 978-3-540-31969-6, 2005 pp. 293–307. Dubois, Larsen and Srba/TAPAAL SMC: Statistical Model Checking of Stochastic Time...

    2005

  28. [29]

    Stochastic Semantics and Statistical Model Checking for Networks of Priced Timed Automata, 2014

    David A, Larsen KG, Legay A, Miku ˇcionis M, Poulsen DB, van Vliet J, Wang Z. Stochastic Semantics and Statistical Model Checking for Networks of Priced Timed Automata, 2014. doi:10.48550/arXiv.1106

    work page doi:10.48550/arxiv.1106 2014

  29. [30]

    ArXiv:1106.3961 [cs] version: 2, URLhttp://arxiv.org/abs/1106.3961

    Pith/arXiv arXiv

  30. [31]

    Sequential Analysis

    Wald A. Sequential Analysis. John Wiley, 1947

    1947

  31. [32]

    Probability and Measure Theory

    Ash RB, Doleans-Dade CA. Probability and Measure Theory. Academic Press, 2000

    2000

  32. [33]

    Memory Efficient Data Structures for Explicit Verification of Timed Systems

    Jensen P, Larsen K, Srba J, Sørensen M, Taankvist J. Memory Efficient Data Structures for Explicit Verification of Timed Systems. In: Proceedings of the 6th NASA Formal Methods Symposium (NFM’14), volume 8430 ofLNCS. Springer-Verlag, 2014 pp. 307–312. doi:10.1007/978-3-319-06200-6\ 26

    work page doi:10.1007/978-3-319-06200-6 2014

  33. [34]

    Photinus carolinus — Wikipedia, The Free Encyclopedia.http://en.wikipedia.org/ w/index.php?title=Photinus%20carolinus&oldid=1237034011, 2025

    Wikipedia. Photinus carolinus — Wikipedia, The Free Encyclopedia.http://en.wikipedia.org/ w/index.php?title=Photinus%20carolinus&oldid=1237034011, 2025. [Online; accessed 09- January-2025]

    2025

  34. [35]

    Modeling Fireflies Synchronization, pp

    Ram ´ırez-´Avila GM, Kurths J, Depick `ere S, Deneubourg JL. Modeling Fireflies Synchronization, pp. 131–156. Springer, 2019. doi:10.1007/978-3-319-78512-7\ 8

    work page doi:10.1007/978-3-319-78512-7 2019

  35. [36]

    A model for the collective synchronization of flashing in Photinus carolinus

    McCrea Madeline EB, E RJ. A model for the collective synchronization of flashing in Photinus carolinus. J. of Royal Soc. Interface, 2022. (19)

    2022

  36. [37]

    Latte: Improving the Latency of Transiently Consistent Network Update Schedules

    Christesen N, Glavind M, Schmid S, Srba J. Latte: Improving the Latency of Transiently Consistent Network Update Schedules. In: Proceedings of 38th International Symposium on Computer Performance, Modeling, Measurements and Evaluation (PERFORMANCE’20), volume 48, no. 3 ofACM SIGMETRICS Performance Evaluation Review. ACM, 2020 pp. 14–26. doi:10.1145/345395...

    work page doi:10.1145/3453953.3453957 2020

  37. [38]

    Methods for Efficient Unfolding of Colored Petri Nets.Fundamenta Informaticae, 2023.189(3–4):297–320

    Bilgram A, Jensen P, Pedersen T, Srba J, Taankvist P. Methods for Efficient Unfolding of Colored Petri Nets.Fundamenta Informaticae, 2023.189(3–4):297–320

    2023

  38. [39]

    All-optical networks.Commun

    Chatterjee S, Pawlowski S. All-optical networks.Commun. ACM, 1999.42(6):74–83. doi:10.1145/ 303849.303865

    arXiv 1999

  39. [40]

    Combining heuristic and exact approaches for solving the routing and spectrum assignment problem.IET Optoelectronics, 2018.12(2):65–72

    Hai DT, Morvan M, Gravey P. Combining heuristic and exact approaches for solving the routing and spectrum assignment problem.IET Optoelectronics, 2018.12(2):65–72. doi:https://doi.org/10.1049/ iet-opt.2017.0013

    arXiv 2018

  40. [41]

    Proactive Modulation Format Allocation Method with Selective Downgrading to Enhance Inter-core Crosstalk Tolerance in SDM-EONs

    Kawaguchi K, Seki Y , Tanigawa Y , Hirota Y , Tode H. Proactive Modulation Format Allocation Method with Selective Downgrading to Enhance Inter-core Crosstalk Tolerance in SDM-EONs. In: 2024 15th International Conference on Network of the Future (NoF). 2024 pp. 159–163. doi:10.1109/NoF62948. 2024.10741410

    work page doi:10.1109/nof62948 2024

  41. [42]

    Performance evaluation of spectrum allocation policies for elastic optical networks

    Chatterjee BC, Oki E. Performance evaluation of spectrum allocation policies for elastic optical networks. In: 2015 17th International Conference on Transparent Optical Networks (ICTON). 2015 pp. 1–4. doi: 10.1109/ICTON.2015.7193485

    work page doi:10.1109/icton.2015.7193485 2015

  42. [43]

    Usability of Deterministic and Stochastic Petri Nets in the Wood Industry: A Case Study

    Horv ´ath ´A. Usability of Deterministic and Stochastic Petri Nets in the Wood Industry: A Case Study. In: Advanced Computational Methods for Knowledge Engineering. Springer, Cham. ISBN 978-3-319- 06569-4, 2014 pp. 119–127

    2014

  43. [44]

    Communication via one- and two-particle operators on Einstein-Podolsky-Rosen states.Physical Review Letters, 1992.69(20):2881–2884

    Bennett CH, Wiesner SJ. Communication via one- and two-particle operators on Einstein-Podolsky-Rosen states.Physical Review Letters, 1992.69(20):2881–2884. doi:10.1103/PhysRevLett.69.2881. URL https://doi.org/10.1103/PhysRevLett.69.2881

    work page doi:10.1103/physrevlett.69.2881 1992

  44. [45]

    Nielsen and Isaac L

    Nielsen MA, Chuang IL. Quantum Computation and Quantum Information. Cambridge University Press, 10th anniversary edition edition, 2010. ISBN 978-1-107-00217-3. doi:10.1017/CBO9780511976667. 34Dubois, Larsen and Srba/TAPAAL SMC: Statistical Model Checking of Stochastic Timed-Arc Petri Nets

    work page doi:10.1017/cbo9780511976667 2010

  45. [46]

    Quantum Two-Way Protocol Beyond Su- perdense Coding: Joint Transfer of Data and Entanglement.IEEE Transactions on Quantum Engineering,

    Jensen KS, Valentini L, Christensen RB, Chiani M, Popovski P. Quantum Two-Way Protocol Beyond Su- perdense Coding: Joint Transfer of Data and Entanglement.IEEE Transactions on Quantum Engineering,

  46. [47]

    doi:10.1109/TQE.2025.3528238

    work page doi:10.1109/tqe.2025.3528238 2025

  47. [48]

    URLhttps://quantum.cloud.ibm.com/computers?system= ibm_miami

    IBM Miami calibration data, 2026. URLhttps://quantum.cloud.ibm.com/computers?system= ibm_miami

    2026

  48. [49]

    The Theory of Quantum Information

    Watrous J. The Theory of Quantum Information. Cambridge University Press, 2018. doi:10.1017/ 9781316848142

    2018

  49. [50]

    Efficient error models for fault-tolerant architectures and the Pauli twirling ap- proximation.Physical Review A, 2013.88(1):012314

    Geller MR, Zhou Z. Efficient error models for fault-tolerant architectures and the Pauli twirling ap- proximation.Physical Review A, 2013.88(1):012314. doi:10.1103/PhysRevA.88.012314. URL https://doi.org/10.1103/PhysRevA.88.012314

    work page doi:10.1103/physreva.88.012314 2013

  50. [51]

    The Theory of Error-Correcting Codes

    MacWilliams FJ, Sloane NJA. The Theory of Error-Correcting Codes. North-Holland, 1977. ISBN 978-0-444-85193-2

    1977