Bounded Parametric Verification for Distributed Time Petri Nets with Discrete-Time Semantics

Issue title: Concurrency Specification and Programming (CS&P)

Article type: Research Article

Authors: Knapik, Michał | Penczek, Wojciech | Szreter, Maciej | Półrola,

Affiliations: Polish Academy of Sciences, ICS, Ordona 21, 01-237 Warsaw, Poland. [email protected], [email protected], [email protected] | University of Łódź, FMCS, Banacha 22, 90-238 Łódź, Poland. [email protected]

Note: [] Address for correspondence: Polish Academy of Sciences, ICS Ordona 21, 01-237 Warsaw, Poland

Note: [] Also affiliated with: Institute of Informatics, Podlasie Academy, Sienkiewicza 51, 08-110 Siedlce, Poland

Abstract: Bounded Model Checking (BMC) is an efficient technique applicable to verification of temporal properties of (timed) distributed systems. In this paper we show for the first time how to apply BMC to parametric verification of time Petri nets with discrete-time semantics. The properties are expressed by formulas of the logic PRTECTL - a parametric extension of the existential fragment of Computation Tree Logic (CTL).

DOI: 10.3233/FI-2010-272

Journal: Fundamenta Informaticae, vol. 101, no. 1-2, pp. 9-27, 2010