Pith. sign in

REVIEW 3 major objections 5 minor 1 cited by

Formal Verification of Digital Twins with TLA and Information Leakage Control

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

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

Pith's one-line read A digital twin can be specified as a TLA state machine derived from its probabilistic graphical model, and a weakened non-interference property yields statistical leakage guarantees.

desk verdict Competent TLA+ model checking that finds a real orchestration bug, but the headline 'formal guarantee' is undermined by an unproven abstraction gap. read the letter →

arxiv 2411.18798 v1 pith:MBDNEX3M submitted 2024-11-27 cs.CR cs.DCcs.ITcs.SYeess.SYmath.IT

Luwen Huang , Lav R. Varshney , Karen E. Willcox This is my paper · ORCID
classification cs.CRcs.DCcs.ITcs.SYeess.SYmath.IT MSC 68Q6068Q85
keywords digitaltwinsformalverificationTLAmodelcheckingprobabilisticgraphicalnon-interferenceinformationleakagesystemidentification
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

This paper tries to establish that a digital twin can be given a formal correctness guarantee by turning its probabilistic graphical model into a finite state machine written in the Temporal Logic of Actions (TLA). On this representation, orchestration-level properties such as 'the physical and digital twins must eventually synchronize' can be checked by model checking, so failures show up as concrete execution traces. The paper also argues that strict non-interference is impractical for digital twins and offers a weakening in which an adversary is allowed to learn some information, but the accuracy of any attempt to reconstruct the hidden system model is formally bounded. The route is demonstrated on a UAV digital twin, where model checking exposed a stale-command bug that had slipped into an early specification. If the central claim is right, formal verification can catch system-level orchestration errors in safety-critical digital twins rather than only component-level faults.

What carries the argument

The load-bearing object is the derived finite state machine $\text{Digital Twin} := I \land N \land F$, built from the digital twin's probabilistic graphical model: each variable $v_i$ becomes a process whose transition is driven by its PGM parents, and the next-state predicate is the disjunction $N := \omega_1 \lor \dots \lor \omega_N \lor T$. The second mechanism is the channel augmentation of Algorithm 1, which represents each distributed edge as a network variable plus a received-value variable, with the channel abstracted as a queue and the fairness assumption $\mathrm{SF}(i=1)$ guaranteeing eventual delivery of the newest message. The third mechanism is the statistical weakening of non-interference: instead of banning all information flow, Theorem 1 bounds the accuracy of a system-identification estimator, so the leakage guarantee is stated as how well the adversary can reconstruct the system's health model rather than how many bits are revealed.

What would settle it

Run the same verified specification against a higher-fidelity simulation or the physical testbed in a regime the abstraction rules out—sensor noise outside $\{-1,0,1\}$, a channel that withholds the newest message for many consecutive steps, or damage increments of $\delta=2$—and check whether a property verified in TLA (for example the eventual-synchronization property P1) fails in the richer setting. One such divergence would show that the abstract state machine does not preserve the behaviors the guarantee depends on.

Watch

Extended reading notes

Core claim

The central discovery is that a digital twin can be written as the TLA state machine $\text{Digital Twin} := I \land N \land F$, where $I$ is the initial-state predicate, $N$ is the disjunction of process actions $\omega := W(v_i) \to v_i$ derived from the PGM's parent–child dependencies, and $F$ collects fairness conditions. Distributed communication is folded in by augmenting the PGM: for each communicated variable $X$ the model adds a received-value variable $X_{\mathrm{in}}$ and a network variable $N_X$, abstracting the channel as a queue with deterministic writes and nondeterministic reads under the strong-fairness condition that the newest message is eventually delivered. The paper's second claim is that generalized non-interference can be weakened through system identification: when health decreases by a Poisson amount with rate $\lambda_{a(t)}$ under the executed action, an adversary who sees health and action histories can estimate each $\lambda_i$ with zero bias and with $\Pr(|\hat\lambda_i - \lambda_i| \ge \epsilon) \le \lambda_i/(N_i \epsilon^2)$, a finite-sample bound on leakage of the health model. This weakening is what lets property P11 about model confidentiality pass where strict generalized non-interference would fail.

Load-bearing premise

The load-bearing premise is that the hand-built finite abstraction—structural health as 0–100 with unit damage, sensor noise restricted to $\{-1,0,1\}$, digital-state fluctuation bounds, and a threshold control policy—preserves precisely those behaviors on which synchronization and leakage properties depend; no refinement or simulation evidence shows the transfer from model to physical system.

Editorial extensions

If this is right

  • If the derivation is sound, any digital twin expressible as a PGM can be carried through the same TLA route, so orchestration-level verification is not specific to the UAV example.
  • A designed property, P8, fails under model checking, and the failing trace points to a missing timestamp check in the command-receive process; this shows the method surfaces concrete implementation-level bugs that component-correctness checks miss.
  • The weakened leakage bound turns property P11 into a checkable statement: an adversary's finite-sample ability to reconstruct the health model is bounded, so controlled leakage is compatible with formal verification.
  • The reported state-space growth makes scalability explicit: the baseline check takes about 15 hours, and the three-sensor variant generates roughly 42 million total states and requires about two days to check.
  • The same specification, after adding the timestamp guard, is re-checked successfully, demonstrating an iterative loop in which model checking finds a violation, the design is fixed, and the property is restored.

Reading between the lines

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

  • A natural next step the paper leaves implicit is refinement: proving a refinement map from this abstract state machine to executable code would turn the model-checking result into a guarantee about the actual implementation.
  • The leakage analysis assumes the adversary observes exact health and action traces; extending it to noisy or partial observations would require a sequential estimator, but the same system-identification framing should carry through.
  • The 'eventually synchronized' property rests on the strong-fairness assumption that the newest message is eventually delivered; a discriminating stress test would run the twin under a channel that can drop the newest message indefinitely and ask whether P1 still holds.
  • The atomicity observation—splitting the damage-and-control step shrank the state space from about 12 million to 1 million states—suggests that abstraction choices can affect scalability in non-obvious ways, so automated abstraction refinement could make such choices systematic.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

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

Referee Report

3 major / 5 minor

Summary. The paper proposes a methodology for formally verifying digital twins using the Temporal Logic of Actions (TLA). A digital twin is represented as a finite state machine (FSM) derived from its probabilistic graphical model (PGM), with an augmentation for distributed communication channels. The authors apply this to a UAV digital twin, model-checking synchronization properties (e.g., eventual synchronization of physical and digital states) and a weakened non-interference property with statistical leakage bounds. Model checking reportedly found a timestamp-validation bug in the specification, which was then fixed. The paper also introduces a weakening of generalized non-interference, supported by a Chebyshev-based statistical guarantee on parameter estimation from leaked health/action data.

Significance. If the abstraction gap were closed, this could be a valuable contribution: it connects PGM-based digital twin descriptions to TLA model checking, makes orchestration-level properties explicit, and proposes a practical way to relax non-interference using system-identification bounds. Concrete strengths include the publicly available TLA specification, the use of a real model checker that found a genuine specification bug, and a correct (though elementary) probabilistic bound in Theorem 1. The case study is transparent about state-space sizes and model-checking resources. However, the central claim that the paper provides a formal guarantee for the digital twin is currently only established for the abstracted FSM, not for the concrete system it is meant to represent.

major comments (3)
  1. [§IV-C, Tables I–VII] The central claim of a formal guarantee for the digital twin is not established because no refinement or simulation relation is given between the hand-abstracted FSM and the concrete PGM/ROS2 system. The abstraction replaces the probabilistic damage process with a deterministic δ=1 step (Table I), truncates the digital state fluctuation to two standard deviations via ζ2 and ζ3 (Table V), and simplifies control to a threshold Dmin (Table VI). A property verified on the FSM does not automatically transfer to the real system unless the FSM is shown to be a sound over-approximation (or exact abstraction) of the concrete semantics. In particular, truncating D to ζ bounds is an under-approximation for tail events, so a liveness property that holds in the FSM may fail for a concrete process whose digital state moves outside those bounds. The paper should either prove a simulation relation between the PGM semantics and the FSM, or explicitly state that the verified guarantees are conditional on the abstraction being adequate.
  2. [§IV-E, Theorem 1] The statistical leakage guarantee is derived from a Poisson damage model with direct observation of health h(t) and action a(t), but the model-checked FSM uses nondeterministic damage and abstract variables. No theorem or formal argument connects Theorem 1 to property P11 in the property-part diagram (Fig. 8). As written, the claim that the weakening "allows us to satisfy property P11" conflates two different models: the Poisson model used in Theorem 1 and the discrete FSM verified by TLC. To make this load-bearing step sound, the paper must either show that the Poisson model is the actual system model underlying the FSM, or prove that the abstraction preserves the information-leakage bound.
  3. [Table IV and Appendix A, Eq. (15)] Strong fairness SF(i=1) guarantees that the most recent message is eventually delivered; this is an assumption about the communication channel, not a verified property. The paper itself notes in §IV-A that the communication channel is potentially unreliable, so the model-checked properties P5 and P7, which rely on eventual delivery, are only meaningful under a fairness assumption that the real channel may not satisfy. The paper should either model message loss explicitly (as a possible action or fairness assumption) or provide a concrete protocol-level justification for why SF(i=1) holds in the target deployment.
minor comments (5)
  1. [Abstract] The phrase "an implementation abstraction that defines the properties required for correct system behavior" is unclear; it should be rephrased to distinguish the specification, the abstraction, and the properties.
  2. [§III-B] There is a typo: "distributed comopnents" should be "distributed components".
  3. [§V-B] The sentence "where seemingly fixes fixes can become obscured" contains a repeated word; it should be corrected.
  4. [§IV-E, Eq. (13)] The estimator definition uses Δh(t+1) without defining it; consider writing h(t)-h(t+1) explicitly for clarity.
  5. [Fig. 8 and §IV-D] The property-part diagram is described as partial, and P11 is referenced in the security discussion but not fully defined in the text; a brief statement of each property's formalization would help the reader connect the diagram to the verification results.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the TLA model is checked against independently specified properties and the leakage bound follows from an explicit statistical model, not from the verification outcome.

full rationale

The paper's central chain is PGM -> FSM (Eq. 3) -> abstraction (Tables I-VII) -> TLA specification -> TLC model checking. The FSM derivation is a definitional translation of PGM parent sets into transition processes; it does not define the verified properties, and the model checker found a genuine violation (the P8 timestamp bug, Sec. V-B), so the properties are not constructed to make verification pass. The statistical guarantee in Theorem 1 is derived from the explicitly stated Poisson damage assumption and the sample-mean estimator in Eq. (13), using standard variance/Chebyshev bounds; it is not fitted to model-checking data nor does it presuppose P11. The main weakness is the absence of a refinement or simulation proof linking the abstracted FSM to the concrete PGM/ROS2 implementation; that is a soundness gap and correctness risk, not a circular reduction. Self-citations to [2] and [39] supply the PGM framework and hardware testbed, but these are independent published sources and are not invoked as an unverified uniqueness or ansatz-justifying chain. No step was found where an equation reduces to another by construction or where a fitted parameter is renamed as a prediction.

Assumptions & free parameters 5 free parameters · 6 assumptions · 0 invented entities

Everything downstream rests on the truth of the abstraction axioms: the TLA verification is only as strong as the mapping from PGM and physical channels to the state machine. The ledger shows no invented physical entities, but several hand-fitted abstraction constants and modeling choices that are not independently justified.

free parameters (5)
  • damage decrement δ = 1
    Table I (5) sets structural health loss to exactly 1 per control execution, a hand-chosen abstraction of the probabilistic damage in (4).
  • sensor noise set ϵ = {-1, 0, 1}
    Table II (7): nondeterministic noise range chosen from the empirical sample in (6), not derived from the sensor error distribution.
  • digital state fluctuation bounds ζ2, ζ3 = ζ2 in [-1,1], ζ3 in [-5,5]
    Table V (11): two-standard-deviation bounds set from prior statistical analysis of the black-box model ψ; these are fitted constants.
  • control threshold Dmin = not specified
    Table VI (12): U is set to 3 when d >= Dmin, but Dmin's value is never given; it is inherited from prior analysis of optimization outputs.
  • baseline model parameters = M=2, η=2, Cmax=3, Tmax=4
    Section V baseline parameters chosen for tractability; state space size and verification results depend on them.
assumptions (6)
  • domain assumption The digital twin is faithfully modeled by the PGM of [2] and its finite state machine translation.
    Section III-A builds Eqs. (1)-(3) on the PGM framework without proving that the abstraction preserves all properties of the physical system.
  • domain assumption Interleaving semantics with one process at a time is an adequate model of concurrency for digital twin orchestration.
    Section III-A defines N as a disjunction over processes and abstracts timing details.
  • domain assumption Each message channel can be represented as a queue with nondeterministic read bound η and strong fairness SF(i=1) guaranteeing eventual delivery of the newest message.
    Section IV-C, Tables IV and VII, and Appendix A (15): correctness of the synchronization verification depends on this channel model.
  • ad hoc to paper Creating atomic processes for data generation plus transmission and control computation plus transmission preserves system behavior.
    Section IV-C ObserveEmitObsAtomic in (9) and the analogous control atomicity in Table VII; the paper notes this is a tractability choice.
  • ad hoc to paper Health decrement follows independent Poisson increments with rate λ_a(t) for the leakage bound.
    Section IV-E: Theorem 1 assumes h(t)-h(t+1) ~ Poisson(λ_a(t)) with independent increments; this model is not the same as the TLA abstraction's nondeterministic damage in (5).
  • ad hoc to paper The abstraction parameters (S range 0-100, D range 1-100, damage δ=1, noise ϵ) are adequate to detect orchestration misalignments.
    Section IV-C tables: these choices constrain the state space and the properties verified; no refinement proof is given.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Formal Verification of Digital Twins with TLA and Information Leakage Control." pith.science (2026). https://pith.science/paper/MBDNEX3M

@misc{pith2026241118798,
  author       = {Pith},
  title        = {Pith review of: Formal Verification of Digital Twins with TLA and Information Leakage Control},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/MBDNEX3M}},
  note         = {Machine review of arXiv:2411.18798}
}
read the original abstract

Verifying the correctness of a digital twin provides a formal guarantee that the digital twin operates as intended. Digital twin verification is challenging due to the presence of uncertainties in the virtual representation, the physical environment, and the bidirectional flow of information between physical and virtual. A further challenge is that a digital twin of a complex system is composed of distributed components. This paper presents a methodology to specify and verify digital twin behavior, translating uncertain processes into a formally verifiable finite state machine. We use the Temporal Logic of Actions (TLA) to create a specification, an implementation abstraction that defines the properties required for correct system behavior. Our approach includes a novel weakening of formal security properties, allowing controlled information leakage while preserving theoretical guarantees. We demonstrate this approach on a digital twin of an unmanned aerial vehicle, verifying synchronization of physical-to-virtual and virtual-to-digital data flows to detect unintended misalignments.

Figures

Figures reproduced from arXiv: 2411.18798 by the authors.

Figure 1
Figure 1. Digital twin consisting of a physical system (unmanned aerial vehicle), a virtual representation [PITH_FULL_IMAGE:figures/full_fig_p002_1.png] view at source ↗
Figure 2
Figure 2. Derivation of state machine processes from PGM representation. Nodes represent variables and [PITH_FULL_IMAGE:figures/full_fig_p004_2.png] view at source ↗
Figure 3
Figure 3. PGM with distributed communication required for two processes: (1) [PITH_FULL_IMAGE:figures/full_fig_p005_3.png] view at source ↗
Figures from the paper (10 more)
Figure 4
Figure 4. Figure 4: Augmentation for O, which is communicated over a distributed channel to D. Oin on both the message that was sent and the state of the network. (3) ωOin , which replaces the original process O → D to model the fact that the process input is the received variable Oin, in…
Figure 5
Figure 5. Figure 5: Reproduced with permission from [39]: testbed UAV (top) equipped with individually-transmitting [PITH_FULL_IMAGE:figures/full_fig_p019_5.png]
Figure 6
Figure 6. Figure 6: PGM for UAV Digital Twin [PITH_FULL_IMAGE:figures/full_fig_p020_6.png]
Figure 7
Figure 7. Figure 7: Augmented PGM modeling distributed communication [PITH_FULL_IMAGE:figures/full_fig_p020_7.png]
Figure 8
Figure 8. Figure 8: Partial property-part diagram showing a subset of properties [PITH_FULL_IMAGE:figures/full_fig_p021_8.png]
Figure 9
Figure 9. Figure 9: Visualization of state space: nodes represents states and edges represent transitions from state to [PITH_FULL_IMAGE:figures/full_fig_p021_9.png]
Figure 10
Figure 10. Figure 10: Graph visualization showing the path that leads to safety property violation [PITH_FULL_IMAGE:figures/full_fig_p022_10.png]
Figure 11
Figure 11. Figure 11: Example of a property violation and subsequent fix [PITH_FULL_IMAGE:figures/full_fig_p022_11.png]
Figure 12
Figure 12. Figure 12: Probabilistic graphical model (PGM) describing the UAV DT. [PITH_FULL_IMAGE:figures/full_fig_p023_12.png]
Figure 13
Figure 13. Figure 13: TLA code listing showing the process of receiving asynchronous sensor observations. [PITH_FULL_IMAGE:figures/full_fig_p023_13.png]

Discussion (0). Continue with ORCID to comment.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

  1. Testing, Evaluation, Verification and Validation (TEVV) of Digital Twins: A Comprehensive Framework

    cs.SE 2025-07 reject novelty 3.0 of 10

    A comprehensive TEVV framework for digital twins, using taxonomies and ontologies, but with no empirical validation.

Reference graph

Works this paper leans on

61 extracted references · 61 canonical work pages · cited by 1 Pith paper

  1. [1]

    Washington, DC: The National Academies Press, 2024

    National Academies of Sciences, Engineering, and Medicine, Foundational Research Gaps and Future Directions for Digital Twins. Washington, DC: The National Academies Press, 2024

    work page 2024

  2. [2]

    A probabilistic graphical model foundation for enabling predictive digital twins at scale,

    M. G. Kapteyn, J. V . Pretorius, and K. E. Willcox, “A probabilistic graphical model foundation for enabling predictive digital twins at scale,” Nature Computational Science , vol. 1, pp. 337–347, 2021

    work page 2021

  3. [3]

    Design, modeling and implementation of digital twins,

    M. Segovia and J. Garcia-Alfaro, “Design, modeling and implementation of digital twins,” Sensors, vol. 22, no. 14, 2022

    work page 2022

  4. [4]

    A design framework for adaptive digital twins,

    J. Erkoyuncu, I. Fern ´andez del Amo Blanco, D. Ariansyah, D. Bulka, R. Vrabi ˇc, and R. Roy, “A design framework for adaptive digital twins,” CIRP Annals, vol. 69, 05 2020

    work page 2020

  5. [5]

    General purpose digital twin framework using digital shadow and distributed system concepts,

    A. AboElHassan, A. H. Sakr, and S. Yacout, “General purpose digital twin framework using digital shadow and distributed system concepts,” Computers & Industrial Engineering , vol. 183, p. 109534, 2023

    work page 2023

  6. [6]

    Towards a digital twin architecture with formal analysis capabilities for learning-enabled autonomous systems,

    A. Temperekidis, N. Kekatos, P. Katsaros, W. He, S. Bensalem, H. AbdElSabour, M. AbdElSalam, and A. Salem, “Towards a digital twin architecture with formal analysis capabilities for learning-enabled autonomous systems,” in MESAS 2022: Modelling and Simulation for Autonomous Systems. , 2023, pp. 163–181

    work page 2022

  7. [7]

    Mitra, Verifying Cyber-Physical Systems: A Path to Safe Autonomy

    S. Mitra, Verifying Cyber-Physical Systems: A Path to Safe Autonomy . The MIT Press, 2021

    work page 2021

  8. [8]

    Alur, Principles of Cyber-Physical Systems

    R. Alur, Principles of Cyber-Physical Systems . MIT Press, 2015

    work page 2015

Show all 61 references
  1. [9]

    Reactive sampling-based temporal logic path planning,

    C. I. Vasile and C. Belta, “Reactive sampling-based temporal logic path planning,” in 2014 IEEE International Conference on Robotics and Automation (ICRA) , 2014, pp. 4310–4315

    2014

  2. [10]

    Temporal-logic-based reactive mission and motion planning,

    H. Kress-Gazit, G. E. Fainekos, and G. J. Pappas, “Temporal-logic-based reactive mission and motion planning,” IEEE Transactions on Robotics , vol. 25, no. 6, pp. 1370–1381, 2009

    2009

  3. [11]

    E. A. Lee and S. A. Seshia, Introduction to Embedded Systems, Second Edition: A Cyber-Physical Systems Approach . MIT Press, 2017

    2017

  4. [12]

    Logic & proofs for cyber-physical systems,

    A. Platzer, “Logic & proofs for cyber-physical systems,” in Proceedings of the 8th International Joint Conference on Automated Reasoning, 06 2016, pp. 15–21

    2016

  5. [13]

    Verification of cyberphysical systems,

    M. Sirjani, E. A. Lee, and E. Khamespanah, “Verification of cyberphysical systems,” Mathematics, vol. 8, no. 7, 2020

    2020

  6. [14]

    Algebraicsystems: Compositional verification for autonomous system design,

    G. Bakirtzis and U. Topcu, “Algebraicsystems: Compositional verification for autonomous system design,” in 2022 ACM/IEEE 13th International Conference on Cyber-Physical Systems (ICCPS) , 2022, pp. 308–309

    2022

  7. [15]

    Formal methods for autonomous systems,

    T. Wongpiromsarn, M. Ghasemi, M. Cubuktepe, G. Bakirtzis, S. Carr, M. O. Karabag, C. Neary, P. Gohari, and U. Topcu, “Formal methods for autonomous systems,” Foundations and Trends in Systems and Control, vol. 10, no. 3-4, pp. 180–407, 2023

    2023

  8. [16]

    Formally verified self-adaptation of an incubator digital twin,

    T. Wright, C. Gomes, and J. Woodcock, “Formally verified self-adaptation of an incubator digital twin,” in Leveraging Applications of Formal Methods, Verification and Validation. Practice , T. Margaria and B. Steffen, Eds. Cham: Springer Nature Switzerland, 2022, pp. 89–109

    2022

  9. [17]

    Cyber physical systems: Design challenges,

    E. Lee, “Cyber physical systems: Design challenges,” Electrical Engineering and Computer Sciences , pp. 363–369, 06 2008

    2008

  10. [18]

    The past, present and future of cyber-physical systems: A focus on models,

    E. A. Lee, “The past, present and future of cyber-physical systems: A focus on models,” Sensors (Basel) , vol. 15, pp. 4837–4869, 2015

    2015

  11. [19]

    Distributed policy synthesis of multiagent systems with graph temporal logic specifications,

    M. Cubuktepe, Z. Xu, and U. Topcu, “Distributed policy synthesis of multiagent systems with graph temporal logic specifications,” IEEE Transactions on Control of Network Systems , vol. 8, no. 4, pp. 1799–1810, 2021

    2021

  12. [20]

    Risk and mitigation of nondeterminism in distributed cyber-physical systems,

    S. Bateni, M. Lohstroh, H. S. Wong, H. Kim, S. Lin, C. Menard, and E. A. Lee, “Risk and mitigation of nondeterminism in distributed cyber-physical systems,” in Proceedings of the 21st ACM-IEEE International Conference on Formal Methods and Models for System Design , 2023, pp. 1–11

    2023

  13. [21]

    Timing predictability and security in safety-critical industrial cyber- physical systems: A position paper,

    S. Mubeen, E. Lisova, and A. Vulgarakis Feljan, “Timing predictability and security in safety-critical industrial cyber- physical systems: A position paper,” Applied Sciences, vol. 10, no. 9, 2020

    2020

  14. [22]

    Time in cyber-physical systems,

    A. Shrivastava, P. Derler, Y .-S. L. Baboudr, K. Stanton, M. Khayatian, H. A. Andrade, M. Weiss, J. Eidson, and S. Chandhoke, “Time in cyber-physical systems,” in 2016 International Conference on Hardware/Software Codesign and System Synthesis (CODES+ISSS) , 2016, pp. 1–10

    2016

  15. [23]

    A survey of probabilistic timing analysis techniques for real-time systems,

    R. Davis and L. Cucu-Grosjean, “A survey of probabilistic timing analysis techniques for real-time systems,” Leibniz Transactions on Embedded Systems (LITES) , vol. 6, pp. 03:1–03:60, 05 2019. 14

    2019

  16. [24]

    Statistical verification of autonomous system controllers under timing uncertainties,

    B. Ghosh, C. Hobbs, S. Xu, D. Smith, J. H. Anderson, P. S. Thiagarajan, B. Berg, P. S. Duggirala, and S. Chakraborty, “Statistical verification of autonomous system controllers under timing uncertainties,” Real-Time Systems, 2024. [Online]. Available: https://doi.org/10.1007/s...

    2024 doi

  17. [25]

    A run-time verification method with consideration of uncertainties for cyber–physical systems,

    M. Mehrabian, M. Khayatian, A. Shrivastava, P. Derler, and H. Andrade, “A run-time verification method with consideration of uncertainties for cyber–physical systems,” Microprocessors and Microsystems, vol. 101, p. 104890, 2023

    2023

  18. [26]

    The specification language TLA+,

    S. Merz, “The specification language TLA+,” in Logics of Specification Languages , D. Bjørner and M. C. Henson, Eds. Berlin, Heidelberg: Springer Berlin Heidelberg, 2008, pp. 401–451

    2008

  19. [27]

    Confidential consortium framework: Secure multiparty applications with confidentiality, integrity, and high availability,

    H. Howard, F. Alder, E. Ashton, A. Chamayou, S. Clebsch, M. Costa, A. Delignat-Lavaud, C. Fournet, A. Jeffery, M. Kerner, F. Kounelis, M. A. Kuppe, J. Maffre, M. Russinovich, and C. M. Wintersteiger, “Confidential consortium framework: Secure multiparty applications with confi...

    2023

  20. [28]

    Specification and verification with the TLA+ trifecta: TLC, Apalache, and TLAPS,

    I. Konnov, M. Kuppe, and S. Merz, “Specification and verification with the TLA+ trifecta: TLC, Apalache, and TLAPS,” in Leveraging Applications of Formal Methods, Verification and Validation. Verification Principles. Springer International Publishing, 2022, pp. 88–105

    2022

  21. [29]

    A TLA+ formal specification and verification of a new real-time communication protocol,

    P. Regnier, G. Lima, and A. Andrade, “A TLA+ formal specification and verification of a new real-time communication protocol,” Electronic Notes in Theoretical Computer Science , vol. 240, pp. 221–238, 2009

    2009

  22. [30]

    How Amazon Web Services uses formal methods,

    C. Newcombe, T. Rath, F. Zhang, B. Munteanu, M. Brooker, and M. Deardeuff, “How Amazon Web Services uses formal methods,” Communications of the ACM , 2015

    2015

  23. [31]

    Predictive digital twin for optimizing patient-specific radiotherapy regimens under uncertainty in high-grade gliomas,

    A. Chaudhuri, G. Pash, D. A. Hormuth, G. Lorenzo, M. Kapteyn, C. Wu, E. A. Lima, T. E. Yankeelov, and K. Willcox, “Predictive digital twin for optimizing patient-specific radiotherapy regimens under uncertainty in high-grade gliomas,” Frontiers in Artificial Intelligence , vol...

    2023

  24. [32]

    A digital twin framework for civil engineering structures,

    M. Torzoni, M. Tezzele, S. Mariani, A. Manzoni, and K. E. Willcox, “A digital twin framework for civil engineering structures,” Computer Methods in Applied Mechanics and Engineering , vol. 418, p. 116584, January 2024

    2024

  25. [33]

    Proving the correctness of multiprocess programs,

    L. Lamport, “Proving the correctness of multiprocess programs,” IEEE Transactions on Software Engineering , vol. SE-3, no. 2, pp. 125–143, 1977

    1977

  26. [34]

    The temporal logic of actions,

    ——, “The temporal logic of actions,” ACM Trans. Program. Lang. Syst. , vol. 16, no. 3, p. 872–923, 1994

    1994

  27. [35]

    Specifying and verifying systems with TLA+,

    L. Lamport, J. Matthews, M. Tuttle, and Y . Yu, “Specifying and verifying systems with TLA+,” in Proceedings of the 10th ACM SIGOPS European Workshop , 2002, pp. 45–48

    2002

  28. [36]

    Loopy belief propagation: Convergence and effects of message errors,

    A. T. Ihler, J. W. Fisher, III, and A. S. Willsky, “Loopy belief propagation: Convergence and effects of message errors,” Journal of Machine Learning Research , vol. 6, pp. 905–936, 2005

    2005

  29. [37]

    A mathematical theory of communication,

    C. E. Shannon, “A mathematical theory of communication,” Bell System Technical Journal , vol. 27, no. 3/4, pp. 379– 423/623–656, 1948

    1948

  30. [38]

    Semantic information,

    Y . Bar-Hillel and R. Carnap, “Semantic information,” British Journal for the Philosophy of Science , vol. 4, no. 14, pp. 147–157, Aug. 1953

    1953

  31. [39]

    A hardware testbed for dynamic data-driven aerospace digital twins,

    S. J. Salinger, M. G. Kapteyn, C. Kays, J. V . R. Pretorius, and K. E. Willcox, “A hardware testbed for dynamic data-driven aerospace digital twins,” in Dynamic Data Driven Applications Systems , F. Darema, E. Blasch, S. Ravela, and A. Aved, Eds. Cham: Springer International P...

    2020

  32. [40]

    Goal-directed concept acquisition in requirements elicitation,

    A. Dardenne, S. Fickas, and A. van Lamsweerde, “Goal-directed concept acquisition in requirements elicitation,” in Proceedings of the Sixth International Workshop on Software Specification and Design , 1991, pp. 14–21

    1991

  33. [41]

    Goal-directed requirements acquisition,

    A. Dardenne, A. van Lamsweerde, and S. Fickas, “Goal-directed requirements acquisition,” Science of Computer Programming, vol. 20, no. 1, pp. 3–50, 1993

    1993

  34. [42]

    Information flow and noninterference,

    H. Mantel, “Information flow and noninterference,” in Encyclopedia of Cryptography and Security , H. C. A. van Tilborg and S. Jajodia, Eds. Boston, MA: Springer, 2011, pp. 605–607

    2011

  35. [43]

    Noninterference specifications for secure systems,

    L. Nelson, J. Bornholt, A. Krishnamurthy, E. Torlak, and X. Wang, “Noninterference specifications for secure systems,” SIGOPS Oper. Syst. Rev., vol. 54, no. 1, p. 31–39, 2020

    2020

  36. [44]

    Noninterference and the composability of security properties,

    D. McCullough, “Noninterference and the composability of security properties,” in Proceedings of the 1988 IEEE Symposium on Security and Privacy , 1988, pp. 177–186

    1988

  37. [45]

    An information-theoretic model for adaptive side-channel attacks,

    B. K ¨opf and D. Basin, “An information-theoretic model for adaptive side-channel attacks,” in Proceedings of the 14th ACM Conference on Computer and Communications Security (CCS ’07) , Oct. 2007, pp. 286–296

    2007

  38. [46]

    Ljung, System Identification: Theory for the User , 2nd ed

    L. Ljung, System Identification: Theory for the User , 2nd ed. Prentice Hall, 1999

    1999

  39. [47]

    Let’s talk through physics! Covert cyber-physical data exfiltration on air-gapped edge devices,

    M. Chan, N. Snyder, M. Lucas, L. Garcia, O. Sokolsky, J. Weimer, I. Lee, P. Tabuada, S. Zonouz, and M. Srivastava, “Let’s talk through physics! Covert cyber-physical data exfiltration on air-gapped edge devices,” arXiv:2210.07531 [cs.CR]., Oct. 2022

    arXiv

  40. [48]

    Secure-by-construction synthesis of cyber-physical systems,

    S. Liu, A. Trivedi, X. Yin, and M. Zamani, “Secure-by-construction synthesis of cyber-physical systems,” Annual Reviews in Control, vol. 53, pp. 30–50, 2022

    2022

  41. [49]

    On system identification of complex systems from finite data,

    S. R. Venkatesh and M. A. Dahleh, “On system identification of complex systems from finite data,” IEEE Trans. Automatic Control, vol. 46, no. 2, pp. 235–257, 2001

    2001

  42. [50]

    Finite time LTI system identification,

    T. Sarkar, A. Rakhlin, and M. A. Dahleh, “Finite time LTI system identification,” Journal of Machine Learning Research , vol. 22, pp. 1–61, 2021. 15

    2021

  43. [51]

    Closed loop system identification with known feedback: A non asymptotic viewpoint,

    D. Jones and M. A. Dahleh, “Closed loop system identification with known feedback: A non asymptotic viewpoint,” in Proceedings of the 2022 American Control Conference (ACC) , Jun. 2022

    2022

  44. [52]

    Model checking and the state explosion problem,

    E. M. Clarke, W. Klieber, M. Nov ´aˇcek, and P. Zuliani, “Model checking and the state explosion problem,” in Tools for Practical Software Verification, B. Meyer and M. Nordio, Eds. Berlin, Heidelberg: Springer, 2012, pp. 1–30

    2012

  45. [53]

    Local and global fairness in concurrent systems,

    A. Brook, D. Peled, and S. Schewe, “Local and global fairness in concurrent systems,” in 2015 ACM/IEEE International Conference on Formal Methods and Models for Codesign , 2015, pp. 2–9

    2015

  46. [54]

    Progress, justness, and fairness,

    R. V . Glabbeek and P. H ¨ofner, “Progress, justness, and fairness,” ACM Comput. Surv., vol. 52, no. 4, 2019

    2019

  47. [55]

    Formal specification and verification of autonomous robotic systems: A survey,

    M. Luckcuck, M. Farrell, L. A. Dennis, C. Dixon, and M. Fisher, “Formal specification and verification of autonomous robotic systems: A survey,” ACM Comput. Surv., vol. 52, no. 5, 2019

    2019

  48. [56]

    Abstracting and refining robustness for cyber-physical systems,

    M. Rungger and P. Tabuada, “Abstracting and refining robustness for cyber-physical systems,” in Proceedings of the 17th International Conference on Hybrid Systems: Computation and Control , 2014, pp. 223–232

    2014

  49. [57]

    Distributed scalar quantization for computing: High-resolution analysis and extensions,

    V . Misra, V . K. Goyal, and L. R. Varshney, “Distributed scalar quantization for computing: High-resolution analysis and extensions,” IEEE Transactions on Information Theory , vol. 57, no. 8, pp. 5298–5325, Aug. 2011

    2011

  50. [58]

    Exploiting errors for efficiency: A survey from circuits to applications,

    P. Stanley-Marbell, A. Alaghi, M. Carbin, E. Darulova, L. Dolecek, A. Gerstlauer, G. Gillani, D. Jevdjic, T. Moreau, M. Cacciotti, A. Daglis, N. E. Jerger, B. Falsafi, S. Misailovic, A. Sampson, and D. Zufferey, “Exploiting errors for efficiency: A survey from circuits to appl...

    2021

  51. [59]

    N. A. Lynch, Distributed Algorithms. San Francisco, CA, USA: Morgan Kaufmann Publishers Inc., 1996

    1996

  52. [60]

    On interprocess communication,

    L. Lamport, “On interprocess communication,” Distributed Computing, 1985

    1985

  53. [61]

    Property-part diagrams: A dependence notation for software systems,

    D. Jackson and E. Kang, “Property-part diagrams: A dependence notation for software systems,” IEEE 31st International Conference on Software Engineering , 01 2009. APPENDIX A PGM encodes random variables as nodes and statistical dependencies as edges between nodes. In the DT P...

    2009

Pith tools

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