Files in this item

FilesDescriptionFormat

application/pdf

application/pdftacas17.pdf (452kB)
(no description provided)PDF

Description

Title:Optimal Translation of LTL to Limit Deterministic Automata
Author(s):Kini, Dileep; Viswanathan, Mahesh
Subject(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.
Issue Date:2017
Genre:Technical Report
Type:Text
URI:http://hdl.handle.net/2142/95004
Sponsor:NSF grants CNS 1314485 and CCF 1422798
Date Available in IDEALS:2017-01-19


This item appears in the following Collection(s)

Item Statistics