Free Online Productivity Tools
i2Speak
i2Symbol
i2OCR
iTex2Img
iWeb2Print
iWeb2Shot
i2Type
iPdf2Split
iPdf2Merge
i2Bopomofo
i2Arabic
i2Style
i2Image
i2PDF
iLatex2Rtf
Sci2ools

FSTTCS

2009

Springer

2009

Springer

Linear temporal logic was introduced in order to reason about reactive systems. It is often considered with respect to inﬁnite words, to specify the behaviour of long-running systems. One can consider more general models for linear time, using words indexed by arbitrary linear orderings. We investigate the connections between temporal logic and automata on linear orderings, as introduced by Bruyère and Carton. We provide a doubly exponential procedure to compute from any LTL formula with Until, Since, and the Stavi connectives an automaton that decides whether that formula holds on the input word. In particular, since the emptiness problem for these automata is decidable, this transformation gives a decision procedure for the satisﬁability of the logic.

Related Content

Added |
26 May 2010 |

Updated |
26 May 2010 |

Type |
Conference |

Year |
2009 |

Where |
FSTTCS |

Authors |
Julien Cristau |

Comments (0)