About: Linear temporal logic to Büchi automaton

An Entity of Type: Thing, from Named Graph: http://dbpedia.org, within Data Space: dbpedia.org

In formal verification,finite state model checking needs to find a Büchi automaton (BA) equivalent to a given linear temporal logic (LTL) formula, i.e., such that the LTL formula and the BA recognize the same ω-language. There are algorithms that translate an LTL formula to a BA. This transformation is normally done in two steps. The first step produces a generalized Büchi automaton (GBA) from a LTL formula. The second step translates this GBA into a BA, which involves a relatively easy construction. Since LTL is strictly less expressive than BA, the reverse construction is not always possible.

Property Value
dbo:abstract
  • In formal verification,finite state model checking needs to find a Büchi automaton (BA) equivalent to a given linear temporal logic (LTL) formula, i.e., such that the LTL formula and the BA recognize the same ω-language. There are algorithms that translate an LTL formula to a BA. This transformation is normally done in two steps. The first step produces a generalized Büchi automaton (GBA) from a LTL formula. The second step translates this GBA into a BA, which involves a relatively easy construction. Since LTL is strictly less expressive than BA, the reverse construction is not always possible. The algorithms for transforming LTL to GBA differ in their construction strategies but they all have a common underlying principle, i.e., each state in the constructed automaton represents a set of LTL formulas that are expected to be satisfied by the remaining input word after occurrence of the state during a run. (en)
dbo:wikiPageExternalLink
dbo:wikiPageID
  • 31670156 (xsd:integer)
dbo:wikiPageLength
  • 20712 (xsd:nonNegativeInteger)
dbo:wikiPageRevisionID
  • 1101824819 (xsd:integer)
dbo:wikiPageWikiLink
dbp:bg
  • lightgrey (en)
dbp:title
  • Proof of correctness of the above construction (en)
dbp:titlestyle
  • background:lightblue; (en)
dbp:wikiPageUsesTemplate
dcterms:subject
gold:hypernym
rdfs:comment
  • In formal verification,finite state model checking needs to find a Büchi automaton (BA) equivalent to a given linear temporal logic (LTL) formula, i.e., such that the LTL formula and the BA recognize the same ω-language. There are algorithms that translate an LTL formula to a BA. This transformation is normally done in two steps. The first step produces a generalized Büchi automaton (GBA) from a LTL formula. The second step translates this GBA into a BA, which involves a relatively easy construction. Since LTL is strictly less expressive than BA, the reverse construction is not always possible. (en)
rdfs:label
  • Linear temporal logic to Büchi automaton (en)
owl:sameAs
prov:wasDerivedFrom
foaf:isPrimaryTopicOf
is dbo:wikiPageRedirects of
is dbo:wikiPageWikiLink of
is foaf:primaryTopic of
Powered by OpenLink Virtuoso    This material is Open Knowledge     W3C Semantic Web Technology     This material is Open Knowledge    Valid XHTML + RDFa
This content was extracted from Wikipedia and is licensed under the Creative Commons Attribution-ShareAlike 3.0 Unported License