Tim Strazny

 

1 Publications (with abstracts)

[Str11]

Tim Strazny. Accelerating backward reachability analysis. In Paul Pettersson and Cristina Seceleanu, editors, Proceedings of the 23rd Nordic Workshop on Programming Theory (NWPT'11), pages 2-4. Mälardalen University Sweden, October 2011. Technical report 254/2011.
[ bib ]

In the context of depth-first backward reachability analysis, we identify two general operations which allow for performance improvements, while covering well-known techniques such as partial order methods and pruning. We instantiate these operations with novel backward acceleration techniques and employ methods of guided search in this context. Further, we introduce support-based search trees, a data structure to represent upward-closed sets (ucs's) which allows for efficient implementation of operations necessary for the analysis.

[MS10]

R. Meyer and T. Strazny. Petruchio: From dynamic networks to nets. In Tayssir Touili, Byron Cook, and Paul Jackson, editors, Proceedings of the 22nd International Conference on Computer Aided Verification 2010, CAV 2010, volume 6174 of LNCS, pages 175-179. Springer-Verlag, 2010.
[ bib ]

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.

[MKS09]

R. Meyer, V. Khomenko, and T. Strazny. A practical approach to verification of mobile systems using net unfoldings. Fundamenta Informaticae, 94(3-4):439-471, 2009. Special Issue on Petri Nets 2008, invited version of the ATPN 2008 paper.
[ bib ]

We propose a technique for verification of mobile systems. We translate finite control processes, which are a well-known subset of , into Petri nets, which are subsequently used for model checking. This translation always yields bounded Petri nets with a small bound, and we develop a technique for computing a non-trivial bound by static analysis. Moreover, we introduce the notion of safe processes, which are a subset of finite control processes, for which our translation yields safe Petri nets, and show that every finite control process can be translated into a safe one of at most quadratic size. This gives a possibility to translate every finite control process into a safe Petri net, for which efficient unfolding-based verification is possible. Our experiments show that this approach has a significant advantage over other existing tools for verification of mobile systems in terms of memory consumption and runtime. We also demonstrate the applicability of our method on a realistic model of an automated manufacturing system.

Keywords: finite control processes, safe processes, pi-Calculus, mobile systems, model checking, Petri net unfoldings

[MKS08a]

R. Meyer, V. Khomenko, and T. Strazny. A practical approach to verification of mobile systems using net unfoldings. In Proc. of the 29th International Conference on Application and Theory of Petri Nets and Other Models of Concurrency, ATPN 2008, volume 5062 of LNCS, pages 327-347. Springer-Verlag, 2008.
[ bib ]

In this paper we propose a technique for verification of mobile systems.We translate finite control processes, which are a well-known subset of pi-Calculus, into Petri nets, which are subsequently used for model checking. This translation always yields bounded Petri nets with a small bound, and we develop a technique for computing a non-trivial bound by static analysis. Moreover, we introduce the notion of safe pro- cesses, which are a subset of finite control processes, for which our translation yields safe Petri nets, and show that every finite control process can be translated into a safe one of at most quadratic size. This gives a possibility to translate every finite control process into a safe Petri net, for which efficient unfolding-based verification is possible. Our experiments show that this approach has a significant advantage over other existing tools for verification of mobile systems in terms of memory consumption and runtime.

Keywords: finite control processes, safe processes, pi-Calculus, mobile systems, model checking, Petri net unfoldings

[MKS08b]

R. Meyer, V. Khomenko, and T. Strazny. A practical approach to verification of mobile systems using net unfoldings. Technical Report CS-TR: 1064, School of Computing Science, Newcastle University, January 2008. 29 pages.
[ bib ]

In this paper we propose a technique for verification of mobile systems.We translate finite control processes, which are a well-known subset of pi-Calculus, into Petri nets, which are subsequently used for model checking. This translation always yields bounded Petri nets with a small bound, and we develop a technique for computing a non-trivial bound by static analysis. Moreover, we introduce the notion of safe pro- cesses, which are a subset of finite control processes, for which our translation yields safe Petri nets, and show that every finite control process can be translated into a safe one of at most quadratic size. This gives a possibility to translate every finite control process into a safe Petri net, for which efficient unfolding-based verification is possible. Our experiments show that this approach has a significant advantage over other existing tools for verification of mobile systems in terms of memory consumption and runtime.

Keywords: finite control processes, safe processes, pi-Calculus, mobile systems, model checking, Petri net unfoldings

[SS06]

Tim Strazny and Christian Stehno. Ein Simulator für mehrfach erweiterte höhere Petrinetze. In Matthias Becker and Helena Szczerbicka, editors, 19. Symposium Simulationstechnik (ASIM 2006), pages 171-176. SCS Publishing House e.V., September 2006.
[ bib ]

Petrinetze mit ihrer eindeutigen Semantik und dem zugrunde liegenden mathematischen Modell bewähren sich vermehrt bei Entwurf, Analyse und Steuerung komplexer, asynchroner und verteilter Systeme. Insbesondere zeitbehaftete stochastische gefärbte Petrinetze bieten Möglichkeiten komplizierte Sachverhalte strukturiert und kompakt auszudrücken, jedoch ist die Simulation solcher höheren Petrinetze um ein Vielfaches aufwändiger. Mit Geschwindigkeit und Vielfältigkeit als Hauptziel wurde mit P-UMLaut/Sim ein Simulator für solche mehrfach erweiterten Petrinetze entwickelt.