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.
翻译:本文研究加权基本并行过程(WBPP),这是一种受进程代数和Petri网理论启发、对加权有限自动机进行非线性递归推广的模型。我们的主要成果是提出了一个具有2-EXPSPACE复杂度的WBPP等价性判定算法。虽然(未加权的)BPP语言等价性不可判定,但我们可以利用该算法以相同复杂度判定BPP的多重等价性与无歧义BPP的语言等价性。这些问题是加权上下文无关文法相关模型中长期存在的开放性问题。我们的第二个贡献在于建立了WBPP、多项式微分方程组的幂级数解与组合计数之间的关联。为此,我们引入可构造微分有限幂级数(CDF)——这是由Bergeron和Reutenauer提出的多元微分代数级数类别,旨在为微分方程提供组合解释。CDF级数推广了有理级数、代数级数以及一大类D-有限(全纯)级数,这些级数的等价性判定问题长期悬而未决。我们证明CDF级数对应于交换WBPP级数。基于WBPP与交换性的研究成果,我们进一步证明CDF幂级数的等价性可在2-EXPTIME复杂度内判定。复杂度分析基于代数几何的有效界,具体涉及通过有限多个多元多项式环导子(未必可交换)的重复应用所构造的多项式理想链长度。这是通过推广Novikov和Yakovenko在单导子情形下的结果而实现的,值得注意的是一般情形下理想链的通用界具有非原始递归性。在研究过程中,我们发展了WBPP级数与CDF幂级数的理论体系,揭示了它们若干引人注目的性质。