Pith. sign in

REVIEW 2 major objections 4 minor 23 references

On the k-synchronizability of systems

T0 review · 2 major / 4 minor · reviewed 2026-08-14 · deepseek-v4-flash

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

Pith's one-line read Both reachability and k-synchronizability are decidable for k-synchronizable systems.

desk verdict A mostly solid repair of known decidability claims for k-synchronizable systems, but one printed typo in the central transition relation (Fig. 4) breaks the proof as written. read the letter →

arxiv 1909.01627 v2 pith:O5KS5I7H submitted 2019-09-04 cs.FL cs.CLcs.SCcs.SE

Cinzia Di Giusto (C&A) , Cinzia Giusto (SARDES) , Laetitia Laversa (C&A) , Etienne Lozes This is my paper · ORCID
classification cs.FLcs.CLcs.SCcs.SE MSC 68Q4568Q8568Q60
keywords k-synchronizabilitycommunicatingautomatamailboxcommunicationpeer-to-peerreachabilitydecidabilitycausaldeliverymessagesequencecharts
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 proves that two basic verification questions are decidable for k-synchronizable communicating systems: whether a given global state is reachable, and whether a given system is k-synchronizable in the first place. A system is k-synchronizable when every execution, up to reordering causally independent actions, can be split into rounds that start with at most k sends and end with at most k matching receives. The results hold for both mailbox communication, where each receiver has one FIFO queue, and peer-to-peer communication, where each pair of processes has private FIFO queues. Along the way, the paper corrects two earlier decidability proofs for mailbox automata that had produced false positives and false negatives.

What carries the argument

The central object is the extended conflict graph of an MSC, whose vertices are message exchanges and whose edges record causal order imposed by process timelines, message matching, and mailbox FIFO order. The paper augments this graph with per-process summary nodes $\psi_p$ and two process sets $C_{S,p}$ and $C_{R,p}$, which carry across k-exchange boundaries exactly the information about unmatched sends needed to detect causal-delivery violations. The abstract transition relation $\overset{e,k}{\Longrightarrow}_{cd}$ updates these sets and rejects any k-exchange sequence whose extended conflict graph contains a cycle of the form $v \xrightarrow{SS} v$. For membership, an instrumented system $S'$ adds a forwarding process $\pi$, and the existence of a feasible bad execution is recognized by finite-state relations $\overset{e,k}{\Longrightarrow}_{feas}$ and $\overset{e,k}{\Longrightarrow}_{bad}$, reducing decidability to NFA emptiness.

What would settle it

Enumerate all MSCs over a small system, say three processes and three messages with k=2, and compare the language accepted by the abstract transition relation $\overset{e,k}{\Longrightarrow}_{cd}$ against the actual set of k-synchronous MSCs; any accepted MSC that violates causal delivery, or any k-synchronous MSC that is rejected, would disprove Lemma 1 and the reachability decidability theorem.

Watch

Extended reading notes

Core claim

The central claim is that the set of k-synchronous message sequence charts (MSCs) of a communicating system is a regular language, and this regularity makes both reachability and k-synchronizability decidable. Concretely, the paper proves a graph-theoretic characterization: an MSC satisfying causal delivery is k-synchronous exactly when every strongly connected component of its conflict graph has size at most k and no RS edge lies on a cyclic path. It then builds finite-state abstract transition relations that recognize exactly the sequences of k-exchanges satisfying causal delivery, using summary nodes and per-process sets of causally affected senders and receivers. These abstractions yield decidability of reachability for k-synchronizable mailbox and peer-to-peer systems, and, with an instrumented system containing a special forwarding process, decidability of whether a given system is k-synchronizable.

Load-bearing premise

The argument assumes that carrying only the two per-process sets $C_{S,p}$ and $C_{R,p}$ together with summary nodes from one k-exchange to the next preserves every causal-delivery violation that could arise between exchanges; if some cross-exchange dependency is invisible to these sets, the reachability decidability proof collapses.

Editorial extensions

If this is right

  • Reachability of a global control state in any k-synchronizable mailbox or peer-to-peer system is decidable, even when some executions use buffers larger than k.
  • Deadlock-freedom, unspecified receptions, and absence of orphan messages become decidable for k-synchronizable systems, as noted in the paper's Remark 2.
  • Whether a given system is k-synchronizable is decidable for every k at least 1, in both mailbox and peer-to-peer settings.
  • The corrected characterization implies that earlier Hamiltonian-cycle-based algorithms for k-synchronizability are unsound, so verification tools must check SCC sizes and the absence of RS edges on cycles instead.

Reading between the lines

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

  • The finite-state abstractions presented here translate directly into algorithms: one can build the automata for feasible and bad executions and test emptiness, though the paper does not analyze the resulting complexity.
  • The causal-delivery characterization via SS-cycles in the extended conflict graph likely transfers to other buffering disciplines, such as bags or per-sender queues, by adjusting only the graph rules in Figure 3.
  • The paper's closing conjecture, that forbidding linearisations that are not actual executions would simplify the development, suggests that the separate feasibility machinery might be absorbed into the reachability abstraction if the conjecture holds.
  • The peer-to-peer case needs only forbidden-sender sets rather than the richer summary-node structure, hinting that peer-to-peer k-synchronizability verification may be algorithmically lighter than mailbox verification.
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

2 major / 4 minor

Summary. The paper studies k-synchronizability for communicating automata with mailbox and peer-to-peer semantics. It gives a graph-theoretic characterization of k-synchronous MSCs and of causal delivery, then builds finite-state abstract transition relations to show that reachability is decidable for k-synchronizable systems (Theorems 3 and 5) and that k-synchronizability itself is decidable (Theorems 4 and 6), while repairing flaws in the earlier work [4]. The main technical device is a summary-node abstraction (the nodes ψ_p) that carries the inter-k-exchange information needed to detect causal-delivery violations, together with instrumented-system constructions for the membership problem.

Significance. If the constructions are correct, the paper makes a substantial contribution: it identifies concrete errors in [4] (Example 2 for the SCC/Hamiltonian-cycle issue, Fig. 5 for causal delivery, Example 8 for the feasibility monitor), provides self-contained proofs in an appendix, extends both decidability results to peer-to-peer systems, and states crisp graph-theoretic characterizations (Theorems 1 and 2). The claimed decidability results are the kind of foundational facts that the verification community needs to be able to rely on, so the paper is worth publishing once the technical issues below are resolved.

major comments (2)
  1. [§4, Fig. 4] The last union term in the definition of C′_{X,p} reads {procX(v′) | v SS -> v′, v ∈ Unmp, v ∩ X ≠ ∅}. For X = R this clause is vacuous, because every v ∈ Unmp is either an unmatched send or a summary node ψ_p, so v ∩ R is always empty. Yet C_{R,p} is supposed to record the receivers of messages sent causally after an unmatched send, and the paper's own Example 4 and Fig. 5c state that for e1 = send(q,r,v1) · send(q,s,v2) · rec(q,s,v2), the computation yields C′_{R,r} = {s}. With the printed guard, C′_{R,r} remains empty. Since Lemma 1 and hence Theorem 3 (as well as the feasibility construction in §5, which reuses these sets) depend on this transition relation, the printed definition is not sound. The natural fix is to replace the guard v ∩ X ≠ ∅ by v′ ∩ X ≠ ∅, which would restore Example 4 and the intended invariant, but the manuscript must be corrected and the proof of Lemma 1 rechecked under that correction.
  2. [§4, proof of Lemma 1] The inductive invariants stated at the start of the proof of Lemma 1 do not match the definitions of C_{S,p} and C_{R,p} in §4. In the main text, C_{S,p} is defined as {procS(v) | v′ SS -> v, v′ unmatched, procR(v′) = p} and C_{R,p} as {procR(v) | v′ SS -> v, v′ unmatched, procR(v′) = p, v ∩ R ≠ ∅}. In the proof, however, the induction hypothesis is written as C_{S,p} = {procS(v′) | v SS -> v′, v not matched, procS(v) = p} and C_{R,p} = {procR(v′) | v SS -> v′, v not matched, procR(v) = p, v′ ∩ R ≠ ∅}. These are different sets indexed by different processes, so the induction is not anchored to the same invariant as the transition relation in Fig. 4. This discrepancy must be repaired for the proof of Theorem 3 to be sound as written.
minor comments (4)
  1. [§3, Theorem 1] The condition "no RS edge occurs on any cyclic path" is slightly imprecise; the proof in the appendix works with strongly connected components and cycles, so it would be clearer to state the condition as "no RS edge occurs on any cycle".
  2. [§4, Fig. 4] The variable p is used both as the index of the set being updated and as a bound variable in the second union term of C′_{X,p} (the term {p | p ∈ C_{X,q}, ...}). This overloading makes the rule hard to read and should be renamed.
  3. [§5, Definition 9] The examples illustrating feasibility and badness (Fig. 8) are placed in Appendix A rather than in the main text; a forward reference from Definition 9 would help the reader connect the definitions to the counterexamples.
  4. [Throughout] The arrow symbols in the submitted text appear as garbled tokens such as "/axisshort/axisshort/arrowaxisright"; the final version should use proper glyphs for the extended-edge relation.

Circularity Check

0 steps flagged · score 0.0 of 10

Self-contained decidability proofs; no prediction reduces to fitted input or self-citation.

full rationale

The paper's central claims are Theorems 3-6, which establish decidability by constructing finite-state abstract transition relations. The proof chain is: Definition 6 defines k-synchronous MSCs; Theorem 1 gives a graph-theoretic characterization proved directly from that definition; Theorem 2 characterizes causal delivery via extended conflict graphs and is proved from Definition 4; Lemma 1 shows that the finite abstraction of Fig. 4 accepts exactly the k-synchronous MSCs, with a long induction relating local abstract transitions to edges of the global extended conflict graph. The reachability decidability then follows from finiteness of abstract configurations, not from assuming the target result. The membership decidability similarly builds automata for feasible and bad executions (Lemmas 4-6) and proves an iff characterization with Lemma 2. No parameter is fitted to the target result: the sets C_{S,p} and C_{R,p} are defined uniformly and the acceptance condition p not in C'_{R,p} is not calibrated against a particular system or reachability query. The relationship to [4] is explicitly corrective: the paper identifies flaws in earlier proofs and supplies new constructions, so the earlier work is not an unverified load-bearing premise. The only self-citation involving the authors ([9], Finkel and Lozes) appears in the related-work discussion of a different synchronizability notion and is not used to justify any theorem. The skeptic's observation about the guard 'v ∩ X ≠ ∅' in Fig. 4 is a potential soundness defect in the printed transition relation, not a circular reduction: even if the clause needs correction, the proof does not assume its own conclusion. Therefore there is no significant circularity.

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

The paper introduces no fitted parameters. It relies on the standard communicating-automata model and standard automata-theoretic facts, both stated in the paper. The only new constructs are proof artifacts (summary nodes, the forwarder process π), which are fully defined and carry no independent empirical postulation.

assumptions (3)
  • domain assumption Communicating automata with unbounded FIFO buffers (mailbox: one buffer per receiver; peer-to-peer: one buffer per sender-receiver pair) is the target model for k-synchronizability.
    The decidability results are stated for this model (Definitions 2, 11, 12). A different buffer discipline would require re-evaluation.
  • domain assumption Every non-k-synchronizable system admits a borderline violation of the form e'·r with r a receive action.
    Stated and argued in Section 5 before Lemma 2; it is a well-foundedness argument over finite prefixes and is essential for reducing non-k-synchronizability to the existence of a feasible bad execution.
  • standard math Standard automata-theoretic facts: finite automata can recognize k-exchanges over a finite alphabet, and emptiness is decidable for finite automata.
    Invoked in Theorems 3 and 4 to conclude decidability from the finite-state transition relations.
invented entities (2)
  • Forwarder process π (instrumented system S')
    purpose: Receives messages deviated from their original destination and later forwards them, enabling detection of borderline violations (Definition 10).
    A proof artifact with exact transition rules; it is not an empirical postulation and provides no independent falsifiable handle on the world.
  • Summary nodes ψ_p in extended conflict graphs
    purpose: Abstract all past unmatched messages directed to process p so that causal delivery can be checked with finite memory across k-exchanges (Section 4, Fig. 4).
    Internal to the proof of Lemma 1; they are not observable behaviors of the original system.

how reviews work

0 comments
Cite this review

Pith. "Pith review of On the k-synchronizability of systems." pith.science (2026). https://pith.science/paper/O5KS5I7H

@misc{pith2026190901627,
  author       = {Pith},
  title        = {Pith review of: On the k-synchronizability of systems},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/O5KS5I7H}},
  note         = {Machine review of arXiv:1909.01627}
}
read the original abstract

In this paper, we work on the notion of k-synchronizability: a system is k-synchronizable if any of its executions, up to reordering causally independent actions, can be divided into a succession of k-bounded interaction phases. We show two results (both for mailbox and peer-to-peer automata): first, the reachability problem is decidable for k-synchronizable systems; second, the membership problem (whether a given system is k-synchronizable) is decidable as well. Our proofs fix several important issues in previous attempts to prove these two results for mailbox automata.

Figures

Figures reproduced from arXiv: 1909.01627 by the authors.

Figure 1
Figure 1. (a) and (b): two MSCs that violate causal delivery. (c) and ( [PITH_FULL_IMAGE:figures/full_fig_p004_1.png] view at source ↗
Figure 2
Figure 2. (a) the MSC of Example 1.1. (b) the MSC of Example 1.2. (c) the [PITH_FULL_IMAGE:figures/full_fig_p006_2.png] view at source ↗
Figure 3
Figure 3. Deduction rules for extended dependency edges of the con [PITH_FULL_IMAGE:figures/full_fig_p008_3.png] view at source ↗
Figures from the paper (9 more)
Figure 4
Figure 4. Figure 4: Definition of the relation e,k ==⇒ cd all past unmatched messages sent to p that occurred in some k-exchange before e. E′ is the set E of edges XY −→ among message exchanges of e, as in Definition 5, augmented with the following set of extra edges taking into account t…
Figure 5
Figure 5. Figure 5: (a) an MSC (b) its associated global conflict graph, (c) the c [PITH_FULL_IMAGE:figures/full_fig_p010_5.png]
Figure 6
Figure 6. Figure 6: Definition of the relation e,k ===⇒ feas Comparison with [4]. In [4] the authors verify that an execution is feasible with a monitor which reviews the actions of the execution and adds processes that no longer are allowed to send a message to the receiver of π. Unfortu…
Figure 7
Figure 7. Figure 7: Definition of the relation e,k ===⇒ bad and at least one of the two holds: either sawRS = True, or cnt = k + 2. Comparison with [4]. As for the notion of feasibility, to determine if an execution is bad, in [4] the authors use a monitor that builds a path between the s…
Figure 8
Figure 8. Figure 8: MSCs of problematic executions A Comparison with [4] (Examples and additional material) Let po and src be the partial orders on the set of actions obtained respectively from ≺po and ≺src by assuming that if i ≺po j then λ(i) < λ(j) ∈ po and if i ≺src j then λ(i) < λ(j)…
Figure 9
Figure 9. Figure 9: MSCs violating causal delivery This entails that msc(e1) satisfies causal delivery. However, there is no execution corresponding to this MSC as it is impossible to find a linearisation of msc(e1). In our Definition 4, instead, we add the requirement that a linearisatio…
Figure 10
Figure 10. Figure 10: Definition of transition e,k ==⇒ cd p2p in a peer-to-peer system Definition 13 (Peer-to-peer causal delivery). Let msc = (Ev, λ, ≺) be an MSC. We say that msc satisfies causal delivery if there is a linearisation e = a1 . . . an such that for any two send events i ≺ j…
Figure 11
Figure 11. Figure 11: Definition of transition e,k ===⇒ feas p2p in a peer-to-peer system Proof. There are only finitely many abstract configurations of the form (~l, B) with ~l a tuple of control states and B : P → (2P ). Therefore e,k ==⇒ cd p2p is a rela￾tion on a finite set, and the se…
Figure 12
Figure 12. Figure 12: Definition of the relation e,k ===⇒ bad p2p in a peer-to-peer system rec(π, q, v). Then there is one and only one send to π such that expπ = p and destπ = q. By contradiction, suppose that there is a matched message v ′ = {ai , aj} belonging to a k-exchange in e ′ 2 s…

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

23 extracted references · 14 canonical work pages

  1. [4]

    In: Chockl er, H., Weissenbacher, G

    Bouajjani, A., Enea, C., Ji, K., Qadeer, S.: On the complet eness of verifying mes- sage passing programs under bounded asynchrony. In: Chockl er, H., Weissenbacher, G. (eds.) Computer Aided Verification - 30th International C onference, CA V 2018, Held as Part of the Federated Logic Conference, FloC 2018, Ox ford, UK, July 14- 17, 2018, Proceedings, Part ...

    doi:10.1007/9 2018

  2. [1]

    Formal Methods in System De - sign 52(3), 260–276 (2018)

    Akroun, L., Sala¨ un, G.: Automated verification of automa ta commu- nicating via FIFO and bag buffers. Formal Methods in System De - sign 52(3), 260–276 (2018). https://doi.org/10.1007/s10703-01 7-0285-8, https://doi.org/10.1007/s10703-017-0285-8

    work page doi:10.1007/s10703-01 2018

  3. [2]

    Basu, S., Bultan, T.: On deciding synchronizability for a syn- chronously communicating systems. Theor. Comput. Sci. 656, 60–75 (2016). https://doi.org/10.1016/j.tcs.2016.09. 023, https://doi.org/10.1016/j.tcs.2016.09.023

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

  4. [5]

    In: Alur, R., Peled, D.A

    Bouajjani, A., Habermehl, P., Vojnar, T.: Abstract regul ar model check- ing. In: Alur, R., Peled, D.A. (eds.) Computer Aided Verifica tion, 16th International Conference, CA V 2004, Boston, MA, USA, July 1 3-17, 2004, Proceedings. Lecture Notes in Computer Science, vol. 3114, pp. 372–386. Springer (2004). https://doi.org/10.1007/978- 3-540-27813-9 29, htt...

    doi:10.1007/978- 2004

  5. [6]

    In: Bourne z, O., Potapov, I

    Chaouch-Saad, M., Charron-Bost, B., Merz, S.: A reductio n theorem for the veri- fication of round-based distributed algorithms. In: Bourne z, O., Potapov, I. (eds.) Reachability Problems, 3rd International Workshop, RP 200 9, Palaiseau, France, September 23-25, 2009. Proceedings. Lecture Notes in Compu ter Science, vol. 5797, pp. 93–106. Springer (2009). ...

    doi:10.1007/97 2009

  6. [7]

    In: Dolev, D

    Chou, C., Gafni, E.: Understanding and verifying distrib uted algorithms us- ing stratified decomposition. In: Dolev, D. (ed.) Proceedin gs of the Sev- enth Annual ACM Symposium on Principles of Distributed Comp uting, Toronto, Ontario, Canada, August 15-17, 1988. pp. 44–65. AC M (1988). https://doi.org/10.1145/62546.62556, https://doi.org/10.1145/62546.62556

    arXiv 1988

  7. [8]

    Elrad, T., Francez, N.: Decomposition of distributed pro grams into communication-closed layers. Sci. Comput. Program. 2(3), 155–173 (1982). https://doi.org/10.1016/0167-6423(83) 90013-8, https://doi.org/10.1016/0167-6423(83)90013-8

    work page doi:10.1016/0167-6423(83 1982

  8. [9]

    In: Chatzigiannakis, I., Indyk, P., Kuhn, F., Muscholl, A

    Finkel, A., Lozes, ´E.: Synchronizability of communicating finite state machines is not decidable. In: Chatzigiannakis, I., Indyk, P., Kuhn, F., Muscholl, A. (eds.) 44th International Colloquium on Au tomata, Languages, and Programming, ICALP 2017, July 10-14, 2017, W arsaw, 20 C. Di Giusto et al. Poland. LIPIcs, vol. 80, pp. 122:1–122:14. Schloss Dagstuh ...

    work page doi:10.4230/lipics.icalp.2017.122 2017

Show all 23 references
  1. [10]

    Genest, B., Kuske, D., Muscholl, A.: On communicating au tomata with bounded channels. Fundam. Inform. 80(1-3), 147–167 (2007), http://content.iospress.com/articles/fundamenta-informaticae/fi80-1-3-09

    2007

  2. [11]

    , Jhala, R.: Pre- tend synchrony: synchronous verification of asynchronous d istributed pro- grams

    von Gleissenthall, K., Kici, R.G., Bakst, A., Stefan, D. , Jhala, R.: Pre- tend synchrony: synchronous verification of asynchronous d istributed pro- grams. PACMPL 3(POPL), 59:1–59:30 (2019). https://doi.org/10.1145/329 0372, https://doi.org/10.1145/3290372

    2019 doi

  3. [12]

    In: Schewe, S., Zhang, L

    Kragl, B., Qadeer, S., Henzinger, T.A.: Synchronizing t he asynchronous. In: Schewe, S., Zhang, L. (eds.) 29th International Confere nce on Con- currency Theory, CONCUR 2018, September 4-7, 2018, Beijing , China. LIPIcs, vol. 118, pp. 21:1–21:17. Schloss Dagstuhl - Leibni z-Ze...

    2018 doi

  4. [13]

    In: Ramakrishnan, C.R., Rehof, J

    La Torre, S., Madhusudan, P., Parlato, G.: Context-boun ded analysis of con- current queue systems. In: Ramakrishnan, C.R., Rehof, J. (e ds.) Tools and Algorithms for the Construction and Analysis of Systems, 14 th International Conference, TACAS 2008, Held as Part of the Join...

    2008

  5. [14]

    Lipton, R.J.: Reduction: A method of proving properties of parallel programs. Commun. ACM 18(12), 717–721 (1975). https://doi.org/10.1145/361227.3 61234, https://doi.org/10.1145/361227.361234

    1975

  6. [15]

    In: D ediu, A., Fernau, H., Mart ´ ın-Vide, C

    Muscholl, A.: Analysis of communicating automata. In: D ediu, A., Fernau, H., Mart ´ ın-Vide, C. (eds.) Language and Automata Theory an d Appli- cations, 4th International Conference, LATA 2010, Trier, G ermany, May 24-28, 2010. Proceedings. Lecture Notes in Computer Scienc e,...

    2010 doi

  7. [16]

    v ∈ V , then both message exchanges v and v′ with v unmatched and v′ matched are in the current k-exchange then we can easily reach a contradiction and the proof proceeds as in the base case

  8. [17]

    We want to show that if this is the case we can reconstruct a cyclic path in the extended conflict graph, which is a contradiction

    v =ψp, then by inductive hypothesis there exists a non-matched messag e vp ∈V belonging to a previous k-exchange. We want to show that if this is the case we can reconstruct a cyclic path in the extended conflict graph, which is a contradiction. We assume that by inductive hypo...

  9. [18]

    destπ =q if and only if a message of the form ( q, v) was sent to π in e′

  10. [19]

    there is at most one message sent to π in e′

  11. [20]

    The first two points easily follow from the definition of e,k = = =⇒ feas

    let υstart denote the unique vertex in CG(e′) (if it exists) such that procR(υstart) = π; for all X ∈ {S,R }, Cπ X = {procX (v) | (v∩X ⁄= ∅ & υstart SS /axisshort/axisshort/arrowaxisrightv in CG(e′)) or (v,X ) = (υstart,S )}. The first two points easily follow from the definitio...

  12. [21]

    υstart − →∗ RS − →− →∗υstop, or

  13. [22]

    the size of the set Post∗(υstart) ∩ Pre∗(υstop) is greater or equal to k + 2. Proof. Since msc(e′) is k-synchronous and e′ = deviate(e ·r), msc(e) (without the last reception r) is k-synchronous. By Theorem 1, e′ is bad if and only if CG(e ·r) contains either a cyclic path wit...

  14. [23]

    If sawRS = True then ∃ei where sawRS = False and sawRS′ = True

    We suppose that sawRS = True. If sawRS = True then ∃ei where sawRS = False and sawRS′ = True. In this k-exchange, ∃p ∈ P such that p ∈ P , lastisRec(p) = True and ∃v such that procS(v) = p and v ∈ Pree′ (Q′). Since p ∈ P , then there is a path υstart − →∗ RS − →v in CG(e′). On...

  15. [24]

    As previously, e′ is feasible by Lemma 4

    We suppose that cnt = k + 2. As previously, e′ is feasible by Lemma 4. Eachv belongs to Postei (Pi) ∩ Preei (Q′ i) \υstart also belongs to Post∗(υstart) ∩ Pre∗(υstop) then | Post∗(υstart) ∩ Pre∗(υstop) |≥k + 2. Therefore, e′ is bad. Therefore, in both cases, e′ is feasible and...

Pith tools

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