Pith. sign in

REVIEW 4 major objections 6 minor 42 references

Towards Bridging Formal Methods and Human Interpretability

T0 review · 4 major / 6 minor · reviewed 2026-08-07 · deepseek-v4-flash

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

Pith's one-line read Traditional complexity metrics predict how hard engineers find LTS designs to read, and ranking repair candidates by Albin complexity reduced comprehension time by 39% in a small trial.

desk verdict First real measurement of LTS comprehension against graph metrics; referee it, but check the duplicated-looking State Space/Max Depth row and the n=2 case study before trusting the correlations. read the letter →

arxiv 2506.09759 v1 pith:DAML5IIG submitted 2025-06-11 cs.SE

Abhijit Paul , Proma Chowdhury , Kazi Sakib This is my paper · ORCID
classification cs.SE
keywords labeledtransitionsystemshumancomprehensiondesignmetricsAlbincomplexityBradley-TerrymodelKendall'staupairwisecomparisonrepair
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 asks whether standard software-engineering and graph-theory metrics can predict how easily engineers understand labeled transition system (LTS) designs, the diagrams used by model checkers and design repair tools. The authors built a dataset of 148 LTS designs, selected 48 for pairwise human comparisons, and used a Bradley-Terry model to turn 324 comparisons into a comprehension ranking. They report that Albin complexity ($\tau = 0.444$), state space size ($\tau = 0.420$), cyclomatic complexity ($\tau = 0.366$), and redundancy ($\tau = 0.315$) correlate most strongly with that ranking. In a two-annotator case study with the Fortis repair tool, presenting 16 redesigns ordered by Albin complexity reduced understanding time from 66 to 40 minutes, a 39% drop. If these metric-comprehension links hold, repair and visualization tools could order or generate designs that people actually find readable.

What carries the argument

The load-bearing object is Albin complexity, a one-line graph score $C = n + \sum_i \deg(v_i) + L$, where $n$ is the number of states, $\deg(v_i)$ is each state's degree, and $L$ is the longest path length in edges; the paper uses it both as a correlation target and as the ranking key in the Fortis case study. The methodology around it pairs a psychometric pipeline (pairwise comparisons, Bradley-Terry ranking) with Kendall's tau correlation, and supplements Albin with two structural metrics estimated for LTS diagrams: redundancy via neighbor-set overlap (Jaccard similarity) and modularity via community detection. The same pipeline is what lets the paper convert subjective difficulty judgments into a stable ranking that metrics can be tested against.

What would settle it

A replication that adds the 76 discarded 'too complex' designs to the annotation set, or runs the Fortis ordering test with more than one annotator per condition, would settle the claim: the central result fails if Albin complexity's Kendall tau drops to near zero on the expanded set or if Albin-ordered presentation no longer reduces median comprehension time relative to random ordering.

Watch

Extended reading notes

Core claim

The paper's central claim is that human comprehension of LTS designs is not arbitrary: it is approximated by a few cheap graph statistics. The best single predictor is Albin complexity, defined as the number of states plus the sum of all node degrees plus the longest path length in edges, which produced a Kendall's tau of 0.444 against the human-derived ranking. State space size and maximum depth tied at 0.420, cyclomatic complexity at 0.366, and redundancy at 0.315, while average branching factor showed weak correlation and modularity, computed by a community-detection algorithm, correlated negatively. The authors then claim that applying Albin complexity to order Fortis redesigns of a voting system cut comprehension time by 39% (from 66 to 40 minutes), suggesting that ordering repair candidates from simple to complex helps engineers build understanding incrementally.

Load-bearing premise

The load-bearing assumption is that the 48 sampled designs, after 76 were discarded as too complex, and the two annotators in the case study are representative of real LTS designs and real system engineers; if the sample is unrepresentative, both the correlations and the 39% time reduction may not transfer.

Editorial extensions

If this is right

  • If the correlations hold, design repair tools can sort their output by Albin complexity, letting engineers start with easy repairs and work toward hard ones, without changing the repair logic.
  • The four correlated metrics—Albin complexity, state space size, cyclomatic complexity, and redundancy—are concrete candidates for objective functions in tools that generate or rank redesigns.
  • Average branching factor and modularity should probably not be used as comprehension proxies, since their correlations with human rankings were weak or negative.
  • Pairwise comparison with a Bradley-Terry model is a workable method for collecting human complexity judgments on formal designs when direct ordinal ratings are unreliable.
  • The 39% time saving suggests that ordering design alternatives by predicted interpretability is a testable improvement to LTS-based tool workflows, not just a theoretical correlation.

Reading between the lines

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

  • The metric-comprehension link is likely to be extended from reading time to functional outcomes: if Albin-ranked designs actually support understanding, engineers should also find bugs and inconsistencies faster when designs are ordered this way—an experiment the paper did not run.
  • Because 76 of the original 148 designs were discarded as too complex, the reported correlations may only apply to a mid-range of complexity; including the discarded designs could weaken or strengthen Albin complexity's predictive power, and this is testable on the published dataset.
  • Albin complexity is cheap enough to compute live, so an interactive LTS viewer could highlight high-complexity states or reorder tool output on the fly; this is a natural deployment that the paper only gestures at.
  • The case study's two-annotator design means the 39% figure is a point estimate, not a measured effect; a randomized trial with more participants and counterbalanced ordering would be needed before treating the time saving as stable.
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.

Referee Report

4 major / 6 minor

Summary. The paper reports the first study, to the authors' knowledge, of human comprehension of Labeled Transition System (LTS) designs. It constructs a dataset of 148 LTS designs, samples 48, collects 324 pairwise complexity judgments from three annotators, ranks designs with the Bradley-Terry model, and computes Kendall's tau correlations between seven graph/software metrics and the human-derived ranking. The authors report that Albin complexity, state space size, cyclomatic complexity, and redundancy correlate significantly with human rankings, and they present a Fortis case study in which ranking 16 redesigns by Albin complexity reduced one annotator's comprehension time from 66 to 40 minutes (a 39% reduction).

Significance. If the correlation results hold, the paper would make a genuinely useful contribution by connecting formal-methods artifacts to human interpretability, a largely neglected dimension in LTS tooling. The dataset construction and pairwise-annotation protocol are strengths, as is the reported intent to release source code and annotations. The authors are appropriately cautious in framing the work as preliminary. The main significance is limited by three load-bearing weaknesses: a plausible data-integrity problem in Table I, a highly selective dataset, and a two-annotator case study. With verification and re-analysis, the paper could provide a foundation for future, more rigorous studies of comprehensibility-aware design repair.

major comments (4)
  1. [Section IV-A, Table I] State Space Size and Max Depth are reported with identical Kendall's tau values (0.4202020202) and identical p-values (4.71E-05). These metrics are defined differently in Section III-C: state space size is the number of nodes n, while max depth is described as a longest-path parameter (L in edge count). Two distinct graph quantities producing the same rank correlation to ten decimal places is implausible unless the underlying metric vectors are identical, one row was copied, or the dataset is degenerate. Because Albin Complexity is defined as n + sum(deg(vi)) + L, this issue also affects the credibility of the headline metric. Please verify the computations, report the actual 48-element metric arrays or a hash/checksum, and re-run the correlations if an error is found.
  2. [Section III-B] The manuscript states that 76 of 148 specifications were eliminated because they were 'too complex to understand without prior knowledge of the system.' Since the study's dependent variable is comprehension, excluding designs on exactly that basis may truncate the complexity range and inflate or distort the reported correlations. The criteria for this exclusion are not specified, and the authors do not report how many designs were dropped per source or whether the retained 72 designs still span the intended complexity spectrum. Please provide the exclusion criteria, quantify the excluded designs, and, if feasible, perform a robustness check on a subset of the excluded designs.
  3. [Section IV-B] The Fortis case study uses only two annotators, one per condition. With n=2, the 39% time reduction (66 versus 40 minutes) cannot be distinguished from individual differences in reading speed or familiarity with the voting system. The paper also does not report how comprehension was measured (e.g., whether annotators had to answer questions about the repairs), the variance across designs, or any measure of inter-rater agreement. Please clarify the task protocol, report per-design times, and either provide a within-subject design or explicitly reframe the case study as an illustrative demonstration rather than evidence of effectiveness.
  4. [Section IV-A and Section IV-B] Albin complexity is selected as the 'best-performing metric' based on the highest Kendall's tau in the same 48-design dataset, and then the same metric is used for the Fortis case study without any correction for multiple comparisons or out-of-sample validation. This selection-on-the-maximum approach creates an overfitting risk: the reported tau value for Albin complexity is the maximum of seven correlations and will tend to be optimistic. Please provide confidence intervals for each tau, a multiple-comparison correction, or a validation on held-out designs or a separate dataset before presenting Albin complexity as the recommended metric.
minor comments (6)
  1. [Section III-A] The dataset counts do not reconcile cleanly: the paper says 97 specifications were collected from Kramer's book, 4 system specifications from Fortis, and 'yielding 51 designs' after generating redesigns, yet the total is said to be 148. Please clarify the precise derivation of the 148 and the later 48-design sample.
  2. [Section III-C] Average branching factor and max depth are mentioned in the State Space Size paragraph but are never formally defined as separate metrics. Please provide explicit definitions (e.g., whether average branching factor is mean out-degree and whether max depth is longest path in edges or nodes).
  3. [Section IV-B] The repository link appears only in a footnote after the case study. Please move it to a dedicated data and code availability statement and confirm that the annotated pairwise comparisons and metric values are included, as claimed in Section VI.
  4. [Section III-B] The agreement score of 75.748% is reported without specifying how it is computed (e.g., percentage of pairs on which all three annotators agreed, or pairwise agreement averaged). Please clarify.
  5. [Throughout] There are minor typos and formatting issues, including 'figure-2' instead of 'Figure 2' and 'degree f each node' in the modularity algorithm; these should be corrected.
  6. [References] References [1] and [8] both cite Magee and Kramer's 'Concurrency: State Models & Java Programs' with different subtitles and publishers; please merge them.

Circularity Check

0 steps flagged · score 0.0 of 10

No circularity found: human rankings and metric definitions are independent; the identical Kendall tau values for State Space Size and Max Depth are a data-integrity concern, not a demonstrated circular reduction.

full rationale

I examined the derivation chain from pairwise annotation to Bradley-Terry ranking, metric computation, Kendall's tau correlation, and the Fortis case study. The human-derived rankings come from three annotators' pairwise comparisons, which are independent of the seven graph metrics defined in Section III-C. The metrics (cyclomatic complexity, state size, max depth, Albin complexity, modularity, redundancy, branching factor) are computed directly from LTS graph structure with no parameters fitted to the human rankings, so the correlations in Table I compare two independently constructed orderings. Selecting Albin complexity as the best metric on the same 48 designs is an in-sample selection and overfitting risk, not a circularity. The case study applies the pre-selected Albin formula to 16 new Fortis redesigns and measures comprehension time independently; the 39% reduction is not forced by construction because the metric was not fitted to those times. No load-bearing self-citations or imported uniqueness theorems appear. The identical tau and p-values for State Space Size and Max Depth in Table I are suspicious and may indicate duplicate computation or a monotone dependency, but the paper's definitions do not equate L with n, so this is a correctness and reproducibility threat rather than a circular step that can be demonstrated from the text. Overall score 0.

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

The central claim rests on an unvalidated metric definition and a subjectively curated sample.

assumptions (4)
  • domain assumption Human comprehension of an LTS design can be represented as a scalar ranking consistent across annotators.
    The study reduces comprehension to pairwise preference and Bradley-Terry ranking (Section III-B).
  • ad hoc to paper The Albin complexity formula n + sum(deg(vi)) + L, attributed to Albin, is a valid measure of design complexity.
    Defined in Section III-C without derivation from Albin's cited work.
  • domain assumption State space size and max depth are distinct metrics; the identical tau and p-values in Table I imply they may be collinear in this dataset.
    Table I reports identical values for both metrics, suggesting the formula or data may conflate them.
  • domain assumption The 48 sampled designs after exclusion are representative of LTS designs used in practice.
    The exclusion of 76 specs in Section III-B is subjective and may bias the sample.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Towards Bridging Formal Methods and Human Interpretability." pith.science (2026). https://pith.science/paper/DAML5IIG

@misc{pith2026250609759,
  author       = {Pith},
  title        = {Pith review of: Towards Bridging Formal Methods and Human Interpretability},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/DAML5IIG}},
  note         = {Machine review of arXiv:2506.09759}
}
abstract

Labeled Transition Systems (LTS) are integral to model checking and design repair tools. System engineers frequently examine LTS designs during model checking or design repair to debug, identify inconsistencies, and validate system behavior. Despite LTS's significance, no prior research has examined human comprehension of these designs. To address this, we draw on traditional software engineering and graph theory, identifying 7 key metrics: cyclomatic complexity, state space size, average branching factor, maximum depth, Albin complexity, modularity, and redundancy. We created a dataset of 148 LTS designs, sampling 48 for 324 paired comparisons, and ranked them using the Bradley-Terry model. Through Kendall's Tau correlation analysis, we found that Albin complexity ($\tau = 0.444$), state space size ($\tau = 0.420$), cyclomatic complexity ($\tau = 0.366$), and redundancy ($\tau = 0.315$) most accurately reflect human comprehension of LTS designs. To showcase the metrics' utility, we applied the Albin complexity metric within the Fortis design repair tool, ranking system redesigns. This ranking reduced annotators' comprehension time by 39\%, suggesting that metrics emphasizing human factors can enhance formal design interpretability.

Figures

Figures reproduced from arXiv: 2506.09759 by the authors.

Figure 1
Figure 1. Process to evaluate the metrics III. METHODOLOGY To evaluate how well the identified design metrics can approximate human comprehension in LTS design, we need a human annotated dataset of LTS designs where annotators rank the designs based on perceived complexity. Hence, our methodology is comprised of three sections: dataset construc￾tion, annotation and finally experimentation. More specifically, we first construc… view at source ↗
Figure 2
Figure 2. Voting System [12] presented the redesigns in their original, unranked order, while the second group ordered them from least to most complex based on their Albin Complexity scores. We hypothesized that the ranked ordering would reduce comprehension time by presenting simpler designs first, allowing annotators to incrementally build understanding before examining more complex designs. The results supported this hypot… view at source ↗

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

42 extracted references · 37 canonical work pages

  1. [1]

    Magee and J

    J. Magee and J. Kramer,Concurrency: State Models and Java Programs, 2nd ed. London: Wiley, 2006

    work page 2006

  2. [2]

    Jackson,Software Abstractions: logic, language, and analysis

    D. Jackson,Software Abstractions: logic, language, and analysis. MIT press, 2012

    work page 2012

  3. [3]

    The complexity of social groups and social systems described by graph structures,

    P. S. Albin, “The complexity of social groups and social systems described by graph structures,”Mathematical Social Sciences, vol. 1, no. 1, pp. 101–129, 1980

    work page 1980

  4. [4]

    Edmonds,Syntactic measures of complexity

    B. Edmonds,Syntactic measures of complexity. The University of Manchester (United Kingdom), 1999

    work page 1999

  5. [5]

    The model checker spin,

    G. J. Holzmann, “The model checker spin,”IEEE Transactions on Software Engineering, vol. 23, no. 5, pp. 279–295, 1997

    1997

  6. [6]

    Further generalizations of the jaccard index,

    L. d. F. Costa, “Further generalizations of the jaccard index,”arXiv preprint arXiv:2110.09619, 2021

    arXiv 2021

  7. [7]

    Modularity and community structure in networks,

    M. E. Newman, “Modularity and community structure in networks,” Proceedings of the national academy of sciences, vol. 103, no. 23, pp. 8577–8582, 2006

    work page 2006

  8. [8]

    Magee and J

    J. Magee and J. Kramer,Concurrency: State Models & Java Programs, 2nd ed. Wiley, 2006

    work page 2006

Show all 42 references
  1. [9]

    Decreasing annotation burden of pairwise comparisons with human-in-the-loop sorting: Application in medical image artifact rating,

    I. Jang, G. Danley, K. Chang, and J. Kalpathy-Cramer, “Decreasing annotation burden of pairwise comparisons with human-in-the-loop sorting: Application in medical image artifact rating,”arXiv preprint arXiv:2202.04823, 2022

    2022 arXiv

  2. [10]

    Mm algorithms for generalized bradley-terry models,

    D. R. Hunter, “Mm algorithms for generalized bradley-terry models,” The annals of statistics, vol. 32, no. 1, pp. 384–406, 2004

    2004

  3. [11]

    A new measure of rank correlation,

    M. G. Kendall, “A new measure of rank correlation,”Biometrika, vol. 30, no. 1/2, pp. 81–93, 1938

    1938

  4. [12]

    Fortis: A tool for analysis and repair of robust software systems,

    C. Zhang, I. Dardik, R. Meira-G ´oes, D. Garlan, and E. Kang, “Fortis: A tool for analysis and repair of robust software systems,” in2023 Formal Methods in Computer-Aided Design (FMCAD). IEEE, 2023, pp. 1–9

    2023

  5. [13]

    Metric based evaluation and improvement of software designs,

    C. W. Butler, “Metric based evaluation and improvement of software designs,”Journal of Software Engineering and Applications, vol. 14, no. 8, pp. 389–399, 2021

    2021

  6. [14]

    Software engineering: a practitioner’s approach,

    R. S. Pressman, “Software engineering: a practitioner’s approach,” Pressman and Associates, 2005

    2005

  7. [15]

    Software engineering (ed.),

    I. Sommerville, “Software engineering (ed.),”America: Pearson Educa- tion Inc, 2011

    2011

  8. [16]

    Bass,Software architecture in practice

    L. Bass,Software architecture in practice. Pearson Education India, 2012

    2012

  9. [17]

    Ieee recommended practice for architectural description of software-intensive systems,

    I. A. W. Groupet al., “Ieee recommended practice for architectural description of software-intensive systems,”IEEE std, vol. 1471, 2000

    2000

  10. [18]

    Promoting the use of design evaluation techniques within software development,

    F. Almansour and L. Stuart, “Promoting the use of design evaluation techniques within software development,” inProceedings of the 28th In- ternational BCS Human Computer Interaction Conference (HCI 2014). BCS Learning & Development, 2014

    2014

  11. [19]

    Assessing the comprehension of uml class diagrams via eye tracking,

    S. Yusuf, H. Kagdi, and J. I. Maletic, “Assessing the comprehension of uml class diagrams via eye tracking,” in15th IEEE International Conference on Program Comprehension (ICPC’07). IEEE, 2007, pp. 113–122

    2007

  12. [20]

    Evaluating the layout quality of uml class diagrams using machine learning,

    G. Bergstr ¨om, F. Hujainah, T. Ho-Quang, R. Jolak, S. A. Rukmono, A. Nurwidyantoro, and M. R. Chaudron, “Evaluating the layout quality of uml class diagrams using machine learning,”Journal of Systems and Software, vol. 192, p. 111413, 2022. [Online]. Available: https://www.sc...

    2022

  13. [21]

    Hart,Investigating user experience and user engagement for design

    J. Hart,Investigating user experience and user engagement for design. The University of Manchester (United Kingdom), 2015

    2015

  14. [22]

    Evaluation of software impact designed for biomedical research: Are we measuring what’s meaningful?

    A. Afiaz, A. A. Ivanov, J. Chamberlin, D. Hanauer, C. L. Savonen, M. J. Goldman, M. Morgan, M. Reich, A. Getka, A. Holmeset al., “Evaluation of software impact designed for biomedical research: Are we measuring what’s meaningful?”ArXiv, 2023

    2023

  15. [23]

    User engagement by user-centred design in e-health,

    A. Sutcliffe, S. Thew, O. De Bruijn, I. Buchan, P. Jarvis, J. McNaught, and R. Procter, “User engagement by user-centred design in e-health,” Philosophical Transactions of the Royal Society A: Mathematical, Phys- ical and Engineering Sciences, vol. 368, no. 1926, pp. 4209–4224, 2010

    1926

  16. [24]

    Participatory design, user involvement and health it evaluation,

    A. Kushniruk and C. Nøhr, “Participatory design, user involvement and health it evaluation,” inEvidence-based health informatics. IOS Press, 2016, pp. 139–151

    2016

  17. [25]

    Evaluating large language models in software design: A comparative analysis of uml class diagram generation,

    D. De Bari, “Evaluating large language models in software design: A comparative analysis of uml class diagram generation,” Ph.D. disserta- tion, Politecnico di Torino, 2024

    2024

  18. [26]

    Three simulation algorithms for labelled transition systems,

    G. C ´ec´e, “Three simulation algorithms for labelled transition systems,” arXiv preprint arXiv:1301.1638, 2013

    2013 arXiv

  19. [27]

    Approximate analyzing of labeled transition systems,

    Q. Yu, S. Yang, and J. Wu, “Approximate analyzing of labeled transition systems,”Mathematical Problems in Engineering, vol. 2015, no. 1, p. 963597, 2015

    2015

  20. [28]

    On the complexity of techniques that make transition systems implementable by boolean nets,

    R. Devillers and R. Tredup, “On the complexity of techniques that make transition systems implementable by boolean nets,”Fundamenta Informaticae, vol. 189, 2023

    2023

  21. [29]

    Evaluation of mechanism transitions

    B. Richerzhagen, “Evaluation of mechanism transitions.” Springer, Cham, 2019, pp. 105–151

    2019

  22. [30]

    Labeled transition systems

    R. Gorrieri, “Labeled transition systems.” Springer, Cham, 2017, pp. 15–34

    2017

  23. [31]

    Detecting community structure in networks,

    M. E. Newman, “Detecting community structure in networks,”The European physical journal B, vol. 38, pp. 321–330, 2004

    2004

  24. [32]

    Enhancing model checking in verification by ai techniques,

    F. Buccafurri, T. Eiter, G. Gottlob, and N. Leone, “Enhancing model checking in verification by ai techniques,”Artificial Intelligence, vol. 112, no. 1-2, pp. 57–104, 1999

    1999

  25. [33]

    System design modification with actions,

    M. V . De Menezes, S. do Lago Pereira, and L. N. de Barros, “System design modification with actions,” inAdvances in Artificial Intelligence– SBIA 2010: 20th Brazilian Symposium on Artificial Intelligence, S ˜ao Bernardo do Campo, Brazil, October 23-28, 2010. Proceedings 20. S...

    2010

  26. [34]

    Abstract model repair,

    G. Chatzieleftheriou, B. Bonakdarpour, P. Katsaros, and S. A. Smolka, “Abstract model repair,”Logical Methods in Computer Science, vol. 11, 2015

    2015

  27. [35]

    Fixing targets and evaluating design alternatives by pairwise comparisons–the compare method,

    B. Yannou and E. Coatan ´ea, “Fixing targets and evaluating design alternatives by pairwise comparisons–the compare method,”Revue d’Ing´enierie Num ´erique collaborative, vol. 1, no. 1-2, pp. 145–163, 2009

    2009

  28. [36]

    H. A. David,The method of paired comparisons. London, 1963, vol. 12

    1963

  29. [37]

    Efficient bayesian inference for generalized bradley–terry models,

    F. Caron and A. Doucet, “Efficient bayesian inference for generalized bradley–terry models,”Journal of Computational and Graphical Statis- tics, vol. 21, no. 1, pp. 174–196, 2012

    2012

  30. [38]

    Active ranking using pairwise com- parisons,

    K. G. Jamieson and R. Nowak, “Active ranking using pairwise com- parisons,”Advances in neural information processing systems, vol. 24, 2011

    2011

  31. [39]

    A graph complexity measure based on the spectral analysis of the laplace operator,

    D. M. Mateos, F. Morana, and H. Aimar, “A graph complexity measure based on the spectral analysis of the laplace operator,”Chaos, Solitons & Fractals, vol. 156, p. 111817, 2022

    2022

  32. [40]

    The state explosion problem,

    A. Valmari, “The state explosion problem,” inAdvanced Course on Petri Nets. Springer, 1996, pp. 429–528

    1996

  33. [41]

    On the criteria to be used in decomposing systems into modules,

    D. L. Parnas, “On the criteria to be used in decomposing systems into modules,”Communications of the ACM, vol. 15, no. 12, pp. 1053–1058, 1972

    1972

  34. [42]

    Symmetry and model checking,

    E. A. Emerson and A. P. Sistla, “Symmetry and model checking,”Formal methods in system design, vol. 9, no. 1, pp. 105–131, 1996

    1996

Pith tools

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