Applying compiler techniques to reachability analysis of high-level models

Reference:

Marko Mäkelä. Applying compiler techniques to reachability analysis of high-level models. In Hans-Dieter Burkhard, Ludwik Czaja, Andrzej Skowron, and Peter Starke, editors, Workshop on Concurrency, Specification & Programming 2000, number 140 in Informatik-Bericht, pages 129–142. Humboldt-Universität zu Berlin, Germany, October 2000.

Abstract:

Using a tool for high-level Petri nets as an example, this article shows how techniques familiar from compilers can make reachability analysers more powerful. Syntax transformations can be applied to extend the modelling language with convenient short-hand notations, such as universal and existential quantification and multi-set summation. The process of reachability analysis can be dramatically sped up by compiling models to executable machine code that performs all model-dependent tasks, such as computing the successors of a state. This work describes a code generator implementation and the way the generated code is linked with the reachability analyser code.

Keywords:

reachability analysis, compilers, syntax transformations, code generation

Suggested BibTeX entry:

@inproceedings{MakelaMarko-Makela:compiler,
    author = {Marko M{\"a}kel{\"a}},
    booktitle = {Workshop on Concurrency, Specification \& Programming 2000},
    editor = {Burkhard, Hans-Dieter and Czaja, Ludwik and Skowron, Andrzej and Starke, Peter},
    month = {October},
    number = {140},
    organization = {Humboldt-Universit{\"a}t zu Berlin, Germany},
    pages = {129--142},
    series = {Informatik-Bericht},
    title = {Applying compiler techniques to reachability analysis of high-level models},
    year = {2000},
}