On non-local propositional and local one-variable quantified CTL*

descriptionPublicationkeyboard_double_arrow_right Article 25 Jun 2003Publisher:IEEE Comput. SocJournal:Proceedings Ninth International Symposium on Temporal Representation and Reasoning

Authors: Frank Wolter; Sebastian Bauer; Ian Hodkinson; Michael Zakharyaschev;

doi: 10.1109/time.2002.1027466

On non-local propositional and local one-variable quantified CTL*

- Summary
- Metrics

Abstract

We prove decidability of 'non local' propositional CTL*, where truth values of atoms may depend on the branch of evaluation. This result is then used to show decidability of the 'weak' one-variable fragment of first-order (local) CTL*, in which all temporal operators and path quantifiers except 'tomorrow' are applicable only to sentences. Various spatio-temporal logics based on combinations of CTL* and RCC-8 can be embedded into this fragment, and so are decidable.

Related Organizations

Imperial College London
United Kingdom
Leipzig University
Germany

Impact byBIP!

	citations This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).	4
	popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network.	Average
	influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).	Average
	impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network.	Average