Files in this item



application/pdfPBA-TR.pdf (368kB)
(no description provided)PDF


Title:Probabilistic Büchi Automata for LTL\GU
Author(s):Kini, Dileep; Viswanathan, Mahesh
Subject(s):Model Checking
Linear Temporal Logic
Probabilistic Automata
Abstract:LTL\GU is a fragment of linear temporal logic (LTL), where negations appear only on propositions, and formulas are built using the temporal operators X (next), F (eventually), G (always), and U (until, with the restriction that no until operator occurs in the scope of an always operator. Our main result is the construction of probabilistic Bu ̈chi automata for this logic that are exponential in the size of the formula. One consequence of our construction is a new, improved EXPTIME model checking algorithm (as opposed to the previously known doubly exponential time) for Markov Decision Processes and LTL\GU formulae.
Issue Date:2015
Genre:Technical Report
Date Available in IDEALS:2015-01-07

This item appears in the following Collection(s)

Item Statistics