English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Tools annual

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Tools monthly

Global: Zendy Plus monthly

Presents the access of premium content as premium feature

Premium Content

Global: Zendy Plus annual

Global: Zendy Free Plan

Parametric time Petri nets with inhibitor arcs (PITPNs) support flexibilityfor timed systems by allowing parameters in firing bounds. In this paper wepresent and prove correct a concrete and a symbolic rewriting logic semanticsfor PITPNs. We show how this allows us to use Maude combined with SMT solvingto provide sound and complete formal analyses for PITPNs. We develop a newgeneral folding approach for symbolic reachability that terminates whenever theparametric state-class graph of the PITPN is finite. We explain how almost allformal analysis and parameter synthesis supported by the state-of-the-art PITPNtool Rom\'eo can be done in Maude with SMT. In addition, we also supportanalysis and parameter synthesis from parametric initial markings, as well asfull LTL model checking and analysis with user-defined execution strategies.Experiments on three benchmarks show that our methods outperform Rom\'eo inmany cases.

Symbolic Analysis and Parameter Synthesis for Time Petri Nets Using Maude and SMT Solving