| Title | Optimizing tla+ specifications for model checking / |
|---|---|
| Translation of Title | TLA+ specifikacijų optimizavimas modelių tikrinimui. |
| Authors | Jasinskas, Marijus |
| Full Text |
|
| Pages | 198 |
| Keywords [eng] | TLA+, TLC, Ben-Or algoritmas, formalūs metodai, specifikacijų rašymo gairės, būsenų erdvės redukcija, būsenų erdvės sprogimas, Ben-Or algorithm, formal methods, specification writing guidelines, state space reduction, state space explosion. |
| Abstract [eng] | In this thesis, a mitigation of the state space explosion problem is presented in the form of TLA+ specification writing guidelines that can reduce the state space size when applied to TLA+ specifications. These guidelines are defined based on the decisions made when writing TLA+ specifications of the Ben-Or distributed consensus algorithm, which has been an important part of research related to the verification of randomized consensus algorithms. Distributed algorithm TLA+ specification writing decisions relate to the conclusions made in the literature review and a paper in which specification writing guidelines for the mCRL2 language are described. Presented guideline state space reduction effectiveness is measured by comparing the total state space sizes of respective written Ben-Or TLA+ specifications. |
| Dissertation Institution | Vilniaus universitetas. |
| Type | Master thesis |
| Language | English |
| Publication date | 2024 |