Rabinizer: Small deterministic automata for LTL(F,G)

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

17 Scopus citations

Abstract

We present Rabinizer, a tool for translating formulae of the fragment of linear temporal logic with the operators F (eventually) and G (globally) into deterministic Rabin automata. Contrary to tools like ltl2dstar, which translate the formula into a Büchi automaton and apply Safra's determinization procedure, Rabinizer uses a direct construction based on the logical structure of the formulae. We describe a number of optimizations of the basic procedure, crucial for the good performance of Rabinizer, and present an experimental comparison.

Original languageEnglish
Title of host publicationAutomated Technology for Verification and Analysis - 10th International Symposium, ATVA 2012, Proceedings
Pages72-76
Number of pages5
DOIs
StatePublished - 2012
Event10th International Symposium on Automated Technology for Verification and Analysis, ATVA 2012 - Thiruvananthapuram, India
Duration: 3 Oct 20126 Oct 2012

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume7561 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference10th International Symposium on Automated Technology for Verification and Analysis, ATVA 2012
Country/TerritoryIndia
CityThiruvananthapuram
Period3/10/126/10/12

Fingerprint

Dive into the research topics of 'Rabinizer: Small deterministic automata for LTL(F,G)'. Together they form a unique fingerprint.

Cite this