DocumentCode
2783900
Title
Translating Structural Process Properties to Petri Net Markings
Author
Linker, Sven
Author_Institution
Carl von Ossietzky Univ. Oldenburg, Oldenburg, Germany
fYear
2012
fDate
27-29 June 2012
Firstpage
82
Lastpage
91
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;
fLanguage
English
Publisher
ieee
Conference_Titel
Application of Concurrency to System Design (ACSD), 2012 12th International Conference on
Conference_Location
Hamburg
ISSN
1550-4808
Print_ISBN
978-1-4673-1687-3
Type
conf
DOI
10.1109/ACSD.2012.11
Filename
6253459
Link To Document