Sciweavers

FUIN
2010

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

13 years 8 months ago
Bounded Parametric Verification for Distributed Time Petri Nets with Discrete-Time Semantics
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).
Michal Knapik, Wojciech Penczek, Maciej Szreter, A
Added 02 Mar 2011
Updated 02 Mar 2011
Type Journal
Year 2010
Where FUIN
Authors Michal Knapik, Wojciech Penczek, Maciej Szreter, Agata Pólrola
Comments (0)