Petruchio
A theory of structural stationarity in the π-calculus Automata-theoretic representations have proven useful in the automatic and exact analysis of computing systems. We propose a new semantical mapping of π-Calculus processes into place/transition Petri nets. Our translation exploits the connections created by restricted names and can yield finite nets even for processes with unbounded name and unbounded process creation. The property of structural stationarity characterises the processes mapped to finite nets. We provide exact conditions for structural stationarity using novel characteristic functions. As application of the theory, we identify a rich syntactic class of structurally stationary processes, called finite handler processes. Our Petri net translation facilitates the automatic verification of a case study modelled in this class
Keywords for this software
References in zbMATH (referenced in 16 articles , 2 standard articles )
Showing results 1 to 16 of 16.
Sorted by year (- Lomuscio, Alessio; Pirovano, Edoardo: A counter abstraction technique for verifying properties of probabilistic swarm systems (2022)
- Bhattacharyya, Anirban; Mokhov, Andrey; Pierce, Ken: An empirical comparison of formalisms for modelling and analysis of dynamic reconfiguration of dependable systems (2017)
- D’Osualdo, Emanuele; Luke Ong, C.-H.: On hierarchical communication topologies in the (\pi)-calculus (2016)
- Khomenko, Victor; Meyer, Roland; Hüchting, Reiner: A polynomial translation of (\pi)-calculus FCPS to safe Petri nets (2013)
- Acciai, Lucia; Boreale, Michele: Deciding safety properties in infinite-state pi-calculus via behavioural types (2012)
- Gloria, Antoine: Numerical homogenization: survey, new results, and perspectives (2012)
- Kaiser, Alexander; Kroening, Daniel; Wahl, Thomas: Efficient coverability analysis by proof minimization (2012)
- Meyer, Roland; Khomenko, Victor; Hüchting, Reiner: A polynomial translation of (\pi)-calculus (FCP) to safe Petri nets (2012)
- Rosa-Velardo, Fernando; Martos-Salgado, María: Multiset rewriting for the verification of depth-bounded processes with name binding (2012)
- Meyer, Roland; Strazny, Tim: \textscPetruchio: From dynamic networks to nets (2010) ioport
- Baldan, Paolo; Bonchi, Filippo; Gadducci, Fabio: Encoding asynchronous interactions using open Petri nets (2009)
- Busi, Nadia; Gorrieri, Roberto: Distributed semantics for the (\pi)-calculus based on Petri nets with inhibitor ARCS (2009)
- Meyer, Roland: A theory of structural stationarity in the (\pi)-calculus (2009)
- Meyer, Roland; Gorrieri, Roberto: On the relationship between (\pi)-calculus and finite place/transition Petri nets (2009)
- Meyer, Roland; Khomenko, Victor; Strazny, Tim: A practical approach to verification of mobile systems using net unfolding (2009)
- Meyer, Roland; Khomenko, Victor; Strazny, Tim: A practical approach to verification of mobile systems using net unfoldings (2008)
Further publications can be found at: http://petruchio.informatik.uni-oldenburg.de/33467.html