Withdraw
Loading…
Probabilistic Büchi Automata for LTL\GU
Kini, Dileep; Viswanathan, Mahesh
Content Files

Loading…
Download Files
Loading…
Download Counts (All Files)
Loading…
Edit File
Loading…
Permalink
https://hdl.handle.net/2142/72686
Description
- Title
- Probabilistic Büchi Automata for LTL\GU
- Author(s)
- Kini, Dileep
- Viswanathan, Mahesh
- Issue Date
- 2015
- Keyword(s)
- Model Checking
- Linear Temporal Logic
- Probabilistic Automata
- Date of Ingest
- 2015-01-07T16:33:09Z
- 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.
- Type of Resource
- text
- Genre of Resource
- Technical Report
- Language
- en
- Permalink
- http://hdl.handle.net/2142/72686
Owning Collections
Manage Files
Loading…
Edit Collection Membership
Loading…
Edit Metadata
Loading…
Edit Properties
Loading…
Embargoes
Loading…