Optimal Translation of LTL to Limit Deterministic Automata

Kini, Dileep; Viswanathan, Mahesh

Permalink

https://hdl.handle.net/2142/95004 Copy

Description

Title

Optimal Translation of LTL to Limit Deterministic Automata

Author(s)

• Kini, Dileep
• Viswanathan, Mahesh

Issue Date

2017

Keyword(s)

• Probabilistic Model Checking
• Linear Temporal Logic
• Verification
• Automata

Abstract

A crucial step in model checking Markov Decision Processes (MDP) is to translate the LTL specification into automata. Efforts have been made in improving deterministic automata construction for LTL but such translations are double exponential in the worst case. For model checking MDPs though limit deterministic automata suffice. Recently it was shown how to translate the fragment LTL\GU to exponential sized limit deterministic automata which speeds up the model checking problem by an exponential factor for that fragment. In this paper we show how to construct limit deterministic automata for full LTL. This translation is not only efficient for LTL\GU but for a larger fragment LTL_D which is provably more expressive. We show experimental results demonstrating that our construction yields smaller automata when compared to state of the art techniques that translate LTL to deterministic and limit deterministic automata.

Type of Resource

text

Permalink

http://hdl.handle.net/2142/95004

Sponsor(s)/Grant Number(s)

NSF grants CNS 1314485 and CCF 1422798

Owning Collections