Jaime Arias ; Kyungmin Bae ; Carlos Olarte ; Peter Csaba Ölveczky ; Laure Petrucci - A rewriting-logic-with-SMT-based formal analysis and parameter synthesis framework for parametric time Petri nets

fi:12781 - Fundamenta Informaticae, November 10, 2024, Volume 192, Issues 3-4: Petri Nets 2023
A rewriting-logic-with-SMT-based formal analysis and parameter synthesis framework for parametric time Petri netsArticle

Authors: Jaime Arias ; Kyungmin Bae ; Carlos Olarte ; Peter Csaba Ölveczky ; Laure Petrucci

    This paper presents a concrete and a symbolic rewriting logic semantics for parametric time Petri nets with inhibitor arcs (PITPNs), a flexible model of timed systems where parameters are allowed in firing bounds. We prove that our semantics is bisimilar to the "standard" semantics of PITPNs. This allows us to use the rewriting logic tool Maude, combined with SMT solving, to provide sound and complete formal analyses for PITPNs. We develop and implement a new general folding approach for symbolic reachability, so that Maude-with-SMT reachability analysis terminates whenever the parametric state-class graph of the PITPN is finite. Our work opens up the possibility of using the many formal analysis capabilities of Maude -- including full LTL model checking, analysis with user-defined analysis strategies, and even statistical model checking -- for such nets. We illustrate this by explaining how almost all formal analysis and parameter synthesis methods supported by the state-of-the-art PITPN tool Romeo can be performed using Maude with SMT. In addition, we also support analysis and parameter synthesis from parametric initial markings, as well as full LTL model checking and analysis with user-defined execution strategies. Experiments show that our methods outperform Romeo in many cases.


    Volume: Volume 192, Issues 3-4: Petri Nets 2023
    Published on: November 10, 2024
    Accepted on: August 19, 2024
    Submitted on: January 4, 2024
    Keywords: Computer Science - Logic in Computer Science

    Consultation statistics

    This page has been seen 8 times.
    This article's PDF has been downloaded 9 times.