paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Minimization of Dynamical Systems over Monoids

幺半群上的动力系统最小化
LICS 2023 38th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)2023匹配度 2/10 · 该论文属于形式语义/形式化方法中的双模拟与动力系统最小化,虽然涉及形式化验证和划分细化算法,但与用户核心方向(PL与LLM/Agentic程序静态分析、浮点程序分析、贝叶斯程序分析及其与LLM交叉)没有直接关系,也未涉及LLM、静态分析工具或工业落地。引用 2 inbox
Georgios Argyris, Alberto Lluch Lafuente, Alexander Leguizamon Robayo, Mirco Tribastone, Max Tschaikowski, Andrea Vandin
crossref: 2026-09-12dblp: 2026-09-12arxiv: 2026-09-12

AI 速览

一句话:提出广义前向双模拟及划分细化算法,统一并扩展动力系统在交换幺半群上的最小化。

针对动力系统最小化中双模拟定义依赖具体模型的问题,论文在交换幺半群上提出广义前向双模拟(GFB),并给出计算最粗划分的划分细化算法。该框架在 (ℝ,+) 上统一 Markov 链概率双模拟与非线性 ODE 前向双模拟,在 (ℝ,•) 下产生乘积型非线性约简。作者用 GFB 最小化原型评估:在 60 个 Boolean 网络中发现保析取/合取约简并带来分析加速,解释两个网络的生物意义,并分析一个原本不可处理的大型网络;随机化版本在 21 个加权动力网络上得到保乘积约简。

问题
如何为 Markov 链、ODE、Boolean 网络等不同动力模型提供统一的双模拟最小化框架,并计算最粗等价划分。
方法
在交换幺半群上定义广义前向双模拟(GFB),设计划分细化算法求最粗 GFB,并给出随机化扩展。
评估
在 60 个 Boolean 网络和 21 个加权动力网络上实现原型,报告约简效果、分析加速及生物解释。
原文摘要(Abstract)

Quantitative notions of bisimulation are well-known tools for the minimization of dynamical models such as Markov chains and ordinary differential equations (ODEs). In forward bisimulations, each state in the quotient model represents an equivalence class and the dynamical evolution gives the overall sum of its members in the original model. Here we introduce generalized forward bisimulation (GFB) for dynamical systems over commutative monoids and develop a partition refinement algorithm to compute the coarsest one. When the monoid is (ℝ,+), we recover probabilistic bisimulation for Markov chains and more recent forward bisimulations for nonlinear ODEs. Using (ℝ,•) we get nonlinear reductions for discrete-time dynamical systems and ODEs where each variable in the quotient model represents the product of original variables in the equivalence class. When the domain is a finite set such as the Booleans $\mathbb{B}$, we can apply GFB to Boolean networks (BN), a widely used dynamical model in computational biology. Using a prototype implementation of our minimization algorithm for GFB, we find disjunction- and conjunction-preserving reductions on 60 BN from two well-known repositories, and demonstrate the obtained analysis speed-ups. We also provide the biological interpretation of the reduction obtained for two selected BN, and we show how GFB enables the analysis of a large one that could not be analyzed otherwise. Using a randomized version of our algorithm we find product-preserving (therefore non-linear) reductions on 21 dynamical weighted networks from the literature that could not be handled by the exact algorithm.

链接与引用

DOI 原文 · arXiv · PDF(开放获取) · DBLP

BibTeX
@inproceedings{abs-2206-15169,
  title = {Minimization of Dynamical Systems over Monoids},
  author = {Georgios Argyris and Alberto Lluch Lafuente and Alexander Leguizamon Robayo and Mirco Tribastone and Max Tschaikowski and Andrea Vandin},
  booktitle = {LICS},
  year = {2023},
  doi = {10.1109/lics56636.2023.10175697}
}