Parametric verification: an introduction

DOI10.1007/978-3-662-60651-3_3zbMATH Open1464.68224arXiv1907.00555OpenAlexW3098753623MaRDI QIDQ2032913FDOQ2032913

Laure Petrucci, Wojciech Penczek, Michał Knapik, Didier Lime, Étienne André

Publication date: 14 June 2021

Abstract: This paper constitutes a short introduction to parametric verification of concurrent systems. It originates from two 1-day tutorial sessions held at the Petri nets conferences in Toru'n (2016) and Zaragoza (2017). The paper presents not only the basic formal concepts tackled in the video version, but also an extensive literature to provide the reader with further references covering the area. We first introduce motivation behind parametric verification in general, and then focus on different models and approaches, for verifying several kinds of systems. They include Parametric Timed Automata, for modelling real-time systems, where the timing constraints are not necessarily known a priori. Similarly, Parametric Interval Markov Chains allow for modelling systems where probabilities of events occurrences are intervals with parametric bounds. Parametric Petri Nets allow for compact representation of systems, and cope with different types of parameters. Finally, Action Synthesis aims at enabling or disabling actions in a concurrent system to guarantee some of its properties. Some tools implementing these approaches were used during hands-on sessions at the tutorial. The corresponding practicals are freely available on the Web.

Full work available at URL: https://arxiv.org/abs/1907.00555

Recommendations

• Parametric model-checking of stopwatch Petri nets
• scientific article; zbMATH DE number 5175527
• Parametric model checking with VerICS
• scientific article
• A method for parametric verification of the behavior of time Petri nets

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Cited In (4)

• Automatizing parametric reasoning on distributed concurrent systems
• On completeness of liveness synthesis for parametric timed automata (Extended Abstract)
• Timed automata relaxation for reachability
• Title not available (Why is that?)

This page was built for publication: Parametric verification: an introduction

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