Sign in
Author

Conference

Journal

Organization

Year

DOI
Look for results that meet for the following criteria:
since
equal to
before
between
and
Search in all fields of study
Limit my searches in the following fields of study
Agriculture Science
Arts & Humanities
Biology
Chemistry
Computer Science
Economics & Business
Engineering
Environmental Sciences
Geosciences
Material Science
Mathematics
Medicine
Physics
Social Science
Multidisciplinary
Keywords
(4)
cumulant
Model Checking
Satisfiability
Upper Bound
Subscribe
Academic
Publications
The Complexity of CTL* + Linear Past
The Complexity of CTL* + Linear Past,10.1007/9783540784999_14,Laura Bozzelli
Edit
The Complexity of CTL* + Linear Past
(
Citations: 2
)
BibTex

RIS

RefWorks
Download
Laura Bozzelli
We investigate the complexity of
satisfiability
and finitestate modelchecking problems for the branchingtime logic CTL *lp^*_{lp} , an extension of CTL* with pasttime operators, where past is linear, finite, and cumulative. It is wellknown that CTL *lp^*_{lp} has the same expressiveness as standard CTL*, but the translation of CTL *lp^*_{lp} into CTL* is of nonelementary complexity, and no elementary upper bounds are known for its
satisfiability
and finitestate
model checking
problems. In this paper, we provide an elegant and uniform framework to solve these problems, which nontrivially extends the standard automatatheoretic approach to CTL* modelchecking. In particular, we show that the
satisfiability
problem for CTL *lp^*_{lp} is 2Exptimecomplete, which is the same complexity as that of CTL*, but for the existential fragment of CTL *lp^*_{lp} , the problem is Expspacecomplete, hence exponentially harder than that of the existential fragment of CTL*. For the modelchecking, the problem is already Expspacecomplete for the existential and universal fragments of CTL *lp^*_{lp} . For full CTL *lp^*_{lp} , the proposed algorithm runs in time polynomial in the size of the Kripke structure and doubly exponential in the size of the formula. Thus, the exact complexity of modelchecking full CTL *lp^*_{lp} remains open: it lies somewhere between Expspace and 2Exptime.
Conference:
Foundations of Software Science and Computation Structure  FoSSaCS
, pp. 186200, 2008
DOI:
10.1007/9783540784999_14
Cumulative
Annual
View Publication
The following links allow you to view full publications. These links are maintained by other sources not affiliated with Microsoft Academic Search.
(
www.springerlink.com
)
(
www.springerlink.com
)
(
dx.doi.org
)
(
www.informatik.unitrier.de
)
More »
Citation Context
(2)
...A twoway version of these automata was studied by
Bozzelli (2008)
...
Volker Weber
.
BranchingTime Logics Repeatedly Referring to States
...In both cases, past modalities do not increase the complexity: PCTL is EXPTIMEcomplete [16] and PCTL ∗ has recently been shown to be 2EXPTIMEcomplete by Bozzelli [
3
]...
...They allow for an easy translation from CTL ∗ [18] and have proved useful in studies of CTL ∗ with past [17,
3
]...
...Symmetric twoway HAA have been used by Bozzelli to prove membership in 2EXPTIME for CTL ∗ with past [
3
]...
...do not enforce that infinite paths in a run move only downward in the tree from a certain point on. Therefore, our results on symmetric twoway HAA are not implied by [
3
]...
...Nevertheless, the restricted version of [
3
] would suffice to prove our results on the complexity of branchingtime logics...
...This yields the following theorem, which has been proved before by Bozzelli for a slightly more restricted model [
3
]...
Volker Weber
.
On the Complexity of BranchingTime Logics
References
(22)
Design and synthesis of synchronization skeletons using branching time temporal logic
(
Citations: 1136
)
Edmund M. Clarke
,
E. Allen Emerson
Conference:
Logic of Programs
, pp. 5271, 1981
``Sometimes'' and ``Not Never'' Revisited: On Branching Versus Linear Time
(
Citations: 132
)
E. Allen Emerson
,
Joseph Y. Halpern
Conference:
ACM SIGPLANSIGACT Symposium on Principles of Programming Languages  POPL
, pp. 127140, 1983
Computation Tree Logic CTL* and Path Quantifiers in the Monadic Theory of the Binary Tree
(
Citations: 83
)
Thilo Hafer
,
Wolfgang Thomas
Conference:
International Colloquium on Automata, Languages and Programming  ICALP
, pp. 269279, 1987
Once and For All
(
Citations: 44
)
Orna Kupferman
,
Amir Pnueli
Conference:
Logic in Computer Science  LICS
, pp. 2535, 1995
Weak alternating automata and tree automata emptiness
(
Citations: 51
)
Orna Kupferman
,
Moshe Y. Vardi
Conference:
ACM Symposium on Theory of Computing  STOC
, pp. 224233, 1998
Sort by:
Citations
(2)
BranchingTime Logics Repeatedly Referring to States
(
Citations: 3
)
Volker Weber
Journal:
Journal of Logic, Language and Information  JOLLI
, vol. 18, no. 4, pp. 593624, 2009
On the Complexity of BranchingTime Logics
(
Citations: 2
)
Volker Weber
Journal:
Computing Research Repository  CORR
, vol. abs/0906.2, pp. 530545, 2009