University of Twente Student Theses
Translating LTL to the equational µ-calculus using Büchi automata optimisations
Kemp, T. (2018) Translating LTL to the equational µ-calculus using Büchi automata optimisations.
|
PDF
654kB |
| Abstract: | Two important temporal logics used in model checking are Linear Temporal Logic (LTL) and µ-calculus. LTL can be translated to µ-calculus by using Büchi automata as an intermediate form. This paper focuses on the translation from Büchi automata to the equational µ-calculus. The model checking library Spot can be used to translate LTL to Büchi automata. The optimisations performed by Spot combined with a translation from Büchi automata to an equational variant of the µ-calculus lead to an efficient translation. Properties for a system of traffic lights are modelled to illustrate the translation. The translation from LTL to µ-calculus is compared to the translation in the model checker LTSmin. This comparison shows that the translation via Büchi automata produces significantly smaller µ-calculus formulas in most cases. |
| Item Type: | Essay (Bachelor) |
| Faculty: | EEMCS: Electrical Engineering, Mathematics and Computer Science |
| Subject: | 31 mathematics, 54 computer science |
| Programme: | Applied Mathematics BSc (56965) |
| Link to this item: | https://purl.utwente.nl/essays/75026 |
| 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