Model Checking CTL is Almost Always Inherently Sequential
The model checking problem for CTL is known to be P-complete (Clarke, Emerson, and Sistla (1986), see Schnoebelen (2002)). We consider fragments of CTL obtained by restricting the use of temporal modalities or the use of negations---restrictions already studied for LTL by Sistla and Clarke (1985) an...
Main Authors: | Olaf Beyersdorff, Arne Meier, Martin Mundhenk, Thomas Schneider, Michael Thomas, Heribert Vollmer |
---|---|
Format: | Article |
Language: | English |
Published: |
Logical Methods in Computer Science e.V.
2011-05-01
|
Series: | Logical Methods in Computer Science |
Subjects: | |
Online Access: | https://lmcs.episciences.org/1007/pdf |
Similar Items
-
Efficiently Simulating Higher-Order Arithmetic by a First-Order Theory Modulo
by: Guillaume Burel
Published: (2011-03-01) -
Computing metric hulls in graphs
by: Kolja Knauer, et al.
Published: (2019-05-01) -
Constrained ear decompositions in graphs and digraphs
by: Frédéric Havet, et al.
Published: (2019-09-01) -
Understanding the Relative Strength of QBF CDCL Solvers and QBF Resolution
by: Olaf Beyersdorff, et al.
Published: (2023-04-01) -
Quantified CTL: Expressiveness and Complexity
by: François Laroussinie, et al.
Published: (2014-12-01)