The tractability of model checking for LTL: The good, the bad, and the ugly fragments

Michael Bauland; Martin Mundhenk; Thomas Schneider; Henning Schnoor; Ilka Schnoor; Heribert Vollmer

doi:10.1145/1877714.1877719

The tractability of model checking for LTL: The good, the bad, and the ugly fragments

Michael Bauland
, Martin Mundhenk
, Thomas Schneider
, Henning Schnoor
, Ilka Schnoor
, Heribert Vollmer

Institute of Theoretical Computer Science

Research output: Contribution to journal › Article › Research › peer review

Original language	English
Pages (from-to)	13:1-13:28
Journal	ACM Trans. Comput. Log.
Volume	12
Issue number	2
DOIs	https://doi.org/10.1145/1877714.1877719
Publication status	Published - 2011

Access to Document

10.1145/1877714.1877719

https://dblp.org/rec/journals/tocl/BaulandM0SSV11

Cite this

@article{40bbdfdd41334df79f8a515bd2fd0a0e,

title = "The tractability of model checking for LTL: The good, the bad, and the ugly fragments",

author = "Michael Bauland and Martin Mundhenk and Thomas Schneider and Henning Schnoor and Ilka Schnoor and Heribert Vollmer",

note = "Funding information: 1 Supported by the Postdoc Programme of the German Academic Exchange Service (DAAD) 2 Supported in part by DFG VO 630/6-1.",

year = "2011",

doi = "10.1145/1877714.1877719",

language = "English",

volume = "12",

pages = "13:1--13:28",

journal = "ACM Trans. Comput. Log.",

issn = "1557-945X",

publisher = "Association for Computing Machinery",

number = "2",

}

TY - JOUR

T1 - The tractability of model checking for LTL

T2 - The good, the bad, and the ugly fragments

AU - Bauland, Michael

AU - Mundhenk, Martin

AU - Schneider, Thomas

AU - Schnoor, Henning

AU - Schnoor, Ilka

AU - Vollmer, Heribert

N1 - Funding information: 1 Supported by the Postdoc Programme of the German Academic Exchange Service (DAAD) 2 Supported in part by DFG VO 630/6-1.

PY - 2011

Y1 - 2011

U2 - 10.1145/1877714.1877719

DO - 10.1145/1877714.1877719

M3 - Article

SN - 1557-945X

VL - 12

SP - 13:1-13:28

JO - ACM Trans. Comput. Log.

JF - ACM Trans. Comput. Log.

IS - 2

ER -