Optimising the compilation of Petri net models
| Autor: | Fronc, Lukasz, Pommereau, Franck |
|---|---|
| Přispěvatelé: | Davesne, Frédéric, Sciences de l'information, de la matière et de l'ingénierie : Matériels et logiciels pour les systèmes, les calculateurs, les communications (Blanc SIMI 3 2010) - Systèmes biologiques de synthèse : de la conception à la compilation - - SYNBIOTIC2010 - ANR-10-BLAN-0307 - BLANC - VALID, Informatique, Biologie Intégrative et Systèmes Complexes (IBISC), Université d'Évry-Val-d'Essonne (UEVE), ANR-10-BLAN-0307,SYNBIOTIC,Systèmes biologiques de synthèse : de la conception à la compilation(2010) |
| Jazyk: | angličtina |
| Rok vydání: | 2011 |
| Předmět: |
[INFO.INFO-FL]Computer Science [cs]/Formal Languages and Automata Theory [cs.FL]
explicit model-checking model compilation acceleration [INFO.INFO-MO] Computer Science [cs]/Modeling and Simulation [INFO.INFO-MO]Computer Science [cs]/Modeling and Simulation [INFO.INFO-FL] Computer Science [cs]/Formal Languages and Automata Theory [cs.FL] |
| Zdroj: | Proc. of the second International Workshop on Scalable and Usable Model Checking for Petri Net and other models of Concurrency (SUMO 2011) Second International Workshop on Scalable and Usable Model Checking for Petri Net and other models of Concurrency (SUMO 2011) Second International Workshop on Scalable and Usable Model Checking for Petri Net and other models of Concurrency (SUMO 2011), Jun 2011, Kanazawa, Japan. pp.49--64 |
| Popis: | International audience; Compilation of a Petri net model is one way to accelerate its veri cation through state space exploration. In this approach, code to explore the Petri net is generated, which avoids the use a xed exploration tool involving an interpretation" of the Petri net structure. In this paper, we show how peculiarities in the model (like places types, boundedness, invariants, etc., known by construction if adequate modelling tools are used) can be exploited to improve the generated code e ciency. We present a lightweight code generation framework targeting the LLVM language and demonstrate its exibility by considering several kinds of optimisations. Our compiler is called lightweight because the annotations of the compiled models are directly expressed in the target language, which saves from translating them and allows for fast compilation. The accelerations resulting from the optimisations are then evaluated on various Petri net models, showing important speedups and in some cases outperforming state-of-the-art tools. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|