University of Twente Student Theses

Login

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.

[img] 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:http://purl.utwente.nl/essays/75026
Export this item as:BibTeX
EndNote
HTML Citation
Reference Manager

 

Repository Staff Only: item control page