University of Twente Student Theses
Improving Reachability Analysis in Ltsmin - Guards, Read, Write and Copy Dependencies for mcrl2, Promela and Dve
Meijer, J.J.G. (2014) Improving Reachability Analysis in Ltsmin - Guards, Read, Write and Copy Dependencies for mcrl2, Promela and Dve.
|
PDF
1MB |
| Abstract: | To improve symbolic reachability analysis in the model checking toolset LTSmin, we present two improve- ments to existing reachability algorithms. LTSmin uses a disjunctive partitioning scheme to efficiently analyze models of asynchronous systems. In these models transitions can be partitioned into groups, which modify only a small part of the state vector. Currently, there are no well defined notions, for whether a transition group reads and/or writes to an element in the state vector, which can be used in symbolic algorithms. Therefore, we present new definitions for read and write dependencies and show how algorithms can exploit these. This improvement always results in faster state space generation and many models such as 1-safe Petri nets highly benefit of these changes. A major issue we solved to sepa- rate dependencies correctly is that we had to cope with copying values. We provide examples that were intractable for LTSmin before, but can now be computed in a matter of minutes. A transition in a model specification is often of the form “if condition(x1,...,xn) =⇒ A . X(x1’,...,xn’)”. Our second improvement divides the condition into multiple conjuncts. These conjuncts can then be evaluated separately. Symbolic algorithms can exploit this information and prevent computing successors for large sets of states for only one conjunct evaluation. This greatly speeds up state space generation for models such as Sokoban or dining philosophers. We provide examples that show a speedup ranging from twice as fast to hundreds of times faster. An important issue in algorithms that exploit guard-splitting is that they need to support a ternary logic for the evaluation of guards. This is due to the fact that a guard can not only evaluate to true or false, but also to ‘maybe’. Consider for example a term rewriting system that splits the term someterm ∧ false and rewrites both conjuncts individually. We present clear benchmarking results in the form of scatter plots with time and memory usage as well as tables with detailed information about the size of the data structures. We make some important assumptions such as on the completeness of model specifications. We use these assumptions and the benchmarking results to validate our work. |
| Item Type: | Essay (Master) |
| Faculty: | EEMCS: Electrical Engineering, Mathematics and Computer Science |
| Subject: | 54 computer science |
| Programme: | Computer Science MSc (60300) |
| Link to this item: | https://purl.utwente.nl/essays/64834 |
| Export this item as: | BibTeX EndNote HTML Citation Reference Manager |
Show download statistics for this publication
Show download statistics for this publicationRepository Staff Only: item control page