Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Simulating Petri nets with Boolean Matrix Logic Programming

Lun Ai, Stephen H. Muggleton, Shi-Shun Liang, Geoff S. Baldwin

TL;DR

This work addresses efficient reachability analysis for Petri nets embedded in logic programming. It introduces Boolean Matrix Logic Programming (BMLP), which compiles linear and immediately recursive Datalog into boolean matrices and computes transitive closures, enabling scalable evaluation of one-bounded elementary nets (OENs). Two algorithms, Iterative Extension ($O(k n^2)$) and Repeated Matrix Squaring ($O(n^3 \log_2 n)$), implement the framework, and the OEN-to-Datalog transformation guarantees semantic equivalence with reachability. Empirical results on airplane-route graphs and genome-scale metabolic models show substantial speedups over state-of-the-art Prolog systems with tabling and Clingo, highlighting BMLP’s potential for large-scale knowledge-graph analysis and system verification.

Abstract

Recent attention to relational knowledge bases has sparked a demand for understanding how relations change between entities. Petri nets can represent knowledge structure and dynamically simulate interactions between entities, and thus they are well suited for achieving this goal. However, logic programs struggle to deal with extensive Petri nets due to the limitations of high-level symbol manipulations. To address this challenge, we introduce a novel approach called Boolean Matrix Logic Programming (BMLP), utilising boolean matrices as an alternative computation mechanism for Prolog to evaluate logic programs. Within this framework, we propose two novel BMLP algorithms for simulating a class of Petri nets known as elementary nets. This is done by transforming elementary nets into logically equivalent datalog programs. We demonstrate empirically that BMLP algorithms can evaluate these programs 40 times faster than tabled B-Prolog, SWI-Prolog, XSB-Prolog and Clingo. Our work enables the efficient simulation of elementary nets using Prolog, expanding the scope of analysis, learning and verification of complex systems with logic programming techniques.

Simulating Petri nets with Boolean Matrix Logic Programming

TL;DR

This work addresses efficient reachability analysis for Petri nets embedded in logic programming. It introduces Boolean Matrix Logic Programming (BMLP), which compiles linear and immediately recursive Datalog into boolean matrices and computes transitive closures, enabling scalable evaluation of one-bounded elementary nets (OENs). Two algorithms, Iterative Extension () and Repeated Matrix Squaring (), implement the framework, and the OEN-to-Datalog transformation guarantees semantic equivalence with reachability. Empirical results on airplane-route graphs and genome-scale metabolic models show substantial speedups over state-of-the-art Prolog systems with tabling and Clingo, highlighting BMLP’s potential for large-scale knowledge-graph analysis and system verification.

Abstract

Recent attention to relational knowledge bases has sparked a demand for understanding how relations change between entities. Petri nets can represent knowledge structure and dynamically simulate interactions between entities, and thus they are well suited for achieving this goal. However, logic programs struggle to deal with extensive Petri nets due to the limitations of high-level symbol manipulations. To address this challenge, we introduce a novel approach called Boolean Matrix Logic Programming (BMLP), utilising boolean matrices as an alternative computation mechanism for Prolog to evaluate logic programs. Within this framework, we propose two novel BMLP algorithms for simulating a class of Petri nets known as elementary nets. This is done by transforming elementary nets into logically equivalent datalog programs. We demonstrate empirically that BMLP algorithms can evaluate these programs 40 times faster than tabled B-Prolog, SWI-Prolog, XSB-Prolog and Clingo. Our work enables the efficient simulation of elementary nets using Prolog, expanding the scope of analysis, learning and verification of complex systems with logic programming techniques.
Paper Structure (25 sections, 7 theorems, 16 equations, 5 figures, 3 tables, 2 algorithms)

This paper contains 25 sections, 7 theorems, 16 equations, 5 figures, 3 tables, 2 algorithms.

Table of Contents

  1. Introduction
  2. Related work
  3. Preliminaries
  4. Elementary nets
  5. Matrix algebra for datalog
  6. Transforming elementary nets
  7. Boolean matrix logic programming
  8. Problem setting
  9. Framework
  10. Boolean matrix compilation
  11. Iterative extension (BMLP-IE)
  12. Repeated matrix squaring (BMLP-RMS)
  13. Computing reachability
  14. Experiments
  15. Airplane flight routes
  16. ...and 10 more sections

Key Result

Theorem 1

Let $\mathcal{P}$ be a datalog program transformed from an OEN = (P, T, F). For constant symbols $p_1$, $p_2$ in $\mathcal{P}$, $\mathcal{P} \models r(p_1,p_2)$ if and only if $p_2$ is reachable from $p_1$ in the OEN.

Figures (5)

  • Figure 1: Left: A Petri (elementary) net of transit flights between 5 cities with tokens on nodes "Berlin" and "Paris". Transit passengers can take different routes to their destinations. Passengers to New York from Berlin and Paris should arrive before the flights from London and Toronto go to New York. Right: Graphical view of relations in the OpenFlights database describing 67663 airplane flights between 3321 cities.
  • Figure 2: An OEN. Places are ellipses. Transitions are rectangles. Arcs are marked with weights. A black dot is a token. The initial marking is $m(p_3) = m(p_4) = 1$ with a set representation $\{p_3, p_4\}$. Firing transition $t_2$ gives a new marking $\{p_4, p_5\}$.
  • Figure 3: Runtime when the probability $p_t$ of transitions (ground facts) is 0.001 but the No. places (constant symbols) $n$ varies.
  • Figure 4: Runtime when No. places (constant symbols) $n$ = 1000 and the probability $p_t$ of transitions (ground facts) varies.
  • Figure 5: Runtime for computing producible substrates from reactions in the genome-scale metabolic network model iML1515.

Theorems & Definitions (21)

  • Definition 1: OEN transformation
  • Example 1
  • Example 2
  • Theorem 1
  • proof
  • Definition 2: Boolean Matrix Logic Programming (BMLP) problem
  • Example 3
  • Proposition 1
  • proof
  • Proposition 2
  • ...and 11 more