Files in this item

FilesDescriptionFormat

application/pdf

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

Description

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
Type:Text
Language:English
URI:http://hdl.handle.net/2142/72686
Date Available in IDEALS:2015-01-07


This item appears in the following Collection(s)

Item Statistics