pith. sign in

arxiv: 1907.01168 · v1 · pith:UPSL3PU6new · submitted 2019-07-02 · 💻 cs.FL

Kleene Theorems for Free Choice Nets Labelled with Distributed Alphabets

Pith reviewed 2026-05-25 10:54 UTC · model grok-4.3

classification 💻 cs.FL
keywords free choice netsKleene theoremdistributed alphabetssynchronous productsZielonka automataS-coverable nets1-bounded netsdistributed choice property
0
0 comments X

The pith

Free choice nets labelled with distributed alphabets admit expressions corresponding to synchronous products and Zielonka automata after the product condition on final markings is dropped.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper removes an earlier restriction requiring final markings to satisfy a product condition and supplies expressions for the resulting larger classes of free choice nets. These expressions characterize the languages of free choice synchronous products and Zielonka automata. For the subclass of nets that also satisfy the distributed choice property, the work supplies an alternative characterization whose defining properties can be checked in polynomial time. The results are stated for 1-bounded S-coverable nets whose S-components respect the given alphabet distribution. A reader would care because the removal of the product restriction enlarges the set of concurrent systems that can be described by regular-expression-style syntax.

Core claim

Expressions exist for the languages of free choice nets labelled with distributed alphabets once the product condition on the set of final markings is removed; these expressions correspond exactly to free choice synchronous products and Zielonka automata. For the subclass possessing the distributed choice property an alternative characterization is given in terms of properties that are checkable in polynomial time.

What carries the argument

The syntactic expressions that generate the languages accepted by free choice synchronous products and Zielonka automata.

If this is right

  • Languages of the enlarged class of free choice nets can be represented by the supplied expressions.
  • Nets with the distributed choice property can be recognized by polynomially checkable conditions.
  • The characterizations extend directly to Zielonka automata.
  • Removal of the product condition produces a strictly larger class of representable nets.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The polynomial-time checks may support practical decision procedures for properties of distributed systems modeled by these nets.
  • The expressions could serve as a bridge between net-based and automata-based verification techniques for concurrent processes.
  • Further extensions might relate the expressions to other models of distributed computation that use synchronized actions.

Load-bearing premise

The nets are required to be 1-bounded and S-coverable with S-components that respect the given alphabet distribution.

What would settle it

A 1-bounded S-coverable free choice net labelled with a distributed alphabet whose accepted language lies outside the languages generated by the expressions supplied for free choice synchronous products would refute the claimed correspondence.

Figures

Figures reproduced from arXiv: 1907.01168 by Ramchandra Phawade.

Figure 1
Figure 1. Figure 1: Free Choice Net without distributed choice r1 s1 r2 r3 s2 s3 a a a a b c d e [PITH_FULL_IMAGE:figures/full_fig_p002_1.png] view at source ↗
Figure 4
Figure 4. Figure 4: S-cover of the net in [PITH_FULL_IMAGE:figures/full_fig_p007_4.png] view at source ↗
Figure 5
Figure 5. Figure 5: Product system (A1, A2) [PITH_FULL_IMAGE:figures/full_fig_p010_5.png] view at source ↗
Figure 6
Figure 6. Figure 6: Free choice net languages and automata over distributed alphabets We give below the summary of correspondences established for the nets, au￾tomata over distributed alphabets and expressions. To get an expression, for the language of a labelled 1-bounded and S-coverable free choice net (with or without distributed choice) having a finite set of final markings, we use Theorem 4 and Theorem 10. In the reverse… view at source ↗
read the original abstract

We provided (PNSE'2014) expressions for free choice nets having "distributed choice property" which makes the nets "direct product" representable. In a recent work (PNSE'2016), we gave equivalent syntax for a larger class of free choice nets obtained by dropping distributed choice property. In both these works, the classes of free choice nets were restricted by a "product condition" on the set of final markings. In this paper we do away with this restriction and give expressions for the resultant classes of nets which correspond to "free choice synchronous products and Zielonka automata". For free choice nets with distributed choice property, we give an alternative characterization using properties checkable in polynomial time. Free choice nets we consider are 1-bounded, S-coverable, and are labelled with distributed alphabets, where S-components of the associated S-cover respect the given alphabet distribution.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

0 major / 2 minor

Summary. The paper extends the authors' prior PNSE'2014 and PNSE'2016 results on Kleene theorems for free choice nets by removing the product condition on final markings. For 1-bounded, S-coverable free choice nets labelled with distributed alphabets (where S-components respect the alphabet distribution), it supplies expressions corresponding to free choice synchronous products and Zielonka automata; for the distributed-choice-property subclass it supplies an alternative characterization whose properties are checkable in polynomial time.

Significance. If the claimed correspondences and constructions hold, the work enlarges the class of nets admitting syntactic characterizations without the prior product restriction and strengthens links to Zielonka automata; the polynomial-time check for the distributed-choice subclass is a concrete algorithmic contribution. The manuscript builds directly on the authors' earlier PNSE papers but does not reduce new quantities to fitted parameters from those works.

minor comments (2)
  1. Abstract, first sentence: the phrasing 'We provided (PNSE'2014) expressions' is grammatically awkward and should be revised for clarity (e.g., 'In PNSE 2014 we provided expressions...').
  2. Abstract, final sentence: the parenthetical qualifier on S-components could be moved earlier for readability when the scope of the nets is first introduced.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for the careful reading and the positive recommendation for minor revision. No specific major comments were raised in the report.

Circularity Check

0 steps flagged

No significant circularity in derivation chain

full rationale

The paper extends its own prior PNSE results by removing the product condition on final markings and supplies syntactic characterizations for the enlarged classes (free choice synchronous products, Zielonka automata) plus a polynomial-time check for the distributed-choice subclass. These steps rest on the stated restrictions (1-bounded, S-coverable nets with distributed alphabets whose S-components respect the labeling) rather than on any self-definitional loop, fitted parameter renamed as prediction, or load-bearing self-citation whose content is itself unverified. No equation or claim is shown to reduce to its own inputs by construction; the cited earlier works supply independent starting points that the present manuscript enlarges.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The paper works entirely inside the standard definitions of 1-bounded free choice nets, S-covers, and distributed alphabets; no new free parameters, invented entities, or ad-hoc axioms are introduced in the abstract.

axioms (1)
  • domain assumption Free choice nets under consideration are 1-bounded and S-coverable with S-components respecting the alphabet distribution.
    Explicitly stated as the class of nets studied in the final sentence of the abstract.

pith-pipeline@v0.9.0 · 5679 in / 1289 out tokens · 23864 ms · 2026-05-25T10:54:50.379417+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

19 extracted references · 19 canonical work pages

  1. [1]

    Antimirov, V.: Partial derivatives of regular expressio ns and finite automaton con- structions. Theoret. Comp. Sci. 155(2), 291–319 (1996)

  2. [2]

    Brzozowski, J.A.: Derivatives of regular expressions. J . ACM 11(4), 481–494 (1964)

  3. [3]

    Cambridge University Press, New York, USA (1995)

    Desel, J., Esparza, J.: Free choice Petri nets. Cambridge University Press, New York, USA (1995)

  4. [4]

    Garg, V.K., Ragunath, M.: Concurrent regular expression s and their relationship to petri nets. Theoret. Comp. Sci. 96(2), 285–304 (1992)

  5. [5]

    Grabowski, J.: On partial languages. Fundam. Inform. 4(2), 427–498 (1981)

  6. [6]

    Project Mac Report TR-94, MIT (1972)

    Hack, M.H.T.: Analysis of production schemata by Petri ne ts. Project Mac Report TR-94, MIT (1972)

  7. [7]

    In: Proceedings Conference on Decision and Cont rol, CDC

    Iordache, M.V., Antsaklis, P.J.: The ACTS software and it s supervisory control framework. In: Proceedings Conference on Decision and Cont rol, CDC. pp. 7238–

  8. [8]

    In: ACPN

    Jantzen, M.: Language theory of petri nets. In: ACPN. LNCS , vol. 254 (1987)

  9. [9]

    In: SEF M

    Lodaya, K.: Product automata and process algebra. In: SEF M. IEEE (2006)

  10. [10]

    In: DCFS, Proceedings

    Lodaya, K., Mukund, M., Phawade, R.: Kleene theorems for product systems. In: DCFS, Proceedings. LNCS, vol. 6808. Springer (2011)

  11. [11]

    Mirkin, B.G.: An algorithm for constructing a base in a la nguage of regular ex- pressions. Engg. Cybern. 5, 110–116 (1966)

  12. [12]

    In: D’So uza, D., Shankar, P

    Mukund, M.: Automata on distributed alphabets. In: D’So uza, D., Shankar, P. (eds.) Modern Applications of Automata Theory. World Scien tific (2011)

  13. [13]

    Journal of C omputing and Systems Science 13(1), 1–24 (1976)

    Petersen, J.L.: Computation sequence sets. Journal of C omputing and Systems Science 13(1), 1–24 (1976)

  14. [14]

    Phawade, R.: Labelled Free Choice Nets, finite Product Au tomata, and Expres- sions. Ph.D. thesis, Homi Bhabha National Institute (2015)

  15. [15]

    In: Cabac, L., Kristensen, L.M., Rölke, H

    Phawade, R.: Kleene theorems for labelled free choice ne ts without distributed choice. In: Cabac, L., Kristensen, L.M., Rölke, H. (eds.) Pr oc. PNSE. CEUR Work- shop Proceedings, vol. 1591, pp. 132–152. CEUR-WS.org (201 6)

  16. [16]

    In: Daniel Moldt, E.K., Rölke, H

    Phawade, R.: Kleene theorems free choice nets labelled w ith distributed alphabets. In: Daniel Moldt, E.K., Rölke, H. (eds.) Proc. PNSE. CEUR Wor kshop Proceed- ings, vol. 2138, pp. 77–98. CEUR-WS.org (2018)

  17. [17]

    In: Moldt, D., Rölke, H

    Phawade, R., Lodaya, K.: Kleene theorems for labelled fr ee choice nets. In: Moldt, D., Rölke, H. (eds.) Proc. PNSE. CEUR Workshop Proceedings, vol. 1160, pp. 75–89. CEUR-WS.org (2014)

  18. [18]

    Transactions on Petri nets and other models of concurre ncy X, 84–108 (2015)

    Phawade, R., Lodaya, K.: Kleene theorems for synchronou s products with match- ing. Transactions on Petri nets and other models of concurre ncy X, 84–108 (2015)

  19. [19]

    Zielonka, W.: Notes on finite asynchronous automata. Inf orm. Theor. Appl. 21(2), 99–135 (1987)