Title :
Translating Structural Process Properties to Petri Net Markings
Author_Institution :
Carl von Ossietzky Univ. Oldenburg, Oldenburg, Germany
Abstract :
We introduce a spatio-temporal logic PSTL defined on Pi-Calculus processes. This logic is especially suited to formulate properties in relation to the structural semantics of the Pi-Calculus due to Meyer, a representation of processes as Petri nets. To allow for the use of well-researched verification techniques, we present a translation of a subset of PSTL to LTL on Petri nets. We further prove soundness of our translation.
Keywords :
Petri nets; pi calculus; temporal logic; LTL; PSTL; Petri net markings; pi-calculus processes; spatio-temporal logic; structural process property translation; verification techniques; Base stations; Mobile communication; Petri nets; Radio frequency; Semantics; Switches; Syntactics; Pi-Calculus; petri nets; process algebra; spatial logic; temporal logic; verification;
Conference_Titel :
Application of Concurrency to System Design (ACSD), 2012 12th International Conference on
Conference_Location :
Hamburg
Print_ISBN :
978-1-4673-1687-3
DOI :
10.1109/ACSD.2012.11
