@inproceedings{bb700b665eb744f988fbc0b13b441b90,
title = "LTL satisfiability checking revisited",
abstract = "We propose a novel algorithm for the satisfiability problem for Linear Temporal Logic (LTL). Existing approaches first transform the LTL formula into a B'uchi automaton and then perform an emptiness checking of the resulting automaton. Instead, our approach works on-the-fly by inspecting the formula directly, thus enabling finding a satisfying model quickly without constructing the full automaton. This makes our algorithm particularly fast for satisfiable formulas. We report on a prototype implementation, showing that our approach significantly outperforms state-of-the-art tools.",
keywords = "LTL Transition system, LTL satisfiability checking, Obligation Set",
author = "Jianwen Li and Lijun Zhang and Geguang Pu and Vardi, \{Moshe Y.\} and Jifeng He",
year = "2013",
doi = "10.1109/TIME.2013.19",
language = "英语",
isbn = "9780769551128",
series = "Proceedings of the International Workshop on Temporal Representation and Reasoning",
publisher = "Institute of Electrical and Electronics Engineers Inc.",
pages = "91--98",
booktitle = "Proceedings - 20th International Symposium on Temporal Representation and Reasoning, TIME 2013",
address = "美国",
note = "20th International Symposium on Temporal Representation and Reasoning, TIME 2013 ; Conference date: 26-09-2013 Through 28-09-2013",
}