The goal of this paper is to provide exact and terminating algorithms for the formal analysis of deterministic continuous-time control systems with affine input and polynomial state dynamics (in short, polynomial systems). We consider the following semantic properties: zeroness and equivalence, input independence, linearity, and analyticity. Our approach is based on Chen-Fliess series, which provide a unique representation of the dynamics of such systems via their formal generating series. Our starting point is Fliess' seminal work showing how the semantic properties above are mirrored by corresponding combinatorial properties on generating series. Next, we observe that the generating series of polynomial systems coincide with the class of shuffle-finite series, a nonlinear generalisation of Sch\"utzenberger's rational series which has recently been studied in the context of automata theory and enumerative combinatorics. We exploit and extend recent results in the algorithmic analysis of shuffle-finite series (such as zeroness, equivalence, and commutativity) to show that the semantic properties above can be decided exactly and in finite time for polynomial systems. Some of our analyses rely on a novel technical contribution, namely that shuffle-finite series are closed under support restrictions with commutative regular languages, a result of independent interest.

翻译：本文旨在为具有仿射输入与多项式状态动力学（简称多项式系统）的确定性连续时间控制系统提供精确且可终止的形式化分析算法。我们考察以下语义属性：零性与等价性、输入无关性、线性性及解析性。我们的方法基于陈-弗里斯级数，该级数通过形式生成级数为此类系统的动力学提供唯一表示。我们的研究起点是弗里斯的基础性工作，其揭示了上述语义属性如何通过生成级数的组合性质得以反映。进一步，我们观察到多项式系统的生成级数与洗牌有限级数类相重合——这是舒岑伯格有理级数的一种非线性推广，近期已在自动机理论与枚举组合学背景下得到研究。通过利用并扩展洗牌有限级数算法分析领域的最新成果（如零性、等价性与交换性判定），我们证明了上述语义属性可在有限时间内对多项式系统进行精确判定。部分分析依赖于一项新的技术贡献：洗牌有限级数在可交换正则语言支撑限制下具有封闭性，该结论本身具有独立的理论价值。