Pith. sign in

REVIEW 3 major objections 4 minor 36 references

Weakly acyclic diagrams: A data structure for infinite-state symbolic verification

T0 review · 3 major / 4 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 This paper introduces weakly acyclic diagrams, a generalization of OBDDs that represents infinite languages canonically while preserving the memoized dynamic-programming algorithms used in symbolic verification.

desk verdict WADs are a clean, honest extension of OBDDs to infinite weakly acyclic languages; the main caveat is an unproved monotonicity claim in the broadcast-protocol section. read the letter →

arxiv 2411.17250 v2 pith:YGYOD27I submitted 2024-11-26 cs.LO cs.DS

Michael Blondin , Michaël Cadilhac , Xin-Yi Cui , Philipp Czerner , Javier Esparza , Jakob Schulz This is my paper · ORCID
classification cs.LOcs.DS MSC 68Q4568Q60
keywords weaklyacyclicdiagramslanguagesorderedbinarydecisionsymbolicmodelcheckinginfinite-stateverificationwell-structuredtransitionsystemsbackwardreachabilityregular
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

Ordered binary decision diagrams (OBDDs) represent Boolean functions as canonical decision graphs, but only for inputs of a fixed length. This paper introduces weakly acyclic diagrams (WADs), which replace fixed length with a weaker restriction: the underlying directed graph may contain only self-loops as cycles. WADs are canonical minimal deterministic automata for weakly acyclic languages, so they can represent infinite regular languages while still supporting the memoized top-down algorithms that make OBDDs fast. Using WADs, the authors implement symbolic backwards reachability for infinite-state systems whose configuration sets are upward-closed and weakly acyclic, including lossy channel systems, Petri nets, and broadcast protocols, and they report that their prototype is competitive with dedicated tools on a broad benchmark suite.

What carries the argument

The load-bearing object is the master automaton over an alphabet $\Sigma$: its states are all weakly acyclic languages, and reading a letter maps a language to its residual. Because weakly acyclic languages have no infinite descending chains of residuals, every WAD is a finite fragment of this automaton, and that fragment is exactly the minimal DFA for each represented language. The node table representation adds a special self pointer for the case where a residual equals the language itself; memoized recursion over residuals, plus the make procedure that collapses duplicate languages, is what carries all operations.

What would settle it

A decisive test is to apply the contraction-based pre/post algorithm to a fixed-length transducer and a weakly acyclic language whose true pre-image or post-image is known not to be weakly acyclic, such as the paper's own Figure 3 example where the result is $(a+b)^*b$. If the algorithm terminates and returns a WAD whose language differs from the exactly computed pre-image, the claimed correctness guarantee fails; on small alphabets the exact pre-image can be obtained by an independent subset construction.

Watch

Extended reading notes

Core claim

The paper's central discovery is that the algorithmic advantages of OBDDs survive when fixed-length Boolean functions are replaced by weakly acyclic regular languages, meaning languages whose minimal DFA has no cycles except self-loops. For such a language, the set of residuals is partially ordered by the transition relation and has no infinite descending chains, so the 'master automaton' whose states are all weakly acyclic languages gives a canonical minimal DFA for each one. A WAD stores finitely many such languages as a shared node table in which a transition may point to a node or to 'self', and a memoized make procedure guarantees that equal languages share one node. Complement, intersection, union, and pre/post along fixed-length relations are then computed by recursive descent through residuals, exactly in the style of OBDD algorithms; in the pre-compatible case the pre-image computation runs in polynomial time, and in general it terminates and returns a correct WAD whenever the result is weakly acyclic.

Load-bearing premise

The framework depends on the chosen encoding mapping every upward-closed set that the backward reachability algorithm ever constructs to a weakly acyclic language, and on each transition's transducer preserving weak acyclicity under pre-image.

Editorial extensions

If this is right

  • Every weakly acyclic language has a unique minimal WAD representation, generalizing the canonicity of OBDDs to infinite languages.
  • The standard OBDD operations—negation, conjunction, union, and relational pre/post—can be ported to infinite-state symbolic verification with the same memoization-based complexity guarantees.
  • Backwards reachability for well-structured transition systems becomes a uniform WAD computation for lossy channel systems, Petri nets, and broadcast protocols, rather than requiring a purpose-built data structure for each system class.
  • For regular model checking, any run that terminates with all cycle contractions being true self-loops yields a correct answer, and many textbook protocols are weakly acyclic.
  • Pre-compatibility provides a polynomial-time pre-image computation for many lossy-channel-system encodings, making the infinite-state case tractable in practice.

Reading between the lines

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

  • If weakly acyclic languages turn out to be as common in regular model checking benchmarks as the paper's experiments suggest, a unified WAD-based engine could replace several specialized symbolic backends; this is an extrapolation beyond the paper's own claims.
  • The seven regular-model-checking instances where cycle contraction fires leave the weak acyclicity of the result unproven; a natural next step, not taken here, is to make that contraction step produce a certificate or fall back to exact determinization.
  • The class could be widened by allowing bounded nondeterminism, following the paper's closing question about languages like $(a+b)^*b$; if such an extension kept canonical residuals it would cover more protocols.
  • A stress test on parameterized families, such as the ring instances the paper reports scaling to large sizes, could reveal where the residual hierarchy grows too large and where an extrapolation-based widening would be needed.
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 / 4 minor

Summary. The paper introduces weakly acyclic diagrams (WADs), a canonical data structure for weakly acyclic languages, i.e., languages accepted by DFAs whose only cycles are self-loops. It recasts OBDDs as minimal DFAs for fixed-length languages and generalizes them to possibly infinite weakly acyclic languages. The core contributions are: (i) the master-automaton construction, giving a unique minimal WAD per language; (ii) a node-table implementation with a make procedure that maintains canonicity; (iii) OBDD-style top-down algorithms for complement, intersection, and fixed-length Pre/Post with complexity bounds; and (iv) an application to backward reachability for lossy channel systems, Petri nets, and broadcast protocols, implemented in the wadl prototype and evaluated on more than 200 instances.

Significance. If correct, WADs are a valuable addition to symbolic verification: they extend the algorithmic advantages of OBDDs to an infinite class of languages while retaining canonical minimal representations. The theoretical development is self-contained, the main correctness proofs are supplied in the appendix, and the artifact is available. The experiments, especially on lossy channel systems and Petri nets, support the claim that the generic approach is competitive with dedicated tools. The main weakness is the broadcast-protocol section, which omits the well-structured transition system order and monotonicity proof and leaves the transducer encoding of the global broadcast step informal; until those are supplied, the applicability to broadcast protocols is not fully established.

major comments (3)
  1. [Section 5.3 / Section 5 general recipe] The broadcast-protocol section never defines a partial order on configurations nor proves monotonicity of the transition relation. The general recipe in Section 5 relies on the assertion that 'since Pre(X) is upward-closed by monotonicity, Pre_{T_t}(enc(X)) is necessarily weakly acyclic'; for broadcast protocols this inference is not discharged. This is load-bearing because Algorithm 4's correctness (Proposition 10) assumes that the language being transformed is weakly acyclic, so the 32/38 empirical solves cannot be interpreted as soundness evidence until the missing order and monotonicity proof are supplied. Please define the order (e.g., the scattered subword order on state words), prove monotonicity for local, rendez-vous, and broadcast transitions, specify enc(↑C) for this class, and clarify whether the number of processes m is fixed or a parameter.
  2. [Section 5.3 / Figure 6] The transducer encoding for broadcast is underspecified. Broadcast has a global synchronization step ('any other process that can take c?? takes it'), while the operational semantics is given as a length-preserving transducer on words. The paper should specify how a one-pass letter-to-letter transducer guesses the sender and handles receivers that occur before the sender in the word, and it should prove that the transducer's relation coincides with the broadcast transition relation. Without this, it is not clear that Algorithm 4 is being applied to the correct relation.
  3. [Section 6, lossy channel systems experiments] The pre-compatibility tweak 'slightly changes the semantics' of read transitions, and the authors justify it by saying that processes in a common state are indistinguishable and in the benchmarks never share states. This is an unproven, benchmark-specific assumption; the reported comparison with BML and McScM is therefore not strictly a comparison on the original lossy-channel semantics. Please either prove the equivalence for the class of systems considered or clearly state that the comparison is for a restricted-read variant.
minor comments (4)
  1. [Section 2] There is a typo in 'minimial DFA' in the paragraph after Figure 1.
  2. [Section 4.2] The phrase 'exponential worse-case time complexity' should be 'worst-case time complexity'.
  3. [Section 4.3 and Section 5.3] The notation p_(a,b) assumes a total order on the alphabet Σ×Σ for indexing node successor tuples; please state that order explicitly, since the data structure definition in Section 3 only fixes an order for a one-dimensional alphabet.
  4. [Appendix E, Proposition 12 proof] In the monotonicity proof for read transitions, the phrase 'converts w′_i into avy′' appears to be a typo for the suffix after the first a, which is v a y′; as written the notation is confusing.

Circularity Check

0 steps flagged · score 1.0 of 10

No circular derivation: the WAD construction is explicit and self-contained; the only notable gap is an omitted monotonicity/order proof for broadcast protocols, which is a completeness issue, not circularity.

full rationale

The paper's central derivation is self-contained: weakly acyclic languages are defined independently (Section 2), the master automaton (Definition 1) is a representation device whose states are languages, and Proposition 4 only verifies that the recursively defined acceptance semantics agrees with the language labeling — a definitional consistency check, not an empirical prediction. The algorithms in Section 4 are proved directly: complement and intersection by structural induction on residuals (Propositions 15–18), and the Pre procedure via Propositions 8–10, which use the residual characterization of weak acyclicity (Lemma 1) rather than assuming the target result. The uniquification procedure `make` (Algorithm 1) is proved to preserve distinctness by a first-duplicate argument (Proposition 6), and no fitted parameter is renamed as a prediction. Self-citations are not load-bearing: [10] is a pointer to the same full version whose proofs appear in the appendix of this text, [20] is a textbook account of OBDD algorithms reproduced here, and [17,35] supply benchmark instances rather than the theoretical argument. External results on R-trivial languages and poNFAs (e.g., [15,29]) are cited as context, not as the mechanism that makes WADs correct. One genuine gap, flagged in the manuscript itself in the regular-model-checking experiments, is that seven instances require line 9 cycle contraction 'and hence we cannot be certain that the result is weakly acyclic' (Section 6); this is an honest limitation. Similarly, Section 5.3 introduces broadcast protocols and transducers without defining the configuration partial order or proving monotonicity, so the general statement 'since Pre(X) is upward-closed by monotonicity, Pre_{T_t}(enc(X)) is necessarily weakly acyclic' is not discharged for that class in the text and relies on the external result [21]. This is an omission/correctness risk, not circularity, because the missing order can be supplied independently (e.g., the scattered subword order) and no theorem in the paper is shown to be equivalent to its own input.

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

No numerical free parameters are fitted: the theoretical results are parameter-free definitions and proofs. The load-bearing axioms are standard well-quasi-order facts and modeling assumptions that the encodings and transducers exactly capture the semantics of the three system classes. The broadcast-protocol subsection leaves the partial order implicit, which is the largest unstated assumption.

assumptions (6)
  • standard math Higman's lemma: the subword order on channel contents is a well-quasi-order.
    Used in Section 5.1 to guarantee termination of backwards reachability for lossy channel systems.
  • standard math Dickson's lemma: componentwise order on Petri net markings is a well-quasi-order.
    Used in Section 5.2 to guarantee termination for Petri nets.
  • domain assumption For well-structured transition systems, upward-closed sets have finite bases and the backward reachability algorithm terminates.
    Standard theorem from Finkel and Schnoebelen, cited in Section 1 and applied throughout Section 5.
  • domain assumption The fixed-length transducers with X-padding and postprocessing exactly represent the transition relations of the modeled systems.
    Assumed in Sections 5.1-5.3 for lossy channel systems, Petri nets, and broadcast protocols; no complete semantic proof is given for broadcast protocols.
  • domain assumption The partial order for broadcast protocols is the standard subword order, and the transition relation is monotone with respect to it.
    Section 5.3 introduces broadcast protocols but never states the order or proves monotonicity; this is left implicit.
  • ad hoc to paper For LCS benchmarks, the restricted-read transducer tweak does not change safety verification because processes in a common state are indistinguishable and never share a state in the benchmarks.
    Stated in Section 6 as a justification for modifying the transducers to obtain pre-compatibility.
invented entities (2)
  • Weakly acyclic diagrams (WADs) independent evidence
    purpose: Data structure representing finite sets of weakly acyclic languages with OBDD-style operations.
    Implemented in the wadl prototype with benchmark results; the central contribution of the paper.
  • Master automaton
    purpose: Infinite automaton whose states are all weakly acyclic languages; used to define canonical minimal DFAs for WADs.
    Purely definitional theoretical device; not an empirical entity.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Weakly acyclic diagrams: A data structure for infinite-state symbolic verification." pith.science (2026). https://pith.science/paper/YGYOD27I

@misc{pith2026241117250,
  author       = {Pith},
  title        = {Pith review of: Weakly acyclic diagrams: A data structure for infinite-state symbolic verification},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/YGYOD27I}},
  note         = {Machine review of arXiv:2411.17250}
}
read the original abstract

Ordered binary decision diagrams (OBDDs) are a fundamental data structure for the manipulation of Boolean functions, with strong applications to finite-state symbolic model checking. OBDDs allow for efficient algorithms using top-down dynamic programming. From an automata-theoretic perspective, OBDDs essentially are minimal deterministic finite automata recognizing languages whose words have a fixed length (the arity of the Boolean function). We introduce weakly acyclic diagrams (WADs), a generalization of OBDDs that maintains their algorithmic advantages, but can also represent infinite languages. We develop the theory of WADs and show that they can be used for symbolic model checking of various models of infinite-state systems.

Figures

Figures reproduced from arXiv: 2411.17250 by the authors.

Figure 1
Figure 1. Example of a minimal DFA (whose language is weakly acyclic). We say that a DFA A = (Q, Σ, δ, q0, F) is weakly acyclic if for every q ∈ Q, w ∈ Σ+ and a ∈ α(w), it is the case that δ(q, w) = q implies δ(q, a) = q. For example, [PITH_FULL_IMAGE:figures/full_fig_p004_1.png] view at source ↗
Figure 2
Figure 2. Example of the representation of weakly acyclic languages. identifier succ. tuple flag a b p self qΣ∗ 1 qΣ∗ self self 1 We will avoid this: we will maintain a table of nodes such that the language of distinct nodes is distinct. The procedure make of Algorithm 1 serves this purpose. Given a successor tuple s and an acceptance flag b, it first checks whether there is already an entry for language L(s, b), and if not i… view at source ↗
Figure 3
Figure 3. Left: A transducer T that converts each occurrence of letter c into letter b. Right: A weakly acyclic DFA A accepting language (a + b) ∗ c. Yet, under the guarantee that the resulting language is weakly acyclic, we can compute PostR(L) and PreR(L). The key observation is that if a DFA accepting a weakly acyclic language has a cycle, then this cycle can be “contracted”. Thus, given a transducer T and a node q, we app… view at source ↗
Figures from the paper (5 more)
Figure 4
Figure 4. Figure 4: Left: Example of a lossy channel system with Γ = {a, b}. Right: Transducers encoding respectively the transitions read1(a), write2(b) and nop (under the semi-lossy semantics), where s ∈ {p, q, r}, σ ∈ {a, b} and γ stands for any letter. For example, consider the channe…
Figure 5
Figure 5. Figure 5: Left: Example of a Petri net where P = {p, q}, T = {t}, F(p, t) = 2, F(t, p) = 1 = F(q, t) and F(t, q) = 3. Right: Transducer encoding transition t [PITH_FULL_IMAGE:figures/full_fig_p014_5.png]
Figure 6
Figure 6. Figure 6: Left: Example of a broadcast protocol with P = {p, q, r}, Γ = ∅, Γ ′ = {b} and Γ ′′ = {c}. Middle and right: Transducers encoding the transitions, where s ∈ {p, q, r}. 6 Experimental results We developed a prototype C++ library for weakly acyclic diagrams, which we ref…
Figure 7
Figure 7. Figure 7: wadl solves the most instances and does so generally faster, although the competition is close. We further tested the same tools on ring3, ring4, etc. Our tool terminates on large n (e.g. ring99 in 2m38s and ring187 is the largest solved), but the other tools did not s…
Figure 8
Figure 8. Figure 8: Cumulative number of instances decided by wadl over time (semi-log scale) for broadcast protocols (left) and for the other regular model checking instances (right) [PITH_FULL_IMAGE:figures/full_fig_p029_8.png]

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

36 extracted references · 27 canonical work pages

  1. [1]

    International Journal on Software Tools for Technology Transfer 14(2), 109–118 (2012)

    Abdulla, P.A.: Regular model checking. International Journal on Software Tools for Technology Transfer 14(2), 109–118 (2012). https://doi.org/10.1007/ S10009-011-0216-8

    work page 2012

  2. [2]

    In: Model Checking, Synthesis, and Learning – Essays Dedicated to Bengt Jonsson on The Occasion of His 60th Birthday

    Abdulla, P.A.: Regular model checking: Evolution and perspectives. In: Model Checking, Synthesis, and Learning – Essays Dedicated to Bengt Jonsson on The Occasion of His 60th Birthday. Lecture Notes in Computer Science, vol. 13030, pp. 78–96. Springer (2021). https://doi.org/10.1007/978-3-030-91384-7_5

    work page doi:10.1007/978-3-030-91384-7_5 2021

  3. [3]

    In: Proc

    Abdulla, P.A., Cerans, K., Jonsson, B., Tsay, Y.: General decidability theorems for infinite-state systems. In: Proc. 11th Annual IEEE Symposium on Logic in Computer Science (LICS). pp. 313–321. IEEE Computer Society (1996). https: //doi.org/10.1109/LICS.1996.561359

    arXiv 1996

  4. [4]

    In: Proc

    Abdulla, P.A., Jonsson, B.: Verifying programs with unreliable channels. In: Proc. 8th Annual Symposium on Logic in Computer Science (LICS). pp. 160–170 (1993). https://doi.org/10.1109/LICS.1993.287591

    arXiv 1993

  5. [5]

    In: Proc

    Abdulla, P.A., Jonsson, B., Nilsson, M., Saksena, M.: A survey of regular model checking. In: Proc. 15 th International Conference on Concurrency The- ory (CONCUR). vol. 3170, pp. 35–48. Springer (2004). https://doi.org/10.1007/ 978-3-540-28644-8_3

    work page 2004

  6. [6]

    In: Proc

    Abdulla, P.A., Kindahl, M.: Decidability of simulation and bisimulation between lossy channel systems and finite state systems (extended abstract). In: Proc. 6th International Conference on Concurrency Theory (CONCUR). vol. 962, pp. 333–

    work page

  7. [7]

    In: Handbook of Model Checking, pp

    Abdulla, P.A., Sistla, A.P., Talupur, M.: Model checking parameterized systems. In: Handbook of Model Checking, pp. 685–725. Springer (2018). https://doi.org/ 10.1007/978-3-319-10575-8_21

    work page doi:10.1007/978-3-319-10575-8_21 2018

  8. [8]

    IEEE Transactions on Computers27(6), 509– 516 (1978), https://doi.org/10.1109/TC.1978.1675141

    Akers, S.: Binary decision diagrams. IEEE Transactions on Computers27(6), 509– 516 (1978), https://doi.org/10.1109/TC.1978.1675141

    arXiv 1978

Show all 36 references
  1. [9]

    Andersen, H.R.: An introduction to binary decision diagrams (1998)

    1998

  2. [10]

    CoRR abs/2411.17250 (2024)

    Blondin, M., Cadilhac, M., Cui, X., Czerner, P., Esparza, J., Schulz, J.: Weakly acyclic diagrams: A data structure for infinite-state symbolic verification. CoRR abs/2411.17250 (2024). https://doi.org/10.48550/arXiv.2411.17250

    2024 doi arXiv

  3. [11]

    Formal Methods in System Design (FMSD) 14(3), 237–255 (1999)

    Boigelot, B., Godefroid, P.: Symbolic verification of communication protocols with infinite state spaces using QDDs. Formal Methods in System Design (FMSD) 14(3), 237–255 (1999). https://doi.org/10.1023/A:1008719024240

    1999 doi

  4. [12]

    Information and Computation205(2), 199–224 (2007)

    Bouajjani, A., Muscholl, A., Touili, T.: Permutation rewriting and algorithmic verification. Information and Computation205(2), 199–224 (2007). https://doi. org/10.1016/J.IC.2005.11.007

    2007 doi

  5. [13]

    IEEE Transactions on Computers35(8), 677–691 (1986)

    Bryant, R.E.: Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers35(8), 677–691 (1986). https://doi.org/10.1109/TC. 1986.1676819

    1986

  6. [14]

    In: Handbook of Model Checking, pp

    Bryant, R.E.: Binary decision diagrams. In: Handbook of Model Checking, pp. 191–217. Springer (2018). https://doi.org/10.1007/978-3-319-10575-8_7

    2018 doi

  7. [15]

    Journal of Computer and System Sciences20(1), 32–49 (1980), https://doi.org/10.1016/0022-0000(80) 90003-3

    Brzozowski, J.A., Fich, F.E.: Languages ofR-trivial monoids. Journal of Computer and System Sciences20(1), 32–49 (1980), https://doi.org/10.1016/0022-0000(80) 90003-3

    1980 doi

  8. [16]

    In: Handbook of Model Checking, pp

    Chaki, S., Gurfinkel, A.: BDD-based symbolic model checking. In: Handbook of Model Checking, pp. 219–245. Springer (2018). https://doi.org/10.1007/ 978-3-319-10575-8_8 WADs: a data structure for infinite-state symbolic verification 19

    2018

  9. [17]

    In: Proc

    Czerner, P., Esparza, J., Krasotin, V., Welzel-Mohr, C.: Computing inductive in- variants of regular abstraction frameworks. In: Proc. 35th International Confer- ence on Concurrency Theory (CONCUR). LIPIcs, vol. 311, pp. 19:1–19:18 (2024). https://doi.org/10.4230/LIPICS.CONCUR...

    2024

  10. [18]

    International Journal on Software Tools for Technology Transfer (STTT)5(2-3), 268–297 (2004)

    Delzanno, G., Raskin, J., Begin, L.V.: Covering sharing trees: a compact data structure for parameterized verification. International Journal on Software Tools for Technology Transfer (STTT)5(2-3), 268–297 (2004). https://doi.org/10.1007/ S10009-003-0110-0

    2004

  11. [19]

    Eilenberg, S.: Automata, Languages, and Machines, vol. B. Academic Press (1976)

    1976

  12. [20]

    MIT Press (2023)

    Esparza, J., Blondin, M.: Automata theory: An algorithmic approach. MIT Press (2023)

    2023

  13. [21]

    In: Proc

    Esparza, J., Finkel, A., Mayr, R.: On the verification of broadcast protocols. In: Proc. 14th Annual IEEE Symposium on Logic in Computer Science (LICS). pp. 352–359. IEEE Computer Society (1999). https://doi.org/10.1109/LICS.1999. 782630

    1999 doi

  14. [22]

    In: Proc

    Esparza, J., Ledesma-Garza, R., Majumdar, R., Meyer, P.J., Niksic, F.: An SMT- based approach to coverability analysis. In: Proc. 26th International Conference on Computer Aided Verification (CAV). pp. 603–619. Springer (2014). https://doi. org/10.1007/978-3-319-08867-9_40

    2014 doi

  15. [23]

    https://doi.org/10.1016/ S0304-3975(00)00102-X

    Finkel, A., Schnoebelen, Ph.: Well-structured transition systems everywhere! Theoretical Computer Science 256(1-2), 63–92 (2001). https://doi.org/10.1016/ S0304-3975(00)00102-X

    2001

  16. [24]

    Ganty, P., Meuter, C., Delzanno, G., Kalyon, G., Raskin, J.F., Van Begin, L.: Symbolic data structure for sets ofk-uples. Tech. Rep. 570, Université Libre de Bruxelles, Belgium (2007)

    2007

  17. [25]

    In: Proc

    Geffroy, T., Leroux, J., Sutre, G.: Backward coverability with pruning for lossy channel systems. In: Proc. 24 th ACM SIGSOFT International Symposium on Model Checking of Software (SPIN). pp. 132–141. ACM (2017). https://doi.org/ 10.1145/3092282.3092292, The tool BML and the l...

    2017

  18. [26]

    In: Proc

    Heußner, A., Gall, T.L., Sutre, G.: Extrapolation-based path invariants for ab- straction refinement of FIFO systems. In: Proc. 16 th International on Model Checking Software (SPIN). pp. 107–124. Springer (2009). https://doi.org/10. 1007/978-3-642-02652-2_11, The tool McScM is...

    2009

  19. [27]

    In: Proc

    Heußner,A.,Gall,T.L.,Sutre,G.:McScM:Ageneralframeworkfortheverification of communicating machines. In: Proc. 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). pp. 478–484. Springer (2012). https://doi.org/10.1007/978-3-...

    2012 doi

  20. [28]

    BRICS, Department of Computer Science, University of Aarhus (January 2001), notes Series NS-01-1

    Klarlund, N., Møller, A.: MONA Version 1.4 User Manual. BRICS, Department of Computer Science, University of Aarhus (January 2001), notes Series NS-01-1. Available from http://www.brics.dk/mona/

    2001

  21. [29]

    Information and Computation255, 177–192 (2017)

    Krötzsch, M., Masopust, T., Thomazo, M.: Complexity of universality and related problems for partially ordered NFAs. Information and Computation255, 177–192 (2017). https://doi.org/10.1016/j.ic.2017.06.004

    2017 doi

  22. [30]

    Logical Methods in Computer Science17(2) (2021)

    Masopust, T., Krötzsch, M.: Partially ordered automata and piecewise testabil- ity. Logical Methods in Computer Science17(2) (2021). https://doi.org/10.23638/ LMCS-17(2:14)2021

    2021

  23. [31]

    Proceedings of the IEEE 77(4), 541–580 (1989)

    Murata, T.: Petri nets: Properties, analysis and applications. Proceedings of the IEEE 77(4), 541–580 (1989). https://doi.org/10.1109/5.24143 20 M. Blondin et al

    1989 doi

  24. [32]

    North Oxford, London and Plenum (1986)

    Éric Pin, J.: Varieties of formal languages. North Oxford, London and Plenum (1986)

    1986

  25. [33]

    In: Proc

    Ryzhikov, A., Wolf, P.: Monoids of upper triangular matrices over the Boolean semiring. In: Proc. 49th International Symposium on Mathematical Foundations of Computer Science (MFCS). LIPIcs, vol. 306, pp. 81:1–81:18 (2024). https://doi. org/10.4230/LIPICS.MFCS.2024.81

    2024 doi

  26. [34]

    In: Proc

    Schwentick, T., Thérien, D., Vollmer, H.: Partially-ordered two-way automata: A new characterization of DA. In: Proc. 5th International Conference on Devel- opments in Language Theory (DLT). vol. 2295, pp. 239–250. Springer (2001). https://doi.org/10.1007/3-540-46011-X_20

    2001 doi

  27. [35]

    ¬flag(q)

    Welzel-Mohr, C.: Inductive Statements for Regular Transition Systems. Ph.D. the- sis, Technical University of Munich, Germany (2024), https://mediatum.ub.tum. de/1721365 WADs: a data structure for infinite-state symbolic verification 21 A Missing proofs of Section 2 Propositio...

    2024

  28. [347]

    https://doi.org/10.1007/3-540-60218-6_25

    Springer (1995). https://doi.org/10.1007/3-540-60218-6_25

    1995 doi

Pith tools

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