pith. sign in

arxiv: 1907.01240 · v2 · pith:RYBJLHE7new · submitted 2019-07-02 · 💻 cs.FL · cs.LO

Timed Basic Parallel Processes

Lorenzo Clemente , Piotr Hofman , Patrick Totzke This is my paper

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

classification 💻 cs.FL cs.LO
keywords timed basic parallel processescoverabilityreachabilityPSPACE-completeEXPTIME-completetimed automataPetri netsNP-complete
0
0 comments X

The pith

Coverability in timed basic parallel processes is PSPACE-complete and reachability is EXPTIME-complete when targets use unary encoding.

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

The paper defines timed basic parallel processes as an extension of basic parallel processes that adds a global clock while retaining context-free branching. It proves that coverability is PSPACE-complete and reachability is EXPTIME-complete under unary target multiplicities. The one-clock restriction reduces both problems to NP-complete, matching the untimed case. The proofs rest on a polynomial-size existential linear-arithmetic formula that captures reachability for one-clock timed automata.

Core claim

Timed basic parallel processes extend communication-free Petri nets by a global notion of time and can model networks of independent timed automata with process creation. With unary-encoded target multiplicities the coverability problem is PSPACE-complete and the reachability problem is EXPTIME-complete. Both problems become NP-complete when restricted to one-clock TBPP. As an auxiliary result the reachability relation of any one-clock timed automaton is expressible by a polynomial-size formula in the existential fragment of linear arithmetic.

What carries the argument

The polynomial-size existential linear-arithmetic formula that encodes the reachability relation of one-clock timed automata and serves as the basis for the NP upper bounds on one-clock TBPP.

If this is right

  • Verification of networks of timed automata that may create new processes stays inside PSPACE for coverability questions.
  • Restricting every process to a single clock keeps both coverability and reachability inside NP.
  • The polynomial arithmetic encoding of one-clock timed-automaton reachability directly supplies the NP upper bounds for one-clock TBPP.
  • The results separate TBPP sharply from general timed Petri nets, which remain super-Ackermannian or undecidable.

Where Pith is reading between the lines

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

  • The unary-encoding restriction may be relaxed in practice by bounding the numeric constants that appear in any concrete system model.
  • The same arithmetic encoding technique could be tested on other restricted classes of timed systems that combine clocks with limited forms of concurrency.
  • Because one-clock TBPP match the complexity of untimed BPP, existing tools for untimed process algebras may be lifted to the timed setting with only polynomial overhead.

Load-bearing premise

Target multiplicities are encoded in unary rather than binary.

What would settle it

An explicit TBPP instance whose reachability question with unary targets cannot be answered by any exponential-time procedure, or a one-clock TBPP instance whose coverability question lies outside NP.

read the original abstract

Timed basic parallel processes (TBPP) extend communication-free Petri nets (aka. BPP or commutative context-free grammars) by a global notion of time. TBPP can be seen as an extension of timed automata (TA) with context-free branching rules, and as such may be used to model networks of independent timed automata with process creation. We show that the coverability and reachability problems (with unary encoded target multiplicities) are PSPACE-complete and EXPTIME-complete, respectively. For the special case of 1-clock TBPP, both are NP-complete and hence not more complex than for untimed BPP. This contrasts with known super-Ackermannian-completeness and undecidability results for general timed Petri nets. As a result of independent interest, and basis for our NP upper bounds, we show that the reachability relation of 1-clock TA can be expressed by a formula of polynomial size in the existential fragment of linear arithmetic, which improves on recent results from the literature.

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 defines Timed Basic Parallel Processes (TBPP) as BPP extended by a global clock, modeling networks of independent timed automata with process creation. It claims that coverability is PSPACE-complete and reachability is EXPTIME-complete when target multiplicities are encoded in unary; both problems are NP-complete for the 1-clock restriction. As an independent technical contribution, it shows that the reachability relation of 1-clock timed automata is expressible by a polynomial-size formula in the existential fragment of linear arithmetic, which is used to obtain the NP upper bounds and improves on prior results.

Significance. If the stated reductions and the polynomial-size encoding hold, the results give a precise complexity map for context-free timed systems that sits strictly between untimed BPP (NP-complete) and general timed Petri nets (undecidable or super-Ackermannian). The 1-clock TA encoding is of independent interest for verification and supplies the technical basis for the NP membership claims.

minor comments (2)
  1. [Problem statements] The abstract states that target multiplicities are unary-encoded, but the problem definitions in the main body should restate the encoding explicitly (including the distinction from binary encoding) to make the complexity claims self-contained.
  2. [Introduction] The manuscript should include a brief comparison table or paragraph contrasting the new TBPP bounds with the known results for timed Petri nets cited in the abstract.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for the positive summary of our results on Timed Basic Parallel Processes and for recommending minor revision. No specific major comments were raised.

Circularity Check

0 steps flagged

No significant circularity in derivation chain

full rationale

The paper's central claims establish PSPACE-completeness for coverability and EXPTIME-completeness for reachability (under unary target encoding) via explicit reductions from/to known problems in timed automata and Petri nets, with the 1-clock NP-completeness case resting on a new polynomial-size existential linear arithmetic encoding of 1-clock TA reachability. No equation, definition, or self-citation reduces a claimed result to a fitted input or prior author result by construction; the unary restriction is stated upfront as a precondition, and the independent-interest encoding is presented as an external technical lemma rather than a renaming or self-referential fit. The derivation chain therefore remains self-contained against external benchmarks.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The central claims rest on standard definitions of complexity classes and the unary encoding convention; the paper introduces the TBPP model but does not postulate new physical entities or fit numerical parameters.

axioms (1)
  • standard math Standard definitions of PSPACE, EXPTIME and NP from complexity theory
    Invoked to classify coverability and reachability for TBPP.

pith-pipeline@v0.9.0 · 5699 in / 1306 out tokens · 46283 ms · 2026-05-25T10:38:30.539281+00:00 · methodology

discussion (0)

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