Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

A rewriting-logic-with-SMT-based formal analysis and parameter synthesis framework for parametric time Petri nets

Jaime Arias, Kyungmin Bae, Carlos Olarte, Peter Csaba Ölveczky, Laure Petrucci

TL;DR

A new general folding approach for symbolic reachability is developed, so that Maude-with-SMT reachability analysis terminates whenever the parametric state-class graph of the PITPN is finite.

Abstract

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.

A rewriting-logic-with-SMT-based formal analysis and parameter synthesis framework for parametric time Petri nets

TL;DR

A new general folding approach for symbolic reachability is developed, so that Maude-with-SMT reachability analysis terminates whenever the parametric state-class graph of the PITPN is finite.

Abstract

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.
Paper Structure (35 sections, 8 theorems, 14 equations, 9 figures)

This paper contains 35 sections, 8 theorems, 14 equations, 9 figures.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Transition systems and bisimulations
  4. Parametric time Petri nets with inhibitor arcs
  5. Rewriting with SMT and Maude
  6. Rewrite theories.
  7. Rewriting with SMT rocha-rewsmtjlamp-2017.
  8. Maude.
  9. Meta-programming.
  10. A rewriting logic semantics for ITPNs
  11. Formalizing ITPNs in Maude: The theory $\rtheorySem$
  12. Dynamics.
  13. Correctness of the semantics
  14. Some variations of $\rtheorySem$
  15. The theory $\rtheorySemN{1}$
  16. ...and 20 more sections

Key Result

theorem 1

Let $\PN = \tuple{\Place, \Transition, \emptyset, \relPre{(.)}, \relPost{(.)}, \relInhib{(.)}, \markingInit, \parIntervalStatic, true}$ be an ITPN, and $\mathcal{R}_0 = (\Sigma,E,L,R)$. Then, $\approx$ is a bisimulation between the transition systems $\mathcal{S_{\PN}} = (\mathcal{A},a_{0},\rightarr

Figures (9)

  • Figure 1: A PITPN and its valuation.
  • Figure 2: A simple production-consumption system taken from Wang1998.
  • Figure 3: The scheduling case study taken from DBLP:journals/jucs/TraonouezLR09.
  • Figure 4: The tutorial case study.
  • Figure 5: -Synthesis. Execution times in log-scale for and Maude connected with Yices2 (), Maude-SE with Yices2 (), Z3 (), and CVC4 ().
  • ...and 4 more figures

Theorems & Definitions (22)

  • definition 1: Parametric time Petri net with inhibitor arcs
  • definition 2: Semantics of an ITPN paris-paper
  • definition 3
  • definition 4
  • definition 5
  • theorem 1
  • proof
  • lemma 1
  • proof
  • lemma 2
  • ...and 12 more