Expressive completeness of temporal logic of trees
作者:
Bernd-Holger Schlingloff,
期刊:
Journal of Applied Non-Classical Logics
(Taylor Available online 1992)
卷期:
Volume 2,
issue 2
页码: 157-180
ISSN:1166-3081
年代: 1992
DOI:10.1080/11663081.1992.10510780
出版商: Taylor & Francis Group
数据来源: Taylor
摘要:
Many temporal and modal logic languages can be regarded as subsets of first order logic, i.e. the semantics of a temporal logic formula is given as a first order condition on points of the underlying models (Kripke structures). Often the set of possible models is restricted to models which are trees. A temporal logic language is (first order) expressively complete, if for every first order condition for a node of a tree there exists an equivalent temporal formula which expresses the same condition. In this paper expressive completeness of the temporal logic language with the set of operatorsU(until),S(since), andXk(k-next) is proved, and the result is extended to various other tree-like structures.
点击下载:
PDF (1078KB)
返 回