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 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.
|Title of host publication
|2023 38th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2023
|Published - 2023
|38th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2023 - Boston, United States
Duration: 26 Jun 2023 → 29 Jun 2023
|38th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2023
|26/06/2023 → 29/06/2023
|ACM Special Interest Group on Logic and Computation (SIGLOG), Boston University College of Arts and Sciences, Boston University Department of Computer Science, Boston University Rafik B. Hariri Institute for Computing and Computational Science and Engineering, IEEE Technical Committee on Mathematical Foundations of Computing
|Proceedings - Symposium on Logic in Computer Science
Bibliographical noteFunding Information:
Acknowledgments. The work was partially supported by the DFF project REDUCTO 9040-00224B, the Poul Due Jensen Grant 883901, the Villum Investigator Grant S4OS, and the PRIN project SEDUCE 2017TWRCNB.
© 2023 IEEE.