Loading...
Please wait, while we are loading the content...
Similar Documents
Towards Efficient Verification of Systems with Dynamic Process Creation
| Content Provider | Hyper Articles en Ligne (HAL) |
|---|---|
| Author | Klaudel, Hanna Koutny, Maciej Pelz, Elisabeth Pommereau, Franck |
| Copyright Year | 2008 |
| Abstract | Modelling and analysis of dynamic multi-threaded state systems often encounters obstacles when one wants to use automated verification methods, such as model checking. Our aim in this paper is to develop a technical device for coping with one such obstacle, namely that caused by dynamic process creation. We first introduce a general class of coloured Petri nets-not tied to any particular syntax or approach-allowing one to capture systems with dynamic (and concurrent) process creation as well as capable of manipulating data. Following this, we introduce the central notion of our method which is a marking equivalence that can be efficiently computed and then used, for instance, to aggregate markings in a reachability graph. In some situations, such an aggregation may produce a finite representation of an infinite state system which still allows one to establish the relevant be-havioural properties. We show feasibility of the method on an example and provide initial experimental results. |
| Related Links | https://hal.science/hal-02310882/file/KKPP-ICTAC-2008.pdf |
| ISBN | 9783540857624 |
| DOI | 10.1007/978-3-540-85762-4_13 |
| Volume Number | 5160 |
| Language | English |
| Publisher | HAL CCSD Springer Berlin Heidelberg |
| Publisher Date | 2008-09-01 |
| Access Restriction | Open |
| Subject Keyword | multi-threaded systems state-space generation Petri nets marking symmetries Computer Science [cs] |
| Content Type | Text |
| Resource Type | Chapter |
| Subject | Medicine |
