Weighted basic parallel processes and combinatorial enumeration
Lorenzo Clemente
TL;DR
The paper introduces WBPP, a nonlinear weighted extension of basic parallel processes, and proves a fundamental decision result: WBPP equivalence lies in $2\text{-}EXPSPACE$, with immediate corollaries for multiplicity equivalence of BPP and language equivalence of unambiguous BPP. It then builds a deep bridge to constructible differential finite (CDF) power series, showing that commutative WBPP series correspond exactly to CDF power series and obtaining a $2\text{-}EXPTIME$ zeroness procedure for CDF. The work further connects these automata-theoretic objects to combinatorial species, establishing that strongly constructible/constructible species have CDF generating series and that multiplicity equivalence is decidable for a broad class of species. Central to the results are new elementary bounds on chains of polynomial ideals generated by finite sets of (possibly noncommuting) derivations, generalizing Novikov–Yakovenko, which yield elementary complexity despite the expressive strength of the models. Overall, the paper unifies automata theory, differential algebra, and combinatorics to obtain sharp decidability and complexity results for equivalence and zeroness problems across WBPP, BPP, CDF, and constructible species.
Abstract
We study weighted basic parallel processes (WBPP), a nonlinear recursive generalisation of weighted finite automata inspired from process algebra and Petri net theory. Our main result is an algorithm of 2-EXPSPACE complexity for the WBPP equivalence problem. While (unweighted) BPP language equivalence is undecidable, we can use this algorithm to decide multiplicity equivalence of BPP and language equivalence of unambiguous BPP, with the same complexity. These are long-standing open problems for the related model of weighted context-free grammars. Our second contribution is a connection between WBPP, power series solutions of systems of polynomial differential equations, and combinatorial enumeration. To this end we consider constructible differentially finite power series (CDF), a class of multivariate differentially algebraic series introduced by Bergeron and Reutenauer in order to provide a combinatorial interpretation to differential equations. CDF series generalise rational, algebraic, and a large class of D-finite (holonomic) series, for which decidability of equivalence was an open problem. We show that CDF series correspond to commutative WBPP series. As a consequence of our result on WBPP and commutativity, we show that equivalence of CDF power series can be decided with 2-EXPTIME complexity. The complexity analysis is based on effective bounds from algebraic geometry, namely on the length of chains of polynomial ideals constructed by repeated application of finitely many, not necessarily commuting derivations of a multivariate polynomial ring. This is obtained by generalising a result of Novikov and Yakovenko in the case of a single derivation, which is noteworthy since generic bounds on ideal chains are non-primitive recursive in general. On the way, we develop the theory of \WBPP~series and \CDF~power series, exposing several of their appealing properties.