Tim Strazny

 

1 Publications (BibTeX Source)

@INPROCEEDINGS{strazny:2011:accelerating,
  AUTHOR = {Tim Strazny},
  TITLE = {Accelerating Backward Reachability Analysis},
  BOOKTITLE = {Proceedings of the 23rd Nordic Workshop on Programming Theory (NWPT'11)},
  YEAR = {2011},
  EDITOR = {Paul Pettersson and Cristina Seceleanu},
  PAGES = {2--4},
  MONTH = {October},
  ORGANIZATION = {M\"{a}lardalen University Sweden},
  NOTE = {Technical report 254/2011},
  ABSTRACT = {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 \emph{backward
 acceleration} techniques and employ methods of \emph{guided search}
 in this context. Further, we introduce \emph{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.},
  COMMENT = {M\"{a}lardalen Real-Time Research Centre, Box 883, 72123 V\"{a}ster\r{a}s,
 Sweden},
  ISSN = {1404-3041}
}


@INPROCEEDINGS{MS2010,
  EDITOR = {Tayssir Touili and
               Byron Cook and
               Paul Jackson},
  VOLUME = {6174},
  YEAR = {2010},
  PAGES = {175--179},
  ISBN = {978-3-642-14294-9},
  AUTHOR = {R. Meyer and T. Strazny},
  TITLE = {Petruchio: From dynamic networks to nets},
  BOOKTITLE = {Proceedings of the 22nd International Conference on Computer Aided Verification 2010, CAV 2010},
  SERIES = {LNCS},
  PUBLISHER = {Springer-Verlag},
  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.}
}


@ARTICLE{MeyerKhomenkoStrazny2009Unfolding,
  AUTHOR = {R. Meyer and V. Khomenko and T. Strazny},
  TITLE = {A Practical Approach to Verification of Mobile Systems Using Net Unfoldings},
  JOURNAL = {Fundamenta Informaticae},
  PUBLISHER = {IOS Press},
  NOTE = {Special Issue on Petri Nets 2008, invited version of the ATPN 2008 paper},
  VOLUME = {94},
  NUMBER = {3--4},
  PAGES = {439--471},
  YEAR = {2009},
  KEYWORDS = {finite control processes, safe processes, $\pi$-Calculus, mobile
systems, model checking, Petri net unfoldings},
  ABSTRACT = {
We propose a technique for verification of mobile systems. We
translate \emph{finite control processes,} which are a
well-known subset of \picalc, 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 \emph{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.}
}


@INPROCEEDINGS{MeyerKhomenkoStrazny2008Unfolding,
  AUTHOR = {R. Meyer and V. Khomenko and T. Strazny},
  TITLE = {A Practical Approach to Verification of Mobile Systems Using Net Unfoldings},
  BOOKTITLE = {Proc. of the 29th International Conference on Application and Theory of Petri Nets and Other Models of Concurrency, ATPN 2008},
  SERIES = {LNCS},
  VOLUME = {5062},
  PUBLISHER = {Springer-Verlag},
  PAGES = {327--347},
  YEAR = {2008},
  KEYWORDS = {finite control processes, safe processes, $\pi$-Calculus, mobile
systems, model checking, Petri net unfoldings},
  ABSTRACT = {
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.}
}


@TECHREPORT{MeyerKhomenkoStrazny2008UnfoldingTR,
  AUTHOR = {R. Meyer and V. Khomenko and T. Strazny},
  TITLE = {A Practical Approach to Verification of Mobile Systems Using Net
Unfoldings},
  INSTITUTION = {School of Computing Science, Newcastle University},
  MONTH = {January},
  YEAR = {2008},
  NUMBER = {CS-TR: 1064},
  NOTE = {29 pages},
  KEYWORDS = {finite control processes, safe processes, $\pi$-Calculus, mobile
systems, model checking, Petri net unfoldings},
  ABSTRACT = {
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.
}
}


@INPROCEEDINGS{SS06,
  AUTHOR = {Tim Strazny and Christian Stehno},
  TITLE = {{E}in {S}imulator {f}\"{u}r {m}ehrfach {e}rweiterte
{h}\"{o}here {P}etrinetze},
  BOOKTITLE = {19. Symposium Simulationstechnik (ASIM 2006)},
  EDITOR = {Matthias Becker and Helena Szczerbicka},
  YEAR = {2006},
  MONTH = SEP,
  PAGES = {171--176},
  PUBLISHER = {SCS Publishing House e.V.},
  ABSTRACT = {Petrinetze mit ihrer eindeutigen Semantik und dem zugrunde liegenden mathematischen Modell bew\"{a}hren sich vermehrt bei Entwurf, Analyse und Steuerung komplexer, asynchroner und verteilter Systeme. Insbesondere zeitbehaftete stochastische gef\"{a}rbte Petrinetze bieten M\"{o}glichkeiten komplizierte Sachverhalte strukturiert und kompakt auszudr\"{u}cken, jedoch ist die Simulation solcher h\"{o}heren Petrinetze um ein Vielfaches aufw\"{a}ndiger. Mit Geschwindigkeit und Vielf\"{a}ltigkeit als Hauptziel wurde mit P-UMLaut/Sim ein Simulator f\"{u}r solche mehrfach erweiterten Petrinetze entwickelt.}
}