Pith. sign in

REVIEW 4 major objections 4 minor 38 references

Verification of Flat FIFO Systems

T0 review · 4 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 For flat FIFO machines—finite-state systems with unbounded message queues and at most one loop per state—reachability and six related verification problems are NP-complete, while cyclicity is decidable in linear time.

desk verdict Solid NP-completeness results for flat FIFO machines, with a mislabeled theorem on termination/boundedness that should not be cited as-is. read the letter →

arxiv 1908.07282 v5 pith:IUI4O6M4 submitted 2019-08-20 cs.CC cs.LO

Alain Finkel , M. Praveen This is my paper · ORCID
classification cs.CCcs.LO MSC 68Q1768Q4568Q60
keywords flatFIFOmachinesreachabilityNP-completenesslossychannelsystemscounterloopaccelerationtrace-flatteningLTLmodelchecking
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

Flat FIFO machines are finite-state systems with unbounded first-in first-out message channels whose control graph visits each state in at most one loop; they are the standard under-approximation for verifying general FIFO protocols. The paper closes a long-open question by proving that reachability, repeated reachability, repeated control-state reachability, non-termination, unboundedness, channel-unboundedness, and letter-channel-unboundedness are all NP-complete for flat FIFO machines, while cyclicity is decidable in linear time. It also proves reachability NP-complete for flat lossy and flat front-lossy machines, where messages may disappear. A final construction translates any flat FIFO machine into a trace-flattable synchronized system of counter machines that is weakly bisimilar to the original, making LTL model checking decidable and opening a route to a verification tool built on flat submachines.

What carries the argument

The load-bearing identity is the word equation $x^\omega = w y^\omega$ of Lemma 2.4: for an elementary loop that reads $x_c$ and writes $y_c$ on channel $c$, infinite iterability forces the channel content to lie in $w(c)[z^{k-j}]^*$ for a primitive word $z$, turning the channel into a counter of blocks of $z$. This characterization drives the NP upper bounds, while the upper-bound algorithms themselves use the simulation of flat path schemas by multi-head pushdown automata restricted by bounded expressions and the linear reduction of reachability to control-state reachability. For model checking, the central construction is a synchronized system made of a counting abstraction machine and one order machine per channel, related to the original FIFO machine by a weak bisimulation and proved trace-flattable.

What would settle it

Construct a flat lossy FIFO machine with one channel and a target control state, and compare reachable control states under ordinary lossy semantics (any message may vanish from anywhere) with those under front-lossy semantics (only the front message may vanish); a control state reachable in the first setting but not the second would refute the missing reduction behind Theorem 4.5. The same test can be run as a brute-force search over small machines to settle the lemma.

Watch

Extended reading notes

Core claim

On the paper's own terms, the discovery is that flatness makes unbounded FIFO channels behave like counters: the content of each channel along an infinitely iterated loop must settle into the periodic language $w(c)\cdot[z^{k-j}]^*$, so all unbounded growth is exhausted by independent counter-like loops. From this, the paper claims that reachability has the same NP-complete complexity for flat FIFO machines as for flat counter machines, that the standard problems undecidable for general FIFO machines become NP-complete under flatness, and that reachability stays NP-complete when channels may lose messages. In addition, the paper constructs a synchronized product of counter machines, using a counting abstraction machine and order machines, that is weakly bisimilar to the given flat FIFO machine and trace-flattable; the reachability set of this counter system is semilinear, which yields decidability of LTL properties.

Load-bearing premise

The NP upper bound for flat lossy FIFO machines rests on the paper's asserted but unproved reduction of control-state reachability under lossy semantics to the same question under front-lossy semantics; if the two semantics differ on some flat machine, the upper-bound half of Theorem 4.5 collapses.

Editorial extensions

If this is right

  • For flat FIFO machines, reachability, repeated reachability, repeated control-state reachability, termination, boundedness, channel-boundedness, and letter-channel-boundedness are all decidable and NP-complete; cyclicity is solvable in linear time.
  • Every loop that can be iterated infinitely acts on each channel as a counter over the periodic word $w(c)[z^{k-j}]^*$, so unboundedness is witnessed by a single loop whose effect is nonnegative on all channels and positive on at least one.
  • Reachability for flat lossy and flat front-lossy FIFO machines is NP-complete, in contrast to general lossy channel systems, where reachability is far beyond elementary.
  • LTL model checking of flat FIFO machines is decidable through the trace-flattable synchronized counter system, whose reachability set is semilinear.
  • The flat-submachine enumeration strategy used by counter-machine tools applies to general FIFO machines, terminating whenever some flat submachine shares the whole machine's reachability set.

Reading between the lines

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

  • Because the paper's lower bound avoids binary counter encoding, the same 3SAT gadget should transfer to other flat models whose loop effects are unary, suggesting a general principle that flatness reduces unbounded queue or counter behavior to one-dimensional periodic growth.
  • The unproved reduction from lossy to front-lossy control-state reachability, if made fully rigorous, would imply that flat lossy verification only needs prefix constraints; a direct search over small flat machines comparing reachable control states under the two semantics could test this.
  • The bisimulation to a counter system suggests that branching-time model checking of flat FIFO machines might be attacked with existing counter-machine techniques, although the paper leaves CTL* explicitly open.
  • The periodic-channel characterization gives a small, explainable certificate for unboundedness—one loop plus one periodic word per channel—which could be surfaced to users of a future verification tool.
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 / 4 minor

Summary. The paper studies flat FIFO machines and establishes complexity results for reachability and related verification problems. In Section 3 it claims that reachability, repeated reachability, repeated control-state reachability, termination, boundedness, channel-boundedness, and letter-channel-boundedness are NP-complete for flat FIFO machines, with cyclicity decidable in linear time. Section 4 extends the reachability result to flat lossy and flat front-lossy FIFO machines, claiming NP-completeness. Section 5 constructs a synchronized product of counter machines that is weakly bisimilar to a given flat FIFO machine, asserts that this system is trace-flattable, and derives decidability of LTL model checking. The main proofs are based on reductions from 3SAT for lower bounds and on adaptations of prior work of Esparza-Ganty-Majumdar for upper bounds.

Significance. If the issues below are repaired, the paper makes a substantial contribution: it resolves the previously open complexity of reachability for flat FIFO machines, generalizes analogous results for flat counter machines, and provides a new counter-machine-based abstraction with potential applications to model checking. The paper contains several strong elements: an explicit 3SAT reduction covering six properties, a clean linear reduction from reachability to control-state reachability, and a nontrivial construction of a synchronized counter system. However, the significance is currently conditional on correcting the mismatched theorem statement, filling the missing lossy-to-front-lossy reduction, and supplying the missing details in the trace-flattening proof.

major comments (4)
  1. [§3, Theorem 3.17] Theorem 3.17 states that 'termination, boundedness, channel-boundedness and letter-channel-boundedness are NP-complete,' but the proofs in Corollary 3.12 and Theorem 3.16 establish NP-completeness for the complementary problems non-termination, unboundedness, channel-unboundedness, and letter-channel-unboundedness. Since termination is the complement of non-termination over the same instances, and similarly for the other pairs, the theorem as stated would imply NP = coNP. The theorem should be corrected to state NP-completeness for the complement problems, matching the abstract and the surrounding proofs.
  2. [§4, after Lemma 4.4] The NP upper bound for reachability in flat lossy FIFO machines relies on the unproved observation that 'control state reachability in flat lossy machines reduces to control state reachability in flat front-lossy machines.' This is a load-bearing step for Theorem 4.5: without a proof, the lossy upper bound is not established. The equivalence is plausible, but it is not immediate because the two semantics differ in which channel positions can be dropped, and the completed machine used in the reachability reduction must be shown to preserve the equivalence. A formal reduction and its correctness proof should be supplied.
  3. [§4, Lemma 4.4] In the proof of Lemma 4.4 it is claimed that 'since the given front-lossy machine is flat, there is a bounded expression w over Δ whose language is the set of paths from q0 to q.' This is false for flat machines with branching: for example, an acyclic diamond with two distinct paths from q0 to q has a set of paths that is not a single bounded expression of the form w1* w2* ... wk*. The proof should instead enumerate or nondeterministically guess a path schema, as is done in [24], and apply Theorem 4.3 to the bounded expression of that schema.
  4. [§5, Proposition 5.6] The proof of Proposition 5.6 is only a sketch and does not provide a precise construction of the claimed trace-flattening S_flat. It refers to a 'paragraph preceding this lemma' that contains only intuition and a figure, not a formal definition. The induction step does not rigorously define what it means for a component to 'exit' a loop, how the sequentially composed machines are flat, or why the equality traces(Ssync) = f(traces(Sflat)) holds. Since Theorem 5.7 (LTL decidability) depends on this proposition, the construction and proof need to be completed or replaced with a citation to a result that supplies the missing details.
minor comments (4)
  1. [§4, semantics of front-lossy machines] The formal definition of front-lossy semantics omits the loss transition: it gives rules for send and receive transitions but no rule of the form (q, (a)_c · w) → (q, w). Since the prose says 'any letter at the front of any channel can be lost,' the loss transition should be added explicitly to the transition system.
  2. [§4, proof of Lemma 4.4] There are typos in this proof: 'bounded exression' should be 'bounded expression' and 'In our constrction' should be 'In our construction.'
  3. [§5, modified synchronized system] After modifying the order machines to remove τ-transitions, the paper says 'Now a proof similar to that of Proposition 5.4 can be used to show bisimulation.' This does not address why the modified order machines remain flat, especially in the case where merging states could destroy flatness, nor does it prove that the added guards preserve the bisimulation. More detail is needed.
  4. [§3, Corollary 3.9] Corollary 3.9 describes the channel contents as the regular language w(c) · [z^{k-j}_c]^* when the loop is iterated, but this representation is undefined when x_c = ε. The statement should either exclude that case or explain how the empty-retrieval case is handled.

Circularity Check

0 steps flagged · score 1.0 of 10

No circular derivation: the NP-completeness proofs reduce from 3SAT and use independent prior results; the only self-citations are non-load-bearing, and the mislabeled complements in Theorem 3.17 are a correctness error, not circularity.

full rationale

I checked each load-bearing step. The lower bounds (Theorem 3.16) are direct 3SAT reductions via flat FIFO gadgets, and the upper bounds use the external control-state reachability result [24], the external integer-programming lemma [34], and lemmas proved in the text (Lemma 2.4, Lemma 3.8, Proposition 3.11, Corollary 3.12). Lemma 3.8 is credited to the authors' earlier [28, Proposition 5.1], but the proof is reproduced in the paper and extends it to multiple channels with the converse, so the self-citation carries no load. Theorem 5.7 invokes [18, Theorem 1] for LTL preservation by trace-flattenings; that is a published theorem about counter systems and does not assume the flat-FIFO result being claimed. The unsupported reduction in Section 4 from flat lossy to flat front-lossy control-state reachability is a proof gap, not a circular step: it is an asserted implication between two different semantics, not a redefinition of the target as its input. Finally, Theorem 3.17 misnames the proven problems (it states termination/boundedness are NP-complete after proving non-termination/unboundedness NP-complete); this is an internal complement error that would imply NP=coNP, but it is not a circularity because no result is derived from its own conclusion. Overall, the central claims are self-contained against external benchmarks, and no prediction reduces by construction to a fitted parameter or to a definitional identity.

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

The paper is a pure complexity-theory contribution; there are no fitted numerical parameters. It relies on several external theorems and on two unproved internal observations: the lossy-to-front-lossy reduction and the uniqueness of the channel-word mapping. The invented entities are all internal proof devices with no independent empirical handle.

assumptions (9)
  • standard math Levi's Lemma: if uv = vu for words u,v, then both are powers of a common primitive word.
    Used in the proof of Lemma 2.4 as a classical word combinatorics result; no proof is given.
  • domain assumption Sutre's linear reduction from reachability to control-state reachability for FIFO machines, Proposition 3.1.
    The reduction is described in the proof but attributed to a personal communication from Grégoire Sutre; the proof in the text appears complete.
  • domain assumption Esparza-Ganty-Majumdar's theorem that control-state reachability is in NP for single-path (and hence flat) FIFO machines [24, Theorem 7].
    The paper relies on this external NP upper bound. The introduction describes [24] as covering single-path machines, while later sections invoke it for flat machines; the paper's intended justification is that flat machines decompose into finitely many path schemas.
  • domain assumption Esparza-Ganty-Majumdar's theorem computing an existential Presburger formula for path-schema runs in polynomial time [24, Theorem 3].
    Used in Proposition 3.15 to bound the letter-channel-unboundedness problem.
  • standard math Papadimitriou's lemma: if rational LP Ax>=b is unbounded for k·x and there is an integer feasible point, then the integer optimization is unbounded [34, Lemma 3].
    Used in Proposition 3.15 to convert rational unboundedness to integer unboundedness.
  • domain assumption Abdulla et al.'s quadratic-time computation of σ*(L) for SRE L in lossy FIFO loops [1, Corollary 3].
    Used in Theorem 4.1 to compute the reachability set of a flat lossy FIFO machine in exponential time.
  • ad hoc to paper Lossy and front-lossy FIFO semantics are equivalent for control-state reachability.
    Stated without proof in Section 4 after Lemma 4.4; this is load-bearing for Theorem 4.5.
  • domain assumption Trace-flattening preserves LTL model checking [18, Theorem 1].
    Used in Theorem 5.7 to conclude LTL decidability from trace-flattening of the synchronized counter system.
  • ad hoc to paper Flatness implies the trace language of a flat FIFO machine is included in a bounded language, and the Parikh image over transitions determines the channel word h_c(v_c).
    Used in Section 5 to define the bisimulation h; only a one-sentence justification is given.
invented entities (4)
  • Counting abstraction machine S_count
    purpose: Tracks the number of occurrences of each message letter in each channel, ignoring order, using one counter per (message, transition) pair.
    Introduced in Section 5; internal proof device with no separate falsifiable prediction.
  • Order machines S_c_order
    purpose: Tracks the order of letters in each channel by simulating the control path and synchronizing with the counting machine via rendez-vous labels.
    Introduced in Section 5; internal to the bisimulation construction.
  • Synchronized counter system S_sync
    purpose: Weakly bisimilar to the given flat FIFO machine; used to enable model checking and to show trace-flattability.
    Introduced in Section 5; internal construction.
  • Trace-flattening S_flat
    purpose: A flat counter machine with the same traces as S_sync, used to show LTL decidability.
    Introduced in Proposition 5.6; existence is argued by induction, not constructed explicitly.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Verification of Flat FIFO Systems." pith.science (2026). https://pith.science/paper/IUI4O6M4

@misc{pith2026190807282,
  author       = {Pith},
  title        = {Pith review of: Verification of Flat FIFO Systems},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/IUI4O6M4}},
  note         = {Machine review of arXiv:1908.07282}
}
read the original abstract

The decidability and complexity of reachability problems and model-checking for flat counter machines have been explored in detail. However, only few results are known for flat (lossy) FIFO machines, only in some particular cases (a single loop or a single bounded expression). We prove, by establishing reductions between properties, and by reducing SAT to a subset of these properties that many verification problems like reachability, non-termination, unboundedness are NP-complete for flat FIFO machines, generalizing similar existing results for flat counter machines. We also show that reachability is NP-complete for flat lossy FIFO machines and for flat front-lossy FIFO machines. We construct a trace-flattable system of many counter machines communicating via rendez-vous that is bisimilar to a given flat FIFO machine, which allows to model-check the original flat FIFO machine. Our results lay the theoretical foundations and open the way to build a verification tool for (general) FIFO machines based on analysis of flat sub-machines.

Figures

Figures reproduced from arXiv: 1908.07282 by the authors.

Figure 1
Figure 1. FIFO system of Example 2.2 (from [33]) Contributions. We solve the open problem of the complexity of the reachability problem for flat FIFO machines by showing that it is Np-complete; we extend this result to other usual verification properties and show that they are also Np-complete. We also show that the reachability problem is Np-complete for flat (front-)lossy FIFO machines. Then we show that a flat FIFO machine… view at source ↗
Figure 2
Figure 2. Example flat FIFO machine and path schema target qi mod (r+1). We call t1 · · ·tr+1 the label of the loop. A path schema is a flat FIFO machine comprising of a sequence p0`1p1`2p2 · · · lrpr, where p0, . . . , pr are path segments and `1, . . . , `r are elementary loops. There are states q0, q1, . . . , qr+1 such that p0 is a path segment from q0 to q1 and for every i ∈ {1, . . . , r}, pi is a path segment from qi t… view at source ↗
Figure 3
Figure 3. The gadget for variable xi adds either 0 (in the top transition) or 1 (in the bottom edge) to channel xi . At the end of this gadget, channel xi will have either 0 or 1. We will sequentially compose the gadgets for all variables. Starting from the initial control state of [PITH_FULL_IMAGE:figures/full_fig_p012_3.png] view at source ↗
Figures from the paper (4 more)
Figure 3
Figure 3. Figure 3: Gadgets used in the proof of Theorem 3.16 the gadget for variable x1, we reach the final control state of the gadget for variable xn and the contents of the channels x1, . . . , xn determine a truth valuation. The gadget for the example clause c1 = x1 ∨ ¬x2 ∨ x3 (gadge…
Figure 4
Figure 4. Figure 4: The 2-HPDA Ac Hence we deduce that reachability is in Np for both flat front-lossy FIFO machines and flat lossy FIFO machines. To achieve these results, we reduce reachability (in both models) to control-state reachability in a front-lossy FIFO machine. To test whether…
Figure 5
Figure 5. Figure 5: An example flat FIFO machine (a) and the equivalent counter system (d). ψ c : ∆c order → (M × ∆) ∪ {τ} are defined as follows: for every t ∈ ∆, one adds the following transitions in ∆c order: • If t = q1 c!a −−→ q2, one adds to ∆c order the transition t 0 = q1 → q2 and…
Figure 6
Figure 6. Figure 6: Flattening loop `i and for every channel c, all local states of the order machine S c order are in some loop `c. This is the intuition for the next result. Let traces(Ssync) be the set of all runs of Ssync. Let S 0 be another counter machine with set of states Q0 and t…

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

38 extracted references · 38 canonical work pages

  1. [24]

    A perfect model for bounded verification

    Javier Esparza, Pierre Ganty, and Rupak Majumdar. A perfect model for bounded verification. In Proceedings of the 2012 27th Annual IEEE/ACM Symposium on Logic in Computer Science , LICS ’12, pages 285–294, Washington, DC, USA, 2012. IEEE Computer Society

    work page 2012

  2. [1]

    On-the-fly analysis of systems with unbounded, lossy FIFO channels

    Parosh Aziz Abdulla, Ahmed Bouajjani, and Bengt Jonsson. On-the-fly analysis of systems with unbounded, lossy FIFO channels. In CAV, volume 1427 of Lecture Notes in Computer Science , pages 305–318. Springer, 1998

    work page 1998

  3. [2]

    Using forward reachability analysis for verification of lossy channel systems.Formal Methods in System Design, 25(1):39– 65, 2004

    Parosh Aziz Abdulla, Aurore Collomb-Annichini, Ahmed Bouajjani, and Bengt Jonsson. Using forward reachability analysis for verification of lossy channel systems.Formal Methods in System Design, 25(1):39– 65, 2004

    work page 2004

  4. [3]

    Trex: A tool for reachability analysis of complex systems

    Aurore Annichini, Ahmed Bouajjani, and Mihaela Sighireanu. Trex: A tool for reachability analysis of complex systems. In G´ erard Berry, Hubert Comon, and Alain Finkel, editors, Computer Aided Verification, pages 368–372, Berlin, Heidelberg, 2001. Springer Berlin Heidelberg

    work page 2001

  5. [4]

    FAST: Fast Acceleration of Symbolic Transition systems

    S´ ebastien Bardin, Alain Finkel, J´ erˆ ome Leroux, and Laure Petrucci. FAST: Fast Acceleration of Symbolic Transition systems. In Warren A. Hunt, Jr and Fabio Somenzi, editors, Proceedings of the 15th International Conference on Computer Aided Verification (CAV’03) , volume 2725 of Lecture Notes in Computer Science , pages 118–121, Boulder, Colorado, USA...

    work page 2003

  6. [5]

    FAST: Acceleration from theory to practice

    S´ ebastien Bardin, Alain Finkel, J´ erˆ ome Leroux, and Laure Petrucci. FAST: Acceleration from theory to practice. International Journal on Software Tools for Technology Transfer , 10(5):401–424, October 2008

    work page 2008

  7. [6]

    Flat acceleration in symbolic model checking

    S´ ebastien Bardin, Alain Finkel, J´ erˆ ome Leroux, and Philippe Schnoebelen. Flat acceleration in symbolic model checking. In Doron A. Peled and Yih-Kuen Tsay, editors, Proceedings of the 3rd International Symposium on Automated Technology for Verification and Analysis (ATVA’05) , volume 3707 of Lecture Notes in Computer Science , pages 474–488, Taipei, ...

    work page 2005

  8. [7]

    Domain-specific regular acceleration

    Bernard Boigelot. Domain-specific regular acceleration. STTT, 14(2):193–206, 2012

    work page 2012

Show all 38 references
  1. [8]

    The power of QDDs (extended abstract)

    Bernard Boigelot, Patrice Godefroid, Bernard Willems, and Pierre Wolper. The power of QDDs (extended abstract). In Pascal Van Hentenryck, editor, Static Analysis, 4th International Symposium, SAS ’97, Paris, France, September 8-10, 1997, Proceedings, volume 1302 of Lecture Not...

    1997

  2. [9]

    Bounded reachability problems are decidable in FIFO machines

    Benedikt Bollig, Alain Finkel, and Amrita Suresh. Bounded reachability problems are decidable in FIFO machines. In Igor Konnov and Laura Kovacs, editors, Proceedings of the 31st International Conference on Concurrency Theory (CONCUR’20) , volume 171 of Leibniz International Pr...

    2020

  3. [10]

    Symbolic reachability analysis of fifo-channel systems with nonregular sets of configurations

    Ahmed Bouajjani and Peter Habermehl. Symbolic reachability analysis of fifo-channel systems with nonregular sets of configurations. Theor. Comput. Sci. , 221(1-2):211–250, 1999

    1999

  4. [11]

    Cyclic Petri net reachability sets are semi-linear effectively con- structible

    Zakaria Bouziane and Alain Finkel. Cyclic Petri net reachability sets are semi-linear effectively con- structible. In Faron Moller, editor, Proceedings of the 2nd International Workshop on Verification of Infinite State Systems (INFINITY’97) , volume 9 of Electronic Notes in Theo...

    1997

  5. [12]

    Safety problems are np-complete for flat integer programs with octagonal loops

    Marius Bozga, Radu Iosif, and Filip Konecn´ y. Safety problems are np-complete for flat integer programs with octagonal loops. CoRR, abs/1307.5321, 2013

    2013 arXiv

  6. [13]

    Tool demonstration of the FLATA counter automata toolset

    Marius Bozga, Radu Iosif, Filip Konecn´ y, and Tom´ as Vojnar. Tool demonstration of the FLATA counter automata toolset. In Andrei Voronkov, Laura Kov´ acs, and Nikolaj Bjørner, editors,Second International Workshop on Invariant Generation, WING 2009, York, UK, March 29, 2009 ...

    2009

  7. [14]

    On communicating finite-state machines

    Daniel Brand and Pitro Zafiropulo. On communicating finite-state machines. J. ACM, 30(2):323–342, 1983

    1983

  8. [15]

    Choreography and orchestration conformance for system design

    Nadia Busi, Roberto Gorrieri, Claudio Guidi, Roberto Lucchi, and Gianluigi Zavattaro. Choreography and orchestration conformance for system design. In Paolo Ciancarini and Herbert Wiklicky, editors, Coordination Models and Languages, 8th International Conference, COORDINATION ...

    2006

  9. [16]

    Verification of programs with half-duplex communication.Information and Computation, 202(2):166–190, November 2005

    G´ erard C´ ec´ e and Alain Finkel. Verification of programs with half-duplex communication.Information and Computation, 202(2):166–190, November 2005

    2005

  10. [17]

    Model- checking counting temporal logics on flat structures

    Normann Decker, Peter Habermehl, Martin Leucker, Arnaud Sangnier, and Daniel Thoma. Model- checking counting temporal logics on flat structures. In 28th International Conference on Concurrency Theory, CONCUR 2017 , LIPIcs. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2017

    2017

  11. [18]

    Demri, A

    S. Demri, A. Finkel, V. Goranko, and G. van Drimmelen. Towards a model-checker for counter systems. In Susanne Graf and Wenhui Zhang, editors, Automated Technology for Verification and Analysis , pages 493–507, Berlin, Heidelberg, 2006. Springer Berlin Heidelberg

    2006

  12. [19]

    Equivalence between model-checking flat counter systems and presburger arithmetic

    St´ ephane Demri, Amit Dhar, and Arnaud Sangnier. Equivalence between model-checking flat counter systems and presburger arithmetic. Theoretical Computer Science, 2017. Special issue of RP’14, to appear

    2017

  13. [20]

    On the complexity of verifying regular properties on flat counter systems

    St´ ephane Demri, Amit Kumar Dhar, and Arnaud Sangnier. On the complexity of verifying regular properties on flat counter systems. In Fedor V. Fomin, R¯ usi¸ nˇ s Freivalds, Marta Kwiatkowska, and David Peleg, editors, Proceedings of the 40th International Colloquium on Automat...

    2013

  14. [21]

    Taming past LTL and flat counter systems

    St´ ephane Demri, Amit Kumar Dhar, and Arnaud Sangnier. Taming past LTL and flat counter systems. Inf. Comput., 242:306–339, 2015

    2015

  15. [22]

    Model-checking CTL* over flat Presburger counter systems

    St´ ephane Demri, Alain Finkel, Valentin Goranko, and Govert van Drimmelen. Model-checking CTL* over flat Presburger counter systems. Journal of Applied Non-Classical Logics , 20(4):313–344, 2010. Vol. 16:4 VERIFICATION OF FLAT FIFO MACHINES 4:29

    2010

  16. [23]

    Structurally cyclic petri nets.Logical Methods in Computer Science , 11(4), 2015

    Frank Drewes and J´ erˆ ome Leroux. Structurally cyclic petri nets.Logical Methods in Computer Science , 11(4), 2015

    2015

  17. [25]

    Structuration des syst` emes de transitions: applications au contrˆ ole du parall´ elisme par files fifo, Th` ese d’Etat

    Alain Finkel. Structuration des syst` emes de transitions: applications au contrˆ ole du parall´ elisme par files fifo, Th` ese d’Etat. PhD thesis, Universit´ e Paris-Sud, Orsay, 1986

    1986

  18. [26]

    Forward analysis for WSTS, part II: Complete WSTS

    Alain Finkel and Jean Goubault-Larrecq. Forward analysis for WSTS, part II: Complete WSTS. Logical Methods in Computer Science , 8(3:28), September 2012

    2012

  19. [27]

    Synchronizability of communicating finite state machines is not decidable

    Alain Finkel and ´Etienne Lozes. Synchronizability of communicating finite state machines is not decidable. In Ioannis Chatzigiannakis, Piotr Indyk, Anca Muscholl, and Fabian Kuhn, editors, Proceedings of the 44th International Colloquium on Automata, Languages and Programming ...

    2017

  20. [28]

    Purushothaman Iyer, and Gr´ egoire Sutre

    Alain Finkel, S. Purushothaman Iyer, and Gr´ egoire Sutre. Well-abstracted transition systems: Application to FIFO automata. Information and Computation , 181(1):1–31, February 2003

    2003

  21. [29]

    On communicating automata with bounded channels

    Blaise Genest, Dietrich Kuske, and Anca Muscholl. On communicating automata with bounded channels. Fundam. Inform., 80(1-3):147–167, 2007

    2007

  22. [30]

    On the complexity of model checking counter automata

    Christoph Haase. On the complexity of model checking counter automata . PhD thesis, University of Oxford, UK, 2012

    2012

  23. [31]

    Radu Iosif and Arnaud Sangnier. How hard is it to verify flat affine counter systems with the finite monoid property? In Cyrille Artho, Axel Legay, and Doron Peled, editors, Automated Technology for Verification and Analysis - 14th International Symposium, ATVA 2016, Chiba, Japan, ...

    2016

  24. [32]

    Testing for unboundedness of FIFO channels

    Thierry J´ eron and Claude Jard. Testing for unboundedness of FIFO channels. Theor. Comput. Sci. , 113(1):93–117, 1993

    1993

  25. [33]

    Verifying asynchronous interactions via communicating session automata

    Julien Lange and Nobuko Yoshida. Verifying asynchronous interactions via communicating session automata. CoRR, abs/1901.09606, 2019

    1901 arXiv

  26. [34]

    Papadimitriou

    Christos H. Papadimitriou. On the complexity of integer programming. J. ACM, 28(4):765–768, October 1981

    1981

  27. [35]

    Complexity hierarchies beyond elementary

    Sylvain Schmitz. Complexity hierarchies beyond elementary. TOCT, 8(1):3:1–3:36, 2016

    2016

  28. [36]

    On flat lossy channel machines

    Philippe Schnoebelen. On flat lossy channel machines. CoRR, abs/2007.05269, 2020

    2007 arXiv

  29. [37]

    Personal communication, 2018

    Gregoire Sutre. Personal communication, 2018

    2018

  30. [38]

    Communication protocols and error recovery procedures

    Gregor von Bochmann. Communication protocols and error recovery procedures. Operating Systems Review, 9(3):45–50, 1975. This work is licensed under the Creative Commons Attribution License. T o view a copy of this license, visit https://creativecommons.org/licenses/by/4.0/ or ...

    1975

Pith tools

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