Symbolic analysis and parameter synthesis for time Petri nets using Maude and SMT solving

DOI10.1007/978-3-031-33620-1_20MaRDI QIDQ6535202zbMATH OpenFDO

Authors Jaime Arias, Kyungmin Bae, Carlos Olarte, Peter Csaba Ölveczky, Laure Petrucci, Fredrik Rømming

Publication date 16 November 2023

Full work available at URL https://doi.org/10.1007/978-3-031-33620-1_20

zbMATH Keywords

Maudeparameter synthesisparametric timed Petri netsrewriting logicsemanticsSMTsymbolic reachability analysis

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42) Semantics in the theory of computing (68Q55) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• Cost problems for parametric time Petri nets
• Parameter Synthesis for Bounded Cost Reachability in Time Petri Nets
• SMT-based reachability checking for bounded time Petri nets
• Parametric model-checking of stopwatch Petri nets
• Symbolic unfolding of parametric stopwatch Petri nets

Cites work

• Abstract logical model checking of infinite-state systems using narrowing
• Abstraction and completeness for real-time Maude
• All about Maude -- a high-performance logical framework. How to specify, program and verify systems in rewriting logic. With CD-ROM.
• Canonization of reconfigurable PT nets in \texttt{Maude}
• Coloured Petri Nets
• Conditional rewriting logic as a unified model of concurrency
• Cost problems for parametric time Petri nets
• Diagnosis Using Unfoldings of Parametric Time Petri Nets
• Generalized rewrite theories, coherence completion, and symbolic methods
• scientific article; zbMATH DE number 1956600 (Why is no real title available?)
• scientific article; zbMATH DE number 1973125 (Why is no real title available?)
• Model checking
• Model checking reconfigurable Petri nets with Maude
• Parametric model-checking of stopwatch Petri nets
• Parametric Model-Checking of Time Petri Nets with Stopwatches Using the State-Class Graph
• Petri nets are monoids
• Precise robustness analysis of time Petri nets with inhibitor ARCS
• Rewriting modulo SMT and open system analysis
• Romeo: a parametric model-checker for Petri nets with stopwatches
• Semantics and pragmatics of real-time maude
• Specification and analysis of the AER/NCA active network protocol suite in real-time Maude
• Specification of real-time and hybrid systems in rewriting logic
• Twenty years of rewriting logic
• Verifying hierarchical Ptolemy II discrete-event models using real-time maude

Cited in

(3)

• Parameter Synthesis for Bounded Cost Reachability in Time Petri Nets
• A rewriting-logic-with-SMT-based formal analysis and parameter synthesis framework for parametric time Petri nets
• Formal analysis of real-time systems with user-defined strategies in rewriting logic

This page was built for publication: Symbolic analysis and parameter synthesis for time Petri nets using Maude and SMT solving

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6535202)