Abstract
We introduce Petruchio, a tool for computing Petri net translations of dynamic networks. To cater for unbounded architectures beyond the capabilities of existing implementations, the principle fixed-point engine runs interleaved with coverability queries. We discuss algorithmic enhancements and provide experimental evidence that Petruchio copes with models of reasonable size.
Chapter PDF
Similar content being viewed by others
References
Abdulla, P.A., Bouajjani, A., Cederberg, J., Haziza, F., Rezine, A.: Monotonic abstraction for programs with dynamic memory heaps. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 341–354. Springer, Heidelberg (2008)
Abdulla, P.A., Čerans, K., Jonsson, B., Tsay, Y.-K.: Algorithmic analysis of programs with well quasi-ordered domains. Inf. Comp. 160(1-2), 109–127 (2000)
Busi, N., Gorrieri, R.: Distributed semantics for the π-calculus based on Petri nets with inhibitor arcs. JLAP 78(1), 138–162 (2009)
Devillers, R., Klaudel, H., Koutny, M.: A compositional Petri net translation of general π-calculus terms. For Asp. Comp. 20(4-5), 429–450 (2008)
Finkel, A., Schnoebelen, P.: Well-structured transition systems everywhere! TCS 256(1-2), 63–92 (2001)
Hirschkoff, D.: An extensional spatial logic for mobile processes. In: Gardner, P., Yoshida, N. (eds.) CONCUR 2004. LNCS, vol. 3170, pp. 325–339. Springer, Heidelberg (2004)
Joshi, S., König, B.: Applying the graph minor theorem to the verification of graph transformation systems. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 214–226. Springer, Heidelberg (2008)
Khomenko, V., Koutny, M., Niaouris, A.: Applying Petri net unfoldings for verification of mobile systems. In: MOCA, Bericht FBI-HH-B-267/06, pp. 161–178. University of Hamburg (2006)
Khomenko, V., Meyer, R.: Checking π-calculus structural congruence is graph isomorphism complete. In: ACSD, pp. 70–79. IEEE, Los Alamitos (2009)
König, B., Kozioura, V.: Counterexample-guided abstraction refinement for the analysis of graph transformation systems. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 197–211. Springer, Heidelberg (2006)
König, B., Kozioura, V.: Incremental construction of coverability graphs. IPL 103(5), 203–209 (2007)
Model Checking Kit, http://www.fmi.uni-stuttgart.de/szs/tools/mckit/
Meyer, R.: A theory of structural stationarity in the π-calculus. Acta Inf. 46(2), 87–137 (2009)
Meyer, R., Gorrieri, R.: On the relationship between π-calculus and finite place/transition Petri nets. In: Bravetti, M., Zavattaro, G. (eds.) CONCUR 2009. LNCS, vol. 5710, pp. 463–480. Springer, Heidelberg (2009)
Meyer, R., Khomenko, V., Strazny, T.: A practical approach to verification of mobile systems using net unfoldings. Fund. Inf. 94(3-4), 439–471 (2009)
Orava, F., Parrow, J.: An algebraic verification of a mobile network. For. Asp. Comp. 4(6), 497–543 (1992)
Petruchio, http://petruchio.informatik.uni-oldenburg.de
Rensink, A.: Canonical graph shapes. In: Schmidt, D. (ed.) ESOP 2004. LNCS, vol. 2986, pp. 401–415. Springer, Heidelberg (2004)
Sagiv, S., Reps, T.W., Wilhelm, R.: Parametric shape analysis via 3-valued logic. ACM TOPLAS 24(3), 217–298 (2002)
Saksena, M., Wibling, O., Jonsson, B.: Graph grammar modeling and verification of ad hoc routing protocols. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 18–32. Springer, Heidelberg (2008)
Spatial Logic Model Checker, http://ctp.di.fct.unl.pt/SLMC/
Wies, T., Zuffrey, D., Henzinger, T.A.: Forward analysis of depth-bounded processes. In: Ong, L. (ed.) FOSSACS 2010. LNCS, vol. 6014, pp. 94–108. Springer, Heidelberg (2010)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Meyer, R., Strazny, T. (2010). Petruchio: From Dynamic Networks to Nets. In: Touili, T., Cook, B., Jackson, P. (eds) Computer Aided Verification. CAV 2010. Lecture Notes in Computer Science, vol 6174. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-14295-6_19
Download citation
DOI: https://doi.org/10.1007/978-3-642-14295-6_19
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-14294-9
Online ISBN: 978-3-642-14295-6
eBook Packages: Computer ScienceComputer Science (R0)