Timed Basic Parallel Processes



Clemente, Lorenzo, Hofman, Piotr and Totzke, Patrick ORCID: 0000-0001-5274-8190
(2019) Timed Basic Parallel Processes. In: CONCUR, 2019-8-26 - 2019-8-31, Amsterdam.

[img] Text
main.pdf - Author Accepted Manuscript

Download (793kB) | Preview

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.

Item Type: Conference or Workshop Item (Unspecified)
Uncontrolled Keywords: cs.FL, cs.FL, cs.LO
Depositing User: Symplectic Admin
Date Deposited: 13 Aug 2019 10:21
Last Modified: 19 Jan 2023 00:31
DOI: 10.4230/LIPIcs.CONCUR.2019.15
Related URLs:
URI: https://livrepository.liverpool.ac.uk/id/eprint/3051510