An NP-Complete Fragment of LTL

A fragment of linear time temporal logic (LTL) is presented. It is proved that the satisfiability problem for this fragment is NPcomplete. The fragment is larger than previously known NP-complete fragments. It is obtained by prohibiting the use of until operator and requiring to use only next operators indexed by a letter.

• Type: Conference
• Year: 2004
• Where: DLT
• Authors: Anca Muscholl, Igor Walukiewicz
• Keywords: DLT 2004, DLT 2007, NP-complete Fragments, Satisfiability Problem, Time Temporal Logic