AI 中文总结
该研究提出一种生物神经回路的T型Petri网描述，克服了现有模拟方法的时序与精度限制，经三种微回路模拟验证，可提供形式化时序保证，响应时间符合解析预测，适用于快速硬件原型开发。
AI 中文摘要
当前模拟生物神经回路的方法，无论是在通用硬件还是专用神经形态平台上，都受到固定时间步长数值积分、硬件施加的精度限制，以及无法在实时约束下保证事件驱动的脉冲动力学的时序正确性的制约。本文提出一种生物神经回路的Petri网描述，通过将神经元、突触和脉冲事件建模为具有形式可验证时序语义的T型Petri网，克服了这些限制，实现了具备截止期限保证的实时执行，且与连续时间漏积分放电动力学存在解析上可处理的对应关系，与底层积分时间步长无关。为测试该模型，我们展示了三个模拟微回路的结果：反馈抑制、侧抑制和分层特征检测器。Petri神经元重现了每个回路预期的动力学特征，同时全程提供形式化有界时序保证，三种情况下的最坏情况响应时间均与解析预测匹配。
英文摘要
Current approaches to simulating biological neural circuits, whether on general-purpose hardware or dedicated neuromorphic platforms, remain constrained by fixed-timestep numerical integration, hardware-imposed precision limits, and an inability to guarantee timing correctness for event-driven spiking dynamics under real-time constraints. Here, we propose a Petri net description of biological neural circuits that overcomes these limitations by modeling neurons, synapses, and spike events as a T-timed Petri net with formally verifiable timing semantics, enabling deadline-guaranteed real-time execution and analytically tractable correspondence to continuous-time leak-integrate-and-fire dynamics, independent of the underlying integration timestep. To test the model, we present the results of three simulated microcircuits: feedback inhibition, lateral inhibition, and hierarchical feature detector. The Petri neuron reproduces the expected dynamical signatures of each circuit while providing formally bounded timing guarantees throughout, with worst-case response times matching analytical predictions across all three cases.
Comments18 pages, 8 figures
