Affiliations: Polish Academy of Sciences, ICS, Ordona 21, 01-237 Warsaw, Poland. mknapik@ipipan.waw.pl, penczek@ipipan.waw.pl, mszreter@ipipan.waw.pl | University of Łódź, FMCS, Banacha 22, 90-238 Łódź, Poland. polrola@math.uni.lodz.pl
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).
